# Theory SG_Library_Complement

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

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)"

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))"

lemma abs_Max_sum2:
fixes f::"_ ⇒ real"
assumes "finite A" "A ≠ {}"
shows "abs(Max (fA)) ≤ (∑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 (fA)"
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 (fA)"
proof -
have "(inv f) (Inf (fA)) ≤ Inf ((inv f)(fA))"
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 (fA) ≤ f (Inf ((inv f)(fA)))"
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
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›
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
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 (fA)"
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 (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]
next
assume "∄r. a = ereal r"
with ‹0 ≤ a› have "a = ∞"
by (cases a) auto
then show ?thesis
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"

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
qed
then have "A m ⊆ A n" if "m > n" for m n
then show ?thesis
(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))"
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)"
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"
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"]

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
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'

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
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*)


# Theory ME_Library_Complement

(*
File:     ME_Library_Complement.thy
Author:   Manuel Eberl, TU München
*)
theory ME_Library_Complement
imports "HOL-Analysis.Analysis"
begin

(* TODO: could be put in the distribution *)

subsection ‹The trivial measurable space›

text ‹
The trivial measurable space is the smallest possible ‹σ›-algebra, i.e. only the empty set
and everything.
›
definition trivial_measure :: "'a set ⇒ 'a measure" where
"trivial_measure X = sigma X {{}, X}"

lemma space_trivial_measure [simp]: "space (trivial_measure X) = X"

lemma sets_trivial_measure: "sets (trivial_measure X) = {{}, X}"
by (simp add: trivial_measure_def sigma_algebra_trivial sigma_algebra.sigma_sets_eq)

lemma measurable_trivial_measure:
assumes "f ∈ space M → X" and "f - X ∩ space M ∈ sets M"
shows   "f ∈ M →⇩M trivial_measure X"
using assms unfolding measurable_def by (auto simp: sets_trivial_measure)

lemma measurable_trivial_measure_iff:
"f ∈ M →⇩M trivial_measure X ⟷ f ∈ space M → X ∧ f - X ∩ space M ∈ sets M"
unfolding measurable_def by (auto simp: sets_trivial_measure)

subsection ‹Pullback algebras›

text ‹
The pullback algebra $f^{-1}(\Sigma)$ of a ‹σ›-algebra $(\Omega, \Sigma)$ is the smallest
‹σ›-algebra such that $f$ is $f^{-1}(\Sigma)--\Sigma$-measurable.
›
definition (in sigma_algebra) pullback_algebra :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'b set set" where
"pullback_algebra f Ω' = sigma_sets Ω' {f - A ∩ Ω' |A. A ∈ M}"

lemma pullback_algebra_minimal:
assumes "f ∈ M →⇩M N"
shows   "sets.pullback_algebra N f (space M) ⊆ sets M"
proof
fix X assume "X ∈ sets.pullback_algebra N f (space M)"
thus "X ∈ sets M"
unfolding sets.pullback_algebra_def
by induction (use assms in ‹auto simp: measurable_def›)
qed

lemma (in sigma_algebra) in_pullback_algebra: "A ∈ M ⟹ f - A ∩ Ω' ∈ pullback_algebra f Ω'"
unfolding pullback_algebra_def by (rule sigma_sets.Basic) auto

end

# Theory Fekete

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

theory Fekete
imports "HOL-Analysis.Multivariate_Analysis"
begin

text ‹A real sequence is subadditive if $u_{n+m} \leq u_n+u_m$. This implies the
convergence of $u_n/n$ to $Inf\{u_n/n\} \in [-\infty, +\infty)$, a useful result known
as Fekete lemma. We prove it below.

Taking logarithms, the same result applies to submultiplicative sequences. We illustrate
it with the definition of the spectral radius as the limit of $\|x^n\|^{1/n}$, the
convergence following from Fekete lemma.›

text ‹We define subadditive sequences, either from the start or eventually.›

where "subadditive u = (∀m n. u (m+n) ≤ u m + u n)"

assumes "⋀m n. u (m+n) ≤ u m + u n"
unfolding subadditive_def using assms by auto

shows "u (m+n) ≤ u m + u n"
using assms unfolding subadditive_def by auto

"n > 0"
shows "u n ≤ n * u 1"
proof -
have *: "n = 0 ∨ (u n ≤ n * u 1)" for n
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
consider "n = 0" | "n > 0" by auto
then show ?case
proof (cases)
case 1
then show ?thesis by auto
next
case 2
then have "u (Suc n) ≤ u n + u 1" using subadditiveD[OF assms(1), of n 1] by auto
then show ?thesis using Suc.IH 2 by (auto simp add: algebra_simps)
qed
qed
show ?thesis using *[of n] ‹n > 0› by auto
qed

definition eventually_subadditive::"(nat⇒real) ⇒ nat ⇒ bool"
where "eventually_subadditive u N0 = (∀m>N0. ∀n>N0. u (m+n) ≤ u m + u n)"

assumes "⋀m n. m > N0 ⟹ n > N0 ⟹ u (m+n) ≤ u m + u n"
unfolding eventually_subadditive_def using assms by auto

text ‹The main inequality that will lead to convergence is given in the next lemma:
given $n$, then eventually $u_m/m$ is bounded by $u_n/n$, up to an arbitrarily small error.
This is proved by doing the euclidean division of $m$ by $n$ and using the subadditivity.
(the remainder in the euclidean division will give the error term.)›

assumes "eventually_subadditive u N0" "e>0" "n>N0"
shows "∃N>N0. ∀m≥N. u m/m < u n/n + e"
proof -
have ineq_rec: "u(a*n+r) ≤ a * u n + u r" if "n>N0" "r>N0" for a n r
proof (induct a)
case (Suc a)
have "a*n+r>N0" using ‹r>N0› by simp
have "u((Suc a)*n+r) = u(a*n+r+n)" by (simp add: algebra_simps)
also have "... ≤ u(a*n+r)+u n" using assms ‹n>N0› ‹a*n+r>N0› eventually_subadditive_def by blast
also have "... ≤ a*u n + u r + u n" by (simp add: Suc.hyps)
also have "... = (Suc a) * u n + u r" by (simp add: algebra_simps)
finally show ?case by simp
qed (simp)

have "n>0" "real n > 0" using ‹n>N0› by auto
define C where "C = Max {abs(u i) |i. i≤2*n}"
have ineq_C: "abs(u i) ≤ C" if "i ≤ 2 * n" for i
unfolding C_def by (intro Max_ge, auto simp add: that)

have ineq_all_m: "u m/m ≤ u n/n + 3*C/m" if "m≥n" for m
proof -
have "real m>0" using ‹m≥n› ‹0 < real n› by linarith

obtain a0 r0 where "r0<n" "m = a0*n+r0"
using ‹0 < n› mod_div_decomp mod_less_divisor by blast
define a where "a = a0-1"
define r where "r = r0+n"
have "r<2*n" "r≥n" unfolding r_def by (auto simp add: ‹r0<n›)
have "a0>0" using ‹m = a0*n + r0› ‹n ≤ m› ‹r0 < n› not_le by fastforce
then have "m = a * n + r" using a_def r_def ‹m = a0*n+r0› mult_eq_if by auto
then have real_eq: "-r = real n * a - m" by simp

have "r>N0" using ‹r≥n› ‹n>N0› by simp
then have "u m ≤ a * u n + u r" using ineq_rec ‹m = a*n+r› ‹n>N0› by simp
then have "n * u m ≤ n * (a * u n + u r)" using ‹real n>0› by simp
then have "n * u m - m * u n ≤ -r * u n + n * u r"
unfolding real_eq by (simp add: algebra_simps)
also have "... ≤ r * abs(u n) + n * abs(u r)"
also have "... ≤ (2 * n) * C + n * C"
apply (intro add_mono mult_mono ineq_C) using less_imp_le[OF ‹r < 2 * n›] by auto
finally have "n * u m - m * u n ≤ 3*C*n" by auto
then show "u m/m ≤ u n/n + 3*C/m"
using ‹0 < real n› ‹0 < real m› by (simp add: divide_simps mult.commute)
qed

obtain M::nat where M: "M ≥ 3 * C / e" using real_nat_ceiling_ge by auto
define N where "N = M + n + N0 + 1"
have "N > 3 * C / e" "N ≥ n" "N > N0" unfolding N_def using M by auto
have "u m/m < u n/n + e" if "m ≥ N" for m
proof -
have "3 * C / m < e"
using that ‹N > 3 * C / e› ‹e > 0› apply (auto simp add: algebra_simps divide_simps)
by (meson le_less_trans linorder_not_le mult_less_cancel_left_pos of_nat_less_iff)
then show ?thesis using ineq_all_m[of m] ‹n ≤ N› ‹N ≤ m› by auto
qed
then show ?thesis using ‹N0 < N› by blast
qed

text ‹From the inequality above, we deduce the convergence of $u_n/n$ to its infimum. As this
infimum might be $-\infty$, we formulate this convergence in the extended reals. Then, we
specialize it to the real situation, separating the cases where $u_n/n$ is bounded below or not.›

shows "(λm. ereal(u m/m)) ⇢ Inf {ereal(u n/n) | n. n>N0}"
proof -
define v where "v = (λm. ereal(u m/m))"
define V where "V = {v n | n. n>N0}"
define l where "l = Inf V"

have "⋀t. t∈V ⟹ t≥l" by (simp add: Inf_lower l_def)
then have "v n ≥ l" if "n > N0" for n using V_def that by blast
then have lower: "eventually (λn. a < v n) sequentially" if "a < l" for a
by (meson that dual_order.strict_trans1 eventually_at_top_dense)

have upper: "eventually (λn. a > v n) sequentially" if "a > l" for a
proof -
obtain t where "t∈V" "t<a" by (metis ‹a>l› Inf_greatest l_def not_le)
then obtain e::real where "e>0" "t+e < a" by (meson ereal_le_epsilon2 leD le_less_linear)
obtain n where "n>N0" "t = u n/n" using V_def v_def ‹t ∈ V› by blast
then have "u n/n + e < a" using ‹t+e < a› by simp
obtain N where "∀m≥N. u m/m < u n/n + e"
using eventually_subadditive_ineq[OF assms] ‹0 < e› ‹N0 < n› by blast
then have "u m/m < a" if "m ≥ N" for m
using that ‹u n/n + e < a› less_ereal.simps(1) less_trans by blast
then have "v m< a" if "m ≥ N" for m using v_def that by blast
then show ?thesis using eventually_at_top_linorder by auto
qed
show ?thesis
using lower upper unfolding V_def l_def v_def by (simp add: order_tendsto_iff)
qed

shows "(λm. ereal(u m/m)) ⇢ Inf {ereal(u n/n) | n. n>0}"

