--- 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)