# HG changeset patch # User paulson # Date 1568814097 -3600 # Node ID 4e39d87c9737f0dc9e094f7f4d52a5abc7f80a68 # Parent ae2528273eeb8f2b5eedf24a19f917773d701d1d imported new material mostly due to Sébastien Gouëzel diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Sep 18 14:41:37 2019 +0100 @@ -2179,6 +2179,11 @@ shows "continuous F (\x. infdist (f x) A)" using assms unfolding continuous_def by (rule tendsto_infdist) +lemma continuous_on_infdist [continuous_intros]: + assumes "continuous_on S f" + shows "continuous_on S (\x. infdist (f x) A)" +using assms unfolding continuous_on by (auto intro: tendsto_infdist) + lemma compact_infdist_le: fixes A::"'a::heine_borel set" assumes "A \ {}" @@ -3231,9 +3236,6 @@ by (auto simp: setdist_def infdist_def) qed -lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\y. infdist y A)" - by (simp add: continuous_on_setdist infdist_eq_setdist) - proposition setdist_attains_inf: assumes "compact B" "B \ {}" obtains y where "y \ B" "setdist A B = infdist y A" @@ -3244,7 +3246,7 @@ next case False obtain y where "y \ B" and min: "\y'. y' \ B \ infdist y A \ infdist y' A" - using continuous_attains_inf [OF assms continuous_on_infdist] by blast + by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id) show thesis proof have "setdist A B = (INF y\B. infdist y A)" @@ -3266,4 +3268,4 @@ qed (fact \y \ B\) qed -end \ No newline at end of file +end diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1219,8 +1219,10 @@ finally show ?thesis . qed -lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)" - by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric]) +lemma lborel_distr_plus: + fixes c :: "'a::euclidean_space" + shows "distr lborel borel ((+) c) = lborel" +by (subst lborel_affine[of 1 c], auto simp: density_1) interpretation lborel: sigma_finite_measure lborel by (rule sigma_finite_lborel) diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Analysis/Measure_Space.thy Wed Sep 18 14:41:37 2019 +0100 @@ -472,10 +472,23 @@ "a \ sets M \ b \ sets M \ a \ b = {} \ emeasure M a + emeasure M b = emeasure M (a \ b)" using additiveD[OF emeasure_additive] .. -lemma emeasure_Union: +lemma emeasure_Un: "A \ sets M \ B \ sets M \ emeasure M (A \ B) = emeasure M A + emeasure M (B - A)" using plus_emeasure[of A M "B - A"] by auto +lemma emeasure_Un_Int: + assumes "A \ sets M" "B \ sets M" + shows "emeasure M A + emeasure M B = emeasure M (A \ B) + emeasure M (A \ B)" +proof - + have "A = (A-B) \ (A \ B)" by auto + then have "emeasure M A = emeasure M (A-B) + emeasure M (A \ B)" + by (metis Diff_Diff_Int Diff_disjoint assms plus_emeasure sets.Diff) + moreover have "A \ B = (A-B) \ B" by auto + then have "emeasure M (A \ B) = emeasure M (A-B) + emeasure M B" + by (metis Diff_disjoint Int_commute assms plus_emeasure sets.Diff) + ultimately show ?thesis by (metis add.assoc add.commute) +qed + lemma sum_emeasure: "F`I \ sets M \ disjoint_family_on F I \ finite I \ (\i\I. emeasure M (F i)) = emeasure M (\i\I. F i)" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Finite_Set.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1493,12 +1493,11 @@ using card_Un_Int [of A B] by simp lemma card_Un_le: "card (A \ B) \ card A + card B" - apply (cases "finite A") - apply (cases "finite B") - apply (use le_iff_add card_Un_Int in blast) - apply simp - apply simp - done +proof (cases "finite A \ finite B") + case True + then show ?thesis + using le_iff_add card_Un_Int [of A B] by auto +qed auto lemma card_Diff_subset: assumes "finite B" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Groups_Big.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1187,6 +1187,16 @@ using assms card_eq_0_iff finite_UnionD by fastforce qed +lemma card_UN_le: + assumes "finite I" + shows "card(\i\I. A i) \ (\i\I. card(A i))" + using assms +proof induction + case (insert i I) + then show ?case + using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) +qed auto + lemma sum_multicount_gen: assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" shows "sum (\i. (card {j\t. R i j})) s = sum k t" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Limits.thy Wed Sep 18 14:41:37 2019 +0100 @@ -2392,7 +2392,7 @@ by (rule LIMSEQ_imp_Suc) (simp add: True) qed -lemma LIMSEQ_power_zero: "norm x < 1 \ (\n. x ^ n) \ 0" +lemma LIMSEQ_power_zero [tendsto_intros]: "norm x < 1 \ (\n. x ^ n) \ 0" for x :: "'a::real_normed_algebra_1" apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff) diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/CLim.thy --- a/src/HOL/Nonstandard_Analysis/CLim.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/CLim.thy Wed Sep 18 14:41:37 2019 +0100 @@ -11,7 +11,7 @@ begin (*not in simpset?*) -declare hypreal_epsilon_not_zero [simp] +declare epsilon_not_zero [simp] (*??generalize*) lemma lemma_complex_mult_inverse_squared [simp]: "x \ 0 \ x * (inverse x)\<^sup>2 = inverse x" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HDeriv.thy --- a/src/HOL/Nonstandard_Analysis/HDeriv.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Wed Sep 18 14:41:37 2019 +0100 @@ -46,7 +46,7 @@ shows "NSDERIV f x :> D \ NSDERIV f x :> E \ D = E" proof - have "\s. (s::'a star) \ Infinitesimal - {0}" - by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal hypreal_epsilon_not_zero singletonD) + by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal epsilon_not_zero singletonD) with assms show ?thesis by (meson approx_trans3 nsderiv_def star_of_approx_iff) qed diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HLim.thy --- a/src/HOL/Nonstandard_Analysis/HLim.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/HLim.thy Wed Sep 18 14:41:37 2019 +0100 @@ -93,7 +93,7 @@ have "star_of a + of_hypreal \ \ star_of a" by (simp add: approx_def) then show ?thesis - using hypreal_epsilon_not_zero that by (force simp add: NSLIM_def) + using epsilon_not_zero that by (force simp add: NSLIM_def) qed with assms show ?thesis by metis qed @@ -151,7 +151,7 @@ hnorm (starfun f x - star_of L) < star_of r" proof (rule exI, safe) show "0 < \" - by (rule hypreal_epsilon_gt_zero) + by (rule epsilon_gt_zero) next fix x assume neq: "x \ star_of a" @@ -291,7 +291,7 @@ have "\s>0. \x y. hnorm (x - y) < s \ hnorm (starfun f x - starfun f y) < star_of r" proof (rule exI, safe) show "0 < \" - by (rule hypreal_epsilon_gt_zero) + by (rule epsilon_gt_zero) next fix x y :: "'a star" assume "hnorm (x - y) < \" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HLog.thy --- a/src/HOL/Nonstandard_Analysis/HLog.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/HLog.thy Wed Sep 18 14:41:37 2019 +0100 @@ -9,15 +9,6 @@ imports HTranscendental begin - -(* should be in NSA.ML *) -lemma epsilon_ge_zero [simp]: "0 \ \" - by (simp add: epsilon_def star_n_zero_num star_n_le) - -lemma hpfinite_witness: "\ \ {x. 0 \ x \ x \ HFinite}" - by auto - - definition powhr :: "hypreal \ hypreal \ hypreal" (infixr "powhr" 80) where [transfer_unfold]: "x powhr a = starfun2 (powr) x a" @@ -39,7 +30,7 @@ lemma powhr_not_zero [simp]: "\a x. x powhr a \ 0 \ x \ 0" by transfer simp -lemma powhr_divide: "\a x y. 0 < x \ 0 < y \ (x / y) powhr a = (x powhr a) / (y powhr a)" +lemma powhr_divide: "\a x y. 0 \ x \ 0 \ y \ (x / y) powhr a = (x powhr a) / (y powhr a)" by transfer (rule powr_divide) lemma powhr_add: "\a b x. x powhr (a + b) = (x powhr a) * (x powhr b)" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HyperDef.thy --- a/src/HOL/Nonstandard_Analysis/HyperDef.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy Wed Sep 18 14:41:37 2019 +0100 @@ -229,14 +229,17 @@ by (auto simp: epsilon_def star_of_def star_n_eq_iff) qed -lemma hypreal_epsilon_not_zero: "\ \ 0" +lemma epsilon_ge_zero [simp]: "0 \ \" + by (simp add: epsilon_def star_n_zero_num star_n_le) + +lemma epsilon_not_zero: "\ \ 0" using hypreal_of_real_not_eq_epsilon by force -lemma hypreal_epsilon_inverse_omega: "\ = inverse \" +lemma epsilon_inverse_omega: "\ = inverse \" by (simp add: epsilon_def omega_def star_n_inverse) -lemma hypreal_epsilon_gt_zero: "0 < \" - by (simp add: hypreal_epsilon_inverse_omega) +lemma epsilon_gt_zero: "0 < \" + by (simp add: epsilon_inverse_omega) subsection \Embedding the Naturals into the Hyperreals\ diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/NSA.thy --- a/src/HOL/Nonstandard_Analysis/NSA.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1592,7 +1592,7 @@ lemma Infinitesimal_epsilon [simp]: "\ \ Infinitesimal" by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega - simp add: hypreal_epsilon_inverse_omega) + simp add: epsilon_inverse_omega) lemma HFinite_epsilon [simp]: "\ \ HFinite" by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]) diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/NSComplex.thy --- a/src/HOL/Nonstandard_Analysis/NSComplex.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy Wed Sep 18 14:41:37 2019 +0100 @@ -197,8 +197,8 @@ lemma hIm_hcomplex_of_hypreal [simp]: "\z. hIm (hcomplex_of_hypreal z) = 0" by transfer (rule Im_complex_of_real) -lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: "hcomplex_of_hypreal \ \ 0" - by (simp add: hypreal_epsilon_not_zero) +lemma hcomplex_of_epsilon_not_zero [simp]: "hcomplex_of_hypreal \ \ 0" + by (simp add: epsilon_not_zero) subsection \\HComplex\ theorems\ diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1981,14 +1981,12 @@ lemma Cauchy_iff2: "Cauchy X \ (\j. (\M. \m \ M. \n \ M. \X m - X n\ < inverse (real (Suc j))))" by (simp only: metric_Cauchy_iff2 dist_real_def) -lemma lim_1_over_n: "((\n. 1 / of_nat n) \ (0::'a::real_normed_field)) sequentially" +lemma lim_1_over_n [tendsto_intros]: "((\n. 1 / of_nat n) \ (0::'a::real_normed_field)) sequentially" proof (subst lim_sequentially, intro allI impI exI) - fix e :: real - assume e: "e > 0" - fix n :: nat - assume n: "n \ nat \inverse e + 1\" + fix e::real and n + assume e: "e > 0" have "inverse e < of_nat (nat \inverse e + 1\)" by linarith - also note n + also assume "n \ nat \inverse e + 1\" finally show "dist (1 / of_nat n :: 'a) 0 < e" using e by (simp add: divide_simps mult.commute norm_divide) qed diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Series.thy --- a/src/HOL/Series.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Series.thy Wed Sep 18 14:41:37 2019 +0100 @@ -585,19 +585,17 @@ text \Sum of a geometric progression.\ lemma geometric_sums: - assumes less_1: "norm c < 1" + assumes "norm c < 1" shows "(\n. c^n) sums (1 / (1 - c))" proof - - from less_1 have neq_1: "c \ 1" by auto - then have neq_0: "c - 1 \ 0" by simp - from less_1 have lim_0: "(\n. c^n) \ 0" - by (rule LIMSEQ_power_zero) + have neq_0: "c - 1 \ 0" + using assms by auto then have "(\n. c ^ n / (c - 1) - 1 / (c - 1)) \ 0 / (c - 1) - 1 / (c - 1)" - using neq_0 by (intro tendsto_intros) + by (intro tendsto_intros assms) then have "(\n. (c ^ n - 1) / (c - 1)) \ 1 / (1 - c)" by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) - then show "(\n. c ^ n) sums (1 / (1 - c))" - by (simp add: sums_def geometric_sum neq_1) + with neq_0 show "(\n. c ^ n) sums (1 / (1 - c))" + by (simp add: sums_def geometric_sum) qed lemma summable_geometric: "norm c < 1 \ summable (\n. c^n)" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Set_Interval.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1268,6 +1268,18 @@ qed qed +lemma UN_le_add_shift_strict: + "(\ii\{k.. ?A" + proof + fix x assume "x \ ?B" + then obtain i where i: "i \ {k.. M(i)" by auto + then have "i - k < n \ x \ M((i-k) + k)" by auto + then show "x \ ?A" using UN_le_add_shift by blast + qed +qed (fastforce) + lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)" by (auto simp add: atLeast0LessThan) diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Topological_Spaces.thy Wed Sep 18 14:41:37 2019 +0100 @@ -1633,6 +1633,39 @@ "eventually P (nhds a) \ (\f. f \ a \ eventually (\n. P (f n)) sequentially)" using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp +(*Thanks to Sébastien Gouëzel*) +lemma Inf_as_limit: + fixes A::"'a::{linorder_topology, first_countable_topology, complete_linorder} set" + assumes "A \ {}" + shows "\u. (\n. u n \ A) \ u \ Inf A" +proof (cases "Inf A \ A") + case True + show ?thesis + by (rule exI[of _ "\n. Inf A"], auto simp add: True) +next + case False + obtain y where "y \ A" using assms by auto + then have "Inf A < y" using False Inf_lower less_le by auto + obtain F :: "nat \ 'a set" where F: "\i. open (F i)" "\i. Inf A \ F i" + "\u. (\n. u n \ F n) \ u \ Inf A" + by (metis first_countable_topology_class.countable_basis) + define u where "u = (\n. SOME z. z \ F n \ z \ A)" + have "\z. z \ U \ z \ A" if "Inf A \ U" "open U" for U + proof - + obtain b where "b > Inf A" "{Inf A .. U" + using open_right[OF \open U\ \Inf A \ U\ \Inf A < y\] by auto + obtain z where "z < b" "z \ A" + using \Inf A < b\ Inf_less_iff by auto + then have "z \ {Inf A ..z \ A\ \{Inf A .. U\ by auto + qed + then have *: "u n \ F n \ u n \ A" for n + using \Inf A \ F n\ \open (F n)\ unfolding u_def by (metis (no_types, lifting) someI_ex) + then have "u \ Inf A" using F(3) by simp + then show ?thesis using * by auto +qed + lemma tendsto_at_iff_sequentially: "(f \ a) (at x within s) \ (\X. (\i. X i \ s - {x}) \ X \ x \ ((f \ X) \ a))" for f :: "'a::first_countable_topology \ _" diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Sep 17 16:21:31 2019 +0100 +++ b/src/HOL/Transcendental.thy Wed Sep 18 14:41:37 2019 +0100 @@ -2461,7 +2461,7 @@ lemma powr_non_neg[simp]: "\a powr x < 0" for a x::real using powr_ge_pzero[of a x] by arith -lemma powr_divide: "0 < x \ 0 < y \ (x / y) powr a = (x powr a) / (y powr a)" +lemma powr_divide: "\0 \ x; 0 \ y\ \ (x / y) powr a = (x powr a) / (y powr a)" for a b x :: real apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult) apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse) @@ -2471,7 +2471,7 @@ for a b x :: "'a::{ln,real_normed_field}" by (simp add: powr_def exp_add [symmetric] distrib_right) -lemma powr_mult_base: "0 < x \x * x powr y = x powr (1 + y)" +lemma powr_mult_base: "0 \ x \x * x powr y = x powr (1 + y)" for x :: real by (auto simp: powr_add)