"bdd_below {u n/n | n. n>N0}"
shows "(λn. u n/n) ⇢ Inf {u n/n | n. n>N0}"
proof-
have *: "(λn. ereal(u n /n)) ⇢ Inf {ereal(u n/n)|n. n > N0}"
define V where "V = {u n/n | n. n>N0}"
have a: "bdd_below V" "V≠{}" by (auto simp add: V_def assms(2))
have "Inf {ereal(t)| t. t∈V} = ereal(Inf V)" by (subst ereal_Inf'[OF a], simp add: Setcompr_eq_image)
moreover have "{ereal(t)| t. t∈V} = {ereal(u n/n)|n. n > N0}" using V_def by blast
ultimately have "Inf {ereal(u n/n)|n. n > N0} = ereal(Inf {u n/n |n. n > N0})" using V_def by auto
then have "(λn. ereal(u n /n)) ⇢ ereal(Inf {u n/n | n. n>N0})" using * by auto
then show ?thesis by simp
qed

"bdd_below {u n/n | n. n>0}"
shows "(λn. u n/n) ⇢ Inf {u n/n | n. n>0}"

text ‹We reformulate the previous lemma in a more directly usable form, avoiding the infimum.›

"⋀n. n > 0 ⟹ u n ≥ n * (a::real)"
shows "∃l. (λn. u n / n) ⇢ l ∧ (∀n>0. u n ≥ n * l)"
proof -
have B: "bdd_below {u n/n | n. n>0}"
apply (rule bdd_belowI[of _ a]) using assms(2)
apply (metis mult.commute mult_left_le_imp_le of_nat_0_less_iff)
done
define l where "l = Inf {u n/n | n. n>0}"
have *: "u n / n ≥ l" if "n > 0" for n
unfolding l_def using that by (auto intro!: cInf_lower[OF _ B])
show ?thesis
apply (rule exI[of _ l], auto)
using * by (simp add: divide_simps algebra_simps)
qed

"¬ (bdd_below {u n/n | n. n>N0})"
shows "(λn. ereal(u n/n)) ⇢ -∞"
proof -
have *: "(λn. ereal(u n /n)) ⇢ Inf {ereal(u n/n)|n. n > N0}"
define V where "V = {u n/n | n. n>N0}"
then have "¬ bdd_below V" using assms by simp
have "Inf {ereal(t) | t. t∈V} = -∞"
by (rule ereal_bot, metis (mono_tags, lifting) ‹¬ bdd_below V› bdd_below_def
leI Inf_lower2 ereal_less_eq(3) le_less mem_Collect_eq)
moreover have "{ereal(t)| t. t∈V} = {ereal(u n/n)|n. n > N0}" using V_def by blast
ultimately have "Inf {ereal(u n/n)|n. n > N0} = -∞" by auto
then show ?thesis using * by simp
qed

"¬ (bdd_below {u n/n | n. n>0})"
shows "(λn. ereal(u n/n)) ⇢ -∞"

sequences. We reformulate quickly some of the above results in this setting.›

where "superadditive u = (∀m n. u (m+n) ≥ u m + u n)"

"n > 0"
shows "u n ≥ n * u 1"

"⋀n. n > 0 ⟹ u n ≤ n * (a::real)"
shows "∃l. (λn. u n / n) ⇢ l ∧ (∀n>0. u n ≤ n * l)"
proof -
have "∃l. (λn. -u n / n) ⇢ l ∧ (∀n>0. -u n ≥ n * l)"
using assms(2) by auto
then obtain l where l: "(λn. -u n / n) ⇢ l" "(∀n>0. -u n ≥ n * l)" by blast
have "(λn. -((-u n)/n)) ⇢ -l"
by (intro tendsto_intros l)
moreover have "∀n>0. u n ≤ n * (-l)"
using l(2) by (auto simp add: algebra_simps) (metis minus_equation_iff neg_le_iff_le)
ultimately show ?thesis
by auto
qed

text ‹One often encounters sequences which are both subadditive and superadditive, but only up
to an additive constant. Adding or subtracting this constant, one can make the sequence
Such sequences appear notably when dealing with quasimorphisms.›

fixes u::"nat ⇒ real"
assumes "⋀m n. abs(u(m+n) - u m - u n) ≤ C"
shows "convergent (λn. u n/n)"
"abs(u k - k * lim (λn. u n / n)) ≤ C"
proof -
have "(abs (u 0)) ≤ C" using assms[of 0 0] by auto
then have "C ≥ 0" by auto

define v where "v = (λn. u n + C)"
then have vle: "v n ≤ n * v 1" if "n > 0" for n
define w where "w = (λn. u n - C)"
then have wge: "w n ≥ n * w 1" if "n > 0" for n

have I: "v n ≥ w n" for n
unfolding v_def w_def using ‹C ≥ 0› by auto
then have *: "v n ≥ n * w 1" if "n > 0" for n using order_trans[OF wge[OF that]] by auto
then obtain lv where lv: "(λn. v n/n) ⇢ lv" "⋀n. n > 0 ⟹ v n ≥ n * lv"
have *: "w n ≤ n * v 1" if "n > 0" for n using order_trans[OF _ vle[OF that]] I by auto
then obtain lw where lw: "(λn. w n/n) ⇢ lw" "⋀n. n > 0 ⟹ w n ≤ n * lw"

have *: "v n/n = w n /n + 2*C*(1/n)" for n
unfolding v_def w_def by (auto simp add: algebra_simps divide_simps)
have "(λn. w n /n + 2*C*(1/n)) ⇢ lw + 2*C*0"
by (intro tendsto_add tendsto_mult lim_1_over_n lw, auto)
then have "lw = lv"
unfolding *[symmetric] using lv(1) LIMSEQ_unique by auto

have *: "u n/n = w n /n + C*(1/n)" for n
unfolding w_def by (auto simp add: algebra_simps divide_simps)
have "(λn. u n /n) ⇢ lw + C*0"
unfolding * by (intro tendsto_add tendsto_mult lim_1_over_n lw, auto)
then have lu: "convergent (λn. u n/n)" "lim (λn. u n/n) = lw"
by (auto simp add: convergentI limI)
then show "convergent (λn. u n/n)" by simp

show "abs(u k - k * lim (λn. u n / n)) ≤ C"
proof (cases "k>0")
case False
then show ?thesis using assms[of 0 0] by auto
next
case True
have "u k - k * lim (λn. u n/n) = v k - C - k * lv" unfolding lu(2) ‹lw = lv› v_def by auto
also have "... ≥ -C" using lv(2)[OF True] by auto
finally have A: "u k - k * lim (λn. u n/n) ≥ - C" by simp
have "u k - k * lim (λn. u n/n) = w k + C - k * lw" unfolding lu(2) w_def by auto
also have "... ≤ C" using lw(2)[OF True] by auto
finally show ?thesis using A by auto
qed
qed

subsection ‹Submultiplicative sequences, application to the spectral radius›

text ‹In the same way as subadditive sequences, one may define submultiplicative sequences.
Essentially, a sequence is submultiplicative if its logarithm is subadditive. A difference is
that we allow a submultiplicative sequence to take the value $0$, as this shows up in applications.
This implies that we have to distinguish in the proofs the situations where the value $0$
is taken or not. In the latter situation, we can use directly the results from the
subadditive case to deduce convergence. In the former situation, convergence to $0$ is obvious
as the sequence vanishes eventually.›

lemma submultiplicative_converges:
fixes u::"nat⇒real"
assumes "⋀n. u n ≥ 0"
"⋀m n. u (m+n) ≤ u m * u n"
shows "(λn. root n (u n))⇢ Inf {root n (u n) | n. n>0}"
proof -
define v where "v = (λ n. root n (u n))"
define V where "V = {v n | n. n>0}"
then have "V ≠ {}" by blast
have "t ≥ 0" if "t ∈ V" for t using that V_def v_def assms(1) by auto
then have "Inf V ≥ 0" by (simp add: ‹V ≠ {}› cInf_greatest)
have "bdd_below V" by (meson ‹⋀t. t ∈ V ⟹ 0 ≤ t› bdd_below_def)

show ?thesis
proof cases
assume "∃n. u n = 0"
then obtain n where "u n = 0" by auto
then have "u m = 0" if "m ≥ n" for m by (metis that antisym_conv assms(1) assms(2) le_Suc_ex mult_zero_left)
then have *: "v m = 0" if "m ≥ n" for m using v_def that by simp
then have "v ⇢ 0" using lim_explicit by force

have "v (Suc n) ∈ V" using V_def by blast
moreover have "v (Suc n) = 0" using * by auto
ultimately have "Inf V ≤ 0" by (simp add: ‹bdd_below V› cInf_lower)
then have "Inf V = 0" using ‹0 ≤ Inf V› by auto
then show ?thesis using V_def v_def ‹v ⇢ 0› by auto
next
assume "¬ (∃n. u n = 0)"
then have "u n > 0" for n by (metis assms(1) less_eq_real_def)
define w where "w n = ln (u n)" for n
have express_vn: "v n = exp(w n/n)" if "n>0" for n
proof -
have "(exp(w n/n))^n = exp(n*(w n/n))" by (metis exp_of_nat_mult)
also have "... = exp(w n)" by (simp add: ‹0 < n›)
also have "... = u n" by (simp add: ‹⋀n. 0 < u n› w_def)
finally have "exp(w n/n) = root n (u n)" by (metis ‹0 < n› exp_ge_zero real_root_power_cancel)
then show ?thesis unfolding v_def by simp
qed

fix m n
have "w (m+n) = ln (u (m+n))" by (simp add: w_def)
also have "... ≤ ln(u m * u n)"
by (meson ‹⋀n. 0 < u n› assms(2) zero_less_mult_iff ln_le_cancel_iff)
also have "... = ln(u m) + ln(u n)" by (simp add: ‹⋀n. 0 < u n› ln_mult)
also have "... = w m + w n" by (simp add: w_def)
finally show "w (m+n) ≤ w m + w n".
qed

define l where "l = Inf V"
then have "v n≥l" if "n > 0" for n
using V_def that by (metis (mono_tags, lifting) ‹bdd_below V› cInf_lower mem_Collect_eq)
then have lower: "eventually (λn. a < v n) sequentially" if "a < l" for a
by (meson that dual_order.strict_trans1 eventually_at_top_dense)

have upper: "eventually (λn. a > v n) sequentially" if "a > l" for a
proof -
obtain t where "t∈V" "t < a" using ‹V ≠ {}› cInf_lessD l_def ‹a>l› by blast
then have "t > 0" using V_def ‹⋀n. 0 < u n› v_def by auto
then have "a/t > 1" using ‹t<a› by simp
define e where "e = ln(a/t)/2"
have "e > 0" "e < ln(a/t)" unfolding e_def by (simp_all add: ‹1 < a / t› ln_gt_zero)
then have "exp(e) < a/t" by (metis ‹1 < a / t› exp_less_cancel_iff exp_ln less_trans zero_less_one)

obtain n where "n>0" "t = v n" using V_def v_def ‹t ∈ V› by blast
with ‹0 < t› have "v n * exp(e) < a" using ‹exp(e) < a/t›

obtain N where *: "N>0" "⋀m. m≥N ⟹ w m/m < w n/n + e"
have "v m < a" if "m ≥ N" for m
proof -
have "m>0" using that ‹N>0› by simp
have "w m/m < w n/n + e" by (simp add: ‹N ≤ m› *)
then have "exp(w m/m) < exp(w n/n + e)" by simp
also have "... = exp(w n/n) * exp(e)" by (simp add: mult_exp_exp)
finally have "v m < v n * exp(e)" using express_vn ‹m>0› ‹n>0› by simp
then show "v m < a" using ‹v n * exp(e) < a› by simp
qed
then show ?thesis using eventually_at_top_linorder by auto
qed

show ?thesis
using lower upper unfolding v_def l_def V_def by (simp add: order_tendsto_iff)
qed
qed

text ‹An important application of submultiplicativity is to prove the existence of the
spectral radius of a matrix, as the limit of $\|A^n\|^{1/n}$.›

where "spectral_radius x = Inf {root n (norm(x^n))| n. n>0}"

fixes x::"'a::real_normed_algebra_1"
defines "V ≡ {root n (norm(x^n))| n. n>0}"
shows "⋀t. t∈V ⟹ t ≥ spectral_radius x"
"⋀t. t∈V ⟹ t ≥ 0"
"bdd_below V"
"V ≠ {}"
"Inf V ≥ 0"
proof -
show "V≠{}" using V_def by blast
show *: "t ≥ 0" if "t ∈ V" for t using that unfolding V_def using real_root_pos_pos_le by auto
then show "bdd_below V" by (meson bdd_below_def)
then show "Inf V ≥ 0" by (simp add: ‹V ≠ {}› * cInf_greatest)
show "⋀t. t∈V ⟹ t ≥ spectral_radius x" by (metis (mono_tags, lifting) ‹bdd_below V› assms cInf_lower spectral_radius_def)
qed

proof (cases)
assume "¬(n = 0)"
have "root n (norm(x^n)) ≥ spectral_radius x"
using spectral_radius_aux ‹n ≠ 0› by auto
then show ?thesis
by (metis ‹n ≠ 0› spectral_radius_nonneg norm_ge_zero not_gr0 power_mono real_root_pow_pos2)
qed (simp)

"(λn. root n (norm(x^n))) ⇢ spectral_radius x"
proof -
have "norm(x^(m+n)) ≤ norm(x^m) * norm(x^n)" for m n by (simp add: power_add norm_mult_ineq)
then show ?thesis unfolding spectral_radius_def using submultiplicative_converges by auto
qed

end (*of Fekete.thy*)


# Theory Asymptotic_Density

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

section ‹Asymptotic densities›

theory Asymptotic_Density
imports SG_Library_Complement
begin

text ‹The upper asymptotic density of a subset $A$ of the integers is
$\limsup Card(A \cap [0,n)) / n \in [0,1]$. It measures how big a set of integers is,
at some times. In this paragraph, we establish the basic properties of this notion.

There is a corresponding notion of lower asymptotic density, with a liminf instead
of a limsup, measuring how big a set is at all times. The corresponding properties
are proved exactly in the same way.
›

subsection ‹Upper asymptotic densities›

text ‹As limsups are only defined for sequences taking values in a complete lattice
(here the extended reals), we define it in the extended reals and then go back to the reals.
This is a little bit artificial, but it is not a real problem as in the applications we
will never come back to this definition.›

definition upper_asymptotic_density::"nat set ⇒ real"
where "upper_asymptotic_density A = real_of_ereal(limsup (λn. card(A ∩ {..<n})/n))"

text ‹First basic property: the asymptotic density is between $0$ and $1$.›

lemma upper_asymptotic_density_in_01:
"ereal(upper_asymptotic_density A) = limsup (λn. card(A ∩ {..<n})/n)"
"upper_asymptotic_density A ≤ 1"
"upper_asymptotic_density A ≥ 0"
proof -
{
fix n::nat assume "n>0"
have "card(A ∩ {..<n}) ≤ n" by (metis card_lessThan Int_lower2 card_mono finite_lessThan)
then have "card(A ∩ {..<n}) / n ≤ ereal 1" using ‹n>0› by auto
}
then have "eventually (λn. card(A ∩ {..<n}) / n ≤ ereal 1) sequentially"
then have a: "limsup (λn. card(A ∩ {..<n})/n) ≤ 1" by (simp add: Limsup_const Limsup_bounded)

have "card(A ∩ {..<n}) / n ≥ ereal 0" for n by auto
then have "liminf (λn. card(A ∩ {..<n})/n) ≥ 0" by (simp add: le_Liminf_iff less_le_trans)
then have b: "limsup (λn. card(A ∩ {..<n})/n) ≥ 0" by (meson Liminf_le_Limsup order_trans sequentially_bot)

have "abs(limsup (λn. card(A ∩ {..<n})/n)) ≠ ∞" using a b by auto
then show "ereal(upper_asymptotic_density A) = limsup (λn. card(A ∩ {..<n})/n)"
unfolding upper_asymptotic_density_def by auto
show "upper_asymptotic_density A ≤ 1" "upper_asymptotic_density A ≥ 0" unfolding upper_asymptotic_density_def
using a b by (auto simp add: real_of_ereal_le_1 real_of_ereal_pos)
qed

text ‹The two next propositions give the usable characterization of the asymptotic density, in
terms of the eventual cardinality of $A \cap [0, n)$. Note that the inequality is strict for one
implication and large for the other.›

proposition upper_asymptotic_densityD:
fixes l::real
assumes "upper_asymptotic_density A < l"
shows "eventually (λn. card(A ∩ {..<n}) < l * n) sequentially"
proof -
have "limsup (λn. card(A ∩ {..<n})/n) < l"
using assms upper_asymptotic_density_in_01(1) ereal_less_ereal_Ex by auto
then have "eventually (λn. card(A ∩ {..<n})/n < ereal l) sequentially"
using Limsup_lessD by blast
then have "eventually (λn. card(A ∩ {..<n})/n < ereal l ∧ n > 0) sequentially"
using eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n}) < l * n" if "card(A ∩ {..<n})/n < ereal l ∧ n > 0" for n
using that by (simp add: divide_less_eq)
ultimately show "eventually (λn. card(A ∩ {..<n}) < l * n) sequentially"
qed

