(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹SG Libary complements› theory SG_Library_Complement imports "HOL-Probability.Probability" begin text ‹In this file are included many statements that were useful to me, but belong rather naturally to existing theories. In a perfect world, some of these statements would get included into these files. I tried to indicate to which of these classical theories the statements could be added. › subsection ‹Basic logic› text ‹This one is certainly available, but I could not locate it...› lemma equiv_neg: "⟦ P ⟹ Q; ¬P ⟹ ¬Q ⟧ ⟹ (P⟷Q)" by blast subsection ‹Basic set theory› lemma compl_compl_eq_id [simp]: "UNIV - (UNIV - s) = s" by auto abbreviation sym_diff :: "'a set ⇒ 'a set ⇒ 'a set" (infixl "Δ" 70) where "sym_diff A B ≡ ((A - B) ∪ (B-A))" text ‹Not sure the next lemmas are useful, as they are proved solely by auto, so they could be reproved automatically whenever necessary.› lemma sym_diff_inc: "A Δ C ⊆ A Δ B ∪ B Δ C" by auto lemma sym_diff_vimage [simp]: "f-`(A Δ B) = (f-`A) Δ (f-`B)" by auto subsection ‹Set-Interval.thy› text ‹The next two lemmas belong naturally to \verb+Set_Interval.thy+, next to \verb+UN_le_add_shift+. They are not trivially equivalent to the corresponding lemmas with large inequalities, due to the difference when $n = 0$.› lemma UN_le_eq_Un0_strict: "(⋃i<n+1::nat. M i) = (⋃i∈{1..<n+1}. M i) ∪ M 0" (is "?A = ?B") proof show "?A ⊆ ?B" proof fix x assume "x ∈ ?A" then obtain i where i: "i<n+1" "x ∈ M i" by auto show "x ∈ ?B" proof(cases i) case 0 with i show ?thesis by simp next case (Suc j) with i show ?thesis by auto qed qed qed (auto) text ‹I use repeatedly this one, but I could not find it directly› lemma union_insert_0: "(⋃n::nat. A n) = A 0 ∪ (⋃n∈{1..}. A n)" by (metis UN_insert Un_insert_left sup_bot.left_neutral One_nat_def atLeast_0 atLeast_Suc_greaterThan ivl_disj_un_singleton(1)) text ‹Next one could be close to \verb+sum.nat_group+› lemma sum_arith_progression: "(∑r<(N::nat). (∑i<a. f (i*N+r))) = (∑j<a*N. f j)" proof - have *: "(∑r<N. f (i*N+r)) = (∑ j ∈ {i*N..<i*N + N}. f j)" for i by (rule sum.reindex_bij_betw, rule bij_betw_byWitness[where ?f' = "λr. r-i*N"], auto) have "(∑r<N. (∑i<a. f (i*N+r))) = (∑i<a. (∑r<N. f (i*N+r)))" using sum.swap by auto also have "... = (∑i<a. (∑ j ∈ {i*N..<i*N + N}. f j))" using * by auto also have "... = (∑j<a*N. f j)" by (rule sum.nat_group) finally show ?thesis by simp qed subsection ‹Miscellanous basic results› lemma ind_from_1 [case_names 1 Suc, consumes 1]: assumes "n > 0" assumes "P 1" and "⋀n. n > 0 ⟹ P n ⟹ P (Suc n)" shows "P n" proof - have "(n = 0) ∨ P n" proof (induction n) case 0 then show ?case by auto next case (Suc k) consider "Suc k = 1" | "Suc k > 1" by linarith then show ?case apply (cases) using assms Suc.IH by auto qed then show ?thesis using ‹n > 0› by auto qed text ‹This lemma is certainly available somewhere, but I couldn't locate it› lemma tends_to_real_e: fixes u::"nat ⇒ real" assumes "u ⇢ l" "e>0" shows "∃N. ∀n>N. abs(u n -l) < e" by (metis assms dist_real_def le_less lim_sequentially) lemma nat_mod_cong: assumes "a = b+(c::nat)" "a mod n = b mod n" shows "c mod n = 0" proof - let ?k = "a mod n" obtain a1 where "a = a1*n + ?k" by (metis div_mult_mod_eq) moreover obtain b1 where "b = b1*n + ?k" using assms(2) by (metis div_mult_mod_eq) ultimately have "a1 * n + ?k = b1 * n + ?k + c" using assms(1) by arith then have "c = (a1 - b1) * n" by (simp add: diff_mult_distrib) then show ?thesis by simp qed lemma funpow_add': "(f ^^ (m + n)) x = (f ^^ m) ((f ^^ n) x)" by (simp add: funpow_add) text ‹The next two lemmas are not directly equivalent, since $f$ might not be injective.› lemma abs_Max_sum: fixes A::"real set" assumes "finite A" "A ≠ {}" shows "abs(Max A) ≤ (∑a∈A. abs(a))" by (simp add: assms member_le_sum) lemma abs_Max_sum2: fixes f::"_ ⇒ real" assumes "finite A" "A ≠ {}" shows "abs(Max (f`A)) ≤ (∑a∈A. abs(f a))" using assms by (induct rule: finite_ne_induct, auto) subsection ‹Conditionally-Complete-Lattices.thy› lemma mono_cInf: fixes f :: "'a::conditionally_complete_lattice ⇒ 'b::conditionally_complete_lattice" assumes "mono f" "A ≠ {}" "bdd_below A" shows "f(Inf A) ≤ Inf (f`A)" using assms by (simp add: cINF_greatest cInf_lower monoD) lemma mono_bij_cInf: fixes f :: "'a::conditionally_complete_linorder ⇒ 'b::conditionally_complete_linorder" assumes "mono f" "bij f" "A ≠ {}" "bdd_below A" shows "f (Inf A) = Inf (f`A)" proof - have "(inv f) (Inf (f`A)) ≤ Inf ((inv f)`(f`A))" apply (rule cInf_greatest, auto simp add: assms(3)) using mono_inv[OF assms(1) assms(2)] assms by (simp add: mono_def bdd_below_image_mono cInf_lower) then have "Inf (f`A) ≤ f (Inf ((inv f)`(f`A)))" by (metis (no_types, lifting) assms(1) assms(2) mono_def bij_inv_eq_iff) also have "... = f(Inf A)" using assms by (simp add: bij_is_inj) finally show ?thesis using mono_cInf[OF assms(1) assms(3) assms(4)] by auto qed subsection ‹Topological-spaces.thy› lemma open_less_abs [simp]: "open {x. (C::real) < abs x}" proof - have *: "{x. C < abs x} = abs-`{C<..}" by auto show ?thesis unfolding * by (auto intro!: continuous_intros) qed lemma closed_le_abs [simp]: "closed {x. (C::real) ≤ abs x}" proof - have *: "{x. C ≤ ¦x¦} = abs-`{C..}" by auto show ?thesis unfolding * by (auto intro!: continuous_intros) qed text ‹The next statements come from the same statements for true subsequences› lemma eventually_weak_subseq: fixes u::"nat ⇒ nat" assumes "(λn. real(u n)) ⇢ ∞" "eventually P sequentially" shows "eventually (λn. P (u n)) sequentially" proof - obtain N where *: "∀n≥N. P n" using assms(2) unfolding eventually_sequentially by auto obtain M where "∀m≥M. ereal(u m) ≥ N" using assms(1) by (meson Lim_PInfty) then have "⋀m. m ≥ M ⟹ u m ≥ N" by auto then have "⋀m. m ≥ M ⟹ P(u m)" using ‹∀n≥N. P n› by simp then show ?thesis unfolding eventually_sequentially by auto qed lemma filterlim_weak_subseq: fixes u::"nat ⇒ nat" assumes "(λn. real(u n)) ⇢ ∞" shows "LIM n sequentially. u n:> at_top" unfolding filterlim_iff by (metis assms eventually_weak_subseq) lemma limit_along_weak_subseq: fixes u::"nat ⇒ nat" and v::"nat ⇒ _" assumes "(λn. real(u n)) ⇢ ∞" "v ⇢ l" shows "(λ n. v(u n)) ⇢ l" using filterlim_compose[of v, OF _ filterlim_weak_subseq] assms by auto lemma frontier_indist_le: assumes "x ∈ frontier {y. infdist y S ≤ r}" shows "infdist x S = r" proof - have "infdist x S = r" if H: "∀e>0. (∃y. infdist y S ≤ r ∧ dist x y < e) ∧ (∃z. ¬ infdist z S ≤ r ∧ dist x z < e)" proof - have "infdist x S < r + e" if "e > 0" for e proof - obtain y where "infdist y S ≤ r" "dist x y < e" using H ‹e > 0› by blast then show ?thesis by (metis add.commute add_mono_thms_linordered_field(3) infdist_triangle le_less_trans) qed then have A: "infdist x S ≤ r" by (meson field_le_epsilon order.order_iff_strict) have "r < infdist x S + e" if "e > 0" for e proof - obtain y where "¬(infdist y S ≤ r)" "dist x y < e" using H ‹e > 0› by blast then have "r < infdist y S" by auto also have "... ≤ infdist x S + dist y x" by (rule infdist_triangle) finally show ?thesis using ‹dist x y < e› by (simp add: dist_commute) qed then have B: "r ≤ infdist x S" by (meson field_le_epsilon order.order_iff_strict) show ?thesis using A B by auto qed then show ?thesis using assms unfolding frontier_straddle by auto qed subsection ‹Limits› text ‹The next lemmas are not very natural, but I needed them several times› lemma tendsto_shift_1_over_n [tendsto_intros]: fixes f::"nat ⇒ real" assumes "(λn. f n / n) ⇢ l" shows "(λn. f (n+k) / n) ⇢ l" proof - have "(1+k*(1/n))* (f(n+k)/(n+k)) = f(n+k)/n" if "n>0" for n using that by (auto simp add: divide_simps) with eventually_mono[OF eventually_gt_at_top[of "0::nat"] this] have "eventually (λn.(1+k*(1/n))* (f(n+k)/(n+k)) = f(n+k)/n) sequentially" by auto moreover have "(λn. (1+k*(1/n))* (f(n+k)/(n+k))) ⇢ (1+real k*0) * l" by (intro tendsto_intros LIMSEQ_ignore_initial_segment assms) ultimately show ?thesis using Lim_transform_eventually by auto qed lemma tendsto_shift_1_over_n' [tendsto_intros]: fixes f::"nat ⇒ real" assumes "(λn. f n / n) ⇢ l" shows "(λn. f (n-k) / n) ⇢ l" proof - have "(1-k*(1/(n+k)))* (f n/ n) = f n/(n+k)" if "n>0" for n using that by (auto simp add: divide_simps) with eventually_mono[OF eventually_gt_at_top[of "0::nat"] this] have "eventually (λn. (1-k*(1/(n+k)))* (f n/ n) = f n/(n+k)) sequentially" by auto moreover have "(λn. (1-k*(1/(n+k)))* (f n/ n)) ⇢ (1-real k*0) * l" by (intro tendsto_intros assms LIMSEQ_ignore_initial_segment) ultimately have "(λn. f n / (n+k)) ⇢ l" using Lim_transform_eventually by auto then have a: "(λn. f(n-k)/(n-k+k)) ⇢ l" using seq_offset_neg by auto have "f(n-k)/(n-k+k) = f(n-k)/n" if "n>k" for n using that by auto with eventually_mono[OF eventually_gt_at_top[of k] this] have "eventually (λn. f(n-k)/(n-k+k) = f(n-k)/n) sequentially" by auto with Lim_transform_eventually[OF a this] show ?thesis by auto qed declare LIMSEQ_realpow_zero [tendsto_intros] subsection ‹Topology-Euclidean-Space› text ‹A (more usable) variation around \verb+continuous_on_closure_sequentially+. The assumption that the spaces are metric spaces is definitely too strong, but sufficient for most applications.› lemma continuous_on_closure_sequentially': fixes f::"'a::metric_space ⇒ 'b::metric_space" assumes "continuous_on (closure C) f" "⋀(n::nat). u n ∈ C" "u ⇢ l" shows "(λn. f (u n)) ⇢ f l" proof - have "l ∈ closure C" unfolding closure_sequential using assms by auto then show ?thesis using ‹continuous_on (closure C) f› unfolding comp_def continuous_on_closure_sequentially using assms by auto qed subsection ‹Convexity› lemma convex_on_mean_ineq: fixes f::"real ⇒ real" assumes "convex_on A f" "x ∈ A" "y ∈ A" shows "f ((x+y)/2) ≤ (f x + f y) / 2" using convex_onD[OF assms(1), of "1/2" x y] using assms by (auto simp add: divide_simps) lemma convex_on_closure: assumes "convex (C::'a::real_normed_vector set)" "convex_on C f" "continuous_on (closure C) f" shows "convex_on (closure C) f" proof (rule convex_onI) fix x y::'a and t::real assume "x ∈ closure C" "y ∈ closure C" "0 < t" "t < 1" obtain u v::"nat ⇒ 'a" where *: "⋀n. u n ∈ C" "u ⇢ x" "⋀n. v n ∈ C" "v ⇢ y" using ‹x ∈ closure C› ‹y ∈ closure C› unfolding closure_sequential by blast define w where "w = (λn. (1-t) *⇩_{R}(u n) + t *⇩_{R}(v n))" have "w n ∈ C" for n using ‹0 < t› ‹t< 1› convexD[OF ‹convex C› *(1)[of n] *(3)[of n]] unfolding w_def by auto have "w ⇢ ((1-t) *⇩_{R}x + t *⇩_{R}y)" unfolding w_def using *(2) *(4) by (intro tendsto_intros) have *: "f(w n) ≤ (1-t) * f(u n) + t * f (v n)" for n using *(1) *(3) ‹convex_on C f› ‹0<t› ‹t<1› less_imp_le unfolding w_def convex_on_alt[OF assms(1)] by (simp add: add.commute) have i: "(λn. f (w n)) ⇢ f ((1-t) *⇩_{R}x + t *⇩_{R}y)" by (rule continuous_on_closure_sequentially'[OF assms(3) ‹⋀n. w n ∈ C› ‹w ⇢ ((1-t) *⇩_{R}x + t *⇩_{R}y)›]) have ii: "(λn. (1-t) * f(u n) + t * f (v n)) ⇢ (1-t) * f x + t * f y" apply (intro tendsto_intros) apply (rule continuous_on_closure_sequentially'[OF assms(3) ‹⋀n. u n ∈ C› ‹u ⇢ x›]) apply (rule continuous_on_closure_sequentially'[OF assms(3) ‹⋀n. v n ∈ C› ‹v ⇢ y›]) done show "f ((1 - t) *⇩_{R}x + t *⇩_{R}y) ≤ (1 - t) * f x + t * f y" apply (rule LIMSEQ_le[OF i ii]) using * by auto qed lemma convex_on_norm [simp]: "convex_on UNIV (λ(x::'a::real_normed_vector). norm x)" using convex_on_dist[of UNIV "0::'a"] by auto lemma continuous_abs_powr [continuous_intros]: assumes "p > 0" shows "continuous_on UNIV (λ(x::real). ¦x¦ powr p)" apply (rule continuous_on_powr') using assms by (auto intro: continuous_intros) lemma continuous_mult_sgn [continuous_intros]: fixes f::"real ⇒ real" assumes "continuous_on UNIV f" "f 0 = 0" shows "continuous_on UNIV (λx. sgn x * f x)" proof - have *: "continuous_on {0..} (λx. sgn x * f x)" apply (subst continuous_on_cong[of "{0..}" "{0..}" _ f], auto simp add: sgn_real_def assms(2)) by (rule continuous_on_subset[OF assms(1)], auto) have **: "continuous_on {..0} (λx. sgn x * f x)" apply (subst continuous_on_cong[of "{..0}" "{..0}" _ "λx. -f x"], auto simp add: sgn_real_def assms(2)) by (rule continuous_on_subset[of UNIV], auto simp add: assms intro!: continuous_intros) show ?thesis using continuous_on_closed_Un[OF _ _ * **] apply (auto intro: continuous_intros) using continuous_on_subset by fastforce qed lemma DERIV_abs_powr [derivative_intros]: assumes "p > (1::real)" shows "DERIV (λx. ¦x¦ powr p) x :> p * sgn x * ¦x¦ powr (p - 1)" proof - consider "x = 0" | "x>0" | "x < 0" by linarith then show ?thesis proof (cases) case 1 have "continuous_on UNIV (λx. sgn x * ¦x¦ powr (p - 1))" by (auto simp add: assms intro!:continuous_intros) then have "(λh. sgn h * ¦h¦ powr (p-1)) ─0→ (λh. sgn h * ¦h¦ powr (p-1)) 0" using continuous_on_def by blast moreover have "¦h¦ powr p / h = sgn h * ¦h¦ powr (p-1)" for h proof - have "¦h¦ powr p / h = sgn h * ¦h¦ powr p / ¦h¦" by (auto simp add: algebra_simps divide_simps sgn_real_def) also have "... = sgn h * ¦h¦ powr (p-1)" using assms apply (cases "h = 0") apply (auto) by (metis abs_ge_zero powr_diff [symmetric] powr_one_gt_zero_iff times_divide_eq_right) finally show ?thesis by simp qed ultimately have "(λh. ¦h¦ powr p / h) ─0→ 0" by auto then show ?thesis unfolding DERIV_def by (auto simp add: ‹x = 0›) next case 2 have *: "∀⇩_{F}y in nhds x. ¦y¦ powr p = y powr p" unfolding eventually_nhds apply (rule exI[of _ "{0<..}"]) using ‹x > 0› by auto show ?thesis apply (subst DERIV_cong_ev[of _ x _ "(λx. x powr p)" _ "p * x powr (p-1)"]) using ‹x > 0› by (auto simp add: * has_real_derivative_powr) next case 3 have *: "∀⇩_{F}y in nhds x. ¦y¦ powr p = (-y) powr p" unfolding eventually_nhds apply (rule exI[of _ "{..<0}"]) using ‹x < 0› by auto show ?thesis apply (subst DERIV_cong_ev[of _ x _ "(λx. (-x) powr p)" _ "p * (- x) powr (p - real 1) * - 1"]) using ‹x < 0› apply (simp, simp add: *, simp) apply (rule DERIV_fun_powr[of "λy. -y" "-1" "x" p]) using ‹x < 0› by (auto simp add: derivative_intros) qed qed lemma convex_abs_powr: assumes "p ≥ 1" shows "convex_on UNIV (λx::real. ¦x¦ powr p)" proof (cases "p = 1") case True have "convex_on UNIV (λx::real. norm x)" by (rule convex_on_norm) moreover have "¦x¦ powr p = norm x" for x using True by auto ultimately show ?thesis by simp next case False then have "p > 1" using assms by auto define g where "g = (λx::real. p * sgn x * ¦x¦ powr (p - 1))" have *: "DERIV (λx. ¦x¦ powr p) x :> g x" for x unfolding g_def using ‹p>1› by (intro derivative_intros) have **: "g x ≤ g y" if "x ≤ y" for x y proof - consider "x ≥ 0 ∧ y ≥ 0" | "x ≤ 0 ∧ y ≤ 0" | "x < 0 ∧ y > 0" using ‹x ≤ y› by linarith then show ?thesis proof (cases) case 1 then show ?thesis unfolding g_def sgn_real_def using ‹p>1› ‹x ≤ y› by (auto simp add: powr_mono2) next case 2 then show ?thesis unfolding g_def sgn_real_def using ‹p>1› ‹x ≤ y› by (auto simp add: powr_mono2) next case 3 then have "g x ≤ 0" "0 ≤ g y" unfolding g_def using ‹p > 1› by auto then show ?thesis by simp qed qed show ?thesis apply (rule convex_on_realI[of _ _ g]) using * ** by auto qed lemma convex_powr: assumes "p ≥ 1" shows "convex_on {0..} (λx::real. x powr p)" proof - have "convex_on {0..} (λx::real. ¦x¦ powr p)" using convex_abs_powr[OF ‹p ≥ 1›] convex_on_subset by auto moreover have "¦x¦ powr p = x powr p" if "x ∈ {0..}" for x using that by auto ultimately show ?thesis by (simp add: convex_on_def) qed lemma convex_powr': assumes "p > 0" "p ≤ 1" shows "convex_on {0..} (λx::real. - (x powr p))" proof - have "convex_on {0<..} (λx::real. - (x powr p))" apply (rule convex_on_realI[of _ _ "λx. -p * x powr (p-1)"]) apply (auto intro!:derivative_intros simp add: has_real_derivative_powr) using ‹p > 0› ‹p ≤ 1› by (auto simp add: algebra_simps divide_simps powr_mono2') moreover have "continuous_on {0..} (λx::real. - (x powr p))" by (rule continuous_on_minus, rule continuous_on_powr', auto simp add: ‹p > 0› intro!: continuous_intros) moreover have "{(0::real)..} = closure {0<..}" "convex {(0::real)<..}" by auto ultimately show ?thesis using convex_on_closure by metis qed lemma convex_fx_plus_fy_ineq: fixes f::"real ⇒ real" assumes "convex_on {0..} f" "x ≥ 0" "y ≥ 0" "f 0 = 0" shows "f x + f y ≤ f (x+y)" proof - have *: "f a + f b ≤ f (a+b)" if "a ≥ 0" "b ≥ a" for a b proof (cases "a = 0") case False then have "a > 0" "b > 0" using ‹b ≥ a› ‹a ≥ 0› by auto have "(f 0 - f a) / (0 - a) ≤ (f 0 - f (a+b))/ (0 - (a+b))" apply (rule convex_on_diff[OF ‹convex_on {0..} f›]) using ‹a > 0› ‹b > 0› by auto also have "... ≤ (f b - f (a+b)) / (b - (a+b))" apply (rule convex_on_diff[OF ‹convex_on {0..} f›]) using ‹a > 0› ‹b > 0› by auto finally show ?thesis using ‹a > 0› ‹b > 0› ‹f 0 = 0› by (auto simp add: divide_simps algebra_simps) qed (simp add: ‹f 0 = 0›) then show ?thesis using ‹x ≥ 0› ‹y ≥ 0› by (metis add.commute le_less not_le) qed lemma x_plus_y_p_le_xp_plus_yp: fixes p x y::real assumes "p > 0" "p ≤ 1" "x ≥ 0" "y ≥ 0" shows "(x + y) powr p ≤ x powr p + y powr p" using convex_fx_plus_fy_ineq[OF convex_powr'[OF ‹p > 0› ‹p ≤ 1›] ‹x ≥ 0› ‹y ≥ 0›] by auto subsection ‹Nonnegative-extended-real.thy› lemma x_plus_top_ennreal [simp]: "x + ⊤ = (⊤::ennreal)" by simp lemma ennreal_ge_nat_imp_PInf: fixes x::ennreal assumes "⋀N. x ≥ of_nat N" shows "x = ∞" using assms apply (cases x, auto) by (meson not_less reals_Archimedean2) lemma ennreal_archimedean: assumes "x ≠ (∞::ennreal)" shows "∃n::nat. x ≤ n" using assms ennreal_ge_nat_imp_PInf linear by blast lemma e2ennreal_mult: fixes a b::ereal assumes "a ≥ 0" shows "e2ennreal(a * b) = e2ennreal a * e2ennreal b" by (metis assms e2ennreal_neg eq_onp_same_args ereal_mult_le_0_iff linear times_ennreal.abs_eq) lemma e2ennreal_mult': fixes a b::ereal assumes "b ≥ 0" shows "e2ennreal(a * b) = e2ennreal a * e2ennreal b" using e2ennreal_mult[OF assms, of a] by (simp add: mult.commute) lemma SUP_real_ennreal: assumes "A ≠ {}" "bdd_above (f`A)" shows "(SUP a∈A. ennreal (f a)) = ennreal(SUP a∈A. f a)" apply (rule antisym, simp add: SUP_least assms(2) cSUP_upper ennreal_leI) by (metis assms(1) ennreal_SUP ennreal_less_top le_less) lemma e2ennreal_Liminf: "F ≠ bot ⟹ e2ennreal (Liminf F f) = Liminf F (λn. e2ennreal (f n))" by (rule Liminf_compose_continuous_mono[symmetric]) (auto simp: mono_def e2ennreal_mono continuous_on_e2ennreal) lemma e2ennreal_eq_infty[simp]: "0 ≤ x ⟹ e2ennreal x = top ⟷ x = ∞" by (cases x) (auto) lemma ennreal_Inf_cmult: assumes "c>(0::real)" shows "Inf {ennreal c * x |x. P x} = ennreal c * Inf {x. P x}" proof - have "(λx::ennreal. c * x) (Inf {x::ennreal. P x}) = Inf ((λx::ennreal. c * x)`{x::ennreal. P x})" apply (rule mono_bij_Inf) apply (simp add: monoI mult_left_mono) apply (rule bij_betw_byWitness[of _ "λx. (x::ennreal) / c"], auto simp add: assms) apply (metis assms ennreal_lessI ennreal_neq_top mult.commute mult_divide_eq_ennreal not_less_zero) apply (metis assms divide_ennreal_def ennreal_less_zero_iff ennreal_neq_top less_irrefl mult.assoc mult.left_commute mult_divide_eq_ennreal) done then show ?thesis by (simp only: setcompr_eq_image[symmetric]) qed lemma continuous_on_const_minus_ennreal: fixes f :: "'a :: topological_space ⇒ ennreal" shows "continuous_on A f ⟹ continuous_on A (λx. a - f x)" including ennreal.lifting proof (transfer fixing: A; clarsimp) fix f :: "'a ⇒ ereal" and a :: "ereal" assume "0 ≤ a" "∀x. 0 ≤ f x" and f: "continuous_on A f" then show "continuous_on A (λx. max 0 (a - f x))" proof cases assume "∃r. a = ereal r" with f show ?thesis by (auto simp: continuous_on_def minus_ereal_def ereal_Lim_uminus[symmetric] intro!: tendsto_add_ereal_general tendsto_max) next assume "∄r. a = ereal r" with ‹0 ≤ a› have "a = ∞" by (cases a) auto then show ?thesis by (simp add: continuous_on_const) qed qed lemma const_minus_Liminf_ennreal: fixes a :: ennreal shows "F ≠ bot ⟹ a - Liminf F f = Limsup F (λx. a - f x)" by (intro Limsup_compose_continuous_antimono[symmetric]) (auto simp: antimono_def ennreal_mono_minus continuous_on_id continuous_on_const_minus_ennreal) lemma tendsto_cmult_ennreal [tendsto_intros]: fixes c l::ennreal assumes "¬(c = ∞ ∧ l = 0)" "(f ⤏ l) F" shows "((λx. c * f x) ⤏ c * l) F" by (cases "c = 0", insert assms, auto intro!: tendsto_intros) subsection ‹Indicator-Function.thy› text ‹There is something weird with \verb+sum_mult_indicator+: it is defined both in Indicator.thy and BochnerIntegration.thy, with a different meaning. I am surprised there is no name collision... Here, I am using the version from BochnerIntegration.› lemma sum_indicator_eq_card2: assumes "finite I" shows "(∑i∈I. (indicator (P i) x)::nat) = card {i∈I. x ∈ P i}" using sum_mult_indicator [OF assms, of "λy. 1::nat" P "λy. x"] unfolding card_eq_sum by auto lemma disjoint_family_indicator_le_1: assumes "disjoint_family_on A I" shows "(∑ i∈ I. indicator (A i) x) ≤ (1::'a:: {comm_monoid_add,zero_less_one})" proof (cases "finite I") case True then have *: "(∑ i∈ I. indicator (A i) x) = ((indicator (⋃i∈I. A i) x)::'a)" by (simp add: indicator_UN_disjoint[OF True assms(1), of x]) show ?thesis unfolding * unfolding indicator_def by (simp add: order_less_imp_le) next case False then show ?thesis by (simp add: order_less_imp_le) qed subsection ‹sigma-algebra.thy› lemma algebra_intersection: assumes "algebra Ω A" "algebra Ω B" shows "algebra Ω (A ∩ B)" apply (subst algebra_iff_Un) using assms by (auto simp add: algebra_iff_Un) lemma sigma_algebra_intersection: assumes "sigma_algebra Ω A" "sigma_algebra Ω B" shows "sigma_algebra Ω (A ∩ B)" apply (subst sigma_algebra_iff) using assms by (auto simp add: sigma_algebra_iff algebra_intersection) lemma subalgebra_M_M [simp]: "subalgebra M M" by (simp add: subalgebra_def) text ‹The next one is \verb+disjoint_family_Suc+ with inclusions reversed.› lemma disjoint_family_Suc2: assumes Suc: "⋀n. A (Suc n) ⊆ A n" shows "disjoint_family (λi. A i - A (Suc i))" proof - have "A (m+n) ⊆ A n" for m n proof (induct m) case 0 show ?case by simp next case (Suc m) then show ?case by (metis Suc_eq_plus1 assms add.commute add.left_commute subset_trans) qed then have "A m ⊆ A n" if "m > n" for m n by (metis that add.commute le_add_diff_inverse nat_less_le) then show ?thesis by (auto simp add: disjoint_family_on_def) (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less) qed subsection ‹Measure-Space.thy› lemma AE_equal_sum: assumes "⋀i. AE x in M. f i x = g i x" shows "AE x in M. (∑i∈I. f i x) = (∑i∈I. g i x)" proof (cases) assume "finite I" have "∃A. A ∈ null_sets M ∧ (∀x∈ (space M - A). f i x = g i x)" for i using assms(1)[of i] by (metis (mono_tags, lifting) AE_E3) then obtain A where A: "⋀i. A i ∈ null_sets M ∧ (∀x∈ (space M -A i). f i x = g i x)" by metis define B where "B = (⋃i∈I. A i)" have "B ∈ null_sets M" using ‹finite I› A B_def by blast then have "AE x in M. x ∈ space M - B" by (simp add: AE_not_in) moreover { fix x assume "x ∈ space M - B" then have "⋀i. i ∈ I ⟹ f i x = g i x" unfolding B_def using A by auto then have "(∑i∈I. f i x) = (∑i∈I. g i x)" by auto } ultimately show ?thesis by auto qed (simp) lemma emeasure_pos_unionE: assumes "⋀ (N::nat). A N ∈ sets M" "emeasure M (⋃N. A N) > 0" shows "∃N. emeasure M (A N) > 0" proof (rule ccontr) assume "¬(∃N. emeasure M (A N) > 0)" then have "⋀N. A N ∈ null_sets M" using assms(1) by auto then have "(⋃N. A N) ∈ null_sets M" by auto then show False using assms(2) by auto qed lemma (in prob_space) emeasure_intersection: fixes e::"nat ⇒ real" assumes [measurable]: "⋀n. U n ∈ sets M" and [simp]: "⋀n. 0 ≤ e n" "summable e" and ge: "⋀n. emeasure M (U n) ≥ 1 - (e n)" shows "emeasure M (⋂n. U n) ≥ 1 - (∑n. e n)" proof - define V where "V = (λn. space M - (U n))" have [measurable]: "V n ∈ sets M" for n unfolding V_def by auto have *: "emeasure M (V n) ≤ e n" for n unfolding V_def using ge[of n] by (simp add: emeasure_eq_measure prob_compl ennreal_leI) have "emeasure M (⋃n. V n) ≤ (∑n. emeasure M (V n))" by (rule emeasure_subadditive_countably, auto) also have "... ≤ (∑n. ennreal (e n))" using * by (intro suminf_le) auto also have "... = ennreal (∑n. e n)" by (intro suminf_ennreal_eq) auto finally have "emeasure M (⋃n. V n) ≤ suminf e" by simp then have "1 - suminf e ≤ emeasure M (space M - (⋃n. V n))" by (simp add: emeasure_eq_measure prob_compl suminf_nonneg) also have "... ≤ emeasure M (⋂n. U n)" by (rule emeasure_mono) (auto simp: V_def) finally show ?thesis by simp qed lemma null_sym_diff_transitive: assumes "A Δ B ∈ null_sets M" "B Δ C ∈ null_sets M" and [measurable]: "A ∈ sets M" "C ∈ sets M" shows "A Δ C ∈ null_sets M" proof - have "A Δ B ∪ B Δ C ∈ null_sets M" using assms(1) assms(2) by auto moreover have "A Δ C ⊆ A Δ B ∪ B Δ C" by auto ultimately show ?thesis by (meson null_sets_subset assms(3) assms(4) sets.Diff sets.Un) qed lemma Delta_null_of_null_is_null: assumes "B ∈ sets M" "A Δ B ∈ null_sets M" "A ∈ null_sets M" shows "B ∈ null_sets M" proof - have "B ⊆ A ∪ (A Δ B)" by auto then show ?thesis using assms by (meson null_sets.Un null_sets_subset) qed lemma Delta_null_same_emeasure: assumes "A Δ B ∈ null_sets M" and [measurable]: "A ∈ sets M" "B ∈ sets M" shows "emeasure M A = emeasure M B" proof - have "A = (A ∩ B) ∪ (A-B)" by blast moreover have "A-B ∈ null_sets M" using assms null_sets_subset by blast ultimately have a: "emeasure M A = emeasure M (A ∩ B)" using emeasure_Un_null_set by (metis assms(2) assms(3) sets.Int) have "B = (A ∩ B) ∪ (B-A)" by blast moreover have "B-A ∈ null_sets M" using assms null_sets_subset by blast ultimately have "emeasure M B = emeasure M (A ∩ B)" using emeasure_Un_null_set by (metis assms(2) assms(3) sets.Int) then show ?thesis using a by auto qed lemma AE_upper_bound_inf_ereal: fixes F G::"'a ⇒ ereal" assumes "⋀e. (e::real) > 0 ⟹ AE x in M. F x ≤ G x + e" shows "AE x in M. F x ≤ G x" proof - have "AE x in M. ∀n::nat. F x ≤ G x + ereal (1 / Suc n)" using assms by (auto simp: AE_all_countable) then show ?thesis proof (eventually_elim) fix x assume x: "∀n::nat. F x ≤ G x + ereal (1 / Suc n)" show "F x ≤ G x" proof (intro ereal_le_epsilon2[of _ "G x"] allI impI) fix e :: real assume "0 < e" then obtain n where n: "1 / Suc n < e" by (blast elim: nat_approx_posE) have "F x ≤ G x + 1 / Suc n" using x by simp also have "… ≤ G x + e" using n by (intro add_mono ennreal_leI) auto finally show "F x ≤ G x + ereal e" . qed qed qed text ‹Egorov theorem asserts that, if a sequence of functions converges almost everywhere to a limit, then the convergence is uniform on a subset of close to full measure. The first step in the proof is the following lemma, often useful by itself, asserting the same result for predicates: if a property $P_n x$ is eventually true for almost every $x$, then there exists $N$ such that $P_n x$ is true for all $n\geq N$ and all $x$ in a set of close to full measure. › lemma (in finite_measure) Egorov_lemma: assumes [measurable]: "⋀n. (P n) ∈ measurable M (count_space UNIV)" and "AE x in M. eventually (λn. P n x) sequentially" "epsilon > 0" shows "∃U N. U ∈ sets M ∧ (∀n ≥ N. ∀x ∈ U. P n x) ∧ emeasure M (space M - U) < epsilon" proof - define K where "K = (λn. {x ∈ space M. ∃k≥n. ¬(P k x)})" have [measurable]: "K n ∈ sets M" for n unfolding K_def by auto have "x ∉ (⋂n. K n)" if "eventually (λn. P n x) sequentially" for x unfolding K_def using that unfolding K_def eventually_sequentially by auto then have "AE x in M. x ∉ (⋂n. K n)" using assms by auto then have Z: "0 = emeasure M (⋂n. K n)" using AE_iff_measurable[of "(⋂n. K n)" M "λx. x ∉ (⋂n. K n)"] unfolding K_def by auto have *: "(λn. emeasure M (K n)) ⇢ 0" unfolding Z apply (rule Lim_emeasure_decseq) using order_trans by (auto simp add: K_def decseq_def) have "eventually (λn. emeasure M (K n) < epsilon) sequentially" by (rule order_tendstoD(2)[OF * ‹epsilon > 0›]) then obtain N where N: "⋀n. n ≥ N ⟹ emeasure M (K n) < epsilon" unfolding eventually_sequentially by auto define U where "U = space M - K N" have A [measurable]: "U ∈ sets M" unfolding U_def by auto have "space M - U = K N" unfolding U_def K_def by auto then have B: "emeasure M (space M - U) < epsilon" using N by auto have "∀n ≥ N. ∀x ∈ U. P n x" unfolding U_def K_def by auto then show ?thesis using A B by blast qed text ‹The next lemma asserts that, in an uncountable family of disjoint sets, then there is one set with zero measure (and in fact uncountably many). It is often applied to the boundaries of $r$-neighborhoods of a given set, to show that one could choose $r$ for which this boundary has zero measure (this shows up often in relation with weak convergence).› lemma (in finite_measure) uncountable_disjoint_family_then_exists_zero_measure: assumes [measurable]: "⋀i. i ∈ I ⟹ A i ∈ sets M" and "uncountable I" "disjoint_family_on A I" shows "∃i∈I. measure M (A i) = 0" proof - define f where "f = (λ(r::real). {i ∈ I. measure M (A i) > r})" have *: "finite (f r)" if "r > 0" for r proof - obtain N::nat where N: "measure M (space M)/r ≤ N" using real_arch_simple by blast have "finite (f r) ∧ card (f r) ≤ N" proof (rule finite_if_finite_subsets_card_bdd) fix G assume G: "G ⊆ f r" "finite G" then have "G ⊆ I" unfolding f_def by auto have "card G * r = (∑i ∈ G. r)" by auto also have "... ≤ (∑i ∈ G. measure M (A i))" apply (rule sum_mono) using G unfolding f_def by auto also have "... = measure M (⋃i∈G. A i)" apply (rule finite_measure_finite_Union[symmetric]) using ‹finite G› ‹G ⊆ I› ‹disjoint_family_on A I› disjoint_family_on_mono by auto also have "... ≤ measure M (space M)" by (simp add: bounded_measure) finally have "card G ≤ measure M (space M)/r" using ‹r > 0› by (simp add: divide_simps) then show "card G ≤ N" using N by auto qed then show ?thesis by simp qed have "countable (⋃n. f (((1::real)/2)^n))" by (rule countable_UN, auto intro!: countable_finite *) then have "I - (⋃n. f (((1::real)/2)^n)) ≠ {}" using assms(2) by (metis countable_empty uncountable_minus_countable) then obtain i where "i ∈ I" "i ∉ (⋃n. f ((1/2)^n))" by auto then have "measure M (A i) ≤ (1 / 2) ^ n" for n unfolding f_def using linorder_not_le by auto moreover have "(λn. ((1::real) / 2) ^ n) ⇢ 0" by (intro tendsto_intros, auto) ultimately have "measure M (A i) ≤ 0" using LIMSEQ_le_const by force then have "measure M (A i) = 0" by (simp add: measure_le_0_iff) then show ?thesis using ‹i ∈ I› by auto qed text ‹The next statements are useful measurability statements.› lemma measurable_Inf [measurable]: assumes [measurable]: "⋀(n::nat). P n ∈ measurable M (count_space UNIV)" shows "(λx. Inf {n. P n x}) ∈ measurable M (count_space UNIV)" (is "?f ∈ _") proof - define A where "A = (λn. (P n)-`{True} ∩ space M - (⋃m<n. (P m)-`{True} ∩ space M))" have A_meas [measurable]: "A n ∈ sets M" for n unfolding A_def by measurable define B where "B = (λn. if n = 0 then (space M - (⋃n. A n)) else A (n-1))" show ?thesis proof (rule measurable_piecewise_restrict2[of B]) show "B n ∈ sets M" for n unfolding B_def by simp show "space M = (⋃n. B n)" unfolding B_def using sets.sets_into_space [OF A_meas] by auto have *: "?f x = n" if "x ∈ A n" for x n apply (rule cInf_eq_minimum) using that unfolding A_def by auto moreover have **: "?f x = (Inf ({}::nat set))" if "x ∈ space M - (⋃n. A n)" for x proof - have "¬(P n x)" for n apply (induction n rule: nat_less_induct) using that unfolding A_def by auto then show ?thesis by simp qed ultimately have "∃c. ∀x ∈ B n. ?f x = c" for n apply (cases "n = 0") unfolding B_def by auto then show "∃h ∈ measurable M (count_space UNIV). ∀x ∈ B n. ?f x = h x" for n by fastforce qed qed lemma measurable_T_iter [measurable]: fixes f::"'a ⇒ nat" assumes [measurable]: "T ∈ measurable M M" "f ∈ measurable M (count_space UNIV)" shows "(λx. (T^^(f x)) x) ∈ measurable M M" proof - have [measurable]: "(T^^n) ∈ measurable M M" for n::nat by (induction n, auto) show ?thesis by (rule measurable_compose_countable, auto) qed lemma measurable_infdist [measurable]: "(λx. infdist x S) ∈ borel_measurable borel" by (rule borel_measurable_continuous_onI, intro continuous_intros) text ‹The next lemma shows that, in a sigma finite measure space, sets with large measure can be approximated by sets with large but finite measure.› lemma (in sigma_finite_measure) approx_with_finite_emeasure: assumes W_meas: "W ∈ sets M" and W_inf: "emeasure M W > C" obtains Z where "Z ∈ sets M" "Z ⊆ W" "emeasure M Z < ∞" "emeasure M Z > C" proof (cases "emeasure M W = ∞") case True obtain r where r: "C = ennreal r" using W_inf by (cases C, auto) obtain Z where "Z ∈ sets M" "Z ⊆ W" "emeasure M Z < ∞" "emeasure M Z > C" unfolding r using approx_PInf_emeasure_with_finite[OF W_meas True, of r] by auto then show ?thesis using that by blast next case False then have "W ∈ sets M" "W ⊆ W" "emeasure M W < ∞" "emeasure M W > C" using assms apply auto using top.not_eq_extremum by blast then show ?thesis using that by blast qed subsection ‹Nonnegative-Lebesgue-Integration.thy› text ‹The next lemma is a variant of \verb+nn_integral_density+, with the density on the right instead of the left, as seems more common.› lemma nn_integral_densityR: assumes [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable F" shows "(∫⇧^{+}x. f x * g x ∂F) = (∫⇧^{+}x. f x ∂(density F g))" proof - have "(∫⇧^{+}x. f x * g x ∂F) = (∫⇧^{+}x. g x * f x ∂F)" by (simp add: mult.commute) also have "... = (∫⇧^{+}x. f x ∂(density F g))" by (rule nn_integral_density[symmetric], simp_all add: assms) finally show ?thesis by simp qed lemma not_AE_zero_int_ennreal_E: fixes f::"'a ⇒ ennreal" assumes "(∫⇧^{+}x. f x ∂M) > 0" and [measurable]: "f ∈ borel_measurable M" shows "∃A∈sets M. ∃e::real>0. emeasure M A > 0 ∧ (∀x ∈ A. f x ≥ e)" proof (rule not_AE_zero_ennreal_E, auto simp add: assms) assume *: "AE x in M. f x = 0" have "(∫⇧^{+}x. f x ∂M) = (∫⇧^{+}x. 0 ∂M)" by (rule nn_integral_cong_AE, simp add: *) then have "(∫⇧^{+}x. f x ∂M) = 0" by simp then show False using assms by simp qed lemma (in finite_measure) nn_integral_bounded_eq_bound_then_AE: assumes "AE x in M. f x ≤ ennreal c" "(∫⇧^{+}x. f x ∂M) = c * emeasure M (space M)" and [measurable]: "f ∈ borel_measurable M" shows "AE x in M. f x = c" proof (cases) assume "emeasure M (space M) = 0" then show ?thesis by (rule emeasure_0_AE) next assume "emeasure M (space M) ≠ 0" have fin: "AE x in M. f x ≠ top" using assms by (auto simp: top_unique) define g where "g = (λx. c - f x)" have [measurable]: "g ∈ borel_measurable M" unfolding g_def by auto have "(∫⇧^{+}x. g x ∂M) = (∫⇧^{+}x. c ∂M) - (∫⇧^{+}x. f x ∂M)" unfolding g_def by (rule nn_integral_diff, auto simp add: assms ennreal_mult_eq_top_iff) also have "… = 0" using assms(2) by (auto simp: ennreal_mult_eq_top_iff) finally have "AE x in M. g x = 0" by (subst nn_integral_0_iff_AE[symmetric]) auto then have "AE x in M. c ≤ f x" unfolding g_def using fin by (auto simp: ennreal_minus_eq_0) then show ?thesis using assms(1) by auto qed lemma null_sets_density: assumes [measurable]: "h ∈ borel_measurable M" and "AE x in M. h x ≠ 0" shows "null_sets (density M h) = null_sets M" proof - have *: "A ∈ sets M ∧ (AE x∈A in M. h x = 0) ⟷ A ∈ null_sets M" for A proof (auto) assume "A ∈ sets M" "AE x∈A in M. h x = 0" then show "A ∈ null_sets M" unfolding AE_iff_null_sets[OF ‹A ∈ sets M›] using assms(2) by auto next assume "A ∈ null_sets M" then show "AE x∈A in M. h x = 0" by (metis (mono_tags, lifting) AE_not_in eventually_mono) qed show ?thesis apply (rule set_eqI) unfolding null_sets_density_iff[OF ‹h ∈ borel_measurable M›] using * by auto qed text ‹The next proposition asserts that, if a function $h$ is integrable, then its integral on any set with small enough measure is small. The good conceptual proof is by considering the distribution of the function $h$ on $\mathbb{R}$ and looking at its tails. However, there is a less conceptual but more direct proof, based on dominated convergence and a proof by contradiction. This is the proof we give below.› proposition integrable_small_integral_on_small_sets: fixes h::"'a ⇒ real" assumes [measurable]: "integrable M h" and "delta > 0" shows "∃epsilon>(0::real). ∀U ∈ sets M. emeasure M U < epsilon ⟶ abs (∫x∈U. h x ∂M) < delta" proof (rule ccontr) assume H: "¬ (∃epsilon>0. ∀U∈sets M. emeasure M U < ennreal epsilon ⟶ abs(set_lebesgue_integral M U h) < delta)" have "∃f. ∀epsilon∈{0<..}. f epsilon ∈sets M ∧ emeasure M (f epsilon) < ennreal epsilon ∧ ¬(abs(set_lebesgue_integral M (f epsilon) h) < delta)" apply (rule bchoice) using H by auto then obtain f::"real ⇒ 'a set" where f: "⋀epsilon. epsilon > 0 ⟹ f epsilon ∈sets M" "⋀epsilon. epsilon > 0 ⟹ emeasure M (f epsilon) < ennreal epsilon" "⋀epsilon. epsilon > 0 ⟹ ¬(abs(set_lebesgue_integral M (f epsilon) h) < delta)" by blast define A where "A = (λn::nat. f ((1/2)^n))" have [measurable]: "A n ∈ sets M" for n unfolding A_def using f(1) by auto have *: "emeasure M (A n) < ennreal ((1/2)^n)" for n unfolding A_def using f(2) by auto have Large: "¬(abs(set_lebesgue_integral M (A n) h) < delta)" for n unfolding A_def using f(3) by auto have S: "summable (λn. Sigma_Algebra.measure M (A n))" apply (rule summable_comparison_test'[of "λn. (1/2)^n" 0]) apply (rule summable_geometric, auto) apply (subst ennreal_le_iff[symmetric], simp) using less_imp_le[OF *] by (metis * emeasure_eq_ennreal_measure top.extremum_strict) have "AE x in M. eventually (λn. x ∈ space M - A n) sequentially" apply (rule borel_cantelli_AE1, auto simp add: S) by (metis * top.extremum_strict top.not_eq_extremum) moreover have "(λn. indicator (A n) x * h x) ⇢ 0" if "eventually (λn. x ∈ space M - A n) sequentially" for x proof - have "eventually (λn. indicator (A n) x * h x = 0) sequentially" apply (rule eventually_mono[OF that]) unfolding indicator_def by auto then show ?thesis unfolding eventually_sequentially using lim_explicit by force qed ultimately have A: "AE x in M. ((λn. indicator (A n) x * h x) ⇢ 0)" by auto have I: "integrable M (λx. abs(h x))" using ‹integrable M h› by auto have L: "(λn. abs (∫x. indicator (A n) x * h x ∂M)) ⇢ abs (∫x. 0 ∂M)" apply (intro tendsto_intros) apply (rule integral_dominated_convergence[OF _ _ I A]) unfolding indicator_def by auto have "eventually (λn. abs (∫x. indicator (A n) x * h x ∂M) < delta) sequentially" apply (rule order_tendstoD[OF L]) using ‹delta > 0› by auto then show False using Large by (auto simp: set_lebesgue_integral_def) qed text ‹We also give the version for nonnegative ennreal valued functions. It follows from the previous one.› proposition small_nn_integral_on_small_sets: fixes h::"'a ⇒ ennreal" assumes [measurable]: "h ∈ borel_measurable M" and "delta > (0::real)" "(∫⇧^{+}x. h x ∂M) ≠ ∞" shows "∃epsilon>(0::real). ∀U ∈ sets M. emeasure M U < epsilon ⟶ (∫⇧^{+}x∈U. h x ∂M) < delta" proof - define f where "f = (λx. enn2real(h x))" have "AE x in M. h x ≠ ∞" using assms by (metis nn_integral_PInf_AE) then have *: "AE x in M. ennreal (f x) = h x" unfolding f_def using ennreal_enn2real_if by auto have **: "(∫⇧^{+}x. ennreal (f x) ∂M) ≠ ∞" using nn_integral_cong_AE[OF *] assms by auto have [measurable]: "f ∈ borel_measurable M" unfolding f_def by auto have "integrable M f" apply (rule integrableI_nonneg) using assms * f_def ** apply auto using top.not_eq_extremum by blast obtain epsilon::real where H: "epsilon > 0" "⋀U. U ∈ sets M ⟹ emeasure M U < epsilon ⟹ abs(∫x∈U. f x ∂M) < delta" using integrable_small_integral_on_small_sets[OF ‹integrable M f› ‹delta > 0›] by blast have "(∫⇧^{+}x∈U. h x ∂M) < delta" if [measurable]: "U ∈ sets M" "emeasure M U < epsilon" for U proof - have "(∫⇧^{+}x. indicator U x * h x ∂M) = (∫⇧^{+}x. ennreal(indicator U x * f x) ∂M)" apply (rule nn_integral_cong_AE) using * unfolding indicator_def by auto also have "... = ennreal (∫x. indicator U x * f x ∂M)" apply (rule nn_integral_eq_integral) apply (rule Bochner_Integration.integrable_bound[OF ‹integrable M f›]) unfolding indicator_def f_def by auto also have "... < ennreal delta" apply (rule ennreal_lessI) using H(2)[OF that] by (auto simp: set_lebesgue_integral_def) finally show ?thesis by (auto simp add: mult.commute) qed then show ?thesis using ‹epsilon > 0› by auto qed subsection ‹Probability-measure.thy› text ‹The next lemmas ensure that, if sets have a probability close to $1$, then their intersection also does.› lemma (in prob_space) sum_measure_le_measure_inter: assumes "A ∈ sets M" "B ∈ sets M" shows "prob A + prob B ≤ 1 + prob (A ∩ B)" proof - have "prob A + prob B = prob (A ∪ B) + prob (A ∩ B)" by (simp add: assms fmeasurable_eq_sets measure_Un3) also have "... ≤ 1 + prob (A ∩ B)" by auto finally show ?thesis by simp qed lemma (in prob_space) sum_measure_le_measure_inter3: assumes [measurable]: "A ∈ sets M" "B ∈ sets M" "C ∈ sets M" shows "prob A + prob B + prob C ≤ 2 + prob (A ∩ B ∩ C)" using sum_measure_le_measure_inter[of B C] sum_measure_le_measure_inter[of A "B ∩ C"] by (auto simp add: inf_assoc) lemma (in prob_space) sum_measure_le_measure_Inter: assumes [measurable]: "finite I" "I ≠ {}" "⋀i. i ∈ I ⟹ A i ∈ sets M" shows "(∑i∈I. prob (A i)) ≤ real(card I) - 1 + prob (⋂i∈I. A i)" using assms proof (induct I rule: finite_ne_induct) fix x F assume H: "finite F" "F ≠ {}" "x ∉ F" "((⋀i. i ∈ F ⟹ A i ∈ events) ⟹ (∑i∈F. prob (A i)) ≤ real (card F) - 1 + prob (⋂(A ` F)))" and [measurable]: "(⋀i. i ∈ insert x F ⟹ A i ∈ events)" have "(⋂x∈F. A x) ∈ events" using ‹finite F› ‹F ≠ {}› by auto have "(∑i∈insert x F. prob (A i)) = (∑i∈F. prob (A i)) + prob (A x)" using H(1) H(3) by auto also have "... ≤ real (card F)-1 + prob (⋂(A ` F)) + prob (A x)" using H(4) by auto also have "... ≤ real (card F) + prob ((⋂(A ` F)) ∩ A x)" using sum_measure_le_measure_inter[OF ‹(⋂x∈F. A x) ∈ events›, of "A x"] by auto also have "... = real (card (insert x F)) - 1 + prob (⋂(A ` (insert x F)))" using H(1) H(2) unfolding card_insert_disjoint[OF ‹finite F› ‹x ∉ F›] by (simp add: inf_commute) finally show "(∑i∈insert x F. prob (A i)) ≤ real (card (insert x F)) - 1 + prob (⋂(A ` (insert x F)))" by simp qed (auto) text ‹A random variable gives a small mass to small neighborhoods of infinity.› lemma (in prob_space) random_variable_small_tails: assumes "alpha > 0" and [measurable]: "f ∈ borel_measurable M" shows "∃(C::real). prob {x ∈ space M. abs(f x) ≥ C} < alpha ∧ C ≥ K" proof - have *: "(⋂(n::nat). {x∈space M. abs(f x) ≥ n}) = {}" apply auto by (metis real_arch_simple add.right_neutral add_mono_thms_linordered_field(4) not_less zero_less_one) have **: "(λn. prob {x ∈ space M. abs(f x) ≥ n}) ⇢ prob (⋂(n::nat). {x ∈ space M. abs(f x) ≥ n})" by (rule finite_Lim_measure_decseq, auto simp add: decseq_def) have "eventually (λn. prob {x ∈ space M. abs(f x) ≥ n} < alpha) sequentially" apply (rule order_tendstoD[OF _ ‹alpha > 0›]) using ** unfolding * by auto then obtain N::nat where N: "⋀n::nat. n ≥ N ⟹ prob {x ∈ space M. abs(f x) ≥ n} < alpha" unfolding eventually_sequentially by blast have "∃n::nat. n ≥ N ∧ n ≥ K" by (meson le_cases of_nat_le_iff order.trans real_arch_simple) then obtain n::nat where n: "n ≥ N" "n ≥ K" by blast show ?thesis apply (rule exI[of _ "of_nat n"]) using N n by auto qed subsection ‹Distribution-functions.thy› text ‹There is a locale called \verb+finite_borel_measure+ in \verb+distribution-functions.thy+. However, it only deals with real measures, and real weak convergence. I will not need the weak convergence in more general settings, but still it seems more natural to me to do the proofs in the natural settings. Let me introduce the locale \verb+finite_borel_measure'+ for this, although it would be better to rename the locale in the library file.› locale finite_borel_measure' = finite_measure M for M :: "('a::metric_space) measure" + assumes M_is_borel [simp, measurable_cong]: "sets M = sets borel" begin lemma space_eq_univ [simp]: "space M = UNIV" using M_is_borel[THEN sets_eq_imp_space_eq] by simp lemma measurable_finite_borel [simp]: "f ∈ borel_measurable borel ⟹ f ∈ borel_measurable M" by (rule borel_measurable_subalgebra[where N = borel]) auto text ‹Any closed set can be slightly enlarged to obtain a set whose boundary has $0$ measure.› lemma approx_closed_set_with_set_zero_measure_boundary: assumes "closed S" "epsilon > 0" "S ≠ {}" shows "∃r. r < epsilon ∧ r > 0 ∧ measure M {x. infdist x S = r} = 0 ∧ measure M {x. infdist x S ≤ r} < measure M S + epsilon" proof - have [measurable]: "S ∈ sets M" using ‹closed S› by auto define T where "T = (λr. {x. infdist x S ≤ r})" have [measurable]: "T r ∈ sets borel" for r unfolding T_def by measurable have *: "(⋂n. T ((1/2)^n)) = S" unfolding T_def proof (auto) fix x assume *: "∀n. infdist x S ≤ (1 / 2) ^n" have "infdist x S ≤ 0" apply (rule LIMSEQ_le_const[of "λn. (1/2)^n"], intro tendsto_intros) using * by auto then show "x ∈ S" using assms infdist_pos_not_in_closed by fastforce qed have A: "((1::real)/2)^n ≤ (1/2)^m" if "m ≤ n" for m n::nat using that by (simp add: power_decreasing) have "(λn. measure M (T ((1/2)^n))) ⇢ measure M S" unfolding *[symmetric] apply (rule finite_Lim_measure_decseq, auto simp add: T_def decseq_def) using A order.trans by blast then have B: "eventually (λn. measure M (T ((1/2)^n)) < measure M S + epsilon) sequentially" apply (rule order_tendstoD) using ‹epsilon > 0› by simp have C: "eventually (λn. (1/2)^n < epsilon) sequentially" by (rule order_tendstoD[OF _ ‹epsilon > 0›], intro tendsto_intros, auto) obtain n where n: "(1/2)^n < epsilon" "measure M (T ((1/2)^n)) < measure M S + epsilon" using eventually_conj[OF B C] unfolding eventually_sequentially by auto have "∃r∈{0<..<(1/2)^n}. measure M {x. infdist x S = r} = 0" apply (rule uncountable_disjoint_family_then_exists_zero_measure, auto simp add: disjoint_family_on_def) using uncountable_open_interval by fastforce then obtain r where r: "r∈{0<..<(1/2)^n}" "measure M {x. infdist x S = r} = 0" by blast then have r2: "r > 0" "r < epsilon" using n by auto have "measure M {x. infdist x S ≤ r} ≤ measure M {x. infdist x S ≤ (1/2)^n}" apply (rule finite_measure_mono) using r by auto then have "measure M {x. infdist x S ≤ r} < measure M S + epsilon" using n(2) unfolding T_def by auto then show ?thesis using r(2) r2 by auto qed end (* of locale finite_borel_measure'*) sublocale finite_borel_measure ⊆ finite_borel_measure' by (standard, simp add: M_is_borel) subsection ‹Weak-convergence.thy› text ‹Since weak convergence is not implemented as a topology, the fact that the convergence of a sequence implies the convergence of a subsequence is not automatic. We prove it in the lemma below..› lemma weak_conv_m_subseq: assumes "weak_conv_m M_seq M" "strict_mono r" shows "weak_conv_m (λn. M_seq (r n)) M" using assms LIMSEQ_subseq_LIMSEQ unfolding weak_conv_m_def weak_conv_def comp_def by auto context fixes μ :: "nat ⇒ real measure" and M :: "real measure" assumes μ: "⋀n. real_distribution (μ n)" assumes M: "real_distribution M" assumes μ_to_M: "weak_conv_m μ M" begin text ‹The measure of a closed set behaves upper semicontinuously with respect to weak convergence: if $\mu_n \to \mu$, then $\limsup \mu_n(F) \leq \mu(F)$ (and the inequality can be strict, think of the situation where $\mu$ is a Dirac mass at $0$ and $F = \{0\}$, but $\mu_n$ has a density so that $\mu_n(\{0\}) = 0$).› lemma closed_set_weak_conv_usc: assumes "closed S" "measure M S < l" shows "eventually (λn. measure (μ n) S < l) sequentially" proof (cases "S = {}") case True then show ?thesis using ‹measure M S < l› by auto next case False interpret real_distribution M using M by simp define epsilon where "epsilon = l - measure M S" have "epsilon > 0" unfolding epsilon_def using assms(2) by auto obtain r where r: "r > 0" "r < epsilon" "measure M {x. infdist x S = r} = 0" "measure M {x. infdist x S ≤ r} < measure M S + epsilon" using approx_closed_set_with_set_zero_measure_boundary[OF ‹closed S› ‹epsilon > 0› ‹S ≠ {}›] by blast define T where "T = {x. infdist x S ≤ r}" have [measurable]: "T ∈ sets borel" unfolding T_def by auto have "S ⊆ T" unfolding T_def using ‹closed S› ‹r > 0› by auto have "measure M T < l" using r(4) unfolding T_def epsilon_def by auto have "measure M (frontier T) ≤ measure M {x. infdist x S = r}" apply (rule finite_measure_mono) unfolding T_def using frontier_indist_le by auto then have "measure M (frontier T) = 0" using ‹measure M {x. infdist x S = r} = 0› by (auto simp add: measure_le_0_iff) then have "(λn. measure (μ n) T) ⇢ measure M T" using μ_to_M by (simp add: μ emeasure_eq_measure real_distribution_axioms weak_conv_imp_continuity_set_conv) then have *: "eventually (λn. measure (μ n) T < l) sequentially" apply (rule order_tendstoD) using ‹measure M T < l› by simp have **: "measure (μ n) S ≤ measure (μ n) T" for n apply (rule finite_measure.finite_measure_mono) using μ apply (simp add: finite_borel_measure.axioms(1) real_distribution.finite_borel_measure_M) using ‹S ⊆ T› apply simp by (simp add: μ real_distribution.events_eq_borel) show ?thesis apply (rule eventually_mono[OF *]) using ** le_less_trans by auto qed text ‹In the same way, the measure of an open set behaves lower semicontinuously with respect to weak convergence: if $\mu_n \to \mu$, then $\liminf \mu_n(U) \geq \mu(U)$ (and the inequality can be strict). This follows from the same statement for closed sets by passing to the complement.› lemma open_set_weak_conv_lsc: assumes "open S" "measure M S > l" shows "eventually (λn. measure (μ n) S > l) sequentially" proof - interpret real_distribution M using M by auto have [measurable]: "S ∈ events" using assms(1) by auto have "eventually (λn. measure (μ n) (UNIV - S) < 1 - l) sequentially" apply (rule closed_set_weak_conv_usc) using assms prob_compl[of S] by auto moreover have "measure (μ n) (UNIV - S) = 1 - measure (μ n) S" for n proof - interpret mu: real_distribution "μ n" using μ by auto have "S ∈ mu.events" using assms(1) by auto then show ?thesis using mu.prob_compl[of S] by auto qed ultimately show ?thesis by auto qed end (*of context weak_conv_m*) end (*of SG_Library_Complement.thy*)