A little-known material, and some tidying up
authorpaulson <lp15@cam.ac.uk>
Mon, 16 Sep 2019 17:03:13 +0100
changeset 70898 125705f5965f
parent 70896 374caac3d624
child 70899 a95446297373
A little-known material, and some tidying up
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Topological_Spaces.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -4960,7 +4960,7 @@
       (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
      (at x within X)"
   apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real)
-  apply (rule has_vector_derivative_real_complex)
+  apply (rule has_vector_derivative_real_field)
   apply (rule derivative_eq_intros | simp)+
   done
 
@@ -7824,7 +7824,7 @@
   hence h_holo: "h holomorphic_on A"
     by (auto simp: h_def intro!: holomorphic_intros)
   have "\<exists>c. \<forall>x\<in>A. f x / exp (h x) - 1 = c"
-  proof (rule DERIV_zero_constant, goal_cases)
+  proof (rule has_field_derivative_zero_constant, goal_cases)
     case (2 x)
     note [simp] = at_within_open[OF _ \<open>open A\<close>]
     from 2 and z0 and f show ?case
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -1171,7 +1171,7 @@
     by metis
 next
   assume RHS: ?rhs
-  with borel_measurable_simple_function_limit [of f UNIV, unfolded borel_measurable_UNIV_eq]
+  with borel_measurable_simple_function_limit [of f UNIV, unfolded lebesgue_on_UNIV_eq]
   show ?lhs
     by (blast intro: order_trans)
 qed
@@ -2518,13 +2518,13 @@
   have "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) integrable_on UNIV"
     by (simp add: integrable_restrict_UNIV intS)
   then have Df_borel: "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> borel_measurable lebesgue"
-    using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+    using integrable_imp_measurable lebesgue_on_UNIV_eq by force
   have S': "S' \<in> sets lebesgue"
   proof -
     from Df_borel borel_measurable_vimage_open [of _ UNIV]
     have "{x. (if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> T} \<in> sets lebesgue"
       if "open T" for T
-      using that unfolding borel_measurable_UNIV_eq
+      using that unfolding lebesgue_on_UNIV_eq
       by (fastforce simp add: dest!: spec)
     then have "{x. (if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> -{0}} \<in> sets lebesgue"
       using open_Compl by blast
@@ -2649,7 +2649,7 @@
   then have "(\<lambda>x. if x \<in> S then ?D x else 0) integrable_on UNIV"
     by (simp add: integrable_restrict_UNIV)
   then have D_borel: "(\<lambda>x. if x \<in> S then ?D x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-    using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+    using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
   then have Dlt: "{x \<in> S. ?D x < 0} \<in> sets lebesgue"
     unfolding borel_measurable_vimage_halfspace_component_lt
     by (drule_tac x=0 in spec) (auto simp: eq)
@@ -2860,7 +2860,7 @@
     then have "(\<lambda>x. if x \<in> S then ?DP x else 0) integrable_on UNIV"
       by (simp add: integrable_restrict_UNIV)
     then have D_borel: "(\<lambda>x. if x \<in> S then ?DP x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-      using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
     then have SN: "{x \<in> S. ?DP x < 0} \<in> sets lebesgue"
       unfolding borel_measurable_vimage_halfspace_component_lt
       by (drule_tac x=0 in spec) (auto simp: eq)
@@ -2924,7 +2924,7 @@
     then have "(\<lambda>x. if x \<in> T then f x else 0) integrable_on UNIV"
       by (simp add: integrable_restrict_UNIV)
     then have D_borel: "(\<lambda>x. if x \<in> T then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-      using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
     then have TN: "{x \<in> T. f x < 0} \<in> sets lebesgue"
       unfolding borel_measurable_vimage_halfspace_component_lt
       by (drule_tac x=0 in spec) (auto simp: eq)
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -15,33 +15,11 @@
 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
   by (simp add: complex_nonneg_Reals_iff cmod_eq_Re)
 
-lemma has_derivative_mult_right:
-  fixes c:: "'a :: real_normed_algebra"
-  shows "(((*) c) has_derivative ((*) c)) F"
-by (rule has_derivative_mult_right [OF has_derivative_ident])
-
-lemma has_derivative_of_real[derivative_intros, simp]:
-  "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
-  using bounded_linear.has_derivative[OF bounded_linear_of_real] .
-
-lemma has_vector_derivative_real_field:
-  "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
-  using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
-  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
-lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
-
 lemma fact_cancel:
   fixes c :: "'a::real_field"
   shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
   using of_nat_neq_0 by force
 