proposition upper_asymptotic_densityI:
fixes l::real
assumes "eventually (λn. card(A ∩ {..<n}) ≤ l * n) sequentially"
shows "upper_asymptotic_density A ≤ l"
proof -
have "eventually (λn. card(A ∩ {..<n}) ≤ l * n ∧ n > 0) sequentially"
using assms eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n})/n ≤ ereal l" if "card(A ∩ {..<n}) ≤ l * n ∧ n > 0" for n
using that by (simp add: divide_le_eq)
ultimately have "eventually (λn. card(A ∩ {..<n})/n ≤ ereal l) sequentially"
then have "limsup (λn. card(A ∩ {..<n})/n) ≤ ereal l"
then have "ereal(upper_asymptotic_density A) ≤ ereal l"
using upper_asymptotic_density_in_01(1) by auto
then show ?thesis by (simp del: upper_asymptotic_density_in_01)
qed

text ‹The following trivial lemma is useful to control the asymptotic density of unions.›

lemma lem_ge_sum:
fixes l x y::real
assumes "l>x+y"
shows "∃lx ly. l = lx + ly ∧ lx > x ∧ ly > y"
proof -
define lx ly where "lx = x + (l-(x+y))/2" and "ly = y + (l-(x+y))/2"
have "l = lx + ly ∧ lx > x ∧ ly > y" unfolding lx_def ly_def using assms by auto
then show ?thesis by auto
qed

text ‹The asymptotic density of a union is bounded by the sum of the asymptotic densities.›

lemma upper_asymptotic_density_union:
"upper_asymptotic_density (A ∪ B) ≤ upper_asymptotic_density A + upper_asymptotic_density B"
proof -
have "upper_asymptotic_density (A ∪ B) ≤ l" if H: "l > upper_asymptotic_density A + upper_asymptotic_density B" for l
proof -
obtain lA lB where l: "l = lA+lB" and lA: "lA > upper_asymptotic_density A" and lB: "lB > upper_asymptotic_density B"
using lem_ge_sum H by blast
{
fix n assume H: "card (A ∩ {..<n}) < lA * n ∧ card (B ∩ {..<n}) < lB * n"
have "card((A∪B) ∩ {..<n}) ≤ card(A ∩ {..<n}) + card(B ∩ {..<n})"
also have "... ≤ l * n" using l H by (simp add: ring_class.ring_distribs(2))
finally have "card ((A∪B) ∩ {..<n}) ≤ l * n" by simp
}
moreover have "eventually (λn. card (A ∩ {..<n}) < lA * n ∧ card (B ∩ {..<n}) < lB * n) sequentially"
using upper_asymptotic_densityD[OF lA] upper_asymptotic_densityD[OF lB] eventually_conj by blast
ultimately have "eventually (λn. card((A∪B) ∩ {..<n}) ≤ l * n) sequentially"
then show "upper_asymptotic_density (A ∪ B) ≤ l" using upper_asymptotic_densityI by auto
qed
then show ?thesis by (meson dense not_le)
qed

text ‹It follows that the asymptotic density is an increasing function for inclusion.›

lemma upper_asymptotic_density_subset:
assumes "A ⊆ B"
shows "upper_asymptotic_density A ≤ upper_asymptotic_density B"
proof -
have "upper_asymptotic_density A ≤ l" if l: "l > upper_asymptotic_density B" for l
proof -
have "card(A ∩ {..<n}) ≤ card(B ∩ {..<n})" for n
using assms by (metis Int_lower2 Int_mono card_mono finite_lessThan finite_subset inf.left_idem)
then have "card(A ∩ {..<n}) ≤ l * n" if "card(B ∩ {..<n}) < l * n" for n
using that by (meson lessThan_def less_imp_le of_nat_le_iff order_trans)
moreover have "eventually (λn. card(B ∩ {..<n}) < l * n) sequentially"
using upper_asymptotic_densityD l by simp
ultimately have "eventually (λn. card(A ∩ {..<n}) ≤ l * n) sequentially"
then show ?thesis using upper_asymptotic_densityI by auto
qed
then show ?thesis by (meson dense not_le)
qed

text ‹If a set has a density, then it is also its asymptotic density.›

