# HG changeset patch # User paulson # Date 1563455324 -3600 # Node ID 8a7053892d8e5ed3eef59e7ebab0800c5bfed856 # Parent 04f492d004fab6a6e83dd014d82d42b0f6bc02f8# Parent ebd108578ab10be3f9b0be137c78810844ac0fe5 merged diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 18 14:08:44 2019 +0100 @@ -423,77 +423,17 @@ subsection\\F_sigma\ and \G_delta\ sets.\(*FIX ME mv *) -\ \\<^url>\https://en.wikipedia.org/wiki/F-sigma_set\\ -inductive\<^marker>\tag important\ fsigma :: "'a::topological_space set \ bool" where - "(\n::nat. closed (F n)) \ fsigma (\(F ` UNIV))" - -inductive\<^marker>\tag important\ gdelta :: "'a::topological_space set \ bool" where - "(\n::nat. open (F n)) \ gdelta (\(F ` UNIV))" - -lemma fsigma_Union_compact: - fixes S :: "'a::{real_normed_vector,heine_borel} set" - shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV))" -proof safe - assume "fsigma S" - then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = \(F ` UNIV)" - by (meson fsigma.cases image_subsetI mem_Collect_eq) - then have "\D::nat \ 'a set. range D \ Collect compact \ \(D ` UNIV) = F i" for i - using closed_Union_compact_subsets [of "F i"] - by (metis image_subsetI mem_Collect_eq range_subsetD) - then obtain D :: "nat \ nat \ 'a set" - where D: "\i. range (D i) \ Collect compact \ \((D i) ` UNIV) = F i" - by metis - let ?DD = "\n. (\(i,j). D i j) (prod_decode n)" - show "\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV)" - proof (intro exI conjI) - show "range ?DD \ Collect compact" - using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair) - show "S = \ (range ?DD)" - proof - show "S \ \ (range ?DD)" - using D F - by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq) - show "\ (range ?DD) \ S" - using D F by fastforce - qed - qed -next - fix F :: "nat \ 'a set" - assume "range F \ Collect compact" and "S = \(F ` UNIV)" - then show "fsigma (\(F ` UNIV))" - by (simp add: compact_imp_closed fsigma.intros image_subset_iff) -qed - -lemma gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" -proof (induction rule: gdelta.induct) - case (1 F) - have "- \(F ` UNIV) = (\i. -(F i))" - by auto - then show ?case - by (simp add: fsigma.intros closed_Compl 1) -qed - -lemma fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" -proof (induction rule: fsigma.induct) - case (1 F) - have "- \(F ` UNIV) = (\i. -(F i))" - by auto - then show ?case - by (simp add: 1 gdelta.intros open_closed) -qed - -lemma gdelta_complement: "gdelta(- S) \ fsigma S" - using fsigma_imp_gdelta gdelta_imp_fsigma by force - text\A Lebesgue set is almost an \F_sigma\ or \G_delta\.\ lemma lebesgue_set_almost_fsigma: assumes "S \ sets lebesgue" obtains C T where "fsigma C" "negligible T" "C \ T = S" "disjnt C T" proof - { fix n::nat - have "\T. closed T \ T \ S \ S - T \ lmeasurable \ measure lebesgue (S-T) < 1 / Suc n" + obtain T where "closed T" "T \ S" "S-T \ lmeasurable" "emeasure lebesgue (S - T) < ennreal (1 / Suc n)" using sets_lebesgue_inner_closed [OF assms] - by (metis divide_pos_pos less_numeral_extra(1) of_nat_0_less_iff zero_less_Suc) + by (metis of_nat_0_less_iff zero_less_Suc zero_less_divide_1_iff) + then have "\T. closed T \ T \ S \ S - T \ lmeasurable \ measure lebesgue (S-T) < 1 / Suc n" + by (metis emeasure_eq_measure2 ennreal_leI not_le) } then obtain F where F: "\n::nat. closed (F n) \ F n \ S \ S - F n \ lmeasurable \ measure lebesgue (S - F n) < 1 / Suc n" by metis @@ -557,16 +497,16 @@ by (metis neg negligible_iff_null_sets) have "frontier S \ lmeasurable" and mS0: "measure lebesgue (frontier S) = 0" using neg negligible_imp_measurable negligible_iff_measure by blast+ - with \e > 0\ lmeasurable_outer_open + with \e > 0\ sets_lebesgue_outer_open obtain U where "open U" - and U: "frontier S \ U" "U - frontier S \ lmeasurable" "measure lebesgue (U - frontier S) < e" + and U: "frontier S \ U" "U - frontier S \ lmeasurable" "emeasure lebesgue (U - frontier S) < e" by (metis fmeasurableD) with null have "U \ lmeasurable" by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel) have "measure lebesgue (U - frontier S) = measure lebesgue U" using mS0 by (simp add: \U \ lmeasurable\ fmeasurableD measure_Diff_null_set null) with U have mU: "measure lebesgue U < e" - by simp + by (simp add: emeasure_eq_measure2 ennreal_less_iff) show ?thesis proof have "U \ UNIV" @@ -612,12 +552,12 @@ assumes "S \ sets lebesgue" obtains K C where "negligible K" "\n::nat. compact(C n)" "S = (\n. C n) \ K" proof - - have "\T. closed T \ T \ S \ (S - T) \ lmeasurable \ measure lebesgue (S - T) < (1/2)^n" for n + have "\T. closed T \ T \ S \ (S - T) \ lmeasurable \ emeasure lebesgue (S - T) < ennreal ((1/2)^n)" for n using sets_lebesgue_inner_closed assms by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) then obtain C where clo: "\n. closed (C n)" and subS: "\n. C n \ S" and mea: "\n. (S - C n) \ lmeasurable" - and less: "\n. measure lebesgue (S - C n) < (1/2)^n" + and less: "\n. emeasure lebesgue (S - C n) < ennreal ((1/2)^n)" by metis have "\F. (\n::nat. compact(F n)) \ (\n. F n) = C m" for m::nat by (metis clo closed_Union_compact_subsets) @@ -645,7 +585,8 @@ show "S - C n \ lmeasurable" by (simp add: mea) show "measure lebesgue (S - C n) \ e" - using less [of n] n by simp + using less [of n] n + by (simp add: emeasure_eq_measure2 less_le mea) qed qed show "compact (?C n)" for n @@ -758,9 +699,11 @@ have eps_d: "f ` S \ lmeasurable" "?\ (f ` S) \ (B+e) * (?\ S + d)" (is "?MD") if "d > 0" for d proof - - obtain T where "open T" "S \ T" and TS: "(T-S) \ lmeasurable" and "?\ (T-S) < d" - using S \d > 0\ lmeasurable_outer_open by blast - with S have "T \ lmeasurable" and Tless: "?\ T < ?\ S + d" + obtain T where T: "open T" "S \ T" and TS: "(T-S) \ lmeasurable" and "emeasure lebesgue (T-S) < ennreal d" + using S \d > 0\ sets_lebesgue_outer_open by blast + then have "?\ (T-S) < d" + by (metis emeasure_eq_measure2 ennreal_leI not_less) + with S T TS have "T \ lmeasurable" and Tless: "?\ T < ?\ S + d" by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D) have "\r. 0 < r \ r < d \ ball x r \ T \ f ` (S \ ball x r) \ lmeasurable \ ?\ (f ` (S \ ball x r)) \ (B + e) * ?\ (ball x r)" diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jul 18 14:08:44 2019 +0100 @@ -1168,6 +1168,10 @@ qed auto qed +corollary eventually_ae_filter_negligible: + "eventually P (ae_filter lebesgue) \ (\N. negligible N \ {x. \ P x} \ N)" + by (auto simp: completion.AE_iff_null_sets negligible_iff_null_sets null_sets_completion_subset) + lemma starlike_negligible: assumes "closed S" and eq1: "\c x. (a + c *\<^sub>R x) \ S \ 0 \ c \ a + x \ S \ c = 1" @@ -1561,7 +1565,8 @@ using \0 < e\ \0 < B\ by (simp add: divide_simps) obtain T where "open T" "S \ T" "(T - S) \ lmeasurable" "measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)" - by (rule lmeasurable_outer_open [OF \S \ sets lebesgue\ e22]) + using sets_lebesgue_outer_open [OF \S \ sets lebesgue\ e22] + by (metis emeasure_eq_measure2 ennreal_leI linorder_not_le) then have T: "measure lebesgue T \ e/2 / (2 * B * DIM('M)) ^ DIM('N)" using \negligible S\ by (simp add: measure_Diff_null_set negligible_iff_null_sets) have "\r. 0 < r \ r \ 1/2 \ @@ -3563,7 +3568,7 @@ fixes f :: "nat \ 'n::euclidean_space \ 'm::euclidean_space" assumes f: "\k. (f k) integrable_on S" and h: "h integrable_on S" and le: "\k x. x \ S \ norm (f k x) \ h x" - and conv: "\x \ S. (\k. f k x) \ g x" + and conv: "\x. x \ S \ (\k. f k x) \ g x" shows "g integrable_on S" "(\k. integral S (f k)) \ integral S g" proof - have 3: "h absolutely_integrable_on S" @@ -3709,8 +3714,7 @@ using fU absolutely_integrable_on_def by blast show "(\x. if x \ \(s ` UNIV) then norm(f x) else 0) integrable_on UNIV" by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV) - show "\x\UNIV. - (\n. if x \ (\m\n. s m) then f x else 0) + show "\x. (\n. if x \ (\m\n. s m) then f x else 0) \ (if x \ \(s ` UNIV) then f x else 0)" by (force intro: tendsto_eventually eventually_sequentiallyI) qed auto diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Jul 18 14:08:44 2019 +0100 @@ -393,6 +393,9 @@ and measurable_lborel2[simp]: "measurable lborel M = measurable borel M" by (simp_all add: lborel_def) +lemma space_lebesgue_on [simp]: "space (lebesgue_on S) = S" + by (simp add: space_restrict_space) + lemma sets_lebesgue_on_refl [iff]: "S \ sets (lebesgue_on S)" by (metis inf_top.right_neutral sets.top space_borel space_completion space_lborel space_restrict_space) @@ -1290,9 +1293,10 @@ qed (use A N in auto) qed -lemma lmeasurable_outer_open: +lemma sets_lebesgue_outer_open: + fixes e::real assumes S: "S \ sets lebesgue" and "e > 0" - obtains T where "open T" "S \ T" "(T - S) \ lmeasurable" "measure lebesgue (T - S) < e" + obtains T where "open T" "S \ T" "(T - S) \ lmeasurable" "emeasure lebesgue (T - S) < ennreal e" proof - obtain S' where S': "S \ S'" "S' \ sets borel" and null: "S' - S \ null_sets lebesgue" @@ -1315,27 +1319,28 @@ by (simp add: S U(1) sets.Diff) then show "(U - S) \ lmeasurable" unfolding fmeasurable_def using U(3) eq less_le_trans by fastforce - with eq U show "measure lebesgue (U - S) < e" - by (metis \U - S \ lmeasurable\ emeasure_eq_measure2 ennreal_leI not_le) + with eq U show "emeasure lebesgue (U - S) < e" + by (simp add: eq) qed qed lemma sets_lebesgue_inner_closed: + fixes e::real assumes "S \ sets lebesgue" "e > 0" - obtains T where "closed T" "T \ S" "S-T \ lmeasurable" "measure lebesgue (S - T) < e" + obtains T where "closed T" "T \ S" "S-T \ lmeasurable" "emeasure lebesgue (S - T) < ennreal e" proof - have "-S \ sets lebesgue" using assms by (simp add: Compl_in_sets_lebesgue) then obtain T where "open T" "-S \ T" - and T: "(T - -S) \ lmeasurable" "measure lebesgue (T - -S) < e" - using lmeasurable_outer_open assms by blast + and T: "(T - -S) \ lmeasurable" "emeasure lebesgue (T - -S) < e" + using sets_lebesgue_outer_open assms by blast show thesis proof show "closed (-T)" using \open T\ by blast show "-T \ S" using \- S \ T\ by auto - show "S - ( -T) \ lmeasurable" "measure lebesgue (S - (- T)) < e" + show "S - ( -T) \ lmeasurable" "emeasure lebesgue (S - (- T)) < e" using T by (auto simp: Int_commute) qed qed @@ -1348,4 +1353,69 @@ "\closedin (top_of_set S) T; S \ sets lebesgue\ \ T \ sets lebesgue" by (metis borel_closed closedin_closed sets.Int sets_completionI_sets sets_lborel) + +subsection\\F_sigma\ and \G_delta\ sets.\ + +\ \\<^url>\https://en.wikipedia.org/wiki/F-sigma_set\\ +inductive\<^marker>\tag important\ fsigma :: "'a::topological_space set \ bool" where + "(\n::nat. closed (F n)) \ fsigma (\(F ` UNIV))" + +inductive\<^marker>\tag important\ gdelta :: "'a::topological_space set \ bool" where + "(\n::nat. open (F n)) \ gdelta (\(F ` UNIV))" + +lemma fsigma_Union_compact: + fixes S :: "'a::{real_normed_vector,heine_borel} set" + shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV))" +proof safe + assume "fsigma S" + then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = \(F ` UNIV)" + by (meson fsigma.cases image_subsetI mem_Collect_eq) + then have "\D::nat \ 'a set. range D \ Collect compact \ \(D ` UNIV) = F i" for i + using closed_Union_compact_subsets [of "F i"] + by (metis image_subsetI mem_Collect_eq range_subsetD) + then obtain D :: "nat \ nat \ 'a set" + where D: "\i. range (D i) \ Collect compact \ \((D i) ` UNIV) = F i" + by metis + let ?DD = "\n. (\(i,j). D i j) (prod_decode n)" + show "\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV)" + proof (intro exI conjI) + show "range ?DD \ Collect compact" + using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair) + show "S = \ (range ?DD)" + proof + show "S \ \ (range ?DD)" + using D F + by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq) + show "\ (range ?DD) \ S" + using D F by fastforce + qed + qed +next + fix F :: "nat \ 'a set" + assume "range F \ Collect compact" and "S = \(F ` UNIV)" + then show "fsigma (\(F ` UNIV))" + by (simp add: compact_imp_closed fsigma.intros image_subset_iff) +qed + +lemma gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" +proof (induction rule: gdelta.induct) + case (1 F) + have "- \(F ` UNIV) = (\i. -(F i))" + by auto + then show ?case + by (simp add: fsigma.intros closed_Compl 1) +qed + +lemma fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" +proof (induction rule: fsigma.induct) + case (1 F) + have "- \(F ` UNIV) = (\i. -(F i))" + by auto + then show ?case + by (simp add: 1 gdelta.intros open_closed) +qed + +lemma gdelta_complement: "gdelta(- S) \ fsigma S" + using fsigma_imp_gdelta gdelta_imp_fsigma by force + end diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Jul 18 14:08:44 2019 +0100 @@ -145,6 +145,28 @@ with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast qed +lemma tendsto_sup[tendsto_intros]: + fixes X :: "'a \ 'b::ordered_euclidean_space" + assumes "(X \ x) net" "(Y \ y) net" + shows "((\i. sup (X i) (Y i)) \ sup x y) net" + unfolding sup_max eucl_sup by (intro assms tendsto_intros) + +lemma tendsto_inf[tendsto_intros]: + fixes X :: "'a \ 'b::ordered_euclidean_space" + assumes "(X \ x) net" "(Y \ y) net" + shows "((\i. inf (X i) (Y i)) \ inf x y) net" + unfolding inf_min eucl_inf by (intro assms tendsto_intros) + +lemma tendsto_componentwise_max: + assumes f: "(f \ l) F" and g: "(g \ m) F" + shows "((\x. (\i\Basis. max (f x \ i) (g x \ i) *\<^sub>R i)) \ (\i\Basis. max (l \ i) (m \ i) *\<^sub>R i)) F" + by (intro tendsto_intros assms) + +lemma tendsto_componentwise_min: + assumes f: "(f \ l) F" and g: "(g \ m) F" + shows "((\x. (\i\Basis. min (f x \ i) (g x \ i) *\<^sub>R i)) \ (\i\Basis. min (l \ i) (m \ i) *\<^sub>R i)) F" + by (intro tendsto_intros assms) + lemma (in order) atLeastatMost_empty'[simp]: "(\ a \ b) \ {a..b} = {}" by (auto) @@ -336,6 +358,6 @@ fixes a :: "'a::ordered_euclidean_space" shows "ENR{a..b}" by (auto simp: interval_cbox) - + end diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Library/Extended_Nonnegative_Real.thy --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 18 14:08:44 2019 +0100 @@ -920,6 +920,9 @@ "0 \ a \ 0 \ b \ ennreal (a + b) = ennreal a + ennreal b" by (transfer fixing: a b) (auto simp: max_absorb2) +lemma add_mono_ennreal: "x < ennreal y \ x' < ennreal y' \ x + x' < ennreal (y + y')" + by (metis (full_types) add_strict_mono ennreal_less_zero_iff ennreal_plus less_le not_less zero_le) + lemma sum_ennreal[simp]: "(\i. i \ I \ 0 \ f i) \ (\i\I. ennreal (f i)) = ennreal (sum f I)" by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg) diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/Library/Liminf_Limsup.thy Thu Jul 18 14:08:44 2019 +0100 @@ -106,6 +106,12 @@ unfolding Limsup_def eventually_sequentially by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono) +lemma mem_limsup_iff: "x \ limsup A \ (\\<^sub>F n in sequentially. x \ A n)" + by (simp add: Limsup_def) (metis (mono_tags) eventually_mono not_frequently) + +lemma mem_liminf_iff: "x \ liminf A \ (\\<^sub>F n in sequentially. x \ A n)" + by (simp add: Liminf_def) (metis (mono_tags) eventually_mono) + lemma Limsup_const: assumes ntriv: "\ trivial_limit F" shows "Limsup F (\x. c) = c" diff -r 04f492d004fa -r 8a7053892d8e src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Thu Jul 18 12:06:42 2019 +0200 +++ b/src/HOL/NthRoot.thy Thu Jul 18 14:08:44 2019 +0100 @@ -379,6 +379,18 @@ DERIV_odd_real_root[THEN DERIV_cong] DERIV_even_real_root[THEN DERIV_cong]) +lemma power_tendsto_0_iff [simp]: + fixes f :: "'a \ real" + assumes "n > 0" + shows "((\x. f x ^ n) \ 0) F \ (f \ 0) F" +proof - + have "((\x. \root n (f x ^ n)\) \ 0) F \ (f \ 0) F" + by (auto simp: assms root_abs_power tendsto_rabs_zero_iff) + then have "((\x. f x ^ n) \ 0) F \ (f \ 0) F" + by (metis tendsto_real_root abs_0 real_root_zero tendsto_rabs) + with assms show ?thesis + by (auto simp: tendsto_null_power) +qed subsection \Square Root\ @@ -392,20 +404,13 @@ unfolding sqrt_def by (rule real_root_pos_unique [OF pos2]) lemma real_sqrt_abs [simp]: "sqrt (x\<^sup>2) = \x\" - apply (rule real_sqrt_unique) - apply (rule power2_abs) - apply (rule abs_ge_zero) - done + by (metis power2_abs abs_ge_zero real_sqrt_unique) lemma real_sqrt_pow2 [simp]: "0 \ x \ (sqrt x)\<^sup>2 = x" unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2]) lemma real_sqrt_pow2_iff [simp]: "(sqrt x)\<^sup>2 = x \ 0 \ x" - apply (rule iffI) - apply (erule subst) - apply (rule zero_le_power2) - apply (erule real_sqrt_pow2) - done + by (metis real_sqrt_pow2 zero_le_power2) lemma real_sqrt_zero [simp]: "sqrt 0 = 0" unfolding sqrt_def by (rule real_root_zero)