--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Mar 04 21:58:53 2024 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Mar 05 14:32:50 2024 +0000
@@ -4,7 +4,7 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>Elementary Metric Spaces\<close>
+chapter \<open>Elementary Metric Spaces\<close>
theory Elementary_Metric_Spaces
imports
@@ -12,7 +12,7 @@
Metric_Arith
begin
-subsection \<open>Open and closed balls\<close>
+section \<open>Open and closed balls\<close>
definition\<^marker>\<open>tag important\<close> ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "ball x e = {y. dist x y < e}"
@@ -316,7 +316,7 @@
by blast
qed
-subsection \<open>Limit Points\<close>
+section \<open>Limit Points\<close>
lemma islimpt_approachable:
fixes x :: "'a::metric_space"
@@ -349,7 +349,7 @@
by (metis open_ball ball_subset_cball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
-subsection \<open>Perfect Metric Spaces\<close>
+section \<open>Perfect Metric Spaces\<close>
lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
for x :: "'a::{perfect_space,metric_space}"
@@ -362,7 +362,7 @@
not_open_singleton subset_singleton_iff)
-subsection \<open>Finite and discrete\<close>
+section \<open>Finite and discrete\<close>
lemma finite_ball_include:
fixes a :: "'a::metric_space"
@@ -427,7 +427,7 @@
qed
-subsection \<open>Interior\<close>
+section \<open>Interior\<close>
lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
using open_contains_ball_eq [where S="interior S"]
@@ -441,7 +441,7 @@
by (meson mem_interior mem_interior_cball)
-subsection \<open>Frontier\<close>
+section \<open>Frontier\<close>
lemma frontier_straddle:
fixes a :: "'a::metric_space"
@@ -450,7 +450,7 @@
by (auto simp: mem_interior subset_eq ball_def)
-subsection \<open>Limits\<close>
+section \<open>Limits\<close>
proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
by (auto simp: tendsto_iff trivial_limit_eq)
@@ -553,7 +553,7 @@
using assms by (fast intro: tendsto_le tendsto_intros)
-subsection \<open>Continuity\<close>
+section \<open>Continuity\<close>
text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
@@ -656,7 +656,7 @@
unfolding continuous_within by (force intro: Lim_transform_within)
-subsection \<open>Closure and Limit Characterization\<close>
+section \<open>Closure and Limit Characterization\<close>
lemma closure_approachable:
fixes S :: "'a::metric_space set"
@@ -751,7 +751,7 @@
qed
-subsection \<open>Boundedness\<close>
+section \<open>Boundedness\<close>
(* FIXME: This has to be unified with BSEQ!! *)
definition\<^marker>\<open>tag important\<close> (in metric_space) bounded :: "'a set \<Rightarrow> bool"
@@ -882,7 +882,7 @@
qed
-subsection \<open>Compactness\<close>
+section \<open>Compactness\<close>
lemma compact_imp_bounded:
assumes "compact U"
@@ -1097,7 +1097,7 @@
using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis
-subsection \<open>Banach fixed point theorem\<close>
+section \<open>Banach fixed point theorem\<close>
theorem banach_fix:\<comment> \<open>TODO: rename to \<open>Banach_fix\<close>\<close>
assumes s: "complete s" "s \<noteq> {}"
@@ -1245,7 +1245,7 @@
qed
-subsection \<open>Edelstein fixed point theorem\<close>
+section \<open>Edelstein fixed point theorem\<close>
theorem Edelstein_fix:
fixes S :: "'a::metric_space set"
@@ -1286,7 +1286,7 @@
using \<open>a \<in> S\<close> by blast
qed
-subsection \<open>The diameter of a set\<close>
+section \<open>The diameter of a set\<close>
definition\<^marker>\<open>tag important\<close> diameter :: "'a::metric_space set \<Rightarrow> real" where
"diameter S = (if S = {} then 0 else SUP (x,y)\<in>S\<times>S. dist x y)"
@@ -1485,7 +1485,7 @@
qed
-subsection \<open>Metric spaces with the Heine-Borel property\<close>
+section \<open>Metric spaces with the Heine-Borel property\<close>
text \<open>
A metric space (or topological vector space) is said to have the
@@ -1643,7 +1643,7 @@
qed
-subsection \<open>Completeness\<close>
+section \<open>Completeness\<close>
proposition (in metric_space) completeI:
assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
@@ -1869,7 +1869,7 @@
using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
by auto
-subsection \<open>Cauchy continuity\<close>
+section \<open>Cauchy continuity\<close>
definition Cauchy_continuous_on where
"Cauchy_continuous_on \<equiv> \<lambda>S f. \<forall>\<sigma>. Cauchy \<sigma> \<longrightarrow> range \<sigma> \<subseteq> S \<longrightarrow> Cauchy (f \<circ> \<sigma>)"
@@ -1937,7 +1937,7 @@
qed
-subsection\<^marker>\<open>tag unimportant\<close>\<open> Finite intersection property\<close>
+section\<^marker>\<open>tag unimportant\<close>\<open> Finite intersection property\<close>
text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
@@ -1985,7 +1985,7 @@
by (simp add: closed_limpt compact_eq_bounded_closed convergent_imp_bounded islimpt_insert sequence_unique_limpt)
-subsection \<open>Properties of Balls and Spheres\<close>
+section \<open>Properties of Balls and Spheres\<close>
lemma compact_cball[simp]:
fixes x :: "'a::heine_borel"
@@ -2029,7 +2029,7 @@
qed
-subsection \<open>Distance from a Set\<close>
+section \<open>Distance from a Set\<close>
lemma distance_attains_sup:
assumes "compact s" "s \<noteq> {}"
@@ -2066,7 +2066,7 @@
qed
-subsection \<open>Infimum Distance\<close>
+section \<open>Infimum Distance\<close>
definition\<^marker>\<open>tag important\<close> "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
@@ -2299,7 +2299,7 @@
qed
-subsection \<open>Separation between Points and Sets\<close>
+section \<open>Separation between Points and Sets\<close>
proposition separate_point_closed:
fixes S :: "'a::heine_borel set"
@@ -2362,7 +2362,7 @@
qed
-subsection \<open>Uniform Continuity\<close>
+section \<open>Uniform Continuity\<close>
lemma uniformly_continuous_onE:
assumes "uniformly_continuous_on s f" "0 < e"
@@ -2429,7 +2429,7 @@
qed
-subsection \<open>Continuity on a Compact Domain Implies Uniform Continuity\<close>
+section \<open>Continuity on a Compact Domain Implies Uniform Continuity\<close>
text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
@@ -2521,7 +2521,7 @@
by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
-subsection\<^marker>\<open>tag unimportant\<close>\<open> Theorems relating continuity and uniform continuity to closures\<close>
+section\<^marker>\<open>tag unimportant\<close>\<open> Theorems relating continuity and uniform continuity to closures\<close>
lemma continuous_on_closure:
"continuous_on (closure S) f \<longleftrightarrow>
@@ -2765,7 +2765,7 @@
by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
-subsection \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>
+section \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>
lemma openin_contains_ball:
"openin (top_of_set T) S \<longleftrightarrow>
@@ -2796,7 +2796,7 @@
qed
-subsection \<open>Closed Nest\<close>
+section \<open>Closed Nest\<close>
text \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
@@ -2908,7 +2908,7 @@
then show ?thesis ..
qed
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Making a continuous function avoid some value in a neighbourhood\<close>
+section\<^marker>\<open>tag unimportant\<close> \<open>Making a continuous function avoid some value in a neighbourhood\<close>
lemma continuous_within_avoid:
fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
@@ -2958,7 +2958,7 @@
using continuous_at_avoid[of x f a] assms(4)
by auto
-subsection \<open>Consequences for Real Numbers\<close>
+section \<open>Consequences for Real Numbers\<close>
lemma closed_contains_Inf:
fixes S :: "real set"
@@ -3093,7 +3093,7 @@
by auto
-subsection\<open>The infimum of the distance between two sets\<close>
+section\<open>The infimum of the distance between two sets\<close>
definition\<^marker>\<open>tag important\<close> setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
"setdist s t \<equiv>
@@ -3269,4 +3269,72 @@
qed (fact \<open>y \<in> B\<close>)
qed
+
+section \<open>Diameter Lemma\<close>
+
+text \<open>taken from the AFP entry Martingales, by Ata Keskin, TU München\<close>
+
+lemma diameter_comp_strict_mono:
+ fixes s :: "nat \<Rightarrow> 'a :: metric_space"
+ assumes "strict_mono r" "bounded {s i |i. r n \<le> i}"
+ shows "diameter {s (r i) | i. n \<le> i} \<le> diameter {s i | i. r n \<le> i}"
+proof (rule diameter_subset)
+ show "{s (r i) | i. n \<le> i} \<subseteq> {s i | i. r n \<le> i}" using assms(1) monotoneD strict_mono_mono by fastforce
+qed (intro assms(2))
+
+lemma diameter_bounded_bound':
+ fixes S :: "'a :: metric_space set"
+ assumes S: "bdd_above (case_prod dist ` (S\<times>S))" and "x \<in> S" "y \<in> S"
+ shows "dist x y \<le> diameter S"
+proof -
+ have "(x,y) \<in> S\<times>S" using assms by auto
+ then have "dist x y \<le> (SUP (x,y)\<in>S\<times>S. dist x y)"
+ by (metis S cSUP_upper case_prod_conv)
+ with \<open>x \<in> S\<close> show ?thesis by (auto simp: diameter_def)
+qed
+
+lemma bounded_imp_dist_bounded:
+ assumes "bounded (range s)"
+ shows "bounded ((\<lambda>(i, j). dist (s i) (s j)) ` ({n..} \<times> {n..}))"
+ using bounded_dist_comp[OF bounded_fst bounded_snd, OF bounded_Times(1,1)[OF assms(1,1)]] by (rule bounded_subset, force)
+
+text \<open>A sequence is Cauchy, if and only if it is bounded and its diameter tends to zero. The diameter is well-defined only if the sequence is bounded.\<close>
+lemma cauchy_iff_diameter_tends_to_zero_and_bounded:
+ fixes s :: "nat \<Rightarrow> 'a :: metric_space"
+ shows "Cauchy s \<longleftrightarrow> ((\<lambda>n. diameter {s i | i. i \<ge> n}) \<longlonglongrightarrow> 0 \<and> bounded (range s))"
+proof -
+ have "{s i |i. N \<le> i} \<noteq> {}" for N by blast
+ hence diameter_SUP: "diameter {s i |i. N \<le> i} = (SUP (i, j) \<in> {N..} \<times> {N..}. dist (s i) (s j))" for N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup])
+ show ?thesis
+ proof (intro iffI)
+ assume asm: "Cauchy s"
+ have "\<exists>N. \<forall>n\<ge>N. norm (diameter {s i |i. n \<le> i}) < e" if e_pos: "e > 0" for e
+ proof -
+ obtain N where dist_less: "dist (s n) (s m) < (1/2) * e" if "n \<ge> N" "m \<ge> N" for n m using asm e_pos by (metis Cauchy_def mult_pos_pos zero_less_divide_iff zero_less_numeral zero_less_one)
+ {
+ fix r assume "r \<ge> N"
+ hence "dist (s n) (s m) < (1/2) * e" if "n \<ge> r" "m \<ge> r" for n m using dist_less that by simp
+ hence "(SUP (i, j) \<in> {r..} \<times> {r..}. dist (s i) (s j)) \<le> (1/2) * e" by (intro cSup_least) fastforce+
+ also have "... < e" using e_pos by simp
+ finally have "diameter {s i |i. r \<le> i} < e" using diameter_SUP by presburger
+ }
+ moreover have "diameter {s i |i. r \<le> i} \<ge> 0" for r unfolding diameter_SUP using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above, OF asm] by (intro cSup_upper2, auto)
+ ultimately show ?thesis by auto
+ qed
+ thus "(\<lambda>n. diameter {s i |i. n \<le> i}) \<longlonglongrightarrow> 0 \<and> bounded (range s)" using cauchy_imp_bounded[OF asm] by (simp add: LIMSEQ_iff)
+ next
+ assume asm: "(\<lambda>n. diameter {s i |i. n \<le> i}) \<longlonglongrightarrow> 0 \<and> bounded (range s)"
+ have "\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. dist (s n) (s m) < e" if e_pos: "e > 0" for e
+ proof -
+ obtain N where diam_less: "diameter {s i |i. r \<le> i} < e" if "r \<ge> N" for r using LIMSEQ_D asm(1) e_pos by fastforce
+ {
+ fix n m assume "n \<ge> N" "m \<ge> N"
+ hence "dist (s n) (s m) < e" using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above], OF _ diam_less[unfolded diameter_SUP]] asm by auto
+ }
+ thus ?thesis by blast
+ qed
+ then show "Cauchy s" by (simp add: Cauchy_def)
+ qed
+qed
+
end
--- a/src/HOL/Analysis/Set_Integral.thy Mon Mar 04 21:58:53 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Tue Mar 05 14:32:50 2024 +0000
@@ -7,13 +7,13 @@
TODO: keep all these? Need unicode translations as well.
*)
+chapter \<open>Integrals over a Set\<close>
+
theory Set_Integral
imports Radon_Nikodym
begin
-(*
- Notation
-*)
+section \<open>Notation\<close>
definition\<^marker>\<open>tag important\<close> "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
@@ -45,9 +45,7 @@
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
("(3LBINT _:_./ _)" [0,0,10] 10)
-(*
- Basic properties
-*)
+section \<open>Basic properties\<close>
(*
lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
@@ -149,6 +147,13 @@
(* TODO: integral_cmul_indicator should be named set_integral_const *)
(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
+lemma set_integral_scaleR_left:
+ assumes "A \<in> sets M" "c \<noteq> 0 \<Longrightarrow> integrable M f"
+ shows "(LINT t:A|M. f t *\<^sub>R c) = (LINT t:A|M. f t) *\<^sub>R c"
+ unfolding set_lebesgue_integral_def
+ using integrable_mult_indicator[OF assms]
+ by (subst integral_scaleR_left[symmetric], auto)
+
lemma set_integral_scaleR_right [simp]: "(LINT t:A|M. a *\<^sub>R f t) = a *\<^sub>R (LINT t:A|M. f t)"
unfolding set_lebesgue_integral_def
by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
@@ -444,7 +449,7 @@
using intgbl set_integrable_def by blast
qed
-(* Proof from Royden Real Analysis, p. 91. *)
+text \<open>Proof from Royden, \emph{Real Analysis}, p. 91.\<close>
lemma lebesgue_integral_countable_add:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
@@ -489,11 +494,7 @@
by simp
qed
show "LINT x|M. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
- apply (rule Bochner_Integration.integral_cong[OF refl])
- apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
- using sums_unique[OF indicator_sums[OF disj]]
- apply auto
- done
+ by (metis (no_types, lifting) integral_cong sums sums_unique)
qed
lemma set_integral_cont_up:
@@ -562,6 +563,8 @@
qed
+section \<open>Complex integrals\<close>
+
abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
"complex_integrable M f \<equiv> integrable M f"
@@ -610,11 +613,11 @@
"complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
syntax
-"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4CLINT _:_|_. _)" [0,0,0,10] 10)
+ "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+ ("(4CLINT _:_|_. _)" [0,0,0,10] 10)
translations
-"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
+ "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
lemma set_measurable_continuous_on_ivl:
assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
@@ -622,6 +625,7 @@
unfolding set_borel_measurable_def
by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
+section \<open>NN Set Integrals\<close>
text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
notations in this file, they are more in line with sum, and more readable he thinks.\<close>
@@ -656,7 +660,7 @@
by (auto split: split_indicator)
then have "(\<integral>\<^sup>+x. f x * indicator (B \<union> C) x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator B x + f x * indicator C x \<partial>M)"
by simp
- also have "... = (\<integral>\<^sup>+x. f x * indicator B x \<partial>M) + (\<integral>\<^sup>+x. f x * indicator C x \<partial>M)"
+ also have "\<dots> = (\<integral>\<^sup>+x. f x * indicator B x \<partial>M) + (\<integral>\<^sup>+x. f x * indicator C x \<partial>M)"
by (rule nn_integral_add) (auto simp add: assms mes pos)
finally show ?thesis by simp
qed
@@ -719,7 +723,7 @@
proof -
have "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x. (f x * indicator A x + g x * indicator A x) \<partial>M)"
by (auto simp add: indicator_def intro!: nn_integral_cong)
- also have "... = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + (\<integral>\<^sup>+x. g x * indicator A x \<partial>M)"
+ also have "\<dots> = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + (\<integral>\<^sup>+x. g x * indicator A x \<partial>M)"
apply (rule nn_integral_add) using assms(1) assms(2) by auto
finally show ?thesis by simp
qed
@@ -750,9 +754,9 @@
proof -
have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+x. f (g x) \<partial>count_space A)"
by (auto simp add: nn_integral_count_space_indicator[symmetric])
- also have "... = (\<integral>\<^sup>+y. f y \<partial>count_space (g`A))"
+ also have "\<dots> = (\<integral>\<^sup>+y. f y \<partial>count_space (g`A))"
by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
- also have "... = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
+ also have "\<dots> = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
by (auto simp add: nn_integral_count_space_indicator[symmetric])
finally show ?thesis by simp
qed
@@ -855,6 +859,8 @@
then show ?thesis using * by auto
qed
+section \<open>Scheffé's lemma\<close>
+
text \<open>The next lemma shows that \<open>L\<^sup>1\<close> convergence of a sequence of functions follows from almost
everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
@@ -897,7 +903,7 @@
then have "AE x in M. liminf (\<lambda>n. ennreal(G n x)) = ennreal(2 * norm(f x))" using assms(3) by auto
then have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M) = (\<integral>\<^sup>+ x. 2 * ennreal(norm(f x)) \<partial>M)"
by (simp add: nn_integral_cong_AE ennreal_mult)
- also have "... = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)" by (rule nn_integral_cmult) auto
+ also have "\<dots> = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)" by (rule nn_integral_cmult) auto
finally have int_liminf: "(\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M) = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
by simp
@@ -906,11 +912,11 @@
then have "limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M)) =
limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
by simp
- also have "... = (\<integral>\<^sup>+x. norm(f x) \<partial>M) + limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
+ also have "\<dots> = (\<integral>\<^sup>+x. norm(f x) \<partial>M) + limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
by (rule Limsup_const_add, auto simp add: finint)
- also have "... \<le> (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
+ also have "\<dots> \<le> (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
using assms(4) by (simp add: add_left_mono)
- also have "... = 2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
+ also have "\<dots> = 2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
unfolding one_add_one[symmetric] distrib_right by simp
ultimately have a: "limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M)) \<le>
2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)" by simp
@@ -994,6 +1000,7 @@
with eq show ?case by simp
qed
+section \<open>Convergence of integrals over an interval\<close>
text \<open>
The next lemmas relate convergence of integrals over an interval to
@@ -1122,7 +1129,7 @@
using \<open>c>0\<close> A by (auto simp: ennreal_mult'[symmetric])
then have "emeasure M {x \<in> A. u x \<ge> c} = emeasure M ({x \<in> A. ennreal(1/c) * u x \<ge> 1})"
by simp
- also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator A x \<partial>M)"
+ also have "\<dots> \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator A x \<partial>M)"
by (intro nn_integral_Markov_inequality meas assms)
also have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator A x \<partial>M) = ennreal (set_lebesgue_integral M A u)"
unfolding set_lebesgue_integral_def nn_integral_set_ennreal using assms AE
@@ -1178,4 +1185,767 @@
by (simp add: exp_minus field_simps)
qed
+
+section \<open>Integrable Simple Functions\<close>
+
+text \<open>This section is from the Martingales AFP entry, by Ata Keskin, TU München\<close>
+
+text \<open>We restate some basic results concerning Bochner-integrable functions.\<close>
+
+lemma integrable_implies_simple_function_sequence:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes "integrable M f"
+ obtains s where "\<And>i. simple_function M (s i)"
+ and "\<And>i. emeasure M {y \<in> space M. s i y \<noteq> 0} \<noteq> \<infinity>"
+ and "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
+ and "\<And>x i. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
+proof-
+ have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>" using assms unfolding integrable_iff_bounded by auto
+ obtain s where s: "\<And>i. simple_function M (s i)" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)" using borel_measurable_implies_sequence_metric[OF f(1)] unfolding norm_conv_dist by metis
+ {
+ fix i
+ have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ennreal (2 * norm (f x)) \<partial>M)" using s by (intro nn_integral_mono, auto)
+ also have "\<dots> < \<infinity>" using f by (simp add: nn_integral_cmult ennreal_mult_less_top ennreal_mult)
+ finally have sbi: "Bochner_Integration.simple_bochner_integrable M (s i)" using s by (intro simple_bochner_integrableI_bounded) auto
+ hence "emeasure M {y \<in> space M. s i y \<noteq> 0} \<noteq> \<infinity>" by (auto intro: integrableI_simple_bochner_integrable simple_bochner_integrable.cases)
+ }
+ thus ?thesis using that s by blast
+qed
+
+text \<open>Simple functions can be represented by sums of indicator functions.\<close>
+
+lemma simple_function_indicator_representation_banach:
+ fixes f ::"'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
+ assumes "simple_function M f" "x \<in> space M"
+ shows "f x = (\<Sum>y \<in> f ` space M. indicator (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ (is "?l = ?r")
+proof -
+ have "?r = (\<Sum>y \<in> f ` space M. (if y = f x then indicator (f -` {y} \<inter> space M) x *\<^sub>R y else 0))"
+ by (auto intro!: sum.cong)
+ also have "\<dots> = indicator (f -` {f x} \<inter> space M) x *\<^sub>R f x" using assms by (auto dest: simple_functionD)
+ also have "\<dots> = f x" using assms by (auto simp: indicator_def)
+ finally show ?thesis by auto
+qed
+
+lemma simple_function_indicator_representation_AE:
+ fixes f ::"'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
+ assumes "simple_function M f"
+ shows "AE x in M. f x = (\<Sum>y \<in> f ` space M. indicator (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ by (metis (mono_tags, lifting) AE_I2 simple_function_indicator_representation_banach assms)
+
+lemmas simple_function_scaleR[intro] = simple_function_compose2[where h="(*\<^sub>R)"]
+lemmas integrable_simple_function = simple_bochner_integrable.intros[THEN has_bochner_integral_simple_bochner_integrable, THEN integrable.intros]
+
+text \<open>Induction rule for simple integrable functions.\<close>
+
+lemma\<^marker>\<open>tag important\<close> integrable_simple_function_induct[consumes 2, case_names cong indicator add, induct set: simple_function]:
+ fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
+ assumes f: "simple_function M f" "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>"
+ assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>
+ \<Longrightarrow> simple_function M g \<Longrightarrow> emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity>
+ \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
+ assumes indicator: "\<And>A y. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R y)"
+ assumes add: "\<And>f g. simple_function M f \<Longrightarrow> emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
+ simple_function M g \<Longrightarrow> emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
+ (\<And>z. z \<in> space M \<Longrightarrow> norm (f z + g z) = norm (f z) + norm (g z)) \<Longrightarrow>
+ P f \<Longrightarrow> P g \<Longrightarrow> P (\<lambda>x. f x + g x)"
+ shows "P f"
+proof-
+ let ?f = "\<lambda>x. (\<Sum>y\<in>f ` space M. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ have f_ae_eq: "f x = ?f x" if "x \<in> space M" for x using simple_function_indicator_representation_banach[OF f(1) that] .
+ moreover have "emeasure M {y \<in> space M. ?f y \<noteq> 0} \<noteq> \<infinity>" by (metis (no_types, lifting) Collect_cong calculation f(2))
+ moreover have "P (\<lambda>x. \<Sum>y\<in>S. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ "simple_function M (\<lambda>x. \<Sum>y\<in>S. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ "emeasure M {y \<in> space M. (\<Sum>x\<in>S. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<noteq> \<infinity>"
+ if "S \<subseteq> f ` space M" for S using simple_functionD(1)[OF assms(1), THEN rev_finite_subset, OF that] that
+ proof (induction rule: finite_induct)
+ case empty
+ {
+ case 1
+ then show ?case using indicator[of "{}"] by force
+ next
+ case 2
+ then show ?case by force
+ next
+ case 3
+ then show ?case by force
+ }
+ next
+ case (insert x F)
+ have "(f -` {x} \<inter> space M) \<subseteq> {y \<in> space M. f y \<noteq> 0}" if "x \<noteq> 0" using that by blast
+ moreover have "{y \<in> space M. f y \<noteq> 0} = space M - (f -` {0} \<inter> space M)" by blast
+ moreover have "space M - (f -` {0} \<inter> space M) \<in> sets M" using simple_functionD(2)[OF f(1)] by blast
+ ultimately have fin_0: "emeasure M (f -` {x} \<inter> space M) < \<infinity>" if "x \<noteq> 0" using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique)
+ hence fin_1: "emeasure M {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0} \<noteq> \<infinity>" if "x \<noteq> 0" by (metis (mono_tags, lifting) emeasure_mono f(1) indicator_simps(2) linorder_not_less mem_Collect_eq scaleR_eq_0_iff simple_functionD(2) subsetI that)
+
+ have *: "(\<Sum>y\<in>insert x F. indicat_real (f -` {y} \<inter> space M) xa *\<^sub>R y) = (\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) xa *\<^sub>R y) + indicat_real (f -` {x} \<inter> space M) xa *\<^sub>R x" for xa by (metis (no_types, lifting) Diff_empty Diff_insert0 add.commute insert.hyps(1) insert.hyps(2) sum.insert_remove)
+ have **: "{y \<in> space M. (\<Sum>x\<in>insert x F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<subseteq> {y \<in> space M. (\<Sum>x\<in>F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<union> {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0}" unfolding * by fastforce
+ {
+ case 1
+ hence x: "x \<in> f ` space M" and F: "F \<subseteq> f ` space M" by auto
+ show ?case
+ proof (cases "x = 0")
+ case True
+ then show ?thesis unfolding * using insert(3)[OF F] by simp
+ next
+ case False
+ have norm_argument: "norm ((\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y) + indicat_real (f -` {x} \<inter> space M) z *\<^sub>R x) = norm (\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y) + norm (indicat_real (f -` {x} \<inter> space M) z *\<^sub>R x)" if z: "z \<in> space M" for z
+ proof (cases "f z = x")
+ case True
+ have "indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y = 0" if "y \<in> F" for y
+ using True insert(2) z that 1 unfolding indicator_def by force
+ hence "(\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y) = 0" by (meson sum.neutral)
+ then show ?thesis by force
+ next
+ case False
+ then show ?thesis by force
+ qed
+ show ?thesis
+ using False simple_functionD(2)[OF f(1)] insert(3,5)[OF F] simple_function_scaleR fin_0 fin_1
+ by (subst *, subst add, subst simple_function_sum) (blast intro: norm_argument indicator)+
+ qed
+ next
+ case 2
+ hence x: "x \<in> f ` space M" and F: "F \<subseteq> f ` space M" by auto
+ show ?case
+ proof (cases "x = 0")
+ case True
+ then show ?thesis unfolding * using insert(4)[OF F] by simp
+ next
+ case False
+ then show ?thesis unfolding * using insert(4)[OF F] simple_functionD(2)[OF f(1)] by fast
+ qed
+ next
+ case 3
+ hence x: "x \<in> f ` space M" and F: "F \<subseteq> f ` space M" by auto
+ show ?case
+ proof (cases "x = 0")
+ case True
+ then show ?thesis unfolding * using insert(5)[OF F] by simp
+ next
+ case False
+ have "emeasure M {y \<in> space M. (\<Sum>x\<in>insert x F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<le> emeasure M ({y \<in> space M. (\<Sum>x\<in>F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<union> {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0})"
+ using ** simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_mono, force+)
+ also have "\<dots> \<le> emeasure M {y \<in> space M. (\<Sum>x\<in>F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} + emeasure M {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0}"
+ using simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+)
+ also have "\<dots> < \<infinity>" using insert(5)[OF F] fin_1[OF False] by (simp add: less_top)
+ finally show ?thesis by simp
+ qed
+ }
+ qed
+ moreover have "simple_function M (\<lambda>x. \<Sum>y\<in>f ` space M. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)" using calculation by blast
+ moreover have "P (\<lambda>x. \<Sum>y\<in>f ` space M. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)" using calculation by blast
+ ultimately show ?thesis by (intro cong[OF _ _ f(1,2)], blast, presburger+)
+qed
+
+text \<open>Induction rule for non-negative simple integrable functions\<close>
+lemma\<^marker>\<open>tag important\<close> integrable_simple_function_induct_nn[consumes 3, case_names cong indicator add, induct set: simple_function]:
+ fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes f: "simple_function M f" "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" "\<And>x. x \<in> space M \<longrightarrow> f x \<ge> 0"
+ assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> simple_function M g \<Longrightarrow> emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> g x \<ge> 0) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
+ assumes indicator: "\<And>A y. y \<ge> 0 \<Longrightarrow> A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R y)"
+ assumes add: "\<And>f g. (\<And>x. x \<in> space M \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> simple_function M f \<Longrightarrow> emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
+ (\<And>x. x \<in> space M \<Longrightarrow> g x \<ge> 0) \<Longrightarrow> simple_function M g \<Longrightarrow> emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
+ (\<And>z. z \<in> space M \<Longrightarrow> norm (f z + g z) = norm (f z) + norm (g z)) \<Longrightarrow>
+ P f \<Longrightarrow> P g \<Longrightarrow> P (\<lambda>x. f x + g x)"
+ shows "P f"
+proof-
+ let ?f = "\<lambda>x. (\<Sum>y\<in>f ` space M. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ have f_ae_eq: "f x = ?f x" if "x \<in> space M" for x using simple_function_indicator_representation_banach[OF f(1) that] .
+ moreover have "emeasure M {y \<in> space M. ?f y \<noteq> 0} \<noteq> \<infinity>" by (metis (no_types, lifting) Collect_cong calculation f(2))
+ moreover have "P (\<lambda>x. \<Sum>y\<in>S. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ "simple_function M (\<lambda>x. \<Sum>y\<in>S. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ "emeasure M {y \<in> space M. (\<Sum>x\<in>S. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<noteq> \<infinity>"
+ "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> (\<Sum>y\<in>S. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ if "S \<subseteq> f ` space M" for S using simple_functionD(1)[OF assms(1), THEN rev_finite_subset, OF that] that
+ proof (induction rule: finite_subset_induct')
+ case empty
+ {
+ case 1
+ then show ?case using indicator[of 0 "{}"] by force
+ next
+ case 2
+ then show ?case by force
+ next
+ case 3
+ then show ?case by force
+ next
+ case 4
+ then show ?case by force
+ }
+ next
+ case (insert x F)
+ have "(f -` {x} \<inter> space M) \<subseteq> {y \<in> space M. f y \<noteq> 0}" if "x \<noteq> 0"
+ using that by blast
+ moreover have "{y \<in> space M. f y \<noteq> 0} = space M - (f -` {0} \<inter> space M)"
+ by blast
+ moreover have "space M - (f -` {0} \<inter> space M) \<in> sets M"
+ using simple_functionD(2)[OF f(1)] by blast
+ ultimately have fin_0: "emeasure M (f -` {x} \<inter> space M) < \<infinity>" if "x \<noteq> 0"
+ using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique)
+ hence fin_1: "emeasure M {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0} \<noteq> \<infinity>" if "x \<noteq> 0"
+ by (metis (mono_tags, lifting) emeasure_mono f(1) indicator_simps(2) linorder_not_less mem_Collect_eq scaleR_eq_0_iff simple_functionD(2) subsetI that)
+
+ have nonneg_x: "x \<ge> 0" using insert f by blast
+ have *: "(\<Sum>y\<in>insert x F. indicat_real (f -` {y} \<inter> space M) xa *\<^sub>R y) = (\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) xa *\<^sub>R y) + indicat_real (f -` {x} \<inter> space M) xa *\<^sub>R x" for xa by (metis (no_types, lifting) add.commute insert.hyps(1) insert.hyps(4) sum.insert)
+ have **: "{y \<in> space M. (\<Sum>x\<in>insert x F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<subseteq> {y \<in> space M. (\<Sum>x\<in>F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<union> {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0}" unfolding * by fastforce
+ {
+ case 1
+ show ?case
+ proof (cases "x = 0")
+ case True
+ then show ?thesis unfolding * using insert by simp
+ next
+ case False
+ have norm_argument: "norm ((\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y) + indicat_real (f -` {x} \<inter> space M) z *\<^sub>R x)
+ = norm (\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y) + norm (indicat_real (f -` {x} \<inter> space M) z *\<^sub>R x)"
+ if z: "z \<in> space M" for z
+ proof (cases "f z = x")
+ case True
+ have "indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y = 0" if "y \<in> F" for y
+ using True insert z that 1 unfolding indicator_def by force
+ hence "(\<Sum>y\<in>F. indicat_real (f -` {y} \<inter> space M) z *\<^sub>R y) = 0"
+ by (meson sum.neutral)
+ thus ?thesis by force
+ qed (force)
+ show ?thesis using False fin_0 fin_1 f norm_argument
+ by (subst *, subst add, presburger add: insert, intro insert, intro insert, fastforce simp add: indicator_def intro!: insert(2) f(3), auto intro!: indicator insert nonneg_x)
+ qed
+ next
+ case 2
+ show ?case
+ proof (cases "x = 0")
+ case True
+ then show ?thesis unfolding * using insert by simp
+ next
+ case False
+ then show ?thesis unfolding * using insert simple_functionD(2)[OF f(1)] by fast
+ qed
+ next
+ case 3
+ show ?case
+ proof (cases "x = 0")
+ case True
+ then show ?thesis unfolding * using insert by simp
+ next
+ case False
+ have "emeasure M {y \<in> space M. (\<Sum>x\<in>insert x F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0}
+ \<le> emeasure M ({y \<in> space M. (\<Sum>x\<in>F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} \<union> {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0})"
+ using ** simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] insert.IH(2) by (intro emeasure_mono, blast, simp)
+ also have "\<dots> \<le> emeasure M {y \<in> space M. (\<Sum>x\<in>F. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x) \<noteq> 0} + emeasure M {y \<in> space M. indicat_real (f -` {x} \<inter> space M) y *\<^sub>R x \<noteq> 0}"
+ using simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+)
+ also have "\<dots> < \<infinity>" using insert(7) fin_1[OF False] by (simp add: less_top)
+ finally show ?thesis by simp
+ qed
+ next
+ case (4 \<xi>)
+ thus ?case using insert nonneg_x f(3) by (auto simp add: scaleR_nonneg_nonneg intro: sum_nonneg)
+ }
+ qed
+ moreover have "simple_function M (\<lambda>x. \<Sum>y\<in>f ` space M. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ using calculation by blast
+ moreover have "P (\<lambda>x. \<Sum>y\<in>f ` space M. indicat_real (f -` {y} \<inter> space M) x *\<^sub>R y)"
+ using calculation by blast
+ moreover have "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" using f(3) by simp
+ ultimately show ?thesis
+ by (smt (verit) Collect_cong f(1) local.cong)
+qed
+
+lemma finite_nn_integral_imp_ae_finite:
+ fixes f :: "'a \<Rightarrow> ennreal"
+ assumes "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
+ shows "AE x in M. f x < \<infinity>"
+proof (rule ccontr, goal_cases)
+ case 1
+ let ?A = "space M \<inter> {x. f x = \<infinity>}"
+ have *: "emeasure M ?A > 0" using 1 assms(1)
+ by (metis (mono_tags, lifting) assms(2) eventually_mono infinity_ennreal_def nn_integral_noteq_infinite top.not_eq_extremum)
+ have "(\<integral>\<^sup>+x. f x * indicator ?A x \<partial>M) = (\<integral>\<^sup>+x. \<infinity> * indicator ?A x \<partial>M)"
+ by (metis (mono_tags, lifting) indicator_inter_arith indicator_simps(2) mem_Collect_eq mult_eq_0_iff)
+ also have "\<dots> = \<infinity> * emeasure M ?A"
+ using assms(1) by (intro nn_integral_cmult_indicator, simp)
+ also have "\<dots> = \<infinity>"
+ using * by fastforce
+ finally have "(\<integral>\<^sup>+x. f x * indicator ?A x \<partial>M) = \<infinity>" .
+ moreover have "(\<integral>\<^sup>+x. f x * indicator ?A x \<partial>M) \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
+ by (intro nn_integral_mono, simp add: indicator_def)
+ ultimately show ?case using assms(2) by simp
+qed
+
+text \<open>Convergence in L1-Norm implies existence of a subsequence which convergences almost everywhere.
+ This lemma is easier to use than the existing one in \<^theory>\<open>HOL-Analysis.Bochner_Integration\<close>\<close>
+
+lemma cauchy_L1_AE_cauchy_subseq:
+ fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes [measurable]: "\<And>n. integrable M (s n)"
+ and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>i\<ge>N. \<forall>j\<ge>N. LINT x|M. norm (s i x - s j x) < e"
+ obtains r where "strict_mono r" "AE x in M. Cauchy (\<lambda>i. s (r i) x)"
+proof-
+ have "\<exists>r. \<forall>n. (\<forall>i\<ge>r n. \<forall>j\<ge> r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n) \<and> (r (Suc n) > r n)"
+ proof (intro dependent_nat_choice, goal_cases)
+ case 1
+ then show ?case using assms(2) by presburger
+ next
+ case (2 x n)
+ obtain N where *: "LINT x|M. norm (s i x - s j x) < (1 / 2) ^ Suc n" if "i \<ge> N" "j \<ge> N" for i j
+ using assms(2)[of "(1 / 2) ^ Suc n"] by auto
+ {
+ fix i j assume "i \<ge> max N (Suc x)" "j \<ge> max N (Suc x)"
+ hence "integral\<^sup>L M (\<lambda>x. norm (s i x - s j x)) < (1 / 2) ^ Suc n" using * by fastforce
+ }
+ then show ?case by fastforce
+ qed
+ then obtain r where strict_mono: "strict_mono r" and "\<forall>i\<ge>r n. \<forall>j\<ge> r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n" for n
+ using strict_mono_Suc_iff by blast
+ hence r_is: "LINT x|M. norm (s (r (Suc n)) x - s (r n) x) < (1 / 2) ^ n" for n by (simp add: strict_mono_leD)
+
+ define g where "g = (\<lambda>n x. (\<Sum>i\<le>n. ennreal (norm (s (r (Suc i)) x - s (r i) x))))"
+ define g' where "g' = (\<lambda>x. \<Sum>i. ennreal (norm (s (r (Suc i)) x - s (r i) x)))"
+
+ have integrable_g: "(\<integral>\<^sup>+ x. g n x \<partial>M) < 2" for n
+ proof -
+ have "(\<integral>\<^sup>+ x. g n x \<partial>M) = (\<integral>\<^sup>+ x. (\<Sum>i\<le>n. ennreal (norm (s (r (Suc i)) x - s (r i) x))) \<partial>M)"
+ using g_def by simp
+ also have "\<dots> = (\<Sum>i\<le>n. (\<integral>\<^sup>+ x. ennreal (norm (s (r (Suc i)) x - s (r i) x)) \<partial>M))"
+ by (intro nn_integral_sum, simp)
+ also have "\<dots> = (\<Sum>i\<le>n. LINT x|M. norm (s (r (Suc i)) x - s (r i) x))"
+ unfolding dist_norm using assms(1) by (subst nn_integral_eq_integral[OF integrable_norm], auto)
+ also have "\<dots> < ennreal (\<Sum>i\<le>n. (1 / 2) ^ i)"
+ by (intro ennreal_lessI[OF sum_pos sum_strict_mono[OF finite_atMost _ r_is]], auto)
+ also have "\<dots> \<le> ennreal 2"
+ unfolding sum_gp0[of "1 / 2" n] by (intro ennreal_leI, auto)
+ finally show "(\<integral>\<^sup>+ x. g n x \<partial>M) < 2" by simp
+ qed
+
+ have integrable_g': "(\<integral>\<^sup>+ x. g' x \<partial>M) \<le> 2"
+ proof -
+ have "incseq (\<lambda>n. g n x)" for x by (intro incseq_SucI, auto simp add: g_def ennreal_leI)
+ hence "convergent (\<lambda>n. g n x)" for x
+ unfolding convergent_def using LIMSEQ_incseq_SUP by fast
+ hence "(\<lambda>n. g n x) \<longlonglongrightarrow> g' x" for x
+ unfolding g_def g'_def by (intro summable_iff_convergent'[THEN iffD2, THEN summable_LIMSEQ'], blast)
+ hence "(\<integral>\<^sup>+ x. g' x \<partial>M) = (\<integral>\<^sup>+ x. liminf (\<lambda>n. g n x) \<partial>M)" by (metis lim_imp_Liminf trivial_limit_sequentially)
+ also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^sup>+ x. g n x \<partial>M)" by (intro nn_integral_liminf, simp add: g_def)
+ also have "\<dots> \<le> liminf (\<lambda>n. 2)" using integrable_g by (intro Liminf_mono) (simp add: order_le_less)
+ also have "\<dots> = 2"
+ using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
+ finally show ?thesis .
+ qed
+ hence "AE x in M. g' x < \<infinity>"
+ by (intro finite_nn_integral_imp_ae_finite) (auto simp add: order_le_less_trans g'_def)
+ moreover have "summable (\<lambda>i. norm (s (r (Suc i)) x - s (r i) x))" if "g' x \<noteq> \<infinity>" for x
+ using that unfolding g'_def by (intro summable_suminf_not_top) fastforce+
+ ultimately have ae_summable: "AE x in M. summable (\<lambda>i. s (r (Suc i)) x - s (r i) x)"
+ using summable_norm_cancel unfolding dist_norm by force
+
+ {
+ fix x assume "summable (\<lambda>i. s (r (Suc i)) x - s (r i) x)"
+ hence "(\<lambda>n. \<Sum>i<n. s (r (Suc i)) x - s (r i) x) \<longlonglongrightarrow> (\<Sum>i. s (r (Suc i)) x - s (r i) x)"
+ using summable_LIMSEQ by blast
+ moreover have "(\<lambda>n. (\<Sum>i<n. s (r (Suc i)) x - s (r i) x)) = (\<lambda>n. s (r n) x - s (r 0) x)"
+ using sum_lessThan_telescope by fastforce
+ ultimately have "(\<lambda>n. s (r n) x - s (r 0) x) \<longlonglongrightarrow> (\<Sum>i. s (r (Suc i)) x - s (r i) x)" by argo
+ hence "(\<lambda>n. s (r n) x - s (r 0) x + s (r 0) x) \<longlonglongrightarrow> (\<Sum>i. s (r (Suc i)) x - s (r i) x) + s (r 0) x"
+ by (intro isCont_tendsto_compose[of _ "\<lambda>z. z + s (r 0) x"], auto)
+ hence "Cauchy (\<lambda>n. s (r n) x)" by (simp add: LIMSEQ_imp_Cauchy)
+ }
+ hence "AE x in M. Cauchy (\<lambda>i. s (r i) x)" using ae_summable by fast
+ thus ?thesis by (rule that[OF strict_mono(1)])
+qed
+
+subsection \<open>Totally Ordered Banach Spaces\<close>
+
+lemma integrable_max[simp, intro]:
+ fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology}"
+ assumes fg[measurable]: "integrable M f" "integrable M g"
+ shows "integrable M (\<lambda>x. max (f x) (g x))"
+proof (rule Bochner_Integration.integrable_bound)
+ {
+ fix x y :: 'b
+ have "norm (max x y) \<le> max (norm x) (norm y)" by linarith
+ also have "\<dots> \<le> norm x + norm y" by simp
+ finally have "norm (max x y) \<le> norm (norm x + norm y)" by simp
+ }
+ thus "AE x in M. norm (max (f x) (g x)) \<le> norm (norm (f x) + norm (g x))" by simp
+qed (auto intro: Bochner_Integration.integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]])
+
+lemma integrable_min[simp, intro]:
+ fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology}"
+ assumes [measurable]: "integrable M f" "integrable M g"
+ shows "integrable M (\<lambda>x. min (f x) (g x))"
+proof -
+ have "norm (min (f x) (g x)) \<le> norm (f x) \<or> norm (min (f x) (g x)) \<le> norm (g x)" for x by linarith
+ thus ?thesis
+ by (intro integrable_bound[OF integrable_max[OF integrable_norm(1,1), OF assms]], auto)
+qed
+
+text \<open>Restatement of \<open>integral_nonneg_AE\<close> for functions taking values in a Banach space.\<close>
+lemma integral_nonneg_AE_banach:
+ fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes [measurable]: "f \<in> borel_measurable M" and nonneg: "AE x in M. 0 \<le> f x"
+ shows "0 \<le> integral\<^sup>L M f"
+proof cases
+ assume integrable: "integrable M f"
+ hence max: "(\<lambda>x. max 0 (f x)) \<in> borel_measurable M" "\<And>x. 0 \<le> max 0 (f x)" "integrable M (\<lambda>x. max 0 (f x))" by auto
+ hence "0 \<le> integral\<^sup>L M (\<lambda>x. max 0 (f x))"
+ proof -
+ obtain s where *: "\<And>i. simple_function M (s i)"
+ "\<And>i. emeasure M {y \<in> space M. s i y \<noteq> 0} \<noteq> \<infinity>"
+ "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
+ "\<And>x i. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
+ using integrable_implies_simple_function_sequence[OF integrable] by blast
+ have simple: "\<And>i. simple_function M (\<lambda>x. max 0 (s i x))"
+ using * by fast
+ have "\<And>i. {y \<in> space M. max 0 (s i y) \<noteq> 0} \<subseteq> {y \<in> space M. s i y \<noteq> 0}"
+ unfolding max_def by force
+ moreover have "\<And>i. {y \<in> space M. s i y \<noteq> 0} \<in> sets M"
+ using * by measurable
+ ultimately have "\<And>i. emeasure M {y \<in> space M. max 0 (s i y) \<noteq> 0} \<le> emeasure M {y \<in> space M. s i y \<noteq> 0}"
+ by (rule emeasure_mono)
+ hence **:"\<And>i. emeasure M {y \<in> space M. max 0 (s i y) \<noteq> 0} \<noteq> \<infinity>"
+ using *(2) by (auto intro: order.strict_trans1 simp add: top.not_eq_extremum)
+ have "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. max 0 (s i x)) \<longlonglongrightarrow> max 0 (f x)"
+ using *(3) tendsto_max by blast
+ moreover have "\<And>x i. x \<in> space M \<Longrightarrow> norm (max 0 (s i x)) \<le> norm (2 *\<^sub>R f x)"
+ using *(4) unfolding max_def by auto
+ ultimately have tendsto: "(\<lambda>i. integral\<^sup>L M (\<lambda>x. max 0 (s i x))) \<longlonglongrightarrow> integral\<^sup>L M (\<lambda>x. max 0 (f x))"
+ using borel_measurable_simple_function simple integrable by (intro integral_dominated_convergence[OF max(1) _ integrable_norm[OF integrable_scaleR_right], of _ 2 f], blast+)
+ {
+ fix h :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assume "simple_function M h" "emeasure M {y \<in> space M. h y \<noteq> 0} \<noteq> \<infinity>" "\<And>x. x \<in> space M \<longrightarrow> h x \<ge> 0"
+ hence *: "integral\<^sup>L M h \<ge> 0"
+ proof (induct rule: integrable_simple_function_induct_nn)
+ case (cong f g)
+ then show ?case using Bochner_Integration.integral_cong by force
+ next
+ case (indicator A y)
+ hence "A \<noteq> {} \<Longrightarrow> y \<ge> 0" using sets.sets_into_space by fastforce
+ then show ?case using indicator by (cases "A = {}", auto simp add: scaleR_nonneg_nonneg)
+ next
+ case (add f g)
+ then show ?case by (simp add: integrable_simple_function)
+ qed
+ }
+ thus ?thesis using LIMSEQ_le_const[OF tendsto, of 0] ** simple by fastforce
+ qed
+ also have "\<dots> = integral\<^sup>L M f" using nonneg by (auto intro: integral_cong_AE)
+ finally show ?thesis .
+qed (simp add: not_integrable_integral_eq)
+
+lemma integral_mono_AE_banach:
+ fixes f g :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
+ shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
+ using integral_nonneg_AE_banach[of "\<lambda>x. g x - f x"] assms Bochner_Integration.integral_diff[OF assms(1,2)] by force
+
+lemma integral_mono_banach:
+ fixes f g :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes "integrable M f" "integrable M g" "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x"
+ shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
+ using integral_mono_AE_banach assms by blast
+
+subsection \<open>Auxiliary Lemmas for Set Integrals\<close>
+
+lemma nn_set_integral_eq_set_integral:
+ assumes [measurable]:"integrable M f"
+ and "AE x \<in> A in M. 0 \<le> f x" "A \<in> sets M"
+ shows "(\<integral>\<^sup>+x\<in>A. f x \<partial>M) = (\<integral> x \<in> A. f x \<partial>M)"
+proof-
+ have "(\<integral>\<^sup>+x. indicator A x *\<^sub>R f x \<partial>M) = (\<integral> x \<in> A. f x \<partial>M)"
+ unfolding set_lebesgue_integral_def
+ using assms(2) by (intro nn_integral_eq_integral[of _ "\<lambda>x. indicat_real A x *\<^sub>R f x"], blast intro: assms integrable_mult_indicator, fastforce)
+ moreover have "(\<integral>\<^sup>+x. indicator A x *\<^sub>R f x \<partial>M) = (\<integral>\<^sup>+x\<in>A. f x \<partial>M)"
+ by (metis ennreal_0 indicator_simps(1) indicator_simps(2) mult.commute mult_1 mult_zero_left real_scaleR_def)
+ ultimately show ?thesis by argo
+qed
+
+lemma set_integral_restrict_space:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes "\<Omega> \<inter> space M \<in> sets M"
+ shows "set_lebesgue_integral (restrict_space M \<Omega>) A f = set_lebesgue_integral M A (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
+ unfolding set_lebesgue_integral_def
+ by (subst integral_restrict_space, auto intro!: integrable_mult_indicator assms simp: mult.commute)
+
+lemma set_integral_const:
+ fixes c :: "'b::{banach, second_countable_topology}"
+ assumes "A \<in> sets M" "emeasure M A \<noteq> \<infinity>"
+ shows "set_lebesgue_integral M A (\<lambda>_. c) = measure M A *\<^sub>R c"
+ unfolding set_lebesgue_integral_def
+ using assms by (metis has_bochner_integral_indicator has_bochner_integral_integral_eq infinity_ennreal_def less_top)
+
+lemma set_integral_mono_banach:
+ fixes f g :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes "set_integrable M A f" "set_integrable M A g"
+ "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+ shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
+ using assms unfolding set_integrable_def set_lebesgue_integral_def
+ by (auto intro: integral_mono_banach split: split_indicator)
+
+lemma set_integral_mono_AE_banach:
+ fixes f g :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes "set_integrable M A f" "set_integrable M A g" "AE x\<in>A in M. f x \<le> g x"
+ shows "set_lebesgue_integral M A f \<le> set_lebesgue_integral M A g" using assms unfolding set_lebesgue_integral_def by (auto simp add: set_integrable_def intro!: integral_mono_AE_banach[of M "\<lambda>x. indicator A x *\<^sub>R f x" "\<lambda>x. indicator A x *\<^sub>R g x"], simp add: indicator_def)
+
+subsection \<open>Integrability and Measurability of the Diameter\<close>
+
+context
+ fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: {second_countable_topology, banach}" and M
+ assumes bounded: "\<And>x. x \<in> space M \<Longrightarrow> bounded (range (\<lambda>i. s i x))"
+begin
+
+lemma borel_measurable_diameter:
+ assumes [measurable]: "\<And>i. (s i) \<in> borel_measurable M"
+ shows "(\<lambda>x. diameter {s i x |i. n \<le> i}) \<in> borel_measurable M"
+proof -
+ have "{s i x |i. N \<le> i} \<noteq> {}" for x N by blast
+ hence diameter_SUP: "diameter {s i x |i. N \<le> i} = (SUP (i, j) \<in> {N..} \<times> {N..}. dist (s i x) (s j x))" for x N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup])
+
+ have "case_prod dist ` ({s i x |i. n \<le> i} \<times> {s i x |i. n \<le> i}) = ((\<lambda>(i, j). dist (s i x) (s j x)) ` ({n..} \<times> {n..}))" for x by fast
+ hence *: "(\<lambda>x. diameter {s i x |i. n \<le> i}) = (\<lambda>x. Sup ((\<lambda>(i, j). dist (s i x) (s j x)) ` ({n..} \<times> {n..})))" using diameter_SUP by (simp add: case_prod_beta')
+
+ have "bounded ((\<lambda>(i, j). dist (s i x) (s j x)) ` ({n..} \<times> {n..}))" if "x \<in> space M" for x by (rule bounded_imp_dist_bounded[OF bounded, OF that])
+ hence bdd: "bdd_above ((\<lambda>(i, j). dist (s i x) (s j x)) ` ({n..} \<times> {n..}))" if "x \<in> space M" for x using that bounded_imp_bdd_above by presburger
+ have "fst p \<in> borel_measurable M" "snd p \<in> borel_measurable M" if "p \<in> s ` {n..} \<times> s ` {n..}" for p using that by fastforce+
+ hence "(\<lambda>x. fst p x - snd p x) \<in> borel_measurable M" if "p \<in> s ` {n..} \<times> s ` {n..}" for p using that borel_measurable_diff by simp
+ hence "(\<lambda>x. case p of (f, g) \<Rightarrow> dist (f x) (g x)) \<in> borel_measurable M" if "p \<in> s ` {n..} \<times> s ` {n..}" for p unfolding dist_norm using that by measurable
+ moreover have "countable (s ` {n..} \<times> s ` {n..})" by (intro countable_SIGMA countable_image, auto)
+ ultimately show ?thesis unfolding * by (auto intro!: borel_measurable_cSUP bdd)
+qed
+
+lemma integrable_bound_diameter:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "integrable M f"
+ and [measurable]: "\<And>i. (s i) \<in> borel_measurable M"
+ and "\<And>x i. x \<in> space M \<Longrightarrow> norm (s i x) \<le> f x"
+ shows "integrable M (\<lambda>x. diameter {s i x |i. n \<le> i})"
+proof -
+ have "{s i x |i. N \<le> i} \<noteq> {}" for x N by blast
+ hence diameter_SUP: "diameter {s i x |i. N \<le> i} = (SUP (i, j) \<in> {N..} \<times> {N..}. dist (s i x) (s j x))" for x N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup])
+ {
+ fix x assume x: "x \<in> space M"
+ let ?S = "(\<lambda>(i, j). dist (s i x) (s j x)) ` ({n..} \<times> {n..})"
+ have "case_prod dist ` ({s i x |i. n \<le> i} \<times> {s i x |i. n \<le> i}) = (\<lambda>(i, j). dist (s i x) (s j x)) ` ({n..} \<times> {n..})" by fast
+ hence *: "diameter {s i x |i. n \<le> i} = Sup ?S" using diameter_SUP by (simp add: case_prod_beta')
+
+ have "bounded ?S" by (rule bounded_imp_dist_bounded[OF bounded[OF x]])
+ hence Sup_S_nonneg:"0 \<le> Sup ?S" by (auto intro!: cSup_upper2 x bounded_imp_bdd_above)
+
+ have "dist (s i x) (s j x) \<le> 2 * f x" for i j by (intro dist_triangle2[THEN order_trans, of _ 0]) (metis norm_conv_dist assms(3) x add_mono mult_2)
+ hence "\<forall>c \<in> ?S. c \<le> 2 * f x" by force
+ hence "Sup ?S \<le> 2 * f x" by (intro cSup_least, auto)
+ hence "norm (Sup ?S) \<le> 2 * norm (f x)" using Sup_S_nonneg by auto
+ also have "\<dots> = norm (2 *\<^sub>R f x)" by simp
+ finally have "norm (diameter {s i x |i. n \<le> i}) \<le> norm (2 *\<^sub>R f x)" unfolding * .
+ }
+ hence "AE x in M. norm (diameter {s i x |i. n \<le> i}) \<le> norm (2 *\<^sub>R f x)" by blast
+ thus "integrable M (\<lambda>x. diameter {s i x |i. n \<le> i})" using borel_measurable_diameter by (intro Bochner_Integration.integrable_bound[OF assms(1)[THEN integrable_scaleR_right[of 2]]], measurable)
+qed
+end
+
+subsection \<open>Averaging Theorem\<close>
+
+text \<open>We aim to lift results from the real case to arbitrary Banach spaces.
+ Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}.
+ The theorem allows us to make statements about a function’s value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
+
+text \<open>Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof.
+ While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.
+ (Engelking's book \emph{General Topology})\<close>
+
+lemma balls_countable_basis:
+ obtains D :: "'a :: {metric_space, second_countable_topology} set"
+ where "topological_basis (case_prod ball ` (D \<times> (\<rat> \<inter> {0<..})))"
+ and "countable D"
+ and "D \<noteq> {}"
+proof -
+ obtain D :: "'a set" where dense_subset: "countable D" "D \<noteq> {}" "\<lbrakk>open U; U \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>y \<in> D. y \<in> U" for U using countable_dense_exists by blast
+ have "topological_basis (case_prod ball ` (D \<times> (\<rat> \<inter> {0<..})))"
+ proof (intro topological_basis_iff[THEN iffD2], fast, clarify)
+ fix U and x :: 'a assume asm: "open U" "x \<in> U"
+ obtain e where e: "e > 0" "ball x e \<subseteq> U" using asm openE by blast
+ obtain y where y: "y \<in> D" "y \<in> ball x (e / 3)" using dense_subset(3)[OF open_ball, of x "e / 3"] centre_in_ball[THEN iffD2, OF divide_pos_pos[OF e(1), of 3]] by force
+ obtain r where r: "r \<in> \<rat> \<inter> {e/3<..<e/2}" unfolding Rats_def using of_rat_dense[OF divide_strict_left_mono[OF _ e(1)], of 2 3] by auto
+
+ have *: "x \<in> ball y r" using r y by (simp add: dist_commute)
+ hence "ball y r \<subseteq> U" using r by (intro order_trans[OF _ e(2)], simp, metric)
+ moreover have "ball y r \<in> (case_prod ball ` (D \<times> (\<rat> \<inter> {0<..})))" using y(1) r by force
+ ultimately show "\<exists>B'\<in>(case_prod ball ` (D \<times> (\<rat> \<inter> {0<..}))). x \<in> B' \<and> B' \<subseteq> U" using * by meson
+ qed
+ thus ?thesis using that dense_subset by blast
+qed
+
+context sigma_finite_measure
+begin
+
+text \<open>To show statements concerning \<open>\<sigma>\<close>-finite measure spaces, one usually shows the statement for finite measure spaces and uses a limiting argument to show it for the \<open>\<sigma>\<close>-finite case.
+ The following induction scheme formalizes this.\<close>
+lemma sigma_finite_measure_induct[case_names finite_measure, consumes 0]:
+ assumes "\<And>(N :: 'a measure) \<Omega>. finite_measure N
+ \<Longrightarrow> N = restrict_space M \<Omega>
+ \<Longrightarrow> \<Omega> \<in> sets M
+ \<Longrightarrow> emeasure N \<Omega> \<noteq> \<infinity>
+ \<Longrightarrow> emeasure N \<Omega> \<noteq> 0
+ \<Longrightarrow> almost_everywhere N Q"
+ and [measurable]: "Measurable.pred M Q"
+ shows "almost_everywhere M Q"
+proof -
+ have *: "almost_everywhere N Q" if "finite_measure N" "N = restrict_space M \<Omega>" "\<Omega> \<in> sets M" "emeasure N \<Omega> \<noteq> \<infinity>" for N \<Omega> using that by (cases "emeasure N \<Omega> = 0", auto intro: emeasure_0_AE assms(1))
+
+ obtain A :: "nat \<Rightarrow> 'a set" where A: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" and emeasure_finite: "emeasure M (A i) \<noteq> \<infinity>" for i using sigma_finite by metis
+ note A(1)[measurable]
+ have space_restr: "space (restrict_space M (A i)) = A i" for i unfolding space_restrict_space by simp
+ {
+ fix i
+ have *: "{x \<in> A i \<inter> space M. Q x} = {x \<in> space M. Q x} \<inter> (A i)" by fast
+ have "Measurable.pred (restrict_space M (A i)) Q" using A by (intro measurableI, auto simp add: space_restr intro!: sets_restrict_space_iff[THEN iffD2], measurable, auto)
+ }
+ note this[measurable]
+ {
+ fix i
+ have "finite_measure (restrict_space M (A i))" using emeasure_finite by (intro finite_measureI, subst space_restr, subst emeasure_restrict_space, auto)
+ hence "emeasure (restrict_space M (A i)) {x \<in> A i. \<not>Q x} = 0" using emeasure_finite by (intro AE_iff_measurable[THEN iffD1, OF _ _ *], measurable, subst space_restr[symmetric], intro sets.top, auto simp add: emeasure_restrict_space)
+ hence "emeasure M {x \<in> A i. \<not> Q x} = 0" by (subst emeasure_restrict_space[symmetric], auto)
+ }
+ hence "emeasure M (\<Union>i. {x \<in> A i. \<not> Q x}) = 0" by (intro emeasure_UN_eq_0, auto)
+ moreover have "(\<Union>i. {x \<in> A i. \<not> Q x}) = {x \<in> space M. \<not> Q x}" using A by auto
+ ultimately show ?thesis by (intro AE_iff_measurable[THEN iffD2], auto)
+qed
+
+text \<open>Real Functional Analysis - Lang\<close>
+text \<open>The Averaging Theorem allows us to make statements concerning how a function behaves almost everywhere, depending on its behaviour on average.\<close>
+lemma averaging_theorem:
+ fixes f::"_ \<Rightarrow> 'b::{second_countable_topology, banach}"
+ assumes [measurable]: "integrable M f"
+ and closed: "closed S"
+ and "\<And>A. A \<in> sets M \<Longrightarrow> measure M A > 0 \<Longrightarrow> (1 / measure M A) *\<^sub>R set_lebesgue_integral M A f \<in> S"
+ shows "AE x in M. f x \<in> S"
+proof (induct rule: sigma_finite_measure_induct)
+ case (finite_measure N \<Omega>)
+
+ interpret finite_measure N by (rule finite_measure)
+
+ have integrable[measurable]: "integrable N f" using assms finite_measure by (auto simp: integrable_restrict_space integrable_mult_indicator)
+ have average: "(1 / Sigma_Algebra.measure N A) *\<^sub>R set_lebesgue_integral N A f \<in> S" if "A \<in> sets N" "measure N A > 0" for A
+ proof -
+ have *: "A \<in> sets M" using that by (simp add: sets_restrict_space_iff finite_measure)
+ have "A = A \<inter> \<Omega>" by (metis finite_measure(2,3) inf.orderE sets.sets_into_space space_restrict_space that(1))
+ hence "set_lebesgue_integral N A f = set_lebesgue_integral M A f" unfolding finite_measure by (subst set_integral_restrict_space, auto simp add: finite_measure set_lebesgue_integral_def indicator_inter_arith[symmetric])
+ moreover have "measure N A = measure M A" using that by (auto intro!: measure_restrict_space simp add: finite_measure sets_restrict_space_iff)
+ ultimately show ?thesis using that * assms(3) by presburger
+ qed
+
+ obtain D :: "'b set" where balls_basis: "topological_basis (case_prod ball ` (D \<times> (\<rat> \<inter> {0<..})))" and countable_D: "countable D" using balls_countable_basis by blast
+ have countable_balls: "countable (case_prod ball ` (D \<times> (\<rat> \<inter> {0<..})))" using countable_rat countable_D by blast
+
+ obtain B where B_balls: "B \<subseteq> case_prod ball ` (D \<times> (\<rat> \<inter> {0<..}))" "\<Union>B = -S" using topological_basis[THEN iffD1, OF balls_basis] open_Compl[OF assms(2)] by meson
+ hence countable_B: "countable B" using countable_balls countable_subset by fast
+
+ define b where "b = from_nat_into (B \<union> {{}})"
+ have "B \<union> {{}} \<noteq> {}" by simp
+ have range_b: "range b = B \<union> {{}}" using countable_B by (auto simp add: b_def intro!: range_from_nat_into)
+ have open_b: "open (b i)" for i unfolding b_def using B_balls open_ball from_nat_into[of "B \<union> {{}}" i] by force
+ have Union_range_b: "\<Union>(range b) = -S" using B_balls range_b by simp
+
+ {
+ fix v r assume ball_in_Compl: "ball v r \<subseteq> -S"
+ define A where "A = f -` ball v r \<inter> space N"
+ have dist_less: "dist (f x) v < r" if "x \<in> A" for x using that unfolding A_def vimage_def by (simp add: dist_commute)
+ hence AE_less: "AE x \<in> A in N. norm (f x - v) < r" by (auto simp add: dist_norm)
+ have *: "A \<in> sets N" unfolding A_def by simp
+ have "emeasure N A = 0"
+ proof -
+ {
+ assume asm: "emeasure N A > 0"
+ hence measure_pos: "measure N A > 0" unfolding emeasure_eq_measure by simp
+ hence "(1 / measure N A) *\<^sub>R set_lebesgue_integral N A f - v
+ = (1 / measure N A) *\<^sub>R set_lebesgue_integral N A (\<lambda>x. f x - v)"
+ using integrable integrable_const *
+ by (subst set_integral_diff(2), auto simp add: set_integrable_def set_integral_const[OF *] algebra_simps intro!: integrable_mult_indicator)
+ moreover have "norm (\<integral>x\<in>A. (f x - v)\<partial>N) \<le> (\<integral>x\<in>A. norm (f x - v)\<partial>N)"
+ using * by (auto intro!: integral_norm_bound[of N "\<lambda>x. indicator A x *\<^sub>R (f x - v)", THEN order_trans] integrable_mult_indicator integrable simp add: set_lebesgue_integral_def)
+ ultimately have "norm ((1 / measure N A) *\<^sub>R set_lebesgue_integral N A f - v)
+ \<le> set_lebesgue_integral N A (\<lambda>x. norm (f x - v)) / measure N A" using asm by (auto intro: divide_right_mono)
+ also have "\<dots> < set_lebesgue_integral N A (\<lambda>x. r) / measure N A"
+ unfolding set_lebesgue_integral_def
+ using asm * integrable integrable_const AE_less measure_pos
+ by (intro divide_strict_right_mono integral_less_AE[of _ _ A] integrable_mult_indicator)
+ (fastforce simp add: dist_less dist_norm indicator_def)+
+ also have "\<dots> = r" using * measure_pos by (simp add: set_integral_const)
+ finally have "dist ((1 / measure N A) *\<^sub>R set_lebesgue_integral N A f) v < r" by (subst dist_norm)
+ hence "False" using average[OF * measure_pos] by (metis ComplD dist_commute in_mono mem_ball ball_in_Compl)
+ }
+ thus ?thesis by fastforce
+ qed
+ }
+ note * = this
+ {
+ fix b' assume "b' \<in> B"
+ hence ball_subset_Compl: "b' \<subseteq> -S" and ball_radius_pos: "\<exists>v \<in> D. \<exists>r>0. b' = ball v r" using B_balls by (blast, fast)
+ }
+ note ** = this
+ hence "emeasure N (f -` b i \<inter> space N) = 0" for i by (cases "b i = {}", simp) (metis UnE singletonD * range_b[THEN eq_refl, THEN range_subsetD])
+ hence "emeasure N (\<Union>i. f -` b i \<inter> space N) = 0" using open_b by (intro emeasure_UN_eq_0) fastforce+
+ moreover have "(\<Union>i. f -` b i \<inter> space N) = f -` (\<Union>(range b)) \<inter> space N" by blast
+ ultimately have "emeasure N (f -` (-S) \<inter> space N) = 0" using Union_range_b by argo
+ hence "AE x in N. f x \<notin> -S" using open_Compl[OF assms(2)] by (intro AE_iff_measurable[THEN iffD2], auto)
+ thus ?case by force
+qed (simp add: pred_sets2[OF borel_closed] assms(2))
+
+lemma density_zero:
+ fixes f::"'a \<Rightarrow> 'b::{second_countable_topology, banach}"
+ assumes "integrable M f"
+ and density_0: "\<And>A. A \<in> sets M \<Longrightarrow> set_lebesgue_integral M A f = 0"
+ shows "AE x in M. f x = 0"
+ using averaging_theorem[OF assms(1), of "{0}"] assms(2)
+ by (simp add: scaleR_nonneg_nonneg)
+
+text \<open>The following lemma shows that densities are unique in Banach spaces.\<close>
+lemma density_unique_banach:
+ fixes f f'::"'a \<Rightarrow> 'b::{second_countable_topology, banach}"
+ assumes "integrable M f" "integrable M f'"
+ and density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> set_lebesgue_integral M A f = set_lebesgue_integral M A f'"
+ shows "AE x in M. f x = f' x"
+proof-
+ {
+ fix A assume asm: "A \<in> sets M"
+ hence "LINT x|M. indicat_real A x *\<^sub>R (f x - f' x) = 0" using density_eq assms(1,2) by (simp add: set_lebesgue_integral_def algebra_simps Bochner_Integration.integral_diff[OF integrable_mult_indicator(1,1)])
+ }
+ thus ?thesis using density_zero[OF Bochner_Integration.integrable_diff[OF assms(1,2)]] by (simp add: set_lebesgue_integral_def)
+qed
+
+lemma density_nonneg:
+ fixes f::"_ \<Rightarrow> 'b::{second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes "integrable M f"
+ and "\<And>A. A \<in> sets M \<Longrightarrow> set_lebesgue_integral M A f \<ge> 0"
+ shows "AE x in M. f x \<ge> 0"
+ using averaging_theorem[OF assms(1), of "{0..}", OF closed_atLeast] assms(2)
+ by (simp add: scaleR_nonneg_nonneg)
+
+corollary integral_nonneg_eq_0_iff_AE_banach:
+ fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \<le> f x"
+ shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
+proof
+ assume *: "integral\<^sup>L M f = 0"
+ {
+ fix A assume asm: "A \<in> sets M"
+ have "0 \<le> integral\<^sup>L M (\<lambda>x. indicator A x *\<^sub>R f x)" using nonneg by (subst integral_zero[of M, symmetric], intro integral_mono_AE_banach integrable_mult_indicator asm f integrable_zero, auto simp add: indicator_def)
+ moreover have "\<dots> \<le> integral\<^sup>L M f" using nonneg by (intro integral_mono_AE_banach integrable_mult_indicator asm f, auto simp add: indicator_def)
+ ultimately have "set_lebesgue_integral M A f = 0" unfolding set_lebesgue_integral_def using * by force
+ }
+ thus "AE x in M. f x = 0" by (intro density_zero f, blast)
+qed (auto simp add: integral_eq_zero_AE)
+
+corollary integral_eq_mono_AE_eq_AE:
+ fixes f g :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
+ assumes "integrable M f" "integrable M g" "integral\<^sup>L M f = integral\<^sup>L M g" "AE x in M. f x \<le> g x"
+ shows "AE x in M. f x = g x"
+proof -
+ define h where "h = (\<lambda>x. g x - f x)"
+ have "AE x in M. h x = 0" unfolding h_def using assms by (subst integral_nonneg_eq_0_iff_AE_banach[symmetric]) auto
+ then show ?thesis unfolding h_def by auto
+qed
+
end
+
+end