lemma upper_asymptotic_density_lim:
assumes "(λn. card(A ∩ {..<n})/n) ⇢ l"
shows "upper_asymptotic_density A = l"
proof -
have "(λn. ereal(card(A ∩ {..<n})/n)) ⇢ l" using assms by auto
then have "limsup (λn. card(A ∩ {..<n})/n) = l"
using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
then show ?thesis unfolding upper_asymptotic_density_def by auto
qed

text ‹If two sets are equal up to something small, i.e. a set with zero upper density,
then they have the same upper density.›

lemma upper_asymptotic_density_0_diff:
assumes "A ⊆ B" "upper_asymptotic_density (B-A) = 0"
shows "upper_asymptotic_density A = upper_asymptotic_density B"
proof -
have "upper_asymptotic_density B ≤ upper_asymptotic_density A + upper_asymptotic_density (B-A)"
using upper_asymptotic_density_union[of A "B-A"] by (simp add: assms(1) sup.absorb2)
then have "upper_asymptotic_density B ≤ upper_asymptotic_density A"
using assms(2) by simp
then show ?thesis using upper_asymptotic_density_subset[OF assms(1)] by simp
qed

lemma upper_asymptotic_density_0_Delta:
assumes "upper_asymptotic_density (A Δ B) = 0"
shows "upper_asymptotic_density A = upper_asymptotic_density B"
proof -
have "A- (A∩B) ⊆ A Δ B" "B- (A∩B) ⊆ A Δ B"
using assms(1) by (auto simp add: Diff_Int Un_infinite)
then have "upper_asymptotic_density (A - (A∩B)) = 0"
"upper_asymptotic_density (B - (A∩B)) = 0"
using upper_asymptotic_density_subset assms(1) upper_asymptotic_density_in_01(3)
by (metis inf.absorb_iff2 inf.orderE)+
then have "upper_asymptotic_density (A∩B) = upper_asymptotic_density A"
"upper_asymptotic_density (A∩B) = upper_asymptotic_density B"
using upper_asymptotic_density_0_diff by auto
then show ?thesis by simp
qed

text ‹Finite sets have vanishing upper asymptotic density.›

lemma upper_asymptotic_density_finite:
assumes "finite A"
shows "upper_asymptotic_density A = 0"
proof -
have "(λn. card(A ∩ {..<n})/n) ⇢ 0"
proof (rule tendsto_sandwich[where ?f = "λn. 0" and ?h = "λ(n::nat). card A / n"])
have "card(A ∩ {..<n})/n ≤ card A / n" if "n>0" for n
using that ‹finite A› by (simp add: card_mono divide_right_mono)
then show "eventually (λn. card(A ∩ {..<n})/n ≤ card A / n) sequentially"
have "(λn. real (card A)* (1 / real n)) ⇢ real(card A) * 0"
by (intro tendsto_intros)
then show "(λn. real (card A) / real n) ⇢ 0" by auto
qed (auto)
then show "upper_asymptotic_density A = 0" using upper_asymptotic_density_lim by auto
qed

text ‹In particular, bounded intervals have zero upper density.›

lemma upper_asymptotic_density_bdd_interval [simp]:
"upper_asymptotic_density {} = 0"
"upper_asymptotic_density {..N} = 0"
"upper_asymptotic_density {..<N} = 0"
"upper_asymptotic_density {n..N} = 0"
"upper_asymptotic_density {n..<N} = 0"
"upper_asymptotic_density {n<..N} = 0"
"upper_asymptotic_density {n<..<N} = 0"
by (auto intro!: upper_asymptotic_density_finite)

text ‹The density of a finite union is bounded by the sum of the densities.›

lemma upper_asymptotic_density_finite_Union:
assumes "finite I"
shows "upper_asymptotic_density (⋃i∈I. A i) ≤ (∑i∈I. upper_asymptotic_density (A i))"
using assms apply (induction I rule: finite_induct)
using order_trans[OF upper_asymptotic_density_union] by auto

text ‹It is sometimes useful to compute the asymptotic density by shifting a little bit the set:
this only makes a finite difference that vanishes when divided by $n$.›

lemma upper_asymptotic_density_shift:
fixes k::nat and l::int
shows "ereal(upper_asymptotic_density A) = limsup (λn. card(A ∩ {k..nat(n+l)}) / n)"
proof -
define C where "C = k+2*nat(abs(l))+1"
have *: "(λn. C*(1/n)) ⇢ real C * 0"
by (intro tendsto_intros)
have l0: "limsup (λn. C/n) = 0"
apply (rule lim_imp_Limsup, simp) using * by (simp add: zero_ereal_def)

have "card(A ∩ {k..nat(n+l)}) / n ≤ card (A ∩ {..<n})/n + C/n" for n
proof -
have "card(A ∩ {k..nat(n+l)}) ≤ card (A ∩ {..<n} ∪ {n..n + nat(abs(l))})"
by (rule card_mono, auto)
also have "... ≤ card (A ∩ {..<n}) + card {n..n + nat(abs(l))}"
by (rule card_Un_le)
also have "... ≤ card (A ∩ {..<n}) + real C"
unfolding C_def by auto
finally have "card(A ∩ {k..nat(n+l)}) / n ≤ (card (A ∩ {..<n}) + real C) /n"
also have "... = card (A ∩ {..<n})/n + C/n"
finally show ?thesis
by auto
qed
then have "limsup (λn. card(A ∩ {k..nat(n+l)}) / n) ≤ limsup (λn. card (A ∩ {..<n})/n + ereal(C/n))"
also have "... ≤ limsup (λn. card (A ∩ {..<n})/n) + limsup (λn. C/n)"
finally have a: "limsup (λn. card(A ∩ {k..nat(n+l)}) / n) ≤ limsup (λn. card (A ∩ {..<n})/n)"
using l0 by simp

have "card (A ∩ {..<n}) / n ≤ card (A ∩ {k..nat(n+l)})/n + C/n" for n
proof -
have "card ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))}) ≤ card {..<k} + card {n-nat(abs(l))..n + nat(abs(l))}"
by (rule card_Un_le)
also have "... ≤ k + 2*nat(abs(l)) + 1" by auto
finally have *: "card ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))}) ≤ C" unfolding C_def by blast

have "card(A ∩ {..<n}) ≤ card (A ∩ {k..nat(n+l)} ∪ ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))}))"
by (rule card_mono, auto)
also have "... ≤ card (A ∩ {k..nat(n+l)}) + card ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))})"
by (rule card_Un_le)
also have "... ≤ card (A ∩ {k..nat(n+l)}) + C"
using * by auto
finally have "card (A ∩ {..<n}) / n ≤ (card (A ∩ {k..nat(n+l)}) + real C)/n"
also have "... = card (A ∩ {k..nat(n+l)})/n + C/n"
finally show ?thesis
by auto
qed
then have "limsup (λn. card(A ∩ {..<n}) / n) ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n + ereal(C/n))"
also have "... ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n) + limsup (λn. C/n)"
finally have "limsup (λn. card(A ∩ {..<n}) / n) ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n)"
using l0 by simp
then have "limsup (λn. card(A ∩ {..<n}) / n) = limsup (λn. card (A ∩ {k..nat(n+l)})/n)"
using a by auto
then show ?thesis using upper_asymptotic_density_in_01(1) by auto
qed

text ‹Upper asymptotic density is measurable.›

lemma upper_asymptotic_density_meas [measurable]:
assumes [measurable]: "⋀(n::nat). Measurable.pred M (P n)"
shows "(λx. upper_asymptotic_density {n. P n x}) ∈ borel_measurable M"
unfolding upper_asymptotic_density_def by auto

text ‹A finite union of sets with zero upper density still has zero upper density.›

lemma upper_asymptotic_density_zero_union:
assumes "upper_asymptotic_density A = 0" "upper_asymptotic_density B = 0"
shows "upper_asymptotic_density (A ∪ B) = 0"
using upper_asymptotic_density_in_01(3)[of "A ∪ B"] upper_asymptotic_density_union[of A B] unfolding assms by auto

lemma upper_asymptotic_density_zero_finite_Union:
assumes "finite I" "⋀i. i ∈ I ⟹ upper_asymptotic_density (A i) = 0"
shows "upper_asymptotic_density (⋃i∈I. A i) = 0"
using assms by (induction rule: finite_induct, auto intro!: upper_asymptotic_density_zero_union)

text ‹The union of sets with small asymptotic densities can have a large density: think
of $A_n = [0,n]$, it has density $0$, but the union of the $A_n$ has density $1$. However, if one
only wants a set which contains each $A_n$ eventually, then one can obtain a union'' that has
essentially the same density as each $A_n$. This is often used as a replacement for the diagonal
argument in density arguments: if for each $n$ one can find a set $A_n$ with good properties and
a controlled density, then their union'' will have the same properties (eventually) and a
controlled density.›

proposition upper_asymptotic_density_incseq_Union:
assumes "⋀(n::nat). upper_asymptotic_density (A n) ≤ l" "incseq A"
shows "∃B. upper_asymptotic_density B ≤ l ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
proof -
have A: "∃N. ∀j ≥ N. card (A k ∩ {..<j}) < (l + (1/2)^k) * j" for k
proof -
have *: "upper_asymptotic_density (A k) < l + (1/2)^k" using assms(1)[of k]
show ?thesis
using upper_asymptotic_densityD[OF *] unfolding eventually_sequentially by auto
qed
have "∃N. ∀k. (∀j ≥ N k. card (A k ∩ {..<j}) ≤ (l+(1/2)^k) * j) ∧ N (Suc k) > N k"
proof (rule dependent_nat_choice)
fix x k::nat
obtain N where N: "∀j≥N. real (card (A (Suc k) ∩ {..<j})) ≤ (l + (1 / 2) ^ Suc k) * real j"
using A[of "Suc k"] less_imp_le by auto
show "∃y. (∀j≥y. real (card (A(Suc k) ∩ {..<j})) ≤ (l + (1 / 2) ^ Suc k) * real j) ∧ x < y"
apply (rule exI[of _ "max x N + 1"]) using N by auto
next
show "∃x. ∀j≥x. real (card ((A 0) ∩ {..<j})) ≤ (l + (1 / 2) ^ 0) * real j"
using A[of 0] less_imp_le by auto
qed
text ‹Here is the choice of the good waiting function $N$›
then obtain N where N: "⋀k j. j ≥ N k ⟹ card (A k ∩ {..<j}) ≤ (l + (1/2)^k) * j" "⋀k. N (Suc k) > N k"
by blast
then have "strict_mono N" by (simp add: strict_monoI_Suc)
have Nmono: "N k < N l" if "k < l" for k l
using N(2) by (simp add: lift_Suc_mono_less that)

