# HG changeset patch # User hoelzl # Date 1443192871 -7200 # Node ID b77bf45efe21c9da659a94d4bdcd19b0b8d90cda # Parent 6026c14f5e5dc3dc127b62a10bf49660bb343b48 prove Liminf_inverse_ereal diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Filter.thy --- a/src/HOL/Filter.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Filter.thy Fri Sep 25 16:54:31 2015 +0200 @@ -390,6 +390,9 @@ lemma frequently_const[simp]: "F \ bot \ frequently (\x. P) F \ P" by (simp add: frequently_const_iff) +lemma eventually_happens: "eventually P net \ net = bot \ (\x. P x)" + by (metis frequentlyE eventually_frequently) + abbreviation (input) trivial_limit :: "'a filter \ bool" where "trivial_limit F \ F = bot" diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Library/Extended_Real.thy Fri Sep 25 16:54:31 2015 +0200 @@ -1732,6 +1732,14 @@ apply (auto split: ereal.split simp: ereal_uminus_reorder) [] done +lemma at_infty_ereal_eq_at_top: "at \ = filtermap ereal at_top" + unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap + top_ereal_def[symmetric] + apply (subst eventually_nhds_top[of 0]) + apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split) + apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans) + done + lemma ereal_Lim_uminus: "(f ---> f0) net \ ((\x. - f x::ereal) ---> - f0) net" using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\x. - f x" "- f0" net] by auto @@ -3589,6 +3597,34 @@ unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense using lim_ereal by (simp_all add: comp_def) +lemma inverse_infty_ereal_tendsto_0: "inverse -- \ --> (0::ereal)" +proof - + have **: "((\x. ereal (inverse x)) ---> ereal 0) at_infinity" + by (intro tendsto_intros tendsto_inverse_0) + + show ?thesis + by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def) + (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity + intro!: filterlim_mono_eventually[OF **]) +qed + +lemma inverse_ereal_tendsto_pos: + fixes x :: ereal assumes "0 < x" + shows "inverse -- x --> inverse x" +proof (cases x) + case (real r) + with `0 < x` have **: "(\x. ereal (inverse x)) -- r --> ereal (inverse r)" + by (auto intro!: tendsto_inverse) + from real \0 < x\ show ?thesis + by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter + intro!: Lim_transform_eventually[OF _ **] t1_space_nhds) +qed (insert \0 < x\, auto intro!: inverse_infty_ereal_tendsto_0) + +lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \) (at_right (0::ereal))" + unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def + by (subst filterlim_cong[OF refl refl, where g="\x. ereal (inverse x)"]) + (auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right) + lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2 lemma continuous_at_iff_ereal: diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Library/Liminf_Limsup.thy Fri Sep 25 16:54:31 2015 +0200 @@ -150,6 +150,17 @@ shows "Limsup F X \ C" using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp +lemma le_Limsup: + assumes F: "F \ bot" and x: "\\<^sub>F x in F. l \ f x" + shows "l \ Limsup F f" +proof - + have "l = Limsup F (\x. l)" + using F by (simp add: Limsup_const) + also have "\ \ Limsup F f" + by (intro Limsup_mono x) + finally show ?thesis . +qed + lemma le_Liminf_iff: fixes X :: "_ \ _ :: complete_linorder" shows "C \ Liminf F X \ (\yx. y < X x) F)" @@ -308,4 +319,33 @@ then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def) qed +lemma continuous_on_imp_continuous_within: "continuous_on s f \ t \ s \ x \ s \ continuous (at x within t) f" + unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset) + +lemma Liminf_compose_continuous_antimono: + fixes f :: "'a::{complete_linorder, linorder_topology} \ 'b::{complete_linorder, linorder_topology}" + assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \ bot" + shows "Liminf F (\n. f (g n)) = f (Limsup F g)" +proof - + { fix P assume "eventually P F" + have "\x. P x" + proof (rule ccontr) + assume "\ (\x. P x)" then have "P = (\x. False)" + by auto + with \eventually P F\ F show False + by auto + qed } + note * = this + + have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" + unfolding Limsup_def INF_def + by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) + (auto intro: eventually_True) + also have "\ = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" + by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) + (auto dest!: eventually_happens simp: F) + finally show ?thesis + by (auto simp: Liminf_def) +qed + end diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Sep 25 16:54:31 2015 +0200 @@ -2200,18 +2200,35 @@ definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" -lemma vector_derivative_unique_at: - assumes "(f has_vector_derivative f') (at x)" - and "(f has_vector_derivative f'') (at x)" +lemma vector_derivative_unique_within: + assumes not_bot: "at x within s \ bot" + and f': "(f has_vector_derivative f') (at x within s)" + and f'': "(f has_vector_derivative f'') (at x within s)" shows "f' = f''" proof - have "(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" - using assms [unfolded has_vector_derivative_def] - by (rule frechet_derivative_unique_at) + proof (rule frechet_derivative_unique_within) + show "\i\Basis. \e>0. \d. 0 < \d\ \ \d\ < e \ x + d *\<^sub>R i \ s" + proof clarsimp + fix e :: real assume "0 < e" + with islimpt_approachable_real[of x s] not_bot + obtain x' where "x' \ s" "x' \ x" "\x' - x\ < e" + by (auto simp add: trivial_limit_within) + then show "\d. d \ 0 \ \d\ < e \ x + d \ s" + by (intro exI[of _ "x' - x"]) auto + qed + qed (insert f' f'', auto simp: has_vector_derivative_def) then show ?thesis unfolding fun_eq_iff by auto qed +lemma vector_derivative_unique_at: + "(f has_vector_derivative f') (at x) \ (f has_vector_derivative f'') (at x) \ f' = f''" + by (rule vector_derivative_unique_within) auto + +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: "f differentiable net \ (f has_vector_derivative (vector_derivative f net)) net" (is "?l = ?r") @@ -2226,38 +2243,44 @@ by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f') qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def) +lemma vector_derivative_within: + assumes not_bot: "at x within s \ bot" and y: "(f has_vector_derivative y) (at x within s)" + shows "vector_derivative f (at x within s) = y" + using y + by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y]) + (auto simp: differentiable_def has_vector_derivative_def) + +lemma islimpt_closure_open: + fixes s :: "'a::perfect_space set" + assumes "open s" and t: "t = closure s" "x \ t" + shows "x islimpt t" +proof cases + assume "x \ s" + { fix T assume "x \ T" "open T" + then have "open (s \ T)" + using \open s\ by auto + then have "s \ T \ {x}" + using not_open_singleton[of x] by auto + with \x \ T\ \x \ s\ have "\y\t. y \ T \ y \ x" + using closure_subset[of s] by (auto simp: t) } + then show ?thesis + by (auto intro!: islimptI) +next + assume "x \ s" with t show ?thesis + unfolding t closure_def by (auto intro: islimpt_subset) +qed + lemma vector_derivative_unique_within_closed_interval: - assumes "a < b" - and "x \ cbox a b" - assumes "(f has_vector_derivative f') (at x within cbox a b)" - assumes "(f has_vector_derivative f'') (at x within cbox a b)" + assumes ab: "a < b" "x \ cbox a b" + assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)" shows "f' = f''" -proof - - have *: "(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" - apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"]) - using assms(3-)[unfolded has_vector_derivative_def] - using assms(1-2) - apply auto - done - show ?thesis - proof (rule ccontr) - assume **: "f' \ f''" - with * have "(\x. x *\<^sub>R f') 1 = (\x. x *\<^sub>R f'') 1" - by (auto simp: fun_eq_iff) - with ** show False - unfolding o_def by auto - qed -qed + using ab + by (intro vector_derivative_unique_within[OF _ D]) + (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"]) lemma vector_derivative_at: "(f has_vector_derivative f') (at x) \ vector_derivative f (at x) = f'" - apply (rule vector_derivative_unique_at) - defer - apply assumption - unfolding vector_derivative_works[symmetric] differentiable_def - unfolding has_vector_derivative_def - apply auto - done + by (intro vector_derivative_within at_neq_bot) lemma has_vector_derivative_id_at [simp]: "vector_derivative (\x. x) (at a) = 1" by (simp add: vector_derivative_at) @@ -2292,15 +2315,12 @@ done lemma vector_derivative_within_closed_interval: - assumes "a < b" - and "x \ cbox a b" - assumes "(f has_vector_derivative f') (at x within cbox a b)" + assumes ab: "a < b" "x \ cbox a b" + assumes f: "(f has_vector_derivative f') (at x within cbox a b)" shows "vector_derivative f (at x within cbox a b) = f'" - apply (rule vector_derivative_unique_within_closed_interval) - using vector_derivative_works[unfolded differentiable_def] - using assms - apply (auto simp add:has_vector_derivative_def) - done + by (intro vector_derivative_unique_within_closed_interval[OF ab _ f] + vector_derivative_works[THEN iffD1] differentiableI_vector) + fact lemma has_vector_derivative_within_subset: "(f has_vector_derivative f') (at x within s) \ t \ s \ (f has_vector_derivative f') (at x within t)" diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Sep 25 16:54:31 2015 +0200 @@ -313,6 +313,46 @@ apply (metis INF_absorb centre_in_ball) done +lemma continuous_on_inverse_ereal: "continuous_on {0::ereal ..} inverse" + unfolding continuous_on_def +proof clarsimp + fix x :: ereal assume "0 \ x" + moreover have "at 0 within {0 ..} = at_right (0::ereal)" + by (auto simp: filter_eq_iff eventually_at_filter le_less) + moreover have "0 < x \ at x within {0 ..} = at x" + using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \"]) + ultimately show "(inverse ---> inverse x) (at x within {0..})" + by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos) +qed + + +lemma Liminf_inverse_ereal: + assumes nneg: "\\<^sub>F x in F. f x \ (0 :: ereal)" and "F \ bot" + shows "Liminf F (\n. inverse (f n)) = inverse (Limsup F f)" +proof - + def I \ "\x::ereal. if x \ 0 then \ else inverse x" + have "Liminf F (\n. I (f n)) = I (Limsup F f)" + proof (rule Liminf_compose_continuous_antimono) + have "continuous_on ({.. 0} \ {0 ..}) I" + unfolding I_def by (intro continuous_on_cases) (auto intro: continuous_on_const continuous_on_inverse_ereal) + also have "{.. 0} \ {0::ereal ..} = UNIV" + by auto + finally show "continuous_on UNIV I" . + show "antimono I" + unfolding antimono_def I_def by (auto intro: ereal_inverse_antimono) + qed fact + also have "Liminf F (\n. I (f n)) = Liminf F (\n. inverse (f n))" + proof (rule Liminf_eq) + show "\\<^sub>F x in F. I (f x) = inverse (f x)" + using nneg by eventually_elim (auto simp: I_def) + qed + also have "0 \ Limsup F f" + by (intro le_Limsup) fact+ + then have "I (Limsup F f) = inverse (Limsup F f)" + by (auto simp: I_def) + finally show ?thesis . +qed + subsection \monoset\ definition (in order) mono_set: diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 25 16:54:31 2015 +0200 @@ -1551,6 +1551,43 @@ qed qed +lemma interior_Ici: + fixes x :: "'a :: {dense_linorder, linorder_topology}" + assumes "b < x" + shows "interior { x ..} = { x <..}" +proof (rule interior_unique) + fix T assume "T \ {x ..}" "open T" + moreover have "x \ T" + proof + assume "x \ T" + obtain y where "y < x" "{y <.. x} \ T" + using open_left[OF \open T\ \x \ T\ \b < x\] by auto + with dense[OF \y < x\] obtain z where "z \ T" "z < x" + by (auto simp: subset_eq Ball_def) + with \T \ {x ..}\ show False by auto + qed + ultimately show "T \ {x <..}" + by (auto simp: subset_eq less_le) +qed auto + +lemma interior_Iic: + fixes x :: "'a :: {dense_linorder, linorder_topology}" + assumes "x < b" + shows "interior {.. x} = {..< x}" +proof (rule interior_unique) + fix T assume "T \ {.. x}" "open T" + moreover have "x \ T" + proof + assume "x \ T" + obtain y where "x < y" "{x ..< y} \ T" + using open_right[OF \open T\ \x \ T\ \x < b\] by auto + with dense[OF \x < y\] obtain z where "z \ T" "x < z" + by (auto simp: subset_eq Ball_def less_le) + with \T \ {.. x}\ show False by auto + qed + ultimately show "T \ {..< x}" + by (auto simp: subset_eq less_le) +qed auto subsection \Closure of a Set\ @@ -1763,10 +1800,6 @@ text \Some property holds "sufficiently close" to the limit point.\ -lemma eventually_happens: "eventually P net \ trivial_limit net \ (\x. P x)" - unfolding trivial_limit_def - by (auto elim: eventually_rev_mp) - lemma trivial_limit_eventually: "trivial_limit net \ eventually P net" by simp diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Topological_Spaces.thy Fri Sep 25 16:54:31 2015 +0200 @@ -381,6 +381,17 @@ "a \ s \ open s \ NO_MATCH UNIV s \ at a within s = at a" by (simp only: at_within_open) +lemma at_within_nhd: + assumes "x \ S" "open S" "T \ S - {x} = U \ S - {x}" + shows "at x within T = at x within U" + unfolding filter_eq_iff eventually_at_filter +proof (intro allI eventually_subst) + have "eventually (\x. x \ S) (nhds x)" + using \x \ S\ \open S\ by (auto simp: eventually_nhds) + then show "\\<^sub>F n in nhds x. (n \ x \ n \ T \ P n) = (n \ x \ n \ U \ P n)" for P + by eventually_elim (insert \T \ S - {x} = U \ S - {x}\, blast) +qed + lemma at_within_empty [simp]: "at a within {} = bot" unfolding at_within_def by simp @@ -1574,7 +1585,7 @@ "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \ continuous (at_right x) f)" by (simp add: continuous_within filterlim_at_split) -subsubsection\Open-cover compactness\ +subsubsection \Open-cover compactness\ context topological_space begin