# HG changeset patch # User immler # Date 1535525428 -3600 # Node ID 5e013478bced3c56e308806bf8ac8e5996025394 # Parent 99f0aee4adbd1c4a62a903f6d10c4b43e189bfed tagged some theories diff -r 99f0aee4adbd -r 5e013478bced src/HOL/Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Tue Aug 28 21:08:42 2018 +0200 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Wed Aug 29 07:50:28 2018 +0100 @@ -7,7 +7,7 @@ subsection \Definition\ -definition "bcontfun = {f. continuous_on UNIV f \ bounded (range f)}" +definition%important "bcontfun = {f. continuous_on UNIV f \ bounded (range f)}" typedef (overloaded) ('a, 'b) bcontfun ("(_ \\<^sub>C /_)" [22, 21] 21) = "bcontfun::('a::topological_space \ 'b::metric_space) set" @@ -41,7 +41,7 @@ instantiation bcontfun :: (topological_space, metric_space) metric_space begin -lift_definition dist_bcontfun :: "'a \\<^sub>C 'b \ 'a \\<^sub>C 'b \ real" +lift_definition%important dist_bcontfun :: "'a \\<^sub>C 'b \ 'a \\<^sub>C 'b \ real" is "\f g. (SUP x. dist (f x) (g x))" . definition uniformity_bcontfun :: "('a \\<^sub>C 'b \ 'a \\<^sub>C 'b) filter" @@ -175,8 +175,8 @@ subsection \Complete Space\ -instance bcontfun :: (metric_space, complete_space) complete_space -proof +instance%important bcontfun :: (metric_space, complete_space) complete_space +proof%unimportant fix f :: "nat \ ('a, 'b) bcontfun" assume "Cauchy f" \ \Cauchy equals uniform convergence\ then obtain g where "uniform_limit UNIV f g sequentially" @@ -191,9 +191,9 @@ qed -subsection \Supremum norm for a normed vector space\ +subsection%unimportant \Supremum norm for a normed vector space\ -instantiation bcontfun :: (topological_space, real_normed_vector) real_vector +instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector begin lemma uminus_cont: "f \ bcontfun \ (\x. - f x) \ bcontfun" for f::"'a \ 'b" @@ -247,7 +247,7 @@ "bounded (range f) \ norm (f x) \ (SUP x. norm (f x))" by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp) -instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector +instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_normed_vector begin definition norm_bcontfun :: "('a, 'b) bcontfun \ real" @@ -290,7 +290,7 @@ using dist_bound[of f 0 b] assms by (simp add: dist_norm) -subsection \(bounded) continuous extenstion\ +subsection%unimportant \(bounded) continuous extenstion\ lemma integral_clamp: "integral {t0::real..clamp t0 t1 x} f = diff -r 99f0aee4adbd -r 5e013478bced src/HOL/Analysis/Bounded_Linear_Function.thy --- a/src/HOL/Analysis/Bounded_Linear_Function.thy Tue Aug 28 21:08:42 2018 +0200 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Aug 29 07:50:28 2018 +0100 @@ -37,7 +37,7 @@ lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise] -subsection \Intro rules for @{term bounded_linear}\ +subsection%unimportant \Intro rules for @{term bounded_linear}\ named_theorems bounded_linear_intros @@ -79,7 +79,7 @@ bounded_linear_inner_right_comp -subsection \declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\ +subsection%unimportant \declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\ attribute_setup bounded_linear = \Scan.succeed (Thm.declaration_attribute (fn thm => @@ -112,9 +112,9 @@ ]))\ -subsection \type of bounded linear functions\ +subsection \Type of bounded linear functions\ -typedef (overloaded) ('a, 'b) blinfun ("(_ \\<^sub>L /_)" [22, 21] 21) = +typedef%important (overloaded) ('a, 'b) blinfun ("(_ \\<^sub>L /_)" [22, 21] 21) = "{f::'a::real_normed_vector\'b::real_normed_vector. bounded_linear f}" morphisms blinfun_apply Blinfun by (blast intro: bounded_linear_intros) @@ -135,12 +135,12 @@ by (auto simp: Blinfun_inverse) -subsection \type class instantiations\ +subsection \Type class instantiations\ instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector begin -lift_definition norm_blinfun :: "'a \\<^sub>L 'b \ real" is onorm . +lift_definition%important norm_blinfun :: "'a \\<^sub>L 'b \ real" is onorm . lift_definition minus_blinfun :: "'a \\<^sub>L 'b \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" is "\f g x. f x - g x" @@ -158,14 +158,14 @@ lift_definition uminus_blinfun :: "'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" is "\f x. - f x" by (rule bounded_linear_minus) -lift_definition zero_blinfun :: "'a \\<^sub>L 'b" is "\x. 0" +lift_definition%important zero_blinfun :: "'a \\<^sub>L 'b" is "\x. 0" by (rule bounded_linear_zero) -lift_definition plus_blinfun :: "'a \\<^sub>L 'b \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" +lift_definition%important plus_blinfun :: "'a \\<^sub>L 'b \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" is "\f g x. f x + g x" by (metis bounded_linear_add) -lift_definition scaleR_blinfun::"real \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" is "\r f x. r *\<^sub>R f x" +lift_definition%important scaleR_blinfun::"real \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" is "\r f x. r *\<^sub>R f x" by (metis bounded_linear_compose bounded_linear_scaleR_right) definition sgn_blinfun :: "'a \\<^sub>L 'b \ 'a \\<^sub>L 'b" @@ -365,7 +365,7 @@ by (rule convergentI) qed -subsection \On Euclidean Space\ +subsection%unimportant \On Euclidean Space\ lemma Zfun_sum: assumes "finite s" @@ -586,7 +586,7 @@ qed -subsection \concrete bounded linear functions\ +subsection%unimportant \concrete bounded linear functions\ lemma transfer_bounded_bilinear_bounded_linearI: assumes "g = (\i x. (blinfun_apply (f i) x))" diff -r 99f0aee4adbd -r 5e013478bced src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Tue Aug 28 21:08:42 2018 +0200 +++ b/src/HOL/Analysis/Derivative.thy Wed Aug 29 07:50:28 2018 +0100 @@ -3,7 +3,7 @@ Author: Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP *) -section \Multivariate calculus in Euclidean space\ +section \Derivative\ theory Derivative imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function @@ -20,11 +20,11 @@ by (intro derivative_eq_intros) auto -subsection \Derivative with composed bilinear function\ +subsection%unimportant \Derivative with composed bilinear function\ text \More explicit epsilon-delta forms.\ -lemma has_derivative_within': +proposition has_derivative_within': "(f has_derivative f')(at x within s) \ bounded_linear f' \ (\e>0. \d>0. \x'\s. 0 < norm (x' - x) \ norm (x' - x) < d \ @@ -92,7 +92,7 @@ subsection \Differentiability\ -definition +definition%important differentiable_on :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a set \ bool" (infix "differentiable'_on" 50) where "f differentiable_on s \ (\x\s. f differentiable (at x within s))" @@ -113,7 +113,7 @@ "(\x. x \ s \ f differentiable at x) \ f differentiable_on s" by (metis differentiable_at_withinI differentiable_on_def) -corollary differentiable_iff_scaleR: +corollary%unimportant differentiable_iff_scaleR: fixes f :: "real \ 'a::real_normed_vector" shows "f differentiable F \ (\d. (f has_derivative (\x. x *\<^sub>R d)) F)" by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR) @@ -211,7 +211,7 @@ definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)" -lemma frechet_derivative_works: +proposition frechet_derivative_works: "f differentiable net \ (f has_derivative (frechet_derivative f net)) net" unfolding frechet_derivative_def differentiable_def unfolding some_eq_ex[of "\ f' . (f has_derivative f') net"] .. @@ -223,7 +223,7 @@ subsection \Differentiability implies continuity\ -lemma differentiable_imp_continuous_within: +proposition differentiable_imp_continuous_within: "f differentiable (at x within s) \ continuous (at x within s) f" by (auto simp: differentiable_def intro: has_derivative_continuous) @@ -288,7 +288,7 @@ subsection \The chain rule\ -lemma diff_chain_within[derivative_intros]: +proposition diff_chain_within[derivative_intros]: assumes "(f has_derivative f') (at x within s)" and "(g has_derivative g') (at (f x) within (f ` s))" shows "((g \ f) has_derivative (g' \ f'))(at x within s)" @@ -324,7 +324,7 @@ by (auto simp: o_def mult.commute has_vector_derivative_def) -subsection \Composition rules stated just for differentiability\ +subsection%unimportant \Composition rules stated just for differentiability\ lemma differentiable_chain_at: "f differentiable (at x) \ @@ -342,12 +342,12 @@ subsection \Uniqueness of derivative\ -text \ +text%important \ The general result is a bit messy because we need approachability of the limit point from any direction. But OK for nontrivial intervals etc. \ -lemma frechet_derivative_unique_within: +proposition frechet_derivative_unique_within: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes 1: "(f has_derivative f') (at x within S)" and 2: "(f has_derivative f'') (at x within S)" @@ -414,7 +414,7 @@ qed qed -lemma frechet_derivative_unique_within_closed_interval: +proposition frechet_derivative_unique_within_closed_interval: fixes f::"'a::euclidean_space \ 'b::real_normed_vector" assumes ab: "\i. i\Basis \ a\i < b\i" and x: "x \ cbox a b" @@ -611,7 +611,7 @@ subsection \One-dimensional mean value theorem\ -lemma mvt: +theorem mvt: fixes f :: "real \ real" assumes "a < b" and contf: "continuous_on {a..b} f" @@ -1242,7 +1242,7 @@ text \Here's the simplest way of not assuming much about g.\ -lemma has_derivative_inverse: +proposition has_derivative_inverse: fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "compact S" and "x \ S" @@ -1265,7 +1265,9 @@ qed -subsection \Proving surjectivity via Brouwer fixpoint theorem\ +subsection \Inverse function theorem\ + +text \Proving surjectivity via Brouwer fixpoint theorem\ lemma brouwer_surjective: fixes f :: "'n::euclidean_space \ 'n" @@ -1493,7 +1495,7 @@ text \On a region.\ -lemma has_derivative_inverse_on: +theorem has_derivative_inverse_on: fixes f :: "'n::euclidean_space \ 'n" assumes "open S" and derf: "\x. x \ S \ (f has_derivative f'(x)) (at x)" @@ -1650,7 +1652,7 @@ done qed -lemma has_derivative_sequence: +proposition has_derivative_sequence: fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" assumes "convex S" and derf: "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)" @@ -1896,7 +1898,7 @@ subsection \Differentiation of a series\ -lemma has_derivative_series: +proposition has_derivative_series: fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" assumes "convex S" and "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)" @@ -1999,6 +2001,8 @@ shows "(\x. \n. f n x) differentiable (at x0)" using differentiable_series[OF assms, of x0] \x0 \ S\ by blast+ +subsection \Derivative as a vector\ + text \Considering derivative @{typ "real \ 'b::real_normed_vector"} as a vector.\ definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" @@ -2032,7 +2036,7 @@ lemma differentiableI_vector: "(f has_vector_derivative y) F \ f differentiable F" by (auto simp: differentiable_def has_vector_derivative_def) -lemma vector_derivative_works: +proposition vector_derivative_works: "f differentiable net \ (f has_vector_derivative (vector_derivative f net)) net" (is "?l = ?r") proof @@ -2086,55 +2090,6 @@ apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono) done -definition deriv :: "('a \ 'a::real_normed_field) \ 'a \ 'a" where - "deriv f x \ SOME D. DERIV f x :> D" - -lemma DERIV_imp_deriv: "DERIV f x :> f' \ deriv f x = f'" - unfolding deriv_def by (metis some_equality DERIV_unique) - -lemma DERIV_deriv_iff_has_field_derivative: - "DERIV f x :> deriv f x \ (\f'. (f has_field_derivative f') (at x))" - by (auto simp: has_field_derivative_def DERIV_imp_deriv) - -lemma DERIV_deriv_iff_real_differentiable: - fixes x :: real - shows "DERIV f x :> deriv f x \ f differentiable at x" - unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff) - -lemma deriv_cong_ev: - assumes "eventually (\x. f x = g x) (nhds x)" "x = y" - shows "deriv f x = deriv g y" -proof - - have "(\D. (f has_field_derivative D) (at x)) = (\D. (g has_field_derivative D) (at y))" - by (intro ext DERIV_cong_ev refl assms) - thus ?thesis by (simp add: deriv_def assms) -qed - -lemma higher_deriv_cong_ev: - assumes "eventually (\x. f x = g x) (nhds x)" "x = y" - shows "(deriv ^^ n) f x = (deriv ^^ n) g y" -proof - - from assms(1) have "eventually (\x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)" - proof (induction n arbitrary: f g) - case (Suc n) - from Suc.prems have "eventually (\y. eventually (\z. f z = g z) (nhds y)) (nhds x)" - by (simp add: eventually_eventually) - hence "eventually (\x. deriv f x = deriv g x) (nhds x)" - by eventually_elim (rule deriv_cong_ev, simp_all) - thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps) - qed auto - from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp -qed - -lemma real_derivative_chain: - fixes x :: real - shows "f differentiable at x \ g differentiable at (f x) - \ deriv (g o f) x = deriv g (f x) * deriv f x" - by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv) -lemma field_derivative_eq_vector_derivative: - "(deriv f x) = vector_derivative f (at x)" -by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def) - lemma islimpt_closure_open: fixes s :: "'a::perfect_space set" assumes "open s" and t: "t = closure s" "x \ t" @@ -2312,7 +2267,7 @@ subsection\The notion of being field differentiable\ -definition field_differentiable :: "['a \ 'a::real_normed_field, 'a filter] \ bool" +definition%important field_differentiable :: "['a \ 'a::real_normed_field, 'a filter] \ bool" (infixr "(field'_differentiable)" 50) where "f field_differentiable F \ \f'. (f has_field_derivative f') F" @@ -2321,10 +2276,6 @@ unfolding field_differentiable_def differentiable_def using has_field_derivative_imp_has_derivative by auto -lemma field_differentiable_derivI: - "f field_differentiable (at x) \ (f has_field_derivative deriv f x) (at x)" -by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative) - lemma field_differentiable_imp_continuous_at: "f field_differentiable (at x within S) \ continuous (at x within S) f" by (metis DERIV_continuous field_differentiable_def) @@ -2434,12 +2385,6 @@ unfolding field_differentiable_def by (metis at_within_open) -lemma vector_derivative_chain_at_general: - assumes "f differentiable at x" "g field_differentiable at (f x)" - shows "vector_derivative (g \ f) (at x) = vector_derivative f (at x) * deriv g (f x)" - apply (rule vector_derivative_at [OF field_vector_diff_chain_at]) - using assms vector_derivative_works by (auto simp: field_differentiable_derivI) - lemma exp_scaleR_has_vector_derivative_right: "((\t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)" unfolding has_vector_derivative_def @@ -2515,11 +2460,72 @@ using exp_scaleR_has_vector_derivative_right[of A t] by (simp add: exp_times_scaleR_commute) +subsection \Field derivative\ + +definition%important deriv :: "('a \ 'a::real_normed_field) \ 'a \ 'a" where + "deriv f x \ SOME D. DERIV f x :> D" + +lemma DERIV_imp_deriv: "DERIV f x :> f' \ deriv f x = f'" + unfolding deriv_def by (metis some_equality DERIV_unique) + +lemma DERIV_deriv_iff_has_field_derivative: + "DERIV f x :> deriv f x \ (\f'. (f has_field_derivative f') (at x))" + by (auto simp: has_field_derivative_def DERIV_imp_deriv) + +lemma DERIV_deriv_iff_real_differentiable: + fixes x :: real + shows "DERIV f x :> deriv f x \ f differentiable at x" + unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff) + +lemma deriv_cong_ev: + assumes "eventually (\x. f x = g x) (nhds x)" "x = y" + shows "deriv f x = deriv g y" +proof - + have "(\D. (f has_field_derivative D) (at x)) = (\D. (g has_field_derivative D) (at y))" + by (intro ext DERIV_cong_ev refl assms) + thus ?thesis by (simp add: deriv_def assms) +qed + +lemma higher_deriv_cong_ev: + assumes "eventually (\x. f x = g x) (nhds x)" "x = y" + shows "(deriv ^^ n) f x = (deriv ^^ n) g y" +proof - + from assms(1) have "eventually (\x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)" + proof (induction n arbitrary: f g) + case (Suc n) + from Suc.prems have "eventually (\y. eventually (\z. f z = g z) (nhds y)) (nhds x)" + by (simp add: eventually_eventually) + hence "eventually (\x. deriv f x = deriv g x) (nhds x)" + by eventually_elim (rule deriv_cong_ev, simp_all) + thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps) + qed auto + from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp +qed + +lemma real_derivative_chain: + fixes x :: real + shows "f differentiable at x \ g differentiable at (f x) + \ deriv (g o f) x = deriv g (f x) * deriv f x" + by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv) +lemma field_derivative_eq_vector_derivative: + "(deriv f x) = vector_derivative f (at x)" +by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def) + +proposition field_differentiable_derivI: + "f field_differentiable (at x) \ (f has_field_derivative deriv f x) (at x)" +by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative) + +lemma vector_derivative_chain_at_general: + assumes "f differentiable at x" "g field_differentiable at (f x)" + shows "vector_derivative (g \ f) (at x) = vector_derivative f (at x) * deriv g (f x)" + apply (rule vector_derivative_at [OF field_vector_diff_chain_at]) + using assms vector_derivative_works by (auto simp: field_differentiable_derivI) + subsection \Relation between convexity and derivative\ (* TODO: Generalise to real vector spaces? *) -lemma convex_on_imp_above_tangent: +proposition convex_on_imp_above_tangent: assumes convex: "convex_on A f" and connected: "connected A" assumes c: "c \ interior A" and x : "x \ A" assumes deriv: "(f has_field_derivative f') (at c within A)" @@ -2602,7 +2608,7 @@ by (auto intro!: exI[where x="UNIV \ S"] S open_Times) qed -lemma has_derivative_partialsI: +proposition has_derivative_partialsI: fixes f::"'a::real_normed_vector \ 'b::real_normed_vector \ 'c::real_normed_vector" assumes fx: "((\x. f x y) has_derivative fx) (at x within X)" assumes fy: "\x y. x \ X \ y \ Y \ ((\y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)" @@ -2767,7 +2773,7 @@ qed -subsection \Differentiable case distinction\ +subsection%unimportant \Differentiable case distinction\ lemma has_derivative_within_If_eq: "((\x. if P x then f x else g x) has_derivative f') (at x within S) = diff -r 99f0aee4adbd -r 5e013478bced src/HOL/Analysis/Lipschitz.thy --- a/src/HOL/Analysis/Lipschitz.thy Tue Aug 28 21:08:42 2018 +0200 +++ b/src/HOL/Analysis/Lipschitz.thy Wed Aug 29 07:50:28 2018 +0100 @@ -7,11 +7,11 @@ imports Borel_Space begin -definition lipschitz_on +definition%important lipschitz_on where "lipschitz_on C U f \ (0 \ C \ (\x \ U. \y\U. dist (f x) (f y) \ C * dist x y))" bundle lipschitz_syntax begin -notation lipschitz_on ("_-lipschitz'_on" [1000]) +notation%important lipschitz_on ("_-lipschitz'_on" [1000]) end bundle no_lipschitz_syntax begin no_notation lipschitz_on ("_-lipschitz'_on" [1000]) @@ -103,7 +103,7 @@ qed qed (rule lipschitz_on_nonneg[OF f]) -proposition lipschitz_on_concat_max: +lemma lipschitz_on_concat_max: fixes a b c::real assumes f: "L-lipschitz_on {a .. b} f" assumes g: "M-lipschitz_on {b .. c} g" @@ -118,7 +118,7 @@ subsubsection \Continuity\ -lemma lipschitz_on_uniformly_continuous: +proposition lipschitz_on_uniformly_continuous: assumes "L-lipschitz_on X f" shows "uniformly_continuous_on X f" unfolding uniformly_continuous_on_def @@ -132,7 +132,7 @@ by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps) qed -lemma lipschitz_on_continuous_on: +proposition lipschitz_on_continuous_on: "continuous_on X f" if "L-lipschitz_on X f" by (rule uniformly_continuous_imp_continuous[OF lipschitz_on_uniformly_continuous[OF that]]) @@ -143,7 +143,7 @@ subsubsection \Differentiable functions\ -lemma bounded_derivative_imp_lipschitz: +proposition bounded_derivative_imp_lipschitz: assumes "\x. x \ X \ (f has_derivative f' x) (at x within X)" assumes convex: "convex X" assumes "\x. x \ X \ onorm (f' x) \ C" "0 \ C" @@ -154,7 +154,7 @@ qed fact -subsubsection \Structural introduction rules\ +subsubsection%unimportant \Structural introduction rules\ named_theorems lipschitz_intros "structural introduction rules for Lipschitz controls" @@ -480,7 +480,7 @@ subsection \Local Lipschitz continuity (uniform for a family of functions)\ -definition local_lipschitz:: +definition%important local_lipschitz:: "'a::metric_space set \ 'b::metric_space set \ ('a \ 'b \ 'c::metric_space) \ bool" where "local_lipschitz T X f \ \x \ X. \t \ T. @@ -785,7 +785,7 @@ by (auto intro: exI[where x=1]) qed -lemma c1_implies_local_lipschitz: +proposition c1_implies_local_lipschitz: fixes T::"real set" and X::"'a::{banach,heine_borel} set" and f::"real \ 'a \ 'a" assumes f': "\t x. t \ T \ x \ X \ (f t has_derivative blinfun_apply (f' (t, x))) (at x)" diff -r 99f0aee4adbd -r 5e013478bced src/HOL/Analysis/Uniform_Limit.thy --- a/src/HOL/Analysis/Uniform_Limit.thy Tue Aug 28 21:08:42 2018 +0200 +++ b/src/HOL/Analysis/Uniform_Limit.thy Wed Aug 29 07:50:28 2018 +0100 @@ -9,10 +9,13 @@ imports Connected Summation_Tests begin -definition uniformly_on :: "'a set \ ('a \ 'b::metric_space) \ ('a \ 'b) filter" + +subsection \Definition\ + +definition%important uniformly_on :: "'a set \ ('a \ 'b::metric_space) \ ('a \ 'b) filter" where "uniformly_on S l = (INF e:{0 <..}. principal {f. \x\S. dist (f x) (l x) < e})" -abbreviation +abbreviation%important "uniform_limit S f l \ filterlim f (uniformly_on S l)" definition uniformly_convergent_on where @@ -21,7 +24,7 @@ definition uniformly_Cauchy_on where "uniformly_Cauchy_on X f \ (\e>0. \M. \x\X. \(m::nat)\M. \n\M. dist (f m x) (f n x) < e)" -lemma uniform_limit_iff: +proposition uniform_limit_iff: "uniform_limit S f l F \ (\e>0. \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e)" unfolding filterlim_iff uniformly_on_def by (subst eventually_INF_base) @@ -64,7 +67,10 @@ by eventually_elim force qed -lemma swap_uniform_limit: + +subsection \Exchange limits\ + +proposition swap_uniform_limit: assumes f: "\\<^sub>F n in F. (f n \ g n) (at x within S)" assumes g: "(g \ l) F" assumes uc: "uniform_limit S f h F" @@ -108,6 +114,9 @@ using eventually_happens by (metis \\trivial_limit F\) qed + +subsection \Uniform limit theorem\ + lemma tendsto_uniform_limitI: assumes "uniform_limit S f l F" assumes "x \ S" @@ -115,7 +124,7 @@ using assms by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD) -lemma uniform_limit_theorem: +theorem uniform_limit_theorem: assumes c: "\\<^sub>F n in F. continuous_on A (f n)" assumes ul: "uniform_limit A f l F" assumes "\ trivial_limit F" @@ -307,7 +316,10 @@ unfolding uniformly_convergent_on_def convergent_def by (auto dest: tendsto_uniform_limitI) -lemma weierstrass_m_test_ev: + +subsection \Weierstrass M-Test\ + +proposition weierstrass_m_test_ev: fixes f :: "_ \ _ \ _ :: banach" assumes "eventually (\n. \x\A. norm (f n x) \ M n) sequentially" assumes "summable M" @@ -354,7 +366,7 @@ qed text\Alternative version, formulated as in HOL Light\ -corollary series_comparison_uniform: +corollary%unimportant series_comparison_uniform: fixes f :: "_ \ nat \ _ :: banach" assumes g: "summable g" and le: "\n x. N \ n \ x \ A \ norm(f x n) \ g n" shows "\l. \e. 0 < e \ (\N. \n x. N \ n \ x \ A \ dist(sum (f x) {.. _ \