text ‹We can now define the global bad set $B$.›
define B where "B = (⋃k. A k ∩ {N k..})"
text ‹We will now show that it also has density at most $l$.›
have Bcard: "card (B ∩ {..<n}) ≤ (l+(1/2)^k) * n" if "N k ≤ n" "n < N (Suc k)" for n k
proof -
have "{N j..<n} = {}" if "j ∈ {k<..}" for j
using ‹n < N (Suc k)› that by (auto, meson ‹strict_mono N› less_trans not_less_eq strict_mono_less)
then have *: "(⋃j∈{k<..}. A j ∩ {N j..<n}) = {}" by force

have "B ∩ {..<n} = (⋃j. A j ∩ {N j..<n})"
unfolding B_def by auto
also have "... = (⋃j ∈ {..k}. A j ∩ {N j..<n}) ∪ (⋃j∈{k<..}. A j ∩ {N j..<n})"
unfolding UN_Un [symmetric] by (rule arg_cong [of _ _ Union]) auto
also have "... = (⋃j ∈ {..k}. A j ∩ {N j..<n})"
unfolding * by simp
also have "... ⊆ (⋃j ∈ {..k}. A k ∩ {..<n})"
using ‹incseq A› unfolding incseq_def by (auto intro!: UN_mono)
also have "... = A k ∩ {..<n}"
by simp
finally have "card (B ∩ {..<n}) ≤ card (A k ∩ {..<n})"
by (rule card_mono[rotated], auto)
then show ?thesis
using N(1)[OF ‹n ≥ N k›] by simp
qed
have "eventually (λn. card (B ∩ {..<n}) ≤ a * n) sequentially" if "l < a" for a::real
proof -
have "eventually (λk. (l+(1/2)^k) < a) sequentially"
apply (rule order_tendstoD[of _ "l+0"], intro tendsto_intros) using that by auto
then obtain k where "l + (1/2)^k < a"
unfolding eventually_sequentially by auto
have "card (B ∩ {..<n}) ≤ a * n" if "n ≥ N k + 1"for n
proof -
have "n ≥ N k" "n ≥ 1" using that by auto
have "{p. n ≥ N p} ⊆ {..n}"
using ‹strict_mono N› dual_order.trans seq_suble by blast
then have *: "finite {p. n ≥ N p}" "{p. n ≥ N p} ≠ {}"
using ‹n ≥ N k› finite_subset by auto
define m where "m = Max {p. n ≥ N p}"
have "k ≤ m"
unfolding m_def using Max_ge[OF *(1), of k] that by auto
have "N m ≤ n"
unfolding m_def using Max_in[OF *] by auto
have "Suc m ∉ {p. n ≥ N p}"
unfolding m_def using * Max_ge Suc_n_not_le_n by blast
then have "n < N (Suc m)" by simp
have "card (B ∩ {..<n}) ≤ (l+(1/2)^m) * n"
using Bcard[OF ‹N m ≤ n› ‹n < N (Suc m)›] by simp
also have "... ≤ (l + (1/2)^k) * n"
apply (rule mult_right_mono) using ‹k ≤ m› by (auto simp add: power_decreasing)
also have "... ≤ a * n"
using ‹l + (1/2)^k < a› ‹n ≥ 1› by auto
finally show ?thesis by auto
qed
then show ?thesis unfolding eventually_sequentially by auto
qed
then have "upper_asymptotic_density B ≤ a" if "a > l" for a
using upper_asymptotic_densityI that by auto
then have "upper_asymptotic_density B ≤ l"
by (meson dense not_le)
moreover have "∃N. A n ∩ {N..} ⊆ B" for n
apply (rule exI[of _ "N n"]) unfolding B_def by auto
ultimately show ?thesis by auto
qed

text ‹When the sequence of sets is not increasing, one can only obtain a set whose density
is bounded by the sum of the densities.›

proposition upper_asymptotic_density_Union:
assumes "summable (λn. upper_asymptotic_density (A n))"
shows "∃B. upper_asymptotic_density B ≤ (∑n. upper_asymptotic_density (A n)) ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
proof -
define C where "C = (λn. (⋃i≤n. A i))"
have C1: "incseq C"
unfolding C_def incseq_def by fastforce
have C2: "upper_asymptotic_density (C k) ≤ (∑n. upper_asymptotic_density (A n))" for k
proof -
have "upper_asymptotic_density (C k) ≤ (∑i≤k. upper_asymptotic_density (A i))"
unfolding C_def by (rule upper_asymptotic_density_finite_Union, auto)
also have "... ≤ (∑i. upper_asymptotic_density (A i))"
apply (rule sum_le_suminf[OF assms]) using upper_asymptotic_density_in_01 by auto
finally show ?thesis by simp
qed
obtain B where B: "upper_asymptotic_density B ≤ (∑n. upper_asymptotic_density (A n))"
"⋀n. ∃N. C n ∩ {N..} ⊆ B"
using upper_asymptotic_density_incseq_Union[OF C2 C1] by blast
have "∃N. A n ∩ {N..} ⊆ B" for n
using B(2)[of n] unfolding C_def by auto
then show ?thesis using B(1) by blast
qed

text ‹A particular case of the previous proposition, often useful, is when all sets have density
zero.›

proposition upper_asymptotic_density_zero_Union:
assumes "⋀n::nat. upper_asymptotic_density (A n) = 0"
shows "∃B. upper_asymptotic_density B = 0 ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
proof -
have "∃B. upper_asymptotic_density B ≤ (∑n. upper_asymptotic_density (A n)) ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
apply (rule upper_asymptotic_density_Union) unfolding assms by auto
then obtain B where "upper_asymptotic_density B ≤ 0" "⋀n. ∃N. A n ∩ {N..} ⊆ B"
unfolding assms by auto
then show ?thesis
using upper_asymptotic_density_in_01(3)[of B] by auto
qed

subsection ‹Lower asymptotic densities›

text ‹The lower asymptotic density of a set of natural numbers is defined just as its
upper asymptotic density but using a liminf instead of a limsup. Its properties are proved
exactly in the same way.›

definition lower_asymptotic_density::"nat set ⇒ real"
where "lower_asymptotic_density A = real_of_ereal(liminf (λn. card(A ∩ {..<n})/n))"

lemma lower_asymptotic_density_in_01:
"ereal(lower_asymptotic_density A) = liminf (λn. card(A ∩ {..<n})/n)"
"lower_asymptotic_density A ≤ 1"
"lower_asymptotic_density A ≥ 0"
proof -
{
fix n::nat assume "n>0"
have "card(A ∩ {..<n}) ≤ n" by (metis card_lessThan Int_lower2 card_mono finite_lessThan)
then have "card(A ∩ {..<n}) / n ≤ ereal 1" using ‹n>0› by auto
}
then have "eventually (λn. card(A ∩ {..<n}) / n ≤ ereal 1) sequentially"
then have "limsup (λn. card(A ∩ {..<n})/n) ≤ 1" by (simp add: Limsup_const Limsup_bounded)
then have a: "liminf (λn. card(A ∩ {..<n})/n) ≤ 1"
by (meson Liminf_le_Limsup less_le_trans not_le sequentially_bot)

have "card(A ∩ {..<n}) / n ≥ ereal 0" for n by auto
then have b: "liminf (λn. card(A ∩ {..<n})/n) ≥ 0" by (simp add: le_Liminf_iff less_le_trans)

have "abs(liminf (λn. card(A ∩ {..<n})/n)) ≠ ∞" using a b by auto
then show "ereal(lower_asymptotic_density A) = liminf (λn. card(A ∩ {..<n})/n)"
unfolding lower_asymptotic_density_def by auto
show "lower_asymptotic_density A ≤ 1" "lower_asymptotic_density A ≥ 0" unfolding lower_asymptotic_density_def
using a b by (auto simp add: real_of_ereal_le_1 real_of_ereal_pos)
qed

text ‹The lower asymptotic density is bounded by the upper one. When they coincide,
$Card(A \cap [0,n))/n$ converges to this common value.›

lemma lower_asymptotic_density_le_upper:
"lower_asymptotic_density A ≤ upper_asymptotic_density A"
using lower_asymptotic_density_in_01(1) upper_asymptotic_density_in_01(1)
by (metis (mono_tags, lifting) Liminf_le_Limsup ereal_less_eq(3) sequentially_bot)

lemma lower_asymptotic_density_eq_upper:
assumes "lower_asymptotic_density A = l" "upper_asymptotic_density A = l"
shows "(λn. card(A ∩ {..<n})/n) ⇢ l"
apply (rule limsup_le_liminf_real)
using upper_asymptotic_density_in_01(1)[of A] lower_asymptotic_density_in_01(1)[of A] assms by auto

text ‹In particular, when a set has a zero upper density, or a lower density one, then this
implies the corresponding convergence of $Card(A \cap [0,n))/n$.›

lemma upper_asymptotic_density_zero_lim:
assumes "upper_asymptotic_density A = 0"
shows "(λn. card(A ∩ {..<n})/n) ⇢ 0"
apply (rule lower_asymptotic_density_eq_upper)
using assms lower_asymptotic_density_le_upper[of A] lower_asymptotic_density_in_01(3)[of A] by auto

lemma lower_asymptotic_density_one_lim:
assumes "lower_asymptotic_density A = 1"
shows "(λn. card(A ∩ {..<n})/n) ⇢ 1"
apply (rule lower_asymptotic_density_eq_upper)
using assms lower_asymptotic_density_le_upper[of A] upper_asymptotic_density_in_01(2)[of A] by auto

text ‹The lower asymptotic density of a set is $1$ minus the upper asymptotic density of its complement.
although we will rather give direct proofs as they are not more complicated.›

lemma lower_upper_asymptotic_density_complement:
"lower_asymptotic_density A = 1 - upper_asymptotic_density (UNIV - A)"
proof -
{
fix n assume "n>(0::nat)"
have "{..<n} ∩ UNIV - (UNIV - ({..<n} - (UNIV - A))) = {..<n} ∩ A"
by blast
moreover have "{..<n} ∩ UNIV ∩ (UNIV - ({..<n} - (UNIV - A))) = (UNIV - A) ∩ {..<n}"
by blast
ultimately have "card (A ∩ {..<n}) = n - card((UNIV-A) ∩ {..<n})"
by (metis (no_types) Int_commute card_Diff_subset_Int card_lessThan finite_Int finite_lessThan inf_top_right)
then have "card (A ∩ {..<n})/n = (real n - card((UNIV-A) ∩ {..<n})) / n"
by (metis Int_lower2 card_lessThan card_mono finite_lessThan of_nat_diff)
then have "card (A ∩ {..<n})/n = ereal 1 - card((UNIV-A) ∩ {..<n})/n"
using ‹n>0› by (simp add: diff_divide_distrib)
}
then have "eventually (λn. card (A ∩ {..<n})/n = ereal 1 - card((UNIV-A) ∩ {..<n})/n) sequentially"
then have "liminf (λn. card (A ∩ {..<n})/n) = liminf (λn. ereal 1 - card((UNIV-A) ∩ {..<n})/n)"
by (rule Liminf_eq)
also have "... = ereal 1 - limsup (λn. card((UNIV-A) ∩ {..<n})/n)"
by (rule liminf_ereal_cminus, simp)
finally show ?thesis unfolding lower_asymptotic_density_def
by (metis ereal_minus(1) real_of_ereal.simps(1) upper_asymptotic_density_in_01(1))
qed