-lemma bilinear_times:
-  fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
-  by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
-
-lemma linear_cnj: "linear cnj"
-  using bounded_linear.linear[OF bounded_linear_cnj] .
-
 lemma vector_derivative_cnj_within:
   assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
   shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) = 
@@ -83,8 +61,6 @@
 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
   by (intro continuous_on_id continuous_on_norm)
 
-lemmas DERIV_zero_constant = has_field_derivative_zero_constant
-
 lemma DERIV_zero_unique:
   assumes "convex S"
       and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)"
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -4783,8 +4783,7 @@
           then show " (f' has_field_derivative of_int po * pp w * (w - p) powr of_int (po - 1) 
                   + deriv pp w * (w - p) powr of_int po) (at w)"
             unfolding f'_def using \<open>w\<noteq>p\<close>
-            apply (auto intro!: derivative_eq_intros(35) DERIV_cong[OF has_field_derivative_powr_of_int])
-            by (auto intro: derivative_eq_intros)
+            by (auto intro!: derivative_eq_intros DERIV_cong[OF has_field_derivative_powr_of_int])
         qed
         ultimately show "prin w + anal w = ff' w"
           unfolding ff'_def prin_def anal_def
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -4611,7 +4611,7 @@
   have "(UNIV::'a set) \<in> sets lborel"
     by simp
   then show ?thesis
-    using assms borel_measurable_if_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
+    by (metis (mono_tags, lifting) assms borel_measurable_if_D integrable_imp_measurable_weak integrable_restrict_UNIV lebesgue_on_UNIV_eq sets_lebesgue_on_refl)
 qed
 
 lemma integrable_iff_integrable_on:
@@ -4767,7 +4767,7 @@
     then have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on UNIV"
       by (simp add: integrable_restrict_UNIV)
     then have borel: "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-      using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
     then show "{x \<in> S. f x \<noteq> 0} \<in> sets lebesgue"
       unfolding borel_measurable_vimage_open
       by (rule allE [where x = "-{0}"]) auto
@@ -4777,7 +4777,7 @@
     then have "(\<lambda>x. if x \<in> T then f x else 0) integrable_on UNIV"
       by (simp add: integrable_restrict_UNIV)
     then have borel: "(\<lambda>x. if x \<in> T then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-      using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
     then show "{x \<in> T. f x \<noteq> 0} \<in> sets lebesgue"
       unfolding borel_measurable_vimage_open
       by (rule allE [where x = "-{0}"]) auto
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -1360,16 +1360,30 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes N: "N \<in> null_sets (lebesgue_on S)" and S: "S \<in> sets lebesgue"
   shows "f \<in> borel_measurable (lebesgue_on (S-N)) \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
-  unfolding in_borel_measurable borel_measurable_UNIV_eq [symmetric] space_lebesgue_on sets_restrict_UNIV
+  unfolding in_borel_measurable space_lebesgue_on sets_restrict_UNIV
 proof (intro ball_cong iffI)
   show "f -` T \<inter> S \<in> sets (lebesgue_on S)"
     if "f -` T \<inter> (S-N) \<in> sets (lebesgue_on (S-N))" for T
-    using that  assms
-    by (smt Diff_Int_distrib completion.complete2 diff_null_sets_lebesgue inf.idem inf_le2 inf_mono lebesgue_on_UNIV_eq null_setsD2 null_sets_restrict_space sets.Diff sets_restrict_space_iff space_lebesgue_on space_restrict_space)
+  proof -
+    have "N \<inter> S = N"
+      by (metis N S inf.orderE null_sets_restrict_space)
+    moreover have "N \<inter> S \<in> sets lebesgue"
+      by (metis N S inf.orderE null_setsD2 null_sets_restrict_space)
+    moreover have "f -` T \<inter> S \<inter> (f -` T \<inter> N) \<in> sets lebesgue"
+      by (metis N S completion.complete inf.absorb2 inf_le2 inf_mono null_sets_restrict_space)
+    ultimately show ?thesis
+      by (metis Diff_Int_distrib Int_Diff_Un S inf_le2 sets.Diff sets.Un sets_restrict_space_iff space_lebesgue_on space_restrict_space that)
+  qed
   show "f -` T \<inter> (S-N) \<in> sets (lebesgue_on (S-N))"
     if "f -` T \<inter> S \<in> sets (lebesgue_on S)" for T