proposition lower_asymptotic_densityD:
fixes l::real
assumes "lower_asymptotic_density A > l"
shows "eventually (λn. card(A ∩ {..<n}) > l * n) sequentially"
proof -
have "ereal(lower_asymptotic_density A) > l" using assms by auto
then have "liminf (λn. card(A ∩ {..<n})/n) > l"
using lower_asymptotic_density_in_01(1) by auto
then have "eventually (λn. card(A ∩ {..<n})/n > ereal l) sequentially"
using less_LiminfD by blast
then have "eventually (λn. card(A ∩ {..<n})/n > ereal l ∧ n > 0) sequentially"
using eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n}) > l * n" if "card(A ∩ {..<n})/n > ereal l ∧ n > 0" for n
using that divide_le_eq ereal_less_eq(3) less_imp_of_nat_less not_less of_nat_eq_0_iff by fastforce
ultimately show "eventually (λn. card(A ∩ {..<n}) > l * n) sequentially"
qed

proposition lower_asymptotic_densityI:
fixes l::real
assumes "eventually (λn. card(A ∩ {..<n}) ≥ l * n) sequentially"
shows "lower_asymptotic_density A ≥ l"
proof -
have "eventually (λn. card(A ∩ {..<n}) ≥ l * n ∧ n > 0) sequentially"
using assms eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n})/n ≥ ereal l" if "card(A ∩ {..<n}) ≥ l * n ∧ n > 0" for n
using that by (meson ereal_less_eq(3) not_less of_nat_0_less_iff pos_divide_less_eq)
ultimately have "eventually (λn. card(A ∩ {..<n})/n ≥ ereal l) sequentially"
then have "liminf (λn. card(A ∩ {..<n})/n) ≥ ereal l"
then have "ereal(lower_asymptotic_density A) ≥ ereal l"
using lower_asymptotic_density_in_01(1) by auto
then show ?thesis by auto
qed

text ‹One can control the asymptotic density of an intersection in terms of the asymptotic density
of each component›

lemma lower_asymptotic_density_intersection:
"lower_asymptotic_density A + lower_asymptotic_density B ≤ lower_asymptotic_density (A ∩ B) + 1"
using upper_asymptotic_density_union[of "UNIV - A" "UNIV - B"]
unfolding lower_upper_asymptotic_density_complement by (auto simp add: algebra_simps Diff_Int)

lemma lower_asymptotic_density_subset:
assumes "A ⊆ B"
shows "lower_asymptotic_density A ≤ lower_asymptotic_density B"
using upper_asymptotic_density_subset[of "UNIV-B" "UNIV-A"] assms
unfolding lower_upper_asymptotic_density_complement by auto

lemma lower_asymptotic_density_lim:
assumes "(λn. card(A ∩ {..<n})/n) ⇢ l"
shows "lower_asymptotic_density A = l"
proof -
have "(λn. ereal(card(A ∩ {..<n})/n)) ⇢ l" using assms by auto
then have "liminf (λn. card(A ∩ {..<n})/n) = l"
using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
then show ?thesis unfolding lower_asymptotic_density_def by auto
qed

lemma lower_asymptotic_density_finite:
assumes "finite A"
shows "lower_asymptotic_density A = 0"
using lower_asymptotic_density_in_01(3) upper_asymptotic_density_finite[OF assms] lower_asymptotic_density_le_upper
by (metis antisym_conv)

text ‹In particular, bounded intervals have zero lower density.›

lemma lower_asymptotic_density_bdd_interval [simp]:
"lower_asymptotic_density {} = 0"
"lower_asymptotic_density {..N} = 0"
"lower_asymptotic_density {..<N} = 0"
"lower_asymptotic_density {n..N} = 0"
"lower_asymptotic_density {n..<N} = 0"
"lower_asymptotic_density {n<..N} = 0"
"lower_asymptotic_density {n<..<N} = 0"
by (auto intro!: lower_asymptotic_density_finite)

text ‹Conversely, unbounded intervals have density $1$.›

lemma lower_asymptotic_density_infinite_interval [simp]:
"lower_asymptotic_density {N..} = 1"
"lower_asymptotic_density {N<..} = 1"
"lower_asymptotic_density UNIV = 1"
proof -
have "UNIV - {N..} = {..<N}" by auto
then show "lower_asymptotic_density {N..} = 1"
have "UNIV - {N<..} = {..N}" by auto
then show "lower_asymptotic_density {N<..} = 1"
show "lower_asymptotic_density UNIV = 1"
qed

lemma upper_asymptotic_density_infinite_interval [simp]:
"upper_asymptotic_density {N..} = 1"
"upper_asymptotic_density {N<..} = 1"
"upper_asymptotic_density UNIV = 1"
by (metis antisym upper_asymptotic_density_in_01(2) lower_asymptotic_density_infinite_interval lower_asymptotic_density_le_upper)+

text ‹The intersection of sets with lower density one still has lower density one.›

lemma lower_asymptotic_density_one_intersection:
assumes "lower_asymptotic_density A = 1" "lower_asymptotic_density B = 1"
shows "lower_asymptotic_density (A ∩ B) = 1"
using lower_asymptotic_density_in_01(2)[of "A ∩ B"] lower_asymptotic_density_intersection[of A B] unfolding assms by auto

lemma lower_asymptotic_density_one_finite_Intersection:
assumes "finite I" "⋀i. i ∈ I ⟹ lower_asymptotic_density (A i) = 1"
shows "lower_asymptotic_density (⋂i∈I. A i) = 1"
using assms by (induction rule: finite_induct, auto intro!: lower_asymptotic_density_one_intersection)

text ‹As for the upper asymptotic density, there is a modification of the intersection, akin
to the diagonal argument in this context, for which the intersection'' of sets with large
lower density still has large lower density.›

proposition lower_asymptotic_density_decseq_Inter:
assumes "⋀(n::nat). lower_asymptotic_density (A n) ≥ l" "decseq A"
shows "∃B. lower_asymptotic_density B ≥ l ∧ (∀n. ∃N. B ∩ {N..} ⊆ A n)"
proof -
define C where "C = (λn. UNIV - A n)"
have *: "upper_asymptotic_density (C n) ≤ 1 - l" for n
using assms(1)[of n] unfolding C_def lower_upper_asymptotic_density_complement[of "A n"] by auto
have **: "incseq C"
using assms(2) unfolding C_def incseq_def decseq_def by auto
obtain D where D: "upper_asymptotic_density D ≤ 1 - l" "⋀n. ∃N. C n ∩ {N..} ⊆ D"
using upper_asymptotic_density_incseq_Union[OF * **] by blast
define B where "B = UNIV - D"
have "lower_asymptotic_density B ≥ l"
using D(1) lower_upper_asymptotic_density_complement[of B] unfolding B_def by auto
moreover have "∃N. B ∩ {N..} ⊆ A n" for n
using D(2)[of n] unfolding B_def C_def by auto
ultimately show ?thesis by auto
qed

text ‹In the same way, the modified intersection of sets of density $1$ still has density one,
and is eventually contained in each of them.›

proposition lower_asymptotic_density_one_Inter:
assumes "⋀n::nat. lower_asymptotic_density (A n) = 1"
shows "∃B. lower_asymptotic_density B = 1 ∧ (∀n. ∃N. B ∩ {N..} ⊆ A n)"
proof -
define C where "C = (λn. UNIV - A n)"
have *: "upper_asymptotic_density (C n) = 0" for n
using assms(1)[of n] unfolding C_def lower_upper_asymptotic_density_complement[of "A n"] by auto
obtain D where D: "upper_asymptotic_density D = 0" "⋀n. ∃N. C n ∩ {N..} ⊆ D"
using upper_asymptotic_density_zero_Union[OF *] by force
define B where "B = UNIV - D"
have "lower_asymptotic_density B = 1"
using D(1) lower_upper_asymptotic_density_complement[of B] unfolding B_def by auto
moreover have "∃N. B ∩ {N..} ⊆ A n" for n
using D(2)[of n] unfolding B_def C_def by auto
ultimately show ?thesis by auto
qed

text ‹Sets with density $1$ play an important role in relation to Cesaro convergence of nonnegative
bounded sequences: such a sequence converges to $0$ in Cesaro average if and only if it converges
to $0$ along a set of density $1$.

The proof is not hard. Since the Cesaro average tends to $0$, then given $\epsilon>0$ the
proportion of times where $u_n < \epsilon$ tends to $1$, i.e., the set $A_\epsilon$ of such good
times has density $1$. A modified intersection (as constructed in
Proposition~\verb+lower_asymptotic_density_one_Inter+) of these times has density $1$, and
$u_n$ tends to $0$ along this set.
›

theorem cesaro_imp_density_one:
assumes "⋀n. u n ≥ (0::real)" "(λn. (∑i<n. u i)/n) ⇢ 0"
shows "∃A. lower_asymptotic_density A = 1 ∧ (λn. u n * indicator A n) ⇢ 0"
proof -
define B where "B = (λe. {n. u n ≥ e})"
text ‹$B e$ is the set of bad times where $u_n \geq e$. It has density $0$ thanks to
the assumption of Cesaro convergence to $0$.›
have A: "upper_asymptotic_density (B e) = 0" if "e > 0" for e
proof -
have *: "card (B e ∩ {..<n}) / n ≤ (1/e) * ((∑i∈{..<n}. u i)/n)" if "n ≥ 1" for n
proof -
have "e * card (B e ∩ {..<n}) = (∑i∈B e ∩ {..<n}. e)" by auto
also have "... ≤ (∑i∈B e ∩ {..<n}. u i)"
apply (rule sum_mono) unfolding B_def by auto
also have "... ≤ (∑i∈{..<n}. u i)"
apply (rule sum_mono2) using assms by auto
finally show ?thesis
using ‹e > 0› ‹n ≥ 1› by (auto simp add: divide_simps algebra_simps)
qed
have "(λn. card (B e ∩ {..<n}) / n) ⇢ 0"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. (1/e) * ((∑i∈{..<n}. u i)/n)"])
have "(λn. (1/e) * ((∑i∈{..<n}. u i)/n)) ⇢ (1/e) * 0"
by (intro tendsto_intros assms)
then show "(λn. (1/e) * ((∑i∈{..<n}. u i)/n)) ⇢ 0" by simp
show "∀⇩F n in sequentially. real (card (B e ∩ {..<n})) / real n ≤ 1 / e * (sum u {..<n} / real n)"
using * unfolding eventually_sequentially by auto
qed (auto)
then show ?thesis
by (rule upper_asymptotic_density_lim)
qed
define C where "C = (λn::nat. UNIV - B (((1::real)/2)^n))"
have "lower_asymptotic_density (C n) = 1" for n
unfolding C_def lower_upper_asymptotic_density_complement by (auto intro!: A)
then obtain A where A: "lower_asymptotic_density A = 1" "⋀n. ∃N. A ∩ {N..} ⊆ C n"
using lower_asymptotic_density_one_Inter by blast
have E: "eventually (λn. u n * indicator A n < e) sequentially" if "e > 0" for e
proof -
have "eventually (λn. ((1::real)/2)^n < e) sequentially"
by (rule order_tendstoD[OF _ ‹e > 0›], intro tendsto_intros, auto)
then obtain n where n: "((1::real)/2)^n < e"
unfolding eventually_sequentially by auto
obtain N where N: "A ∩ {N..} ⊆ C n"
using A(2) by blast
have "u k * indicator A k < e" if "k ≥ N" for k
proof (cases "k ∈ A")
case True
then have "k ∈ C n" using N that by auto
then have "u k < ((1::real)/2)^n"
unfolding C_def B_def by auto
then have "u k < e"
using n by auto
then show ?thesis
unfolding indicator_def using True by auto
next
case False
then show ?thesis
unfolding indicator_def using ‹e > 0› by auto
qed
then show ?thesis
unfolding eventually_sequentially by auto
qed
have "(λn. u n * indicator A n) ⇢ 0"
apply (rule order_tendstoI[OF _ E])
unfolding indicator_def using ‹⋀n. u n ≥ 0› by (simp add: less_le_trans)
then show ?thesis
using ‹lower_asymptotic_density A = 1› by auto
qed

text ‹The proof of the reverse implication is more direct: in the Cesaro sum, just bound the
elements in $A$ by a small $\epsilon$, and the other ones by a uniform bound, to get a bound
which is $o(n)$.›

theorem density_one_imp_cesaro:
assumes "⋀n. u n ≥ (0::real)" "⋀n. u n ≤ C"
"lower_asymptotic_density A = 1"
"(λn. u n * indicator A n) ⇢ 0"
shows "(λn. (∑i<n. u i)/n) ⇢ 0"
proof (rule order_tendstoI)
fix e::real assume "e < 0"
have "(∑i<n. u i)/n ≥ 0" for n
using assms(1) by (simp add: sum_nonneg divide_simps)
then have "(∑i<n. u i)/n > e" for n
using ‹e < 0› less_le_trans by auto
then show "eventually (λn. (∑i<n. u i)/n > e) sequentially"
unfolding eventually_sequentially by auto
next
fix e::real assume "e > 0"
have "C ≥ 0" using ‹u 0 ≥ 0› ‹u 0 ≤ C› by auto
have "eventually (λn. u n * indicator A n < e/4) sequentially"
using order_tendstoD(2)[OF assms(4), of "e/4"] ‹e>0› by auto
then obtain N where N: "⋀k. k ≥ N ⟹ u k * indicator A k < e/4"
unfolding eventually_sequentially by auto
define B where "B = UNIV - A"
have *: "upper_asymptotic_density B = 0"
using assms unfolding B_def lower_upper_asymptotic_density_complement by auto
have "eventually (λn. card(B ∩ {..<n}) < (e/(4 * (C+1))) * n) sequentially"
apply (rule upper_asymptotic_densityD) using ‹e > 0› ‹C ≥ 0› * by auto
then obtain M where M: "⋀n. n ≥ M ⟹ card(B ∩ {..<n}) < (e/(4 * (C+1))) * n"
unfolding eventually_sequentially by auto

obtain P::nat where P: "P ≥ 4 * N * C/e"
using real_arch_simple by auto
define Q where "Q = N + M + 1 + P"

have "(∑i<n. u i)/n < e" if "n ≥ Q" for n
proof -
have n: "n ≥ N" "n ≥ M" "n ≥ P" "n ≥ 1"
using ‹n ≥ Q› unfolding Q_def by auto
then have n2: "n ≥ 4 * N * C/e" using P by auto
have "(∑i<n. u i) ≤ (∑i∈{..<N} ∪ ({N..<n} ∩ A) ∪ ({N..<n} - A). u i)"
by (rule sum_mono2, auto simp add: assms)
also have "... = (∑i∈{..<N}. u i) + (∑i∈{N..<n} ∩ A. u i) + (∑i∈{N..<n} - A. u i)"
by (subst sum.union_disjoint, auto)+
also have "... = (∑i∈{..<N}. u i) + (∑i∈{N..<n} ∩ A. u i * indicator A i) + (∑i∈{N..<n} - A. u i)"
unfolding indicator_def by auto
also have "... ≤ (∑i∈{..<N}. u i) + (∑i∈{N..<n}. u i * indicator A i) + (∑i∈ B ∩ {..<n}. u i)"
apply (intro add_mono sum_mono2) unfolding B_def using assms by auto
also have "... ≤ (∑i∈{..<N}. C) + (∑i∈{N..<n}. e/4) + (∑i∈B ∩ {..<n}. C)"
apply (intro add_mono sum_mono) using assms less_imp_le[OF N] by auto
also have "... = N * C + (n-N) * e/4 + card(B ∩ {..<n}) * C"
by auto
also have "... ≤ n * e/4 + n * e/4 + (e/(4 * (C+1))) * n * C"
using n2 ‹e > 0› mult_right_mono[OF less_imp_le[OF M[OF ‹n ≥ M›]] ‹C ≥ 0›] by (auto simp add: divide_simps)
also have "... ≤ n * e * 3/4"
using ‹C ≥ 0› ‹e > 0› by (simp add: divide_simps algebra_simps)
also have "... < n * e"
using ‹n ≥ 1› ‹e > 0› by auto
finally show ?thesis
using ‹n ≥ 1› by (simp add: divide_simps algebra_simps)
qed
then show "eventually (λn. (∑i<n. u i)/n < e) sequentially"
unfolding eventually_sequentially by auto
qed

end (*of Asymptotic_Density.thy*)


# Theory Measure_Preserving_Transformations

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

section ‹Measure preserving or quasi-preserving maps›

theory Measure_Preserving_Transformations
imports SG_Library_Complement
begin

text ‹Ergodic theory in general is the study of the properties of measure preserving or
quasi-preserving dynamical systems. In this section, we introduce the basic definitions
in this respect.›

subsection ‹The different classes of transformations›

definition quasi_measure_preserving::"'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) set"
where "quasi_measure_preserving M N
= {f ∈ measurable M N. ∀ A ∈ sets N. (f - A ∩ space M ∈ null_sets M) = (A ∈ null_sets N)}"

lemma quasi_measure_preservingI [intro]:
assumes "f ∈ measurable M N"
"⋀A. A ∈ sets N ⟹ (f - A ∩ space M ∈ null_sets M) = (A ∈ null_sets N)"
shows "f ∈ quasi_measure_preserving M N"
using assms unfolding quasi_measure_preserving_def by auto

lemma quasi_measure_preservingE:
assumes "f ∈ quasi_measure_preserving M N"
shows "f ∈ measurable M N"
"⋀A. A ∈ sets N ⟹ (f - A ∩ space M ∈ null_sets M) = (A ∈ null_sets N)"
using assms unfolding quasi_measure_preserving_def by auto

lemma id_quasi_measure_preserving:
"(λx. x) ∈ quasi_measure_preserving M M"
unfolding quasi_measure_preserving_def by auto

lemma quasi_measure_preserving_composition:
assumes "f ∈ quasi_measure_preserving M N"
"g ∈ quasi_measure_preserving N P"
shows "(λx. g(f x)) ∈ quasi_measure_preserving M P"
proof (rule quasi_measure_preservingI)
have f_meas [measurable]: "f ∈ measurable M N" by (rule quasi_measure_preservingE(1)[OF assms(1)])
have g_meas [measurable]: "g ∈ measurable N P" by (rule quasi_measure_preservingE(1)[OF assms(2)])
then show [measurable]: "(λx. g (f x)) ∈ measurable M P" by auto

fix C assume [measurable]: "C ∈ sets P"
define B where "B = g-C ∩ space N"
have [measurable]: "B ∈ sets N" unfolding B_def by simp
have *: "B ∈ null_sets N ⟷ C ∈ null_sets P"
unfolding B_def using quasi_measure_preservingE(2)[OF assms(2)] by simp

define A where "A = f-B ∩ space M"
have [measurable]: "A ∈ sets M" unfolding A_def by simp
have "A ∈ null_sets M ⟷ B ∈ null_sets N"
unfolding A_def using quasi_measure_preservingE(2)[OF assms(1)] by simp

then have "A ∈ null_sets M ⟷ C ∈ null_sets P" using * by simp
moreover have "A = (λx. g (f x)) - C ∩ space M"
by (auto simp add: A_def B_def) (meson f_meas measurable_space)
ultimately show "((λx. g (f x)) - C ∩ space M ∈ null_sets M) ⟷ C ∈ null_sets P" by simp
qed

lemma quasi_measure_preserving_comp:
assumes "f ∈ quasi_measure_preserving M N"
"g ∈ quasi_measure_preserving N P"
shows "g o f ∈ quasi_measure_preserving M P"
unfolding comp_def using assms quasi_measure_preserving_composition by blast

lemma quasi_measure_preserving_AE:
assumes "f ∈ quasi_measure_preserving M N"
"AE x in N. P x"
shows "AE x in M. P (f x)"
proof -
obtain A where "⋀x. x ∈ space N - A ⟹ P x" "A ∈ null_sets N"
using AE_E3[OF assms(2)] by blast
define B where "B = f-A ∩ space M"
have "B ∈ null_sets M"
unfolding B_def using quasi_measure_preservingE(2)[OF assms(1)] ‹A ∈ null_sets N› by auto
moreover have "x ∈ space M - B ⟹ P (f x)" for x
using ‹⋀x. x ∈ space N - A ⟹ P x› quasi_measure_preservingE(1)[OF assms(1)]
unfolding B_def by (metis (no_types, lifting) Diff_iff IntI measurable_space vimage_eq)
ultimately show ?thesis using AE_not_in AE_space by force
qed