-    using image_eqI inf.commute inf_top_right sets_restrict_space that
-    by (smt Int_Diff S sets.Int_space_eq2 sets_restrict_space_iff space_lebesgue_on)
+  proof -
+    have "(S - N) \<inter> f -` T = (S - N) \<inter> (f -` T \<inter> S)"
+      by blast
+    then have "(S - N) \<inter> f -` T \<in> sets.restricted_space lebesgue (S - N)"
+      by (metis S image_iff sets.Int_space_eq2 sets_restrict_space_iff that)
+    then show ?thesis
+      by (simp add: inf.commute sets_restrict_space)
+  qed
 qed auto
 
 lemma lebesgue_measurable_diff_null:
@@ -1600,4 +1614,53 @@
     using measurable_on_UNIV by blast
 qed
 
+subsection \<open>Measurability on generalisations of the binary product\<close>
+lemma measurable_on_bilinear:
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S"
+  shows "(\<lambda>x. h (f x) (g x)) measurable_on S"
+proof (rule measurable_on_combine [where h = h])
+  show "continuous_on UNIV (\<lambda>x. h (fst x) (snd x))"
+    by (simp add: bilinear_continuous_on_compose [OF continuous_on_fst continuous_on_snd h])
+  show "h 0 0 = 0"
+  by (simp add: bilinear_lzero h)
+qed (auto intro: assms)
+
+lemma borel_measurable_bilinear:
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  assumes "bilinear h" "f \<in> borel_measurable (lebesgue_on S)" "g \<in> borel_measurable (lebesgue_on S)"
+    and S: "S \<in> sets lebesgue"
+  shows "(\<lambda>x. h (f x) (g x)) \<in> borel_measurable (lebesgue_on S)"
+  using assms measurable_on_bilinear [of h f S g]
+  by (simp flip: measurable_on_iff_borel_measurable)
+
+lemma absolutely_integrable_bounded_measurable_product:
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  assumes "bilinear h" and f: "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
+    and bou: "bounded (f ` S)" and g: "g absolutely_integrable_on S"
+  shows "(\<lambda>x. h (f x) (g x)) absolutely_integrable_on S"
+proof -
+  obtain B where "B > 0" and B: "\<And>x y. norm (h x y) \<le> B * norm x * norm y"
+    using bilinear_bounded_pos \<open>bilinear h\<close> by blast
+  obtain C where "C > 0" and C: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> C"
+    using bounded_pos by (metis bou imageI)
+  show ?thesis
+  proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable [OF _ \<open>S \<in> sets lebesgue\<close>])
+    show "norm (h (f x) (g x)) \<le> B * C * norm(g x)" if "x \<in> S" for x
+      by (meson less_le mult_left_mono mult_right_mono norm_ge_zero order_trans that \<open>B > 0\<close> B C)
+    show "(\<lambda>x. h (f x) (g x)) \<in> borel_measurable (lebesgue_on S)"
+      using \<open>bilinear h\<close> f g
+      by (blast intro: borel_measurable_bilinear dest: absolutely_integrable_measurable)
+    show "(\<lambda>x. B * C * norm(g x)) integrable_on S"
+      using \<open>0 < B\<close> \<open>0 < C\<close> absolutely_integrable_on_def g by auto
+  qed
+qed
+
+lemma absolutely_integrable_bounded_measurable_product_real:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
+      and "bounded (f ` S)" and "g absolutely_integrable_on S"
+  shows "(\<lambda>x. f x * g x) absolutely_integrable_on S"
+  using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast
+
 end
--- a/src/HOL/Analysis/Gamma_Function.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -1564,7 +1564,7 @@
     by (subst of_real_in_nonpos_Ints_iff) (auto elim!: nonpos_Ints_cases')
   then have "x \<noteq> 0" by auto
   with x have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)"
-    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
+    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_field
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
   thus "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (x + of_nat k))
                        \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma x +
@@ -1574,7 +1574,7 @@
 next
   fix n :: nat
   have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))"
-    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
+    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_field
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
   thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * prod of_nat {1..n} *
                   (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
@@ -1676,7 +1676,7 @@
   shows "(ln_Gamma has_field_derivative Digamma x) (at x)"
 proof (subst DERIV_cong_ev[OF refl _ refl])
   from assms show "((Re \<circ> ln_Gamma \<circ> complex_of_real) has_field_derivative Digamma x) (at x)"
-    by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex
+    by (auto intro!: derivative_eq_intros has_vector_derivative_real_field
              simp: Polygamma_of_real o_def)
   from eventually_nhds_in_nhd[of x "{0<..}"] assms
     show "eventually (\<lambda>y. ln_Gamma y = (Re \<circ> ln_Gamma \<circ> of_real) y) (nhds x)"
@@ -2816,7 +2816,7 @@
     have "((\<lambda>t. complex_of_real t powr (z - 1)) has_integral
             (of_real 1 powr z / z - of_real 0 powr z / z)) {0..1}" using 0
       by (intro fundamental_theorem_of_calculus_interior)