lemma quasi_measure_preserving_AE':
assumes "f ∈ quasi_measure_preserving M N"
"AE x in M. P (f x)"
"{x ∈ space N. P x} ∈ sets N"
shows "AE x in N. P x"
proof -
have [measurable]: "f ∈ measurable M N" using quasi_measure_preservingE(1)[OF assms(1)] by simp
define U where "U = {x ∈ space N. ¬(P x)}"
have [measurable]: "U ∈ sets N" unfolding U_def using assms(3) by auto
have "f-U ∩ space M = {x ∈ space M. ¬(P (f x))}"
unfolding U_def using ‹f ∈ measurable M N› by (auto, meson measurable_space)
also have "... ∈ null_sets M"
apply (subst AE_iff_null[symmetric]) using assms by auto
finally have "U ∈ null_sets N"
using quasi_measure_preservingE(2)[OF assms(1) ‹U ∈ sets N›] by auto
then show ?thesis unfolding U_def using AE_iff_null by blast
qed

text ‹The push-forward under a quasi-measure preserving map $f$ of a measure absolutely
continuous with respect to $M$ is absolutely continuous with respect to $N$.›
lemma quasi_measure_preserving_absolutely_continuous:
assumes "f ∈ quasi_measure_preserving M N"
"u ∈ borel_measurable M"
shows "absolutely_continuous N (distr (density M u) N f)"
proof -
have [measurable]: "f ∈ measurable M N" using quasi_measure_preservingE[OF assms(1)] by auto
have "S ∈ null_sets (distr (density M u) N f)" if [measurable]: "S ∈ null_sets N" for S
proof -
have [measurable]: "S ∈ sets N" using null_setsD2[OF that] by auto
have *: "AE x in N. x ∉ S"
by (metis AE_not_in that)
have "AE x in M. f x ∉ S"
by (rule quasi_measure_preserving_AE[OF _ *], simp add: assms)
then have *: "AE x in M. indicator S (f x) * u x = 0"
by force

have "emeasure (distr (density M u) N f) S = (∫⇧+x. indicator S x ∂(distr (density M u) N f))"
by auto
also have "... = (∫⇧+x. indicator S (f x) ∂(density M u))"
by (rule nn_integral_distr, auto)
also have "... = (∫⇧+x. indicator S (f x) * u x ∂M)"
by (rule nn_integral_densityR[symmetric], auto simp add: assms)
also have "... = (∫⇧+x. 0 ∂M)"
using * by (rule nn_integral_cong_AE)
finally have "emeasure (distr (density M u) N f) S = 0" by auto
then show ?thesis by auto
qed
then show ?thesis unfolding absolutely_continuous_def by auto
qed

definition measure_preserving::"'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) set"
where "measure_preserving M N
= {f ∈ measurable M N. (∀ A ∈ sets N. emeasure M (f-A ∩ space M) = emeasure N A)}"

lemma measure_preservingE:
assumes "f ∈ measure_preserving M N"
shows "f ∈ measurable M N"
"⋀A. A ∈ sets N ⟹ emeasure M (f-A ∩ space M) = emeasure N A"
using assms unfolding measure_preserving_def by auto

lemma measure_preservingI [intro]:
assumes "f ∈ measurable M N"
"⋀A. A ∈ sets N ⟹ emeasure M (f-A ∩ space M) = emeasure N A"
shows "f ∈ measure_preserving M N"
using assms unfolding measure_preserving_def by auto

lemma measure_preserving_distr:
assumes "f ∈ measure_preserving M N"
shows "distr M N f = N"
proof -
let ?N2 = "distr M N f"
have "sets ?N2 = sets N" by simp
moreover have "emeasure ?N2 A = emeasure N A" if "A ∈ sets N" for A
proof -
have "emeasure ?N2 A = emeasure M (f-A ∩ space M)"
using ‹A ∈ sets N› assms emeasure_distr measure_preservingE(1)[OF assms] by blast
then show "emeasure ?N2 A = emeasure N A"
using ‹A ∈ sets N› measure_preservingE(2)[OF assms] by auto
qed
ultimately show ?thesis by (metis measure_eqI)
qed

lemma measure_preserving_distr':
assumes "f ∈ measurable M N"
shows "f ∈ measure_preserving M (distr M N f)"
proof (rule measure_preservingI)
show "f ∈ measurable M (distr M N f)" using assms(1) by auto
show "emeasure M (f-A ∩ space M) = emeasure (distr M N f) A" if "A ∈ sets (distr M N f)" for A
using that emeasure_distr[OF assms] by auto
qed

lemma measure_preserving_preserves_nn_integral:
assumes "T ∈ measure_preserving M N"
"f ∈ borel_measurable N"
shows "(∫⇧+x. f x ∂N) = (∫⇧+x. f (T x) ∂M)"
proof -
have "(∫⇧+x. f (T x) ∂M) = (∫⇧+y. f y ∂distr M N T)"
using assms nn_integral_distr[of T M N f, OF measure_preservingE(1)[OF assms(1)]] by simp
also have "... = (∫⇧+y. f y ∂N)"
using measure_preserving_distr[OF assms(1)] by simp
finally show ?thesis by simp
qed

lemma measure_preserving_preserves_integral:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "T ∈ measure_preserving M N"
and [measurable]: "integrable N f"
shows "integrable M (λx. f(T x))" "(∫x. f x ∂N) = (∫x. f (T x) ∂M)"
proof -
have a [measurable]: "T ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)])
have b [measurable]: "f ∈ borel_measurable N" by simp
have "distr M N T = N" using measure_preserving_distr[OF assms(1)] by simp
then have "integrable (distr M N T) f" using assms(2) by simp
then show "integrable M (λx. f(T x))" using integrable_distr_eq[OF a b] by simp

have "(∫x. f (T x) ∂M) = (∫y. f y ∂distr M N T)" using integral_distr[OF a b] by simp
then show "(∫x. f x ∂N) = (∫x. f (T x) ∂M)" using ‹distr M N T = N› by simp
qed

lemma measure_preserving_preserves_integral':
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "T ∈ measure_preserving M N"
and [measurable]: "integrable M (λx. f (T x))" "f ∈ borel_measurable N"
shows "integrable N f" "(∫x. f x ∂N) = (∫x. f (T x) ∂M)"
proof -
have a [measurable]: "T ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)])
have "integrable M (λx. f(T x))" using assms(2) unfolding comp_def by auto
then have "integrable (distr M N T) f"
using integrable_distr_eq[OF a assms(3)] by simp
then show *: "integrable N f" using measure_preserving_distr[OF assms(1)] by simp

then show "(∫x. f x ∂N) = (∫x. f (T x) ∂M)"
using measure_preserving_preserves_integral[OF assms(1) *] by simp
qed

lemma id_measure_preserving:
"(λx. x) ∈ measure_preserving M M"
unfolding measure_preserving_def by auto

lemma measure_preserving_is_quasi_measure_preserving:
assumes "f ∈ measure_preserving M N"
shows "f ∈ quasi_measure_preserving M N"
using assms unfolding measure_preserving_def quasi_measure_preserving_def apply auto
by (metis null_setsD1 null_setsI, metis measurable_sets null_setsD1 null_setsI)

lemma measure_preserving_composition:
assumes "f ∈ measure_preserving M N"
"g ∈ measure_preserving N P"
shows "(λx. g(f x)) ∈ measure_preserving M P"
proof (rule measure_preservingI)
have f [measurable]: "f ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)])
have g [measurable]: "g ∈ measurable N P" by (rule measure_preservingE(1)[OF assms(2)])
show [measurable]: "(λx. g (f x)) ∈ measurable M P" by auto

fix C assume [measurable]: "C ∈ sets P"
define B where "B = g-C ∩ space N"
have [measurable]: "B ∈ sets N" unfolding B_def by simp
have *: "emeasure N B = emeasure P C"
unfolding B_def using measure_preservingE(2)[OF assms(2)] by simp

define A where "A = f-B ∩ space M"
have [measurable]: "A ∈ sets M" unfolding A_def by simp
have "emeasure M A = emeasure N B"
unfolding A_def using measure_preservingE(2)[OF assms(1)] by simp

then have "emeasure M A = emeasure P C" using * by simp
moreover have "A = (λx. g(f x))-C ∩ space M"
by (auto simp add: A_def B_def) (meson f measurable_space)
ultimately show "emeasure M ((λx. g(f x))-C ∩ space M) = emeasure P C" by simp
qed

lemma measure_preserving_comp:
assumes "f ∈ measure_preserving M N"
"g ∈ measure_preserving N P"
shows "g o f ∈ measure_preserving M P"
unfolding o_def using measure_preserving_composition assms by blast

lemma measure_preserving_total_measure:
assumes "f ∈ measure_preserving M N"
shows "emeasure M (space M) = emeasure N (space N)"
proof -
have "f ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)])
then have "f-(space N) ∩ space M = space M" by (meson Int_absorb1 measurable_space subsetI vimageI)
then show "emeasure M (space M) = emeasure N (space N)"
by (metis (mono_tags, lifting) measure_preservingE(2)[OF assms(1)] sets.top)
qed

lemma measure_preserving_finite_measure:
assumes "f ∈ measure_preserving M N"
shows "finite_measure M ⟷ finite_measure N"
using measure_preserving_total_measure[OF assms]
by (metis finite_measure.emeasure_finite finite_measureI infinity_ennreal_def)

lemma measure_preserving_prob_space:
assumes "f ∈ measure_preserving M N"
shows "prob_space M ⟷ prob_space N"
using measure_preserving_total_measure[OF assms] by (metis prob_space.emeasure_space_1 prob_spaceI)

locale qmpt = sigma_finite_measure +
fixes T
assumes Tqm: "T ∈ quasi_measure_preserving M M"

locale mpt = qmpt +
assumes Tm: "T ∈ measure_preserving M M"

locale fmpt = mpt + finite_measure

locale pmpt = fmpt + prob_space

lemma qmpt_I:
assumes "sigma_finite_measure M"
"T ∈ measurable M M"
"⋀A. A ∈ sets M ⟹ ((T-A ∩ space M) ∈ null_sets M) ⟷ (A ∈ null_sets M)"
shows "qmpt M T"
unfolding qmpt_def qmpt_axioms_def quasi_measure_preserving_def

lemma mpt_I:
assumes "sigma_finite_measure M"
"T ∈ measurable M M"
"⋀A. A ∈ sets M ⟹ emeasure M (T-A ∩ space M) = emeasure M A"
shows "mpt M T"
proof -
have *: "T ∈ measure_preserving M M"
by (rule measure_preservingI[OF assms(2) assms(3)])
then have **: "T ∈ quasi_measure_preserving M M"
using measure_preserving_is_quasi_measure_preserving by auto
show "mpt M T"
unfolding mpt_def qmpt_def qmpt_axioms_def mpt_axioms_def using * ** assms(1) by auto
qed

lemma fmpt_I:
assumes "finite_measure M"
"T ∈ measurable M M"
"⋀A. A ∈ sets M ⟹ emeasure M (T-A ∩ space M) = emeasure M A"
shows "fmpt M T"
proof -
have *: "T`