-         (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_complex)
+         (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_field)
     thus ?case by simp
   next
     case (Suc n)
@@ -2833,9 +2833,9 @@
     next
       fix t :: real assume t: "t \<in> {0<..<1}"
       show "(?f has_vector_derivative ?f' t) (at t)" using t Suc.prems
-        by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex)
+        by (auto intro!: derivative_eq_intros has_vector_derivative_real_field)
       show "(?g has_vector_derivative ?g' t) (at t)"
-        by (rule has_vector_derivative_real_complex derivative_eq_intros refl)+ simp_all
+        by (rule has_vector_derivative_real_field derivative_eq_intros refl)+ simp_all
     next
       from Suc.prems have [simp]: "z \<noteq> 0" by auto
       from Suc.prems have A: "Re (z + of_nat n) > 0" for n by simp
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -433,10 +433,6 @@
     by (auto simp: restrict_space_def)
 qed
 
-lemma integrable_lebesgue_on_UNIV_eq:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
-  shows "integrable (lebesgue_on UNIV) f = integrable lebesgue f"
-  by (auto simp: integrable_restrict_space)
 lemma integral_restrict_Int:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "S \<in> sets lebesgue" "T \<in> sets lebesgue"
@@ -671,9 +667,6 @@
     by (simp add: borel_measurable_vimage_open)
 qed
 
-lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
-  by auto
-
 lemma borel_measurable_vimage_borel:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
--- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -369,6 +369,10 @@
 lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
   by (simp add: bilinear_def linear_iff)
 
+lemma bilinear_times:
+  fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
+  by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
+
 lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
   by (simp add: bilinear_def linear_iff)
 
--- a/src/HOL/Complex.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Complex.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -611,6 +611,9 @@
 lemma bounded_linear_cnj: "bounded_linear cnj"
   using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp
 
+lemma linear_cnj: "linear cnj"
+  using bounded_linear.linear[OF bounded_linear_cnj] .
+
 lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
   and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
   and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
--- a/src/HOL/Deriv.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Deriv.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -107,6 +107,9 @@
 lemmas has_derivative_mult_left [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_mult_left]
 
+lemmas has_derivative_of_real[derivative_intros, simp] = 
+  bounded_linear.has_derivative[OF bounded_linear_of_real] 
+
 lemma has_derivative_add[simp, derivative_intros]:
   assumes f: "(f has_derivative f') F"
     and g: "(g has_derivative g') F"
@@ -793,6 +796,11 @@
   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
     (simp add: has_field_derivative_iff_has_vector_derivative)
 
+lemma has_vector_derivative_real_field:
+  "(f has_field_derivative f') (at (of_real a)) \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
+  using has_derivative_compose[of of_real of_real a _ f "(*) f'"] 
+  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
+
 lemma has_vector_derivative_continuous:
   "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
@@ -1085,6 +1093,27 @@
 lemmas has_derivative_floor[derivative_intros] =
   floor_has_real_derivative[THEN DERIV_compose_FDERIV]
 
+lemma continuous_floor:
+  fixes x::real
+  shows "x \<notin> \<int> \<Longrightarrow> continuous (at x) (real_of_int \<circ> floor)"
+  using floor_has_real_derivative [where f=id]
+  by (auto simp: o_def has_field_derivative_def intro: has_derivative_continuous)
+
+lemma continuous_frac:
+  fixes x::real
+  assumes "x \<notin> \<int>"
+  shows "continuous (at x) frac"
+proof -
+  have "isCont (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x"
+    using continuous_floor [OF assms] by (simp add: o_def)
+  then have *: "continuous (at x) (\<lambda>x. x - real_of_int \<lfloor>x\<rfloor>)"
+    by (intro continuous_intros)
+  moreover have "\<forall>\<^sub>F x in nhds x. frac x = x - real_of_int \<lfloor>x\<rfloor>"
+    by (simp add: frac_def)
+  ultimately show ?thesis
+    by (simp add: LIM_imp_LIM frac_def isCont_def)
+qed
+
 text \<open>Caratheodory formulation of derivative at a point\<close>
 
 lemma CARAT_DERIV:
--- a/src/HOL/Topological_Spaces.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -2162,6 +2162,9 @@
 lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
   unfolding continuous_within by (rule tendsto_ident_at)
 
+lemma continuous_id[continuous_intros, simp]: "continuous (at x within S) id"
+  by (simp add: id_def)
+
 lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
   unfolding continuous_def by (rule tendsto_const)