Theory Set_Integral
chapter ‹Integrals over a Set›
theory Set_Integral
imports Radon_Nikodym
begin
section ‹Notation›
definition "set_borel_measurable M A f ≡ (λx. indicator A x *⇩R f x) ∈ borel_measurable M"
definition "set_integrable M A f ≡ integrable M (λx. indicator A x *⇩R f x)"
definition "set_lebesgue_integral M A f ≡ lebesgue_integral M (λx. indicator A x *⇩R f x)"
syntax
"_ascii_set_lebesgue_integral" :: "pttrn ⇒ 'a set ⇒ 'a measure ⇒ real ⇒ real"
(‹(‹indent=4 notation=‹binder LINT››LINT (_):(_)/|(_)./ _)› [0,0,0,10] 10)
syntax_consts
"_ascii_set_lebesgue_integral" == set_lebesgue_integral
translations
"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (λx. f)"
section ‹Basic properties›
lemma set_integrable_cong:
assumes "M = M'" "A = A'" "⋀x. x ∈ A ⟹ f x = f' x"
shows "set_integrable M A f = set_integrable M' A' f'"
proof -
have "(λx. indicator A x *⇩R f x) = (λx. indicator A' x *⇩R f' x)"
using assms by (auto simp: indicator_def of_bool_def)
thus ?thesis by (simp add: set_integrable_def assms)
qed
lemma set_borel_measurable_sets:
fixes f :: "_ ⇒ _::real_normed_vector"
assumes "set_borel_measurable M X f" "B ∈ sets borel" "X ∈ sets M"
shows "f -` B ∩ X ∈ sets M"
proof -
have "f ∈ borel_measurable (restrict_space M X)"
using assms unfolding set_borel_measurable_def by (subst borel_measurable_restrict_space_iff) auto
then have "f -` B ∩ space (restrict_space M X) ∈ sets (restrict_space M X)"
by (rule measurable_sets) fact
with ‹X ∈ sets M› show ?thesis
by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
qed
lemma set_integrable_bound:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
and g :: "'a ⇒ 'c::{banach, second_countable_topology}"
assumes "set_integrable M A f" "set_borel_measurable M A g"
assumes "AE x in M. x ∈ A ⟶ norm (g x) ≤ norm (f x)"
shows "set_integrable M A g"
unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
from assms(1) show "integrable M (λx. indicator A x *⇩R f x)"
by (simp add: set_integrable_def)
from assms(2) show "(λx. indicat_real A x *⇩R g x) ∈ borel_measurable M"
by (simp add: set_borel_measurable_def)
from assms(3) show "AE x in M. norm (indicat_real A x *⇩R g x) ≤ norm (indicat_real A x *⇩R f x)"
by eventually_elim (simp add: indicator_def)
qed
lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (λx. 0) = 0"
by (auto simp: set_lebesgue_integral_def)
lemma set_lebesgue_integral_cong:
assumes "A ∈ sets M" and "∀x. x ∈ A ⟶ f x = g x"
shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
unfolding set_lebesgue_integral_def
using assms
by (metis indicator_simps(2) real_vector.scale_zero_left)
lemma set_lebesgue_integral_cong_AE:
assumes [measurable]: "A ∈ sets M" "f ∈ borel_measurable M" "g ∈ borel_measurable M"
assumes "AE x ∈ A in M. f x = g x"
shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
proof-
have "AE x in M. indicator A x *⇩R f x = indicator A x *⇩R g x"
using assms by auto
thus ?thesis
unfolding set_lebesgue_integral_def by (intro integral_cong_AE) auto
qed
lemma set_integrable_cong_AE:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹
AE x ∈ A in M. f x = g x ⟹ A ∈ sets M ⟹
set_integrable M A f = set_integrable M A g"
unfolding set_integrable_def
by (rule integrable_cong_AE) auto
lemma set_integrable_subset:
fixes M A B and f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "set_integrable M A f" "B ∈ sets M" "B ⊆ A"
shows "set_integrable M B f"
proof -
have "set_integrable M B (λx. indicator A x *⇩R f x)"
using assms integrable_mult_indicator set_integrable_def by blast
with ‹B ⊆ A› show ?thesis
unfolding set_integrable_def
by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
qed
lemma set_integrable_restrict_space:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes f: "set_integrable M S f" and T: "T ∈ sets (restrict_space M S)"
shows "set_integrable M T f"
proof -
obtain T' where T_eq: "T = S ∩ T'" and "T' ∈ sets M"
using T by (auto simp: sets_restrict_space)
have ‹integrable M (λx. indicator T' x *⇩R (indicator S x *⇩R f x))›
using ‹T' ∈ sets M› f integrable_mult_indicator set_integrable_def by blast
then show ?thesis
unfolding set_integrable_def
unfolding T_eq indicator_inter_arith by (simp add: ac_simps)
qed
lemma set_integral_scaleR_left:
assumes "A ∈ sets M" "c ≠ 0 ⟹ integrable M f"
shows "(LINT t:A|M. f t *⇩R c) = (LINT t:A|M. f t) *⇩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 *⇩R f t) = a *⇩R (LINT t:A|M. f t)"
unfolding set_lebesgue_integral_def
by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
lemma set_integral_mult_right [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
shows "(LINT t:A|M. a * f t) = a * (LINT t:A|M. f t)"
unfolding set_lebesgue_integral_def
by (subst integral_mult_right_zero[symmetric]) auto
lemma set_integral_mult_left [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
shows "(LINT t:A|M. f t * a) = (LINT t:A|M. f t) * a"
unfolding set_lebesgue_integral_def
by (subst integral_mult_left_zero[symmetric]) auto
lemma set_integral_divide_zero [simp]:
fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
shows "(LINT t:A|M. f t / a) = (LINT t:A|M. f t) / a"
unfolding set_lebesgue_integral_def
by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
(auto split: split_indicator)
lemma set_integrable_scaleR_right [simp, intro]:
shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. a *⇩R f t)"
unfolding set_integrable_def
unfolding scaleR_left_commute by (rule integrable_scaleR_right)
lemma set_integrable_scaleR_left [simp, intro]:
fixes a :: "_ :: {banach, second_countable_topology}"
shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. f t *⇩R a)"
unfolding set_integrable_def
using integrable_scaleR_left[of a M "λx. indicator A x *⇩R f x"] by simp
lemma set_integrable_mult_right [simp, intro]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. a * f t)"
unfolding set_integrable_def
using integrable_mult_right[of a M "λx. indicator A x *⇩R f x"] by simp
lemma set_integrable_mult_right_iff [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
assumes "a ≠ 0"
shows "set_integrable M A (λt. a * f t) ⟷ set_integrable M A f"
proof
assume "set_integrable M A (λt. a * f t)"
then have "set_integrable M A (λt. 1/a * (a * f t))"
using set_integrable_mult_right by blast
then show "set_integrable M A f"
using assms by auto
qed auto
lemma set_integrable_mult_left [simp, intro]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. f t * a)"
unfolding set_integrable_def
using integrable_mult_left[of a M "λx. indicator A x *⇩R f x"] by simp
lemma set_integrable_mult_left_iff [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
assumes "a ≠ 0"
shows "set_integrable M A (λt. f t * a) ⟷ set_integrable M A f"
using assms by (subst set_integrable_mult_right_iff [symmetric]) (auto simp: mult.commute)
lemma set_integrable_divide [simp, intro]:
fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
assumes "a ≠ 0 ⟹ set_integrable M A f"
shows "set_integrable M A (λt. f t / a)"
proof -
have "integrable M (λx. indicator A x *⇩R f x / a)"
using assms unfolding set_integrable_def by (rule integrable_divide_zero)
also have "(λx. indicator A x *⇩R f x / a) = (λx. indicator A x *⇩R (f x / a))"
by (auto split: split_indicator)
finally show ?thesis
unfolding set_integrable_def .
qed
lemma set_integrable_mult_divide_iff [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
assumes "a ≠ 0"
shows "set_integrable M A (λt. f t / a) ⟷ set_integrable M A f"
by (simp add: divide_inverse assms)
lemma set_integral_add [simp, intro]:
fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "set_integrable M A f" "set_integrable M A g"
shows "set_integrable M A (λx. f x + g x)"
and "(LINT x:A|M. f x + g x) = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
lemma set_integral_diff [simp, intro]:
assumes "set_integrable M A f" "set_integrable M A g"
shows "set_integrable M A (λx. f x - g x)" and "(LINT x:A|M. f x - g x) = (LINT x:A|M. f x) - (LINT x:A|M. g x)"
using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
lemma set_integral_uminus: "set_integrable M A f ⟹ (LINT x:A|M. - f x) = - (LINT x:A|M. f x)"
unfolding set_integrable_def set_lebesgue_integral_def
by (subst integral_minus[symmetric]) simp_all
lemma set_integral_complex_of_real:
"(LINT x:A|M. complex_of_real (f x)) = of_real (LINT x:A|M. f x)"
unfolding set_lebesgue_integral_def
by (subst integral_complex_of_real[symmetric])
(auto intro!: Bochner_Integration.integral_cong split: split_indicator)
lemma set_integral_mono:
fixes f g :: "_ ⇒ real"
assumes "set_integrable M A f" "set_integrable M A g"
"⋀x. x ∈ A ⟹ f x ≤ g x"
shows "(LINT x:A|M. f x) ≤ (LINT x:A|M. g x)"
using assms unfolding set_integrable_def set_lebesgue_integral_def
by (auto intro: integral_mono split: split_indicator)
lemma set_integral_mono_AE:
fixes f g :: "_ ⇒ real"
assumes "set_integrable M A f" "set_integrable M A g"
"AE x ∈ A in M. f x ≤ g x"
shows "(LINT x:A|M. f x) ≤ (LINT x:A|M. g x)"
using assms unfolding set_integrable_def set_lebesgue_integral_def
by (auto intro: integral_mono_AE split: split_indicator)
lemma set_integrable_abs: "set_integrable M A f ⟹ set_integrable M A (λx. ¦f x¦ :: real)"
using integrable_abs[of M "λx. f x * indicator A x"]unfolding set_integrable_def by (simp add: abs_mult ac_simps)
lemma set_integrable_abs_iff:
fixes f :: "_ ⇒ real"
shows "set_borel_measurable M A f ⟹ set_integrable M A (λx. ¦f x¦) = set_integrable M A f"
unfolding set_integrable_def set_borel_measurable_def
by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
lemma set_integrable_abs_iff':
fixes f :: "_ ⇒ real"
shows "f ∈ borel_measurable M ⟹ A ∈ sets M ⟹
set_integrable M A (λx. ¦f x¦) = set_integrable M A f"
by (simp add: set_borel_measurable_def set_integrable_abs_iff)
lemma set_integrable_discrete_difference:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "countable X"
assumes diff: "(A - B) ∪ (B - A) ⊆ X"
assumes "⋀x. x ∈ X ⟹ emeasure M {x} = 0" "⋀x. x ∈ X ⟹ {x} ∈ sets M"
shows "set_integrable M A f ⟷ set_integrable M B f"
unfolding set_integrable_def
proof (rule integrable_discrete_difference[where X=X])
show "⋀x. x ∈ space M ⟹ x ∉ X ⟹ indicator A x *⇩R f x = indicator B x *⇩R f x"
using diff by (auto split: split_indicator)
qed fact+
lemma set_integral_discrete_difference:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "countable X"
assumes diff: "(A - B) ∪ (B - A) ⊆ X"
assumes "⋀x. x ∈ X ⟹ emeasure M {x} = 0" "⋀x. x ∈ X ⟹ {x} ∈ sets M"
shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
unfolding set_lebesgue_integral_def
proof (rule integral_discrete_difference[where X=X])
show "⋀x. x ∈ space M ⟹ x ∉ X ⟹ indicator A x *⇩R f x = indicator B x *⇩R f x"
using diff by (auto split: split_indicator)
qed fact+
lemma set_integrable_Un:
fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes f_A: "set_integrable M A f" and f_B: "set_integrable M B f"
and [measurable]: "A ∈ sets M" "B ∈ sets M"
shows "set_integrable M (A ∪ B) f"
proof -
have "set_integrable M (A - B) f"
using f_A by (rule set_integrable_subset) auto
with f_B have "integrable M (λx. indicator (A - B) x *⇩R f x + indicator B x *⇩R f x)"
unfolding set_integrable_def using integrable_add by blast
then show ?thesis
unfolding set_integrable_def
by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
qed
lemma set_integrable_empty [simp]: "set_integrable M {} f"
by (auto simp: set_integrable_def)
lemma set_integrable_UN:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "finite I" "⋀i. i∈I ⟹ set_integrable M (A i) f"
"⋀i. i∈I ⟹ A i ∈ sets M"
shows "set_integrable M (⋃i∈I. A i) f"
using assms
by (induct I) (auto simp: set_integrable_Un sets.finite_UN)
lemma set_integral_Un:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "A ∩ B = {}"
and "set_integrable M A f"
and "set_integrable M B f"
shows "(LINT x:A∪B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
using assms
unfolding set_integrable_def set_lebesgue_integral_def
by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
lemma set_integral_cong_set:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
and ae: "AE x in M. x ∈ A ⟷ x ∈ B"
shows "(LINT x:B|M. f x) = (LINT x:A|M. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_cong_AE)
show "AE x in M. indicator B x *⇩R f x = indicator A x *⇩R f x"
using ae by (auto simp: subset_eq split: split_indicator)
qed (use assms in ‹auto simp: set_borel_measurable_def›)
proposition set_borel_measurable_subset:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes [measurable]: "set_borel_measurable M A f" "B ∈ sets M" and "B ⊆ A"
shows "set_borel_measurable M B f"
proof-
have "set_borel_measurable M B (λx. indicator A x *⇩R f x)"
using assms unfolding set_borel_measurable_def
using borel_measurable_indicator borel_measurable_scaleR by blast
moreover have "(λx. indicator B x *⇩R indicator A x *⇩R f x) = (λx. indicator B x *⇩R f x)"
using ‹B ⊆ A› by (auto simp: fun_eq_iff split: split_indicator)
ultimately show ?thesis
unfolding set_borel_measurable_def by simp
qed
lemma set_integral_Un_AE:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes ae: "AE x in M. ¬ (x ∈ A ∧ x ∈ B)" and [measurable]: "A ∈ sets M" "B ∈ sets M"
and "set_integrable M A f"
and "set_integrable M B f"
shows "(LINT x:A∪B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
proof -
have f: "set_integrable M (A ∪ B) f"
by (intro set_integrable_Un assms)
then have f': "set_borel_measurable M (A ∪ B) f"
using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
have "(LINT x:A∪B|M. f x) = (LINT x:(A - A ∩ B) ∪ (B - A ∩ B)|M. f x)"
proof (rule set_integral_cong_set)
show "AE x in M. (x ∈ A - A ∩ B ∪ (B - A ∩ B)) = (x ∈ A ∪ B)"
using ae by auto
show "set_borel_measurable M (A - A ∩ B ∪ (B - A ∩ B)) f"
using f' by (rule set_borel_measurable_subset) auto
qed fact
also have "… = (LINT x:(A - A ∩ B)|M. f x) + (LINT x:(B - A ∩ B)|M. f x)"
by (auto intro!: set_integral_Un set_integrable_subset[OF f])
also have "… = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
using ae
by (intro arg_cong2[where f="(+)"] set_integral_cong_set)
(auto intro!: set_borel_measurable_subset[OF f'])
finally show ?thesis .
qed
lemma set_integral_finite_Union:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "finite I" "disjoint_family_on A I"
and "⋀i. i ∈ I ⟹ set_integrable M (A i) f" "⋀i. i ∈ I ⟹ A i ∈ sets M"
shows "(LINT x:(⋃i∈I. A i)|M. f x) = (∑i∈I. LINT x:A i|M. f x)"
using assms
proof induction
case (insert x F)
then have "A x ∩ ⋃(A ` F) = {}"
by (meson disjoint_family_on_insert)
with insert show ?case
by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
qed (simp add: set_lebesgue_integral_def)
lemma pos_integrable_to_top:
fixes l::real
assumes "⋀i. A i ∈ sets M" "mono A"
assumes nneg: "⋀x i. x ∈ A i ⟹ 0 ≤ f x"
and intgbl: "⋀i::nat. set_integrable M (A i) f"
and lim: "(λi::nat. LINT x:A i|M. f x) ⇢ l"
shows "set_integrable M (⋃i. A i) f"
unfolding set_integrable_def
apply (rule integrable_monotone_convergence[where f = "λi::nat. λx. indicator (A i) x *⇩R f x" and x = l])
apply (rule intgbl [unfolded set_integrable_def])
prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
apply (rule AE_I2)
using ‹mono A› apply (auto simp: mono_def nneg split: split_indicator) []
proof (rule AE_I2)
{ fix x assume "x ∈ space M"
show "(λi. indicator (A i) x *⇩R f x) ⇢ indicator (⋃i. A i) x *⇩R f x"
proof cases
assume "∃i. x ∈ A i"
then obtain i where "x ∈ A i" ..
then have "∀⇩F i in sequentially. x ∈ A i"
using ‹x ∈ A i› ‹mono A› by (auto simp: eventually_sequentially mono_def)
with eventually_mono have "∀⇩F i in sequentially. indicat_real (A i) x *⇩R f x = indicat_real (⋃ (range A)) x *⇩R f x"
by fastforce
then show ?thesis
by (intro tendsto_eventually)
qed auto }
then show "(λx. indicator (⋃i. A i) x *⇩R f x) ∈ borel_measurable M"
apply (rule borel_measurable_LIMSEQ_real)
apply assumption
using intgbl set_integrable_def by blast
qed
text ‹Proof from Royden, \emph{Real Analysis}, p. 91.›
lemma lebesgue_integral_countable_add:
fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
assumes meas[intro]: "⋀i::nat. A i ∈ sets M"
and disj: "⋀i j. i ≠ j ⟹ A i ∩ A j = {}"
and intgbl: "set_integrable M (⋃i. A i) f"
shows "(LINT x:(⋃i. A i)|M. f x) = (∑i. (LINT x:(A i)|M. f x))"
unfolding set_lebesgue_integral_def
proof (subst integral_suminf[symmetric])
show int_A: "integrable M (λx. indicat_real (A i) x *⇩R f x)" for i
using intgbl unfolding set_integrable_def [symmetric]
by (rule set_integrable_subset) auto
{ fix x assume "x ∈ space M"
have "(λi. indicator (A i) x *⇩R f x) sums (indicator (⋃i. A i) x *⇩R f x)"
by (intro sums_scaleR_left indicator_sums) fact }
note sums = this
have norm_f: "⋀i. set_integrable M (A i) (λx. norm (f x))"
using int_A[THEN integrable_norm] unfolding set_integrable_def by auto
show "AE x in M. summable (λi. norm (indicator (A i) x *⇩R f x))"
using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
show "summable (λi. LINT x|M. norm (indicator (A i) x *⇩R f x))"
proof (rule summableI_nonneg_bounded)
fix n
show "0 ≤ LINT x|M. norm (indicator (A n) x *⇩R f x)"
using norm_f by (auto intro!: integral_nonneg_AE)
have "(∑i<n. LINT x|M. norm (indicator (A i) x *⇩R f x)) = (∑i<n. LINT x:A i|M. norm (f x))"
by (simp add: abs_mult set_lebesgue_integral_def)
also have "… = set_lebesgue_integral M (⋃i<n. A i) (λx. norm (f x))"
using norm_f
by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
also have "… ≤ set_lebesgue_integral M (⋃i. A i) (λx. norm (f x))"
using intgbl[unfolded set_integrable_def, THEN integrable_norm] norm_f
unfolding set_lebesgue_integral_def set_integrable_def
apply (intro integral_mono set_integrable_UN[of "{..<n}", unfolded set_integrable_def])
apply (auto split: split_indicator)
done
finally show "(∑i<n. LINT x|M. norm (indicator (A i) x *⇩R f x)) ≤
set_lebesgue_integral M (⋃i. A i) (λx. norm (f x))"
by simp
qed
show "LINT x|M. indicator (⋃(A ` UNIV)) x *⇩R f x = LINT x|M. (∑i. indicator (A i) x *⇩R f x)"
by (metis (no_types, lifting) integral_cong sums sums_unique)
qed
lemma set_integral_cont_up:
fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
assumes [measurable]: "⋀i. A i ∈ sets M" and A: "incseq A"
and intgbl: "set_integrable M (⋃i. A i) f"
shows "(λi. LINT x:(A i)|M. f x) ⇢ (LINT x:(⋃i. A i)|M. f x)"
unfolding set_lebesgue_integral_def
proof (intro integral_dominated_convergence[where w="λx. indicator (⋃i. A i) x *⇩R norm (f x)"])
have int_A: "⋀i. set_integrable M (A i) f"
using intgbl by (rule set_integrable_subset) auto
show "⋀i. (λx. indicator (A i) x *⇩R f x) ∈ borel_measurable M"
using int_A integrable_iff_bounded set_integrable_def by blast
show "(λx. indicator (⋃(A ` UNIV)) x *⇩R f x) ∈ borel_measurable M"
using integrable_iff_bounded intgbl set_integrable_def by blast
show "integrable M (λx. indicator (⋃i. A i) x *⇩R norm (f x))"
using int_A intgbl integrable_norm unfolding set_integrable_def
by fastforce
{ fix x i assume "x ∈ A i"
with A have "(λxa. indicator (A xa) x::real) ⇢ 1 ⟷ (λxa. 1::real) ⇢ 1"
by (intro filterlim_cong refl)
(fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
then show "AE x in M. (λi. indicator (A i) x *⇩R f x) ⇢ indicator (⋃i. A i) x *⇩R f x"
by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
qed (auto split: split_indicator)
lemma set_integral_cont_down:
fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
assumes [measurable]: "⋀i. A i ∈ sets M" and A: "decseq A"
and int0: "set_integrable M (A 0) f"
shows "(λi::nat. LINT x:(A i)|M. f x) ⇢ (LINT x:(⋂i. A i)|M. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
have int_A: "⋀i. set_integrable M (A i) f"
using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
have "integrable M (λc. norm (indicat_real (A 0) c *⇩R f c))"
by (metis (no_types) int0 integrable_norm set_integrable_def)
then show "integrable M (λx. indicator (A 0) x *⇩R norm (f x))"
by force
have "set_integrable M (⋂i. A i) f"
using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
with int_A show "(λx. indicat_real (⋂(A ` UNIV)) x *⇩R f x) ∈ borel_measurable M"
"⋀i. (λx. indicat_real (A i) x *⇩R f x) ∈ borel_measurable M"
by (auto simp: set_integrable_def)
show "⋀i. AE x in M. norm (indicator (A i) x *⇩R f x) ≤ indicator (A 0) x *⇩R norm (f x)"
using A by (auto split: split_indicator simp: decseq_def)
{ fix x i assume "x ∈ space M" "x ∉ A i"
with A have "(λi. indicator (A i) x::real) ⇢ 0 ⟷ (λi. 0::real) ⇢ 0"
by (intro filterlim_cong refl)
(auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
then show "AE x in M. (λi. indicator (A i) x *⇩R f x) ⇢ indicator (⋂i. A i) x *⇩R f x"
by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
qed
lemma set_integral_at_point:
fixes a :: real
assumes "set_integrable M {a} f"
and [simp]: "{a} ∈ sets M" and "(emeasure M) {a} ≠ ∞"
shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
proof-
have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
by (intro set_lebesgue_integral_cong) simp_all
then show ?thesis using assms
unfolding set_lebesgue_integral_def by simp
qed
section ‹Complex integrals›
abbreviation complex_integrable :: "'a measure ⇒ ('a ⇒ complex) ⇒ bool" where
"complex_integrable M f ≡ integrable M f"
abbreviation complex_lebesgue_integral :: "'a measure ⇒ ('a ⇒ complex) ⇒ complex" (‹integral⇧C›) where
"integral⇧C M f == integral⇧L M f"
syntax
"_complex_lebesgue_integral" :: "pttrn ⇒ complex ⇒ 'a measure ⇒ complex"
(‹(‹open_block notation=‹binder integral››∫⇧C _. _ ∂_)› [0,0] 110)
syntax_consts
"_complex_lebesgue_integral" == complex_lebesgue_integral
translations
"∫⇧Cx. f ∂M" == "CONST complex_lebesgue_integral M (λx. f)"
syntax
"_ascii_complex_lebesgue_integral" :: "pttrn ⇒ 'a measure ⇒ real ⇒ real"
(‹(‹indent=3 notation=‹binder CLINT››CLINT _|_. _)› [0,0,10] 10)
syntax_consts
"_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
translations
"CLINT x|M. f" == "CONST complex_lebesgue_integral M (λx. f)"
lemma complex_integrable_cnj [simp]:
"complex_integrable M (λx. cnj (f x)) ⟷ complex_integrable M f"
proof
assume "complex_integrable M (λx. cnj (f x))"
then have "complex_integrable M (λx. cnj (cnj (f x)))"
by (rule integrable_cnj)
then show "complex_integrable M f"
by simp
qed simp
lemma complex_of_real_integrable_eq:
"complex_integrable M (λx. complex_of_real (f x)) ⟷ integrable M f"
proof
assume "complex_integrable M (λx. complex_of_real (f x))"
then have "integrable M (λx. Re (complex_of_real (f x)))"
by (rule integrable_Re)
then show "integrable M f"
by simp
qed simp
abbreviation complex_set_integrable :: "'a measure ⇒ 'a set ⇒ ('a ⇒ complex) ⇒ bool" where
"complex_set_integrable M A f ≡ set_integrable M A f"
abbreviation complex_set_lebesgue_integral :: "'a measure ⇒ 'a set ⇒ ('a ⇒ complex) ⇒ complex" where
"complex_set_lebesgue_integral M A f ≡ set_lebesgue_integral M A f"
syntax
"_ascii_complex_set_lebesgue_integral" :: "pttrn ⇒ 'a set ⇒ 'a measure ⇒ real ⇒ real"
(‹(‹indent=4 notation=‹binder CLINT››CLINT _:_|_. _)› [0,0,0,10] 10)
syntax_consts
"_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (λx. f)"
lemma set_measurable_continuous_on_ivl:
assumes "continuous_on {a..b} (f :: real ⇒ real)"
shows "set_borel_measurable borel {a..b} f"
unfolding set_borel_measurable_def
by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
section ‹NN Set Integrals›
text‹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.›
abbreviation "set_nn_integral M A f ≡ nn_integral M (λx. f x * indicator A x)"
syntax
"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
(‹(‹notation=‹binder integral››∫⇧+((_)∈(_)./ _)/∂_)› [0,0,0,110] 10)
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
(‹(‹notation=‹binder integral››∫((_)∈(_)./ _)/∂_)› [0,0,0,110] 10)
syntax_consts
"_set_nn_integral" == set_nn_integral and
"_set_lebesgue_integral" == set_lebesgue_integral
translations
"∫⇧+x ∈ A. f ∂M" == "CONST set_nn_integral M A (λx. f)"
"∫x ∈ A. f ∂M" == "CONST set_lebesgue_integral M A (λx. f)"
lemma set_nn_integral_cong:
assumes "M = M'" "A = B" "⋀x. x ∈ space M ∩ A ⟹ f x = g x"
shows "set_nn_integral M A f = set_nn_integral M' B g"
by (metis (mono_tags, lifting) IntI assms indicator_simps(2) mult_eq_0_iff nn_integral_cong)
lemma nn_integral_disjoint_pair:
assumes [measurable]: "f ∈ borel_measurable M"
"B ∈ sets M" "C ∈ sets M"
"B ∩ C = {}"
shows "(∫⇧+x ∈ B ∪ C. f x ∂M) = (∫⇧+x ∈ B. f x ∂M) + (∫⇧+x ∈ C. f x ∂M)"
proof -
have mes: "⋀D. D ∈ sets M ⟹ (λx. f x * indicator D x) ∈ borel_measurable M" by simp
have pos: "⋀D. AE x in M. f x * indicator D x ≥ 0" using assms(2) by auto
have "⋀x. f x * indicator (B ∪ C) x = f x * indicator B x + f x * indicator C x" using assms(4)
by (auto split: split_indicator)
then have "(∫⇧+x. f x * indicator (B ∪ C) x ∂M) = (∫⇧+x. f x * indicator B x + f x * indicator C x ∂M)"
by simp
also have "… = (∫⇧+x. f x * indicator B x ∂M) + (∫⇧+x. f x * indicator C x ∂M)"
by (rule nn_integral_add) (auto simp add: assms mes pos)
finally show ?thesis by simp
qed
lemma nn_integral_disjoint_pair_countspace:
assumes "B ∩ C = {}"
shows "(∫⇧+x ∈ B ∪ C. f x ∂count_space UNIV) = (∫⇧+x ∈ B. f x ∂count_space UNIV) + (∫⇧+x ∈ C. f x ∂count_space UNIV)"
by (rule nn_integral_disjoint_pair) (simp_all add: assms)
lemma nn_integral_null_delta:
assumes "A ∈ sets M" "B ∈ sets M"
"(A - B) ∪ (B - A) ∈ null_sets M"
shows "(∫⇧+x ∈ A. f x ∂M) = (∫⇧+x ∈ B. f x ∂M)"
proof (rule nn_integral_cong_AE)
have *: "AE a in M. a ∉ (A - B) ∪ (B - A)"
using assms(3) AE_not_in by blast
then show ‹AE x in M. f x * indicator A x = f x * indicator B x›
by auto
qed
proposition nn_integral_disjoint_family:
assumes [measurable]: "f ∈ borel_measurable M" "⋀(n::nat). B n ∈ sets M"
and "disjoint_family B"
shows "(∫⇧+x ∈ (⋃n. B n). f x ∂M) = (∑n. (∫⇧+x ∈ B n. f x ∂M))"
proof -
have "(∫⇧+ x. (∑n. f x * indicator (B n) x) ∂M) = (∑n. (∫⇧+ x. f x * indicator (B n) x ∂M))"
by (rule nn_integral_suminf) simp
moreover have "(∑n. f x * indicator (B n) x) = f x * indicator (⋃n. B n) x" for x
proof (cases)
assume "x ∈ (⋃n. B n)"
then obtain n where "x ∈ B n" by blast
have a: "finite {n}" by simp
have "⋀i. i ≠ n ⟹ x ∉ B i" using ‹x ∈ B n› assms(3) disjoint_family_on_def
by (metis IntI UNIV_I empty_iff)
then have "⋀i. i ∉ {n} ⟹ indicator (B i) x = (0::ennreal)" using indicator_def by simp
then have b: "⋀i. i ∉ {n} ⟹ f x * indicator (B i) x = (0::ennreal)" by simp
define h where "h = (λi. f x * indicator (B i) x)"
then have "⋀i. i ∉ {n} ⟹ h i = 0" using b by simp
then have "(∑i. h i) = (∑i∈{n}. h i)"
by (metis sums_unique[OF sums_finite[OF a]])
then have "(∑i. h i) = h n" by simp
then have "(∑n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
then have "(∑n. f x * indicator (B n) x) = f x" using ‹x ∈ B n› indicator_def by simp
then show ?thesis using ‹x ∈ (⋃n. B n)› by auto
next
assume "x ∉ (⋃n. B n)"
then have "⋀n. f x * indicator (B n) x = 0" by simp
have "(∑n. f x * indicator (B n) x) = 0"
by (simp add: ‹⋀n. f x * indicator (B n) x = 0›)
then show ?thesis using ‹x ∉ (⋃n. B n)› by auto
qed
ultimately show ?thesis by simp
qed
lemma nn_set_integral_add:
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
"A ∈ sets M"
shows "(∫⇧+x ∈ A. (f x + g x) ∂M) = (∫⇧+x ∈ A. f x ∂M) + (∫⇧+x ∈ A. g x ∂M)"
proof -
have "(∫⇧+x ∈ A. (f x + g x) ∂M) = (∫⇧+x. (f x * indicator A x + g x * indicator A x) ∂M)"
by (auto simp add: indicator_def intro!: nn_integral_cong)
also have "… = (∫⇧+x. f x * indicator A x ∂M) + (∫⇧+x. g x * indicator A x ∂M)"
apply (rule nn_integral_add) using assms(1) assms(2) by auto
finally show ?thesis by simp
qed
lemma nn_set_integral_cong:
assumes "AE x in M. f x = g x"
shows "(∫⇧+x ∈ A. f x ∂M) = (∫⇧+x ∈ A. g x ∂M)"
apply (rule nn_integral_cong_AE) using assms(1) by auto
lemma nn_set_integral_set_mono:
"A ⊆ B ⟹ (∫⇧+ x ∈ A. f x ∂M) ≤ (∫⇧+ x ∈ B. f x ∂M)"
by (auto intro!: nn_integral_mono split: split_indicator)
lemma nn_set_integral_mono:
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
"A ∈ sets M"
and "AE x∈A in M. f x ≤ g x"
shows "(∫⇧+x ∈ A. f x ∂M) ≤ (∫⇧+x ∈ A. g x ∂M)"
by (auto intro!: nn_integral_mono_AE split: split_indicator simp: assms)
lemma nn_set_integral_space [simp]:
shows "(∫⇧+ x ∈ space M. f x ∂M) = (∫⇧+x. f x ∂M)"
by (metis (mono_tags, lifting) indicator_simps(1) mult.right_neutral nn_integral_cong)
lemma nn_integral_count_compose_inj:
assumes "inj_on g A"
shows "(∫⇧+x ∈ A. f (g x) ∂count_space UNIV) = (∫⇧+y ∈ g`A. f y ∂count_space UNIV)"
proof -
have "(∫⇧+x ∈ A. f (g x) ∂count_space UNIV) = (∫⇧+x. f (g x) ∂count_space A)"
by (auto simp add: nn_integral_count_space_indicator[symmetric])
also have "… = (∫⇧+y. f y ∂count_space (g`A))"
by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
also have "… = (∫⇧+y ∈ g`A. f y ∂count_space UNIV)"
by (auto simp add: nn_integral_count_space_indicator[symmetric])
finally show ?thesis by simp
qed
lemma nn_integral_count_compose_bij:
assumes "bij_betw g A B"
shows "(∫⇧+x ∈ A. f (g x) ∂count_space UNIV) = (∫⇧+y ∈ B. f y ∂count_space UNIV)"
proof -
have "inj_on g A" using assms bij_betw_def by auto
then have "(∫⇧+x ∈ A. f (g x) ∂count_space UNIV) = (∫⇧+y ∈ g`A. f y ∂count_space UNIV)"
by (rule nn_integral_count_compose_inj)
then show ?thesis using assms by (simp add: bij_betw_def)
qed
lemma set_integral_null_delta:
fixes f::"_ ⇒ _ :: {banach, second_countable_topology}"
assumes [measurable]: "integrable M f" "A ∈ sets M" "B ∈ sets M"
and null: "(A - B) ∪ (B - A) ∈ null_sets M"
shows "(∫x ∈ A. f x ∂M) = (∫x ∈ B. f x ∂M)"
proof (rule set_integral_cong_set)
have *: "AE a in M. a ∉ (A - B) ∪ (B - A)"
using null AE_not_in by blast
then show "AE x in M. (x ∈ B) = (x ∈ A)"
by auto
qed (simp_all add: set_borel_measurable_def)
lemma set_integral_space:
assumes "integrable M f"
shows "(∫x ∈ space M. f x ∂M) = (∫x. f x ∂M)"
by (metis (no_types, lifting) indicator_simps(1) integral_cong scaleR_one set_lebesgue_integral_def)
lemma null_if_pos_func_has_zero_nn_int:
fixes f::"'a ⇒ ennreal"
assumes [measurable]: "f ∈ borel_measurable M" "A ∈ sets M"
and "AE x∈A in M. f x > 0" "(∫⇧+x∈A. f x ∂M) = 0"
shows "A ∈ null_sets M"
proof -
have "AE x in M. f x * indicator A x = 0"
by (subst nn_integral_0_iff_AE[symmetric], auto simp add: assms(4))
then have "AE x∈A in M. False" using assms(3) by auto
then show "A ∈ null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
qed
lemma null_if_pos_func_has_zero_int:
assumes [measurable]: "integrable M f" "A ∈ sets M"
and "AE x∈A in M. f x > 0" "(∫x∈A. f x ∂M) = (0::real)"
shows "A ∈ null_sets M"
proof -
have "AE x in M. indicator A x * f x = 0"
apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
using assms integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)]
by (auto simp: set_lebesgue_integral_def)
then have "AE x∈A in M. f x = 0" by auto
then have "AE x∈A in M. False" using assms(3) by auto
then show "A ∈ null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
qed
text‹The next lemma is a variant of ‹density_unique›. Note that it uses the notation
for nonnegative set integrals introduced earlier.›
lemma (in sigma_finite_measure) density_unique2:
assumes [measurable]: "f ∈ borel_measurable M" "f' ∈ borel_measurable M"
assumes density_eq: "⋀A. A ∈ sets M ⟹ (∫⇧+ x ∈ A. f x ∂M) = (∫⇧+ x ∈ A. f' x ∂M)"
shows "AE x in M. f x = f' x"
proof (rule density_unique)
show "density M f = density M f'"
by (intro measure_eqI) (auto simp: emeasure_density intro!: density_eq)
qed (auto simp add: assms)
text ‹The next lemma implies the same statement for Banach-space valued functions
using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
only formulate it for real-valued functions.›
lemma density_unique_real:
fixes f f'::"_ ⇒ real"
assumes M[measurable]: "integrable M f" "integrable M f'"
assumes density_eq: "⋀A. A ∈ sets M ⟹ (∫x ∈ A. f x ∂M) = (∫x ∈ A. f' x ∂M)"
shows "AE x in M. f x = f' x"
proof -
define A where "A = {x ∈ space M. f x < f' x}"
then have [measurable]: "A ∈ sets M" by simp
have "(∫x ∈ A. (f' x - f x) ∂M) = (∫x ∈ A. f' x ∂M) - (∫x ∈ A. f x ∂M)"
using ‹A ∈ sets M› M integrable_mult_indicator set_integrable_def by blast
then have "(∫x ∈ A. (f' x - f x) ∂M) = 0" using assms(3) by simp
then have "A ∈ null_sets M"
using A_def null_if_pos_func_has_zero_int[where ?f = "λx. f' x - f x" and ?A = A] assms by auto
then have "AE x in M. x ∉ A" by (simp add: AE_not_in)
then have *: "AE x in M. f' x ≤ f x" unfolding A_def by auto
define B where "B = {x ∈ space M. f' x < f x}"
then have [measurable]: "B ∈ sets M" by simp
have "(∫x ∈ B. (f x - f' x) ∂M) = (∫x ∈ B. f x ∂M) - (∫x ∈ B. f' x ∂M)"
using ‹B ∈ sets M› M integrable_mult_indicator set_integrable_def by blast
then have "(∫x ∈ B. (f x - f' x) ∂M) = 0" using assms(3) by simp
then have "B ∈ null_sets M"
using B_def null_if_pos_func_has_zero_int[where ?f = "λx. f x - f' x" and ?A = B] assms by auto
then have "AE x in M. x ∉ B" by (simp add: AE_not_in)
then have "AE x in M. f' x ≥ f x" unfolding B_def by auto
then show ?thesis using * by auto
qed
section ‹Scheffé's lemma›
text ‹The next lemma shows that ‹L⇧1› 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
variations) are known as Scheffe lemma.
The formalization is more painful as one should jump back and forth between reals and ereals and justify
all the time positivity or integrability (thankfully, measurability is handled more or less automatically).›
proposition Scheffe_lemma1:
assumes "⋀n. integrable M (F n)" "integrable M f"
"AE x in M. (λn. F n x) ⇢ f x"
"limsup (λn. ∫⇧+ x. norm(F n x) ∂M) ≤ (∫⇧+ x. norm(f x) ∂M)"
shows "(λn. ∫⇧+ x. norm(F n x - f x) ∂M) ⇢ 0"
proof -
have [measurable]: "⋀n. F n ∈ borel_measurable M" "f ∈ borel_measurable M"
using assms(1) assms(2) by simp_all
define G where "G = (λn x. norm(f x) + norm(F n x) - norm(F n x - f x))"
have [measurable]: "⋀n. G n ∈ borel_measurable M" unfolding G_def by simp
have G_pos[simp]: "⋀n x. G n x ≥ 0"
unfolding G_def by (metis ge_iff_diff_ge_0 norm_minus_commute norm_triangle_ineq4)
have finint: "(∫⇧+ x. norm(f x) ∂M) ≠ ∞"
using has_bochner_integral_implies_finite_norm[OF has_bochner_integral_integrable[OF ‹integrable M f›]]
by simp
then have fin2: "2 * (∫⇧+ x. norm(f x) ∂M) ≠ ∞"
by (auto simp: ennreal_mult_eq_top_iff)
{
fix x assume *: "(λn. F n x) ⇢ f x"
then have "(λn. norm(F n x)) ⇢ norm(f x)" using tendsto_norm by blast
moreover have "(λn. norm(F n x - f x)) ⇢ 0" using * Lim_null tendsto_norm_zero_iff by fastforce
ultimately have a: "(λn. norm(F n x) - norm(F n x - f x)) ⇢ norm(f x)" using tendsto_diff by fastforce
have "(λn. norm(f x) + (norm(F n x) - norm(F n x - f x))) ⇢ norm(f x) + norm(f x)"
by (rule tendsto_add) (auto simp add: a)
moreover have "⋀n. G n x = norm(f x) + (norm(F n x) - norm(F n x - f x))" unfolding G_def by simp
ultimately have "(λn. G n x) ⇢ 2 * norm(f x)" by simp
then have "(λn. ennreal(G n x)) ⇢ ennreal(2 * norm(f x))" by simp
then have "liminf (λn. ennreal(G n x)) = ennreal(2 * norm(f x))"
using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
}
then have "AE x in M. liminf (λn. ennreal(G n x)) = ennreal(2 * norm(f x))" using assms(3) by auto
then have "(∫⇧+ x. liminf (λn. ennreal (G n x)) ∂M) = (∫⇧+ x. 2 * ennreal(norm(f x)) ∂M)"
by (simp add: nn_integral_cong_AE ennreal_mult)
also have "… = 2 * (∫⇧+ x. norm(f x) ∂M)" by (rule nn_integral_cmult) auto
finally have int_liminf: "(∫⇧+ x. liminf (λn. ennreal (G n x)) ∂M) = 2 * (∫⇧+ x. norm(f x) ∂M)"
by simp
have "(∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M) = (∫⇧+x. norm(f x) ∂M) + (∫⇧+x. norm(F n x) ∂M)" for n
by (rule nn_integral_add) (auto simp add: assms)
then have "limsup (λn. (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M)) =
limsup (λn. (∫⇧+x. norm(f x) ∂M) + (∫⇧+x. norm(F n x) ∂M))"
by simp
also have "… = (∫⇧+x. norm(f x) ∂M) + limsup (λn. (∫⇧+x. norm(F n x) ∂M))"
by (rule Limsup_const_add, auto simp add: finint)
also have "… ≤ (∫⇧+x. norm(f x) ∂M) + (∫⇧+x. norm(f x) ∂M)"
using assms(4) by (simp add: add_left_mono)
also have "… = 2 * (∫⇧+x. norm(f x) ∂M)"
unfolding one_add_one[symmetric] distrib_right by simp
ultimately have a: "limsup (λn. (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M)) ≤
2 * (∫⇧+x. norm(f x) ∂M)" by simp
have le: "ennreal (norm (F n x - f x)) ≤ ennreal (norm (f x)) + ennreal (norm (F n x))" for n x
by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus flip: ennreal_plus)
then have le2: "(∫⇧+ x. ennreal (norm (F n x - f x)) ∂M) ≤ (∫⇧+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) ∂M)" for n
by (rule nn_integral_mono)
have "2 * (∫⇧+ x. norm(f x) ∂M) = (∫⇧+ x. liminf (λn. ennreal (G n x)) ∂M)"
by (simp add: int_liminf)
also have "… ≤ liminf (λn. (∫⇧+x. G n x ∂M))"
by (rule nn_integral_liminf) auto
also have "liminf (λn. (∫⇧+x. G n x ∂M)) =
liminf (λn. (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M) - (∫⇧+x. norm(F n x - f x) ∂M))"
proof (intro arg_cong[where f=liminf] ext)
fix n
have "⋀x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))"
unfolding G_def by (simp add: ennreal_minus flip: ennreal_plus)
moreover have "(∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) ∂M)
= (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M) - (∫⇧+x. norm(F n x - f x) ∂M)"
proof (rule nn_integral_diff)
from le show "AE x in M. ennreal (norm (F n x - f x)) ≤ ennreal (norm (f x)) + ennreal (norm (F n x))"
by simp
from le2 have "(∫⇧+x. ennreal (norm (F n x - f x)) ∂M) < ∞" using assms(1) assms(2)
by (metis has_bochner_integral_implies_finite_norm integrable.simps Bochner_Integration.integrable_diff)
then show "(∫⇧+x. ennreal (norm (F n x - f x)) ∂M) ≠ ∞" by simp
qed (auto simp add: assms)
ultimately show "(∫⇧+x. G n x ∂M) = (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M) - (∫⇧+x. norm(F n x - f x) ∂M)"
by simp
qed
finally have "2 * (∫⇧+ x. norm(f x) ∂M) + limsup (λn. (∫⇧+x. norm(F n x - f x) ∂M)) ≤
liminf (λn. (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M) - (∫⇧+x. norm(F n x - f x) ∂M)) +
limsup (λn. (∫⇧+x. norm(F n x - f x) ∂M))"
by (intro add_mono) auto
also have "… ≤ (limsup (λn. ∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M) - limsup (λn. ∫⇧+x. norm (F n x - f x) ∂M)) +
limsup (λn. (∫⇧+x. norm(F n x - f x) ∂M))"
by (intro add_mono liminf_minus_ennreal le2) auto
also have "… = limsup (λn. (∫⇧+x. ennreal(norm(f x)) + ennreal(norm(F n x)) ∂M))"
by (intro diff_add_cancel_ennreal Limsup_mono always_eventually allI le2)
also have "… ≤ 2 * (∫⇧+x. norm(f x) ∂M)"
by fact
finally have "limsup (λn. (∫⇧+x. norm(F n x - f x) ∂M)) = 0"
using fin2 by simp
then show ?thesis
by (rule tendsto_0_if_Limsup_eq_0_ennreal)
qed
proposition Scheffe_lemma2:
fixes F::"nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
assumes "⋀ n::nat. F n ∈ borel_measurable M" "integrable M f"
"AE x in M. (λn. F n x) ⇢ f x"
"⋀n. (∫⇧+ x. norm(F n x) ∂M) ≤ (∫⇧+ x. norm(f x) ∂M)"
shows "(λn. ∫⇧+ x. norm(F n x - f x) ∂M) ⇢ 0"
proof (rule Scheffe_lemma1)
fix n::nat
have "(∫⇧+ x. norm(f x) ∂M) < ∞" using assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.cases)
then have "(∫⇧+ x. norm(F n x) ∂M) < ∞" using assms(4)[of n] by auto
then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
qed (auto simp add: assms Limsup_bounded)
lemma tendsto_set_lebesgue_integral_at_right:
fixes a b :: real and f :: "real ⇒ 'a :: {banach,second_countable_topology}"
assumes "a < b" and sets: "⋀a'. a' ∈ {a<..b} ⟹ {a'..b} ∈ sets M"
and "set_integrable M {a<..b} f"
shows "((λa'. set_lebesgue_integral M {a'..b} f) ⤏
set_lebesgue_integral M {a<..b} f) (at_right a)"
proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
case (1 S)
have eq: "(⋃n. {S n..b}) = {a<..b}"
proof safe
fix x n assume "x ∈ {S n..b}"
with 1(1,2)[of n] show "x ∈ {a<..b}" by auto
next
fix x assume "x ∈ {a<..b}"
with order_tendstoD[OF ‹S ⇢ a›, of x] show "x ∈ (⋃n. {S n..b})"
by (force simp: eventually_at_top_linorder dest: less_imp_le)
qed
have "(λn. set_lebesgue_integral M {S n..b} f) ⇢ set_lebesgue_integral M (⋃n. {S n..b}) f"
by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
with eq show ?case by simp
qed
section ‹Convergence of integrals over an interval›
text ‹
The next lemmas relate convergence of integrals over an interval to
improper integrals.
›
lemma tendsto_set_lebesgue_integral_at_left:
fixes a b :: real and f :: "real ⇒ 'a :: {banach,second_countable_topology}"
assumes "a < b" and sets: "⋀b'. b' ∈ {a..<b} ⟹ {a..b'} ∈ sets M"
and "set_integrable M {a..<b} f"
shows "((λb'. set_lebesgue_integral M {a..b'} f) ⤏
set_lebesgue_integral M {a..<b} f) (at_left b)"
proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
case (1 S)
have eq: "(⋃n. {a..S n}) = {a..<b}"
proof safe
fix x n assume "x ∈ {a..S n}"
with 1(1,2)[of n] show "x ∈ {a..<b}" by auto
next
fix x assume "x ∈ {a..<b}"
with order_tendstoD[OF ‹S ⇢ b›, of x] show "x ∈ (⋃n. {a..S n})"
by (force simp: eventually_at_top_linorder dest: less_imp_le)
qed
have "(λn. set_lebesgue_integral M {a..S n} f) ⇢ set_lebesgue_integral M (⋃n. {a..S n}) f"
by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
with eq show ?case by simp
qed
proposition tendsto_set_lebesgue_integral_at_top:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}"
assumes sets: "⋀b. b ≥ a ⟹ {a..b} ∈ sets M"
and int: "set_integrable M {a..} f"
shows "((λb. set_lebesgue_integral M {a..b} f) ⤏ set_lebesgue_integral M {a..} f) at_top"
proof (rule tendsto_at_topI_sequentially)
fix X :: "nat ⇒ real" assume "filterlim X at_top sequentially"
show "(λn. set_lebesgue_integral M {a..X n} f) ⇢ set_lebesgue_integral M {a..} f"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
show "integrable M (λx. indicat_real {a..} x *⇩R norm (f x))"
using integrable_norm[OF int[unfolded set_integrable_def]] by simp
show "AE x in M. (λn. indicator {a..X n} x *⇩R f x) ⇢ indicat_real {a..} x *⇩R f x"
proof
fix x
from ‹filterlim X at_top sequentially›
have "eventually (λn. x ≤ X n) sequentially"
unfolding filterlim_at_top_ge[where c=x] by auto
then show "(λn. indicator {a..X n} x *⇩R f x) ⇢ indicat_real {a..} x *⇩R f x"
by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {a..X n} x *⇩R f x) ≤
indicator {a..} x *⇩R norm (f x)"
by (auto split: split_indicator)
next
from int show "(λx. indicat_real {a..} x *⇩R f x) ∈ borel_measurable M"
by (simp add: set_integrable_def)
next
fix n :: nat
from sets have "{a..X n} ∈ sets M" by (cases "X n ≥ a") auto
with int have "set_integrable M {a..X n} f"
by (rule set_integrable_subset) auto
thus "(λx. indicat_real {a..X n} x *⇩R f x) ∈ borel_measurable M"
by (simp add: set_integrable_def)
qed
qed
proposition tendsto_set_lebesgue_integral_at_bot:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}"
assumes sets: "⋀a. a ≤ b ⟹ {a..b} ∈ sets M"
and int: "set_integrable M {..b} f"
shows "((λa. set_lebesgue_integral M {a..b} f) ⤏ set_lebesgue_integral M {..b} f) at_bot"
proof (rule tendsto_at_botI_sequentially)
fix X :: "nat ⇒ real" assume "filterlim X at_bot sequentially"
show "(λn. set_lebesgue_integral M {X n..b} f) ⇢ set_lebesgue_integral M {..b} f"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
show "integrable M (λx. indicat_real {..b} x *⇩R norm (f x))"
using integrable_norm[OF int[unfolded set_integrable_def]] by simp
show "AE x in M. (λn. indicator {X n..b} x *⇩R f x) ⇢ indicat_real {..b} x *⇩R f x"
proof
fix x
from ‹filterlim X at_bot sequentially›
have "eventually (λn. x ≥ X n) sequentially"
unfolding filterlim_at_bot_le[where c=x] by auto
then show "(λn. indicator {X n..b} x *⇩R f x) ⇢ indicat_real {..b} x *⇩R f x"
by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {X n..b} x *⇩R f x) ≤
indicator {..b} x *⇩R norm (f x)"
by (auto split: split_indicator)
next
from int show "(λx. indicat_real {..b} x *⇩R f x) ∈ borel_measurable M"
by (simp add: set_integrable_def)
next
fix n :: nat
from sets have "{X n..b} ∈ sets M" by (cases "X n ≤ b") auto
with int have "set_integrable M {X n..b} f"
by (rule set_integrable_subset) auto
thus "(λx. indicat_real {X n..b} x *⇩R f x) ∈ borel_measurable M"
by (simp add: set_integrable_def)
qed
qed
theorem integral_Markov_inequality':
fixes u :: "'a ⇒ real"
assumes [measurable]: "set_integrable M A u" and "A ∈ sets M"
assumes "AE x in M. x ∈ A ⟶ u x ≥ 0" and "0 < (c::real)"
shows "emeasure M {x∈A. u x ≥ c} ≤ (1/c::real) * (∫x∈A. u x ∂M)"
proof -
have "(λx. u x * indicator A x) ∈ borel_measurable M"
using assms by (auto simp: set_integrable_def mult_ac)
hence "(λx. ennreal (u x * indicator A x)) ∈ borel_measurable M"
by measurable
also have "(λx. ennreal (u x * indicator A x)) = (λx. ennreal (u x) * indicator A x)"
by (intro ext) (auto simp: indicator_def)
finally have meas: "… ∈ borel_measurable M" .
from assms(3) have AE: "AE x in M. 0 ≤ u x * indicator A x"
by eventually_elim (auto simp: indicator_def)
have nonneg: "set_lebesgue_integral M A u ≥ 0"
unfolding set_lebesgue_integral_def
by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF AE]) (auto simp: mult_ac)
have A: "A ⊆ space M"
using ‹A ∈ sets M› by (simp add: sets.sets_into_space)
have "{x ∈ A. u x ≥ c} = {x ∈ A. ennreal(1/c) * u x ≥ 1}"
using ‹c>0› A by (auto simp: ennreal_mult'[symmetric])
then have "emeasure M {x ∈ A. u x ≥ c} = emeasure M ({x ∈ A. ennreal(1/c) * u x ≥ 1})"
by simp
also have "… ≤ ennreal(1/c) * (∫⇧+ x. ennreal(u x) * indicator A x ∂M)"
by (intro nn_integral_Markov_inequality meas assms)
also have "(∫⇧+ x. ennreal(u x) * indicator A x ∂M) = ennreal (set_lebesgue_integral M A u)"
unfolding set_lebesgue_integral_def nn_integral_set_ennreal using assms AE
by (subst nn_integral_eq_integral) (simp_all add: mult_ac set_integrable_def)
finally show ?thesis
using ‹c > 0› nonneg by (subst ennreal_mult) auto
qed
theorem integral_Markov_inequality'_measure:
assumes [measurable]: "set_integrable M A u" and "A ∈ sets M"
and "AE x in M. x ∈ A ⟶ 0 ≤ u x" "0 < (c::real)"
shows "measure M {x∈A. u x ≥ c} ≤ (∫x∈A. u x ∂M) / c"
proof -
have nonneg: "set_lebesgue_integral M A u ≥ 0"
unfolding set_lebesgue_integral_def
by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF assms(3)])
(auto simp: mult_ac)
have le: "emeasure M {x∈A. u x ≥ c} ≤ ennreal ((1/c) * (∫x∈A. u x ∂M))"
by (rule integral_Markov_inequality') (use assms in auto)
also have "… < top"
by auto
finally have "ennreal (measure M {x∈A. u x ≥ c}) = emeasure M {x∈A. u x ≥ c}"
by (intro emeasure_eq_ennreal_measure [symmetric]) auto
also note le
finally show ?thesis using nonneg
by (subst (asm) ennreal_le_iff)
(auto intro!: divide_nonneg_pos Bochner_Integration.integral_nonneg_AE assms)
qed
theorem%important (in finite_measure) Chernoff_ineq_ge:
assumes s: "s > 0"
assumes integrable: "set_integrable M A (λx. exp (s * f x))" and "A ∈ sets M"
shows "measure M {x∈A. f x ≥ a} ≤ exp (-s * a) * (∫x∈A. exp (s * f x) ∂M)"
proof -
have "{x∈A. f x ≥ a} = {x∈A. exp (s * f x) ≥ exp (s * a)}"
using s by auto
also have "measure M … ≤ set_lebesgue_integral M A (λx. exp (s * f x)) / exp (s * a)"
by (intro integral_Markov_inequality'_measure assms) auto
finally show ?thesis
by (simp add: exp_minus field_simps)
qed
theorem%important (in finite_measure) Chernoff_ineq_le:
assumes s: "s > 0"
assumes integrable: "set_integrable M A (λx. exp (-s * f x))" and "A ∈ sets M"
shows "measure M {x∈A. f x ≤ a} ≤ exp (s * a) * (∫x∈A. exp (-s * f x) ∂M)"
proof -
have "{x∈A. f x ≤ a} = {x∈A. exp (-s * f x) ≥ exp (-s * a)}"
using s by auto
also have "measure M … ≤ set_lebesgue_integral M A (λx. exp (-s * f x)) / exp (-s * a)"
by (intro integral_Markov_inequality'_measure assms) auto
finally show ?thesis
by (simp add: exp_minus field_simps)
qed
section ‹Integrable Simple Functions›
text ‹This section is from the Martingales AFP entry, by Ata Keskin, TU München›
text ‹We restate some basic results concerning Bochner-integrable functions.›
lemma integrable_implies_simple_function_sequence:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "integrable M f"
obtains s where "⋀i. simple_function M (s i)"
and "⋀i. emeasure M {y ∈ space M. s i y ≠ 0} ≠ ∞"
and "⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x"
and "⋀x i. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)"
proof-
have f: "f ∈ borel_measurable M" "(∫⇧+x. norm (f x) ∂M) < ∞" using assms unfolding integrable_iff_bounded by auto
obtain s where s: "⋀i. simple_function M (s i)" "⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x" "⋀i x. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)" using borel_measurable_implies_sequence_metric[OF f(1)] unfolding norm_conv_dist by metis
{
fix i
have "(∫⇧+x. norm (s i x) ∂M) ≤ (∫⇧+x. ennreal (2 * norm (f x)) ∂M)" using s by (intro nn_integral_mono, auto)
also have "… < ∞" 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 ∈ space M. s i y ≠ 0} ≠ ∞" by (auto intro: integrableI_simple_bochner_integrable simple_bochner_integrable.cases)
}
thus ?thesis using that s by blast
qed
text ‹Simple functions can be represented by sums of indicator functions.›
lemma simple_function_indicator_representation_banach:
fixes f ::"'a ⇒ 'b :: {second_countable_topology, banach}"
assumes "simple_function M f" "x ∈ space M"
shows "f x = (∑y ∈ f ` space M. indicator (f -` {y} ∩ space M) x *⇩R y)"
(is "?l = ?r")
proof -
have "?r = (∑y ∈ f ` space M. (if y = f x then indicator (f -` {y} ∩ space M) x *⇩R y else 0))"
by (auto intro!: sum.cong)
also have "… = indicator (f -` {f x} ∩ space M) x *⇩R f x" using assms by (auto dest: simple_functionD)
also have "… = f x" using assms by (auto simp: indicator_def)
finally show ?thesis by auto
qed
lemma simple_function_indicator_representation_AE:
fixes f ::"'a ⇒ 'b :: {second_countable_topology, banach}"
assumes "simple_function M f"
shows "AE x in M. f x = (∑y ∈ f ` space M. indicator (f -` {y} ∩ space M) x *⇩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="(*⇩R)"]
lemmas integrable_simple_function = simple_bochner_integrable.intros[THEN has_bochner_integral_simple_bochner_integrable, THEN integrable.intros]
text ‹Induction rule for simple integrable functions.›
lemma integrable_simple_function_induct[consumes 2, case_names cong indicator add, induct set: simple_function]:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach}"
assumes f: "simple_function M f" "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞"
assumes cong: "⋀f g. simple_function M f ⟹ emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞
⟹ simple_function M g ⟹ emeasure M {y ∈ space M. g y ≠ 0} ≠ ∞
⟹ (⋀x. x ∈ space M ⟹ f x = g x) ⟹ P f ⟹ P g"
assumes indicator: "⋀A y. A ∈ sets M ⟹ emeasure M A < ∞ ⟹ P (λx. indicator A x *⇩R y)"
assumes add: "⋀f g. simple_function M f ⟹ emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞ ⟹
simple_function M g ⟹ emeasure M {y ∈ space M. g y ≠ 0} ≠ ∞ ⟹
(⋀z. z ∈ space M ⟹ norm (f z + g z) = norm (f z) + norm (g z)) ⟹
P f ⟹ P g ⟹ P (λx. f x + g x)"
shows "P f"
proof-
let ?f = "λx. (∑y∈f ` space M. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
have f_ae_eq: "f x = ?f x" if "x ∈ space M" for x using simple_function_indicator_representation_banach[OF f(1) that] .
moreover have "emeasure M {y ∈ space M. ?f y ≠ 0} ≠ ∞" by (metis (no_types, lifting) Collect_cong calculation f(2))
moreover have "P (λx. ∑y∈S. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
"simple_function M (λx. ∑y∈S. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
"emeasure M {y ∈ space M. (∑x∈S. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ≠ ∞"
if "S ⊆ 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} ∩ space M) ⊆ {y ∈ space M. f y ≠ 0}" if "x ≠ 0" using that by blast
moreover have "{y ∈ space M. f y ≠ 0} = space M - (f -` {0} ∩ space M)" by blast
moreover have "space M - (f -` {0} ∩ space M) ∈ sets M" using simple_functionD(2)[OF f(1)] by blast
ultimately have fin_0: "emeasure M (f -` {x} ∩ space M) < ∞" if "x ≠ 0" using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique)
hence fin_1: "emeasure M {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 0} ≠ ∞" if "x ≠ 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 *: "(∑y∈insert x F. indicat_real (f -` {y} ∩ space M) xa *⇩R y) = (∑y∈F. indicat_real (f -` {y} ∩ space M) xa *⇩R y) + indicat_real (f -` {x} ∩ space M) xa *⇩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 ∈ space M. (∑x∈insert x F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ⊆ {y ∈ space M. (∑x∈F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ∪ {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 0}" unfolding * by fastforce
{
case 1
hence x: "x ∈ f ` space M" and F: "F ⊆ 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 ((∑y∈F. indicat_real (f -` {y} ∩ space M) z *⇩R y) + indicat_real (f -` {x} ∩ space M) z *⇩R x) = norm (∑y∈F. indicat_real (f -` {y} ∩ space M) z *⇩R y) + norm (indicat_real (f -` {x} ∩ space M) z *⇩R x)" if z: "z ∈ space M" for z
proof (cases "f z = x")
case True
have "indicat_real (f -` {y} ∩ space M) z *⇩R y = 0" if "y ∈ F" for y
using True insert(2) z that 1 unfolding indicator_def by force
hence "(∑y∈F. indicat_real (f -` {y} ∩ space M) z *⇩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 ∈ f ` space M" and F: "F ⊆ 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 ∈ f ` space M" and F: "F ⊆ 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 ∈ space M. (∑x∈insert x F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ≤ emeasure M ({y ∈ space M. (∑x∈F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ∪ {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 0})"
using ** simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_mono, force+)
also have "… ≤ emeasure M {y ∈ space M. (∑x∈F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} + emeasure M {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 0}"
using simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+)
also have "… < ∞" 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 (λx. ∑y∈f ` space M. indicat_real (f -` {y} ∩ space M) x *⇩R y)" using calculation by blast
moreover have "P (λx. ∑y∈f ` space M. indicat_real (f -` {y} ∩ space M) x *⇩R y)" using calculation by blast
ultimately show ?thesis by (intro cong[OF _ _ f(1,2)], blast, presburger+)
qed
text ‹Induction rule for non-negative simple integrable functions›
lemma integrable_simple_function_induct_nn[consumes 3, case_names cong indicator add, induct set: simple_function]:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes f: "simple_function M f" "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞" "⋀x. x ∈ space M ⟶ f x ≥ 0"
assumes cong: "⋀f g. simple_function M f ⟹ emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞ ⟹ (⋀x. x ∈ space M ⟹ f x ≥ 0) ⟹ simple_function M g ⟹ emeasure M {y ∈ space M. g y ≠ 0} ≠ ∞ ⟹ (⋀x. x ∈ space M ⟹ g x ≥ 0) ⟹ (⋀x. x ∈ space M ⟹ f x = g x) ⟹ P f ⟹ P g"
assumes indicator: "⋀A y. y ≥ 0 ⟹ A ∈ sets M ⟹ emeasure M A < ∞ ⟹ P (λx. indicator A x *⇩R y)"
assumes add: "⋀f g. (⋀x. x ∈ space M ⟹ f x ≥ 0) ⟹ simple_function M f ⟹ emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞ ⟹
(⋀x. x ∈ space M ⟹ g x ≥ 0) ⟹ simple_function M g ⟹ emeasure M {y ∈ space M. g y ≠ 0} ≠ ∞ ⟹
(⋀z. z ∈ space M ⟹ norm (f z + g z) = norm (f z) + norm (g z)) ⟹
P f ⟹ P g ⟹ P (λx. f x + g x)"
shows "P f"
proof-
let ?f = "λx. (∑y∈f ` space M. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
have f_ae_eq: "f x = ?f x" if "x ∈ space M" for x using simple_function_indicator_representation_banach[OF f(1) that] .
moreover have "emeasure M {y ∈ space M. ?f y ≠ 0} ≠ ∞" by (metis (no_types, lifting) Collect_cong calculation f(2))
moreover have "P (λx. ∑y∈S. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
"simple_function M (λx. ∑y∈S. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
"emeasure M {y ∈ space M. (∑x∈S. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ≠ ∞"
"⋀x. x ∈ space M ⟹ 0 ≤ (∑y∈S. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
if "S ⊆ 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} ∩ space M) ⊆ {y ∈ space M. f y ≠ 0}" if "x ≠ 0"
using that by blast
moreover have "{y ∈ space M. f y ≠ 0} = space M - (f -` {0} ∩ space M)"
by blast
moreover have "space M - (f -` {0} ∩ space M) ∈ sets M"
using simple_functionD(2)[OF f(1)] by blast
ultimately have fin_0: "emeasure M (f -` {x} ∩ space M) < ∞" if "x ≠ 0"
using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique)
hence fin_1: "emeasure M {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 0} ≠ ∞" if "x ≠ 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 ≥ 0" using insert f by blast
have *: "(∑y∈insert x F. indicat_real (f -` {y} ∩ space M) xa *⇩R y) = (∑y∈F. indicat_real (f -` {y} ∩ space M) xa *⇩R y) + indicat_real (f -` {x} ∩ space M) xa *⇩R x" for xa by (metis (no_types, lifting) add.commute insert.hyps(1) insert.hyps(4) sum.insert)
have **: "{y ∈ space M. (∑x∈insert x F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ⊆ {y ∈ space M. (∑x∈F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ∪ {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 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 ((∑y∈F. indicat_real (f -` {y} ∩ space M) z *⇩R y) + indicat_real (f -` {x} ∩ space M) z *⇩R x)
= norm (∑y∈F. indicat_real (f -` {y} ∩ space M) z *⇩R y) + norm (indicat_real (f -` {x} ∩ space M) z *⇩R x)"
if z: "z ∈ space M" for z
proof (cases "f z = x")
case True
have "indicat_real (f -` {y} ∩ space M) z *⇩R y = 0" if "y ∈ F" for y
using True insert z that 1 unfolding indicator_def by force
hence "(∑y∈F. indicat_real (f -` {y} ∩ space M) z *⇩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 ∈ space M. (∑x∈insert x F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0}
≤ emeasure M ({y ∈ space M. (∑x∈F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} ∪ {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 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 "… ≤ emeasure M {y ∈ space M. (∑x∈F. indicat_real (f -` {x} ∩ space M) y *⇩R x) ≠ 0} + emeasure M {y ∈ space M. indicat_real (f -` {x} ∩ space M) y *⇩R x ≠ 0}"
using simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+)
also have "… < ∞" using insert(7) fin_1[OF False] by (simp add: less_top)
finally show ?thesis by simp
qed
next
case (4 ξ)
thus ?case using insert nonneg_x f(3) by (auto simp add: scaleR_nonneg_nonneg intro: sum_nonneg)
}
qed
moreover have "simple_function M (λx. ∑y∈f ` space M. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
using calculation by blast
moreover have "P (λx. ∑y∈f ` space M. indicat_real (f -` {y} ∩ space M) x *⇩R y)"
using calculation by blast
moreover have "⋀x. x ∈ space M ⟹ 0 ≤ 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 ⇒ ennreal"
assumes "f ∈ borel_measurable M" "(∫⇧+x. f x ∂M) < ∞"
shows "AE x in M. f x < ∞"
proof (rule ccontr, goal_cases)
case 1
let ?A = "space M ∩ {x. f x = ∞}"
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 "(∫⇧+x. f x * indicator ?A x ∂M) = (∫⇧+x. ∞ * indicator ?A x ∂M)"
by (metis (mono_tags, lifting) indicator_inter_arith indicator_simps(2) mem_Collect_eq mult_eq_0_iff)
also have "… = ∞ * emeasure M ?A"
using assms(1) by (intro nn_integral_cmult_indicator, simp)
also have "… = ∞"
using * by fastforce
finally have "(∫⇧+x. f x * indicator ?A x ∂M) = ∞" .
moreover have "(∫⇧+x. f x * indicator ?A x ∂M) ≤ (∫⇧+x. f x ∂M)"
by (intro nn_integral_mono, simp add: indicator_def)
ultimately show ?case using assms(2) by simp
qed
text ‹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>‹HOL-Analysis.Bochner_Integration››
lemma cauchy_L1_AE_cauchy_subseq:
fixes s :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "⋀n. integrable M (s n)"
and "⋀e. e > 0 ⟹ ∃N. ∀i≥N. ∀j≥N. LINT x|M. norm (s i x - s j x) < e"
obtains r where "strict_mono r" "AE x in M. Cauchy (λi. s (r i) x)"
proof-
have "∃r. ∀n. (∀i≥r n. ∀j≥ r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n) ∧ (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 ≥ N" "j ≥ N" for i j
using assms(2)[of "(1 / 2) ^ Suc n"] by auto
{
fix i j assume "i ≥ max N (Suc x)" "j ≥ max N (Suc x)"
hence "integral⇧L M (λ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 "∀i≥r n. ∀j≥ 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 = (λn x. (∑i≤n. ennreal (norm (s (r (Suc i)) x - s (r i) x))))"
define g' where "g' = (λx. ∑i. ennreal (norm (s (r (Suc i)) x - s (r i) x)))"
have integrable_g: "(∫⇧+ x. g n x ∂M) < 2" for n
proof -
have "(∫⇧+ x. g n x ∂M) = (∫⇧+ x. (∑i≤n. ennreal (norm (s (r (Suc i)) x - s (r i) x))) ∂M)"
using g_def by simp
also have "… = (∑i≤n. (∫⇧+ x. ennreal (norm (s (r (Suc i)) x - s (r i) x)) ∂M))"
by (intro nn_integral_sum, simp)
also have "… = (∑i≤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 "… < ennreal (∑i≤n. (1 / 2) ^ i)"
by (intro ennreal_lessI[OF sum_pos sum_strict_mono[OF finite_atMost _ r_is]], auto)
also have "… ≤ ennreal 2"
unfolding sum_gp0[of "1 / 2" n] by (intro ennreal_leI, auto)
finally show "(∫⇧+ x. g n x ∂M) < 2" by simp
qed
have integrable_g': "(∫⇧+ x. g' x ∂M) ≤ 2"
proof -
have "incseq (λn. g n x)" for x by (intro incseq_SucI, auto simp add: g_def ennreal_leI)
hence "convergent (λn. g n x)" for x
unfolding convergent_def using LIMSEQ_incseq_SUP by fast
hence "(λn. g n x) ⇢ g' x" for x
unfolding g_def g'_def by (intro summable_iff_convergent'[THEN iffD2, THEN summable_LIMSEQ'], blast)
hence "(∫⇧+ x. g' x ∂M) = (∫⇧+ x. liminf (λn. g n x) ∂M)" by (metis lim_imp_Liminf trivial_limit_sequentially)
also have "… ≤ liminf (λn. ∫⇧+ x. g n x ∂M)" by (intro nn_integral_liminf, simp add: g_def)
also have "… ≤ liminf (λn. 2)" using integrable_g by (intro Liminf_mono) (simp add: order_le_less)
also have "… = 2"
using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
finally show ?thesis .
qed
hence "AE x in M. g' x < ∞"
by (intro finite_nn_integral_imp_ae_finite) (auto simp add: order_le_less_trans g'_def)
moreover have "summable (λi. norm (s (r (Suc i)) x - s (r i) x))" if "g' x ≠ ∞" for x
using that unfolding g'_def by (intro summable_suminf_not_top) fastforce+
ultimately have ae_summable: "AE x in M. summable (λi. s (r (Suc i)) x - s (r i) x)"
using summable_norm_cancel unfolding dist_norm by force
{
fix x assume "summable (λi. s (r (Suc i)) x - s (r i) x)"
hence "(λn. ∑i<n. s (r (Suc i)) x - s (r i) x) ⇢ (∑i. s (r (Suc i)) x - s (r i) x)"
using summable_LIMSEQ by blast
moreover have "(λn. (∑i<n. s (r (Suc i)) x - s (r i) x)) = (λn. s (r n) x - s (r 0) x)"
using sum_lessThan_telescope by fastforce
ultimately have "(λn. s (r n) x - s (r 0) x) ⇢ (∑i. s (r (Suc i)) x - s (r i) x)" by argo
hence "(λn. s (r n) x - s (r 0) x + s (r 0) x) ⇢ (∑i. s (r (Suc i)) x - s (r i) x) + s (r 0) x"
by (intro isCont_tendsto_compose[of _ "λz. z + s (r 0) x"], auto)
hence "Cauchy (λn. s (r n) x)" by (simp add: LIMSEQ_imp_Cauchy)
}
hence "AE x in M. Cauchy (λi. s (r i) x)" using ae_summable by fast
thus ?thesis by (rule that[OF strict_mono(1)])
qed
subsection ‹Totally Ordered Banach Spaces›
lemma integrable_max[simp, intro]:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology}"
assumes fg[measurable]: "integrable M f" "integrable M g"
shows "integrable M (λx. max (f x) (g x))"
proof (rule Bochner_Integration.integrable_bound)
{
fix x y :: 'b
have "norm (max x y) ≤ max (norm x) (norm y)" by linarith
also have "… ≤ norm x + norm y" by simp
finally have "norm (max x y) ≤ norm (norm x + norm y)" by simp
}
thus "AE x in M. norm (max (f x) (g x)) ≤ 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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology}"
assumes [measurable]: "integrable M f" "integrable M g"
shows "integrable M (λx. min (f x) (g x))"
proof -
have "norm (min (f x) (g x)) ≤ norm (f x) ∨ norm (min (f x) (g x)) ≤ 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 ‹Restatement of ‹integral_nonneg_AE› for functions taking values in a Banach space.›
lemma integral_nonneg_AE_banach:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes [measurable]: "f ∈ borel_measurable M" and nonneg: "AE x in M. 0 ≤ f x"
shows "0 ≤ integral⇧L M f"
proof cases
assume integrable: "integrable M f"
hence max: "(λx. max 0 (f x)) ∈ borel_measurable M" "⋀x. 0 ≤ max 0 (f x)" "integrable M (λx. max 0 (f x))" by auto
hence "0 ≤ integral⇧L M (λx. max 0 (f x))"
proof -
obtain s where *: "⋀i. simple_function M (s i)"
"⋀i. emeasure M {y ∈ space M. s i y ≠ 0} ≠ ∞"
"⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x"
"⋀x i. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)"
using integrable_implies_simple_function_sequence[OF integrable] by blast
have simple: "⋀i. simple_function M (λx. max 0 (s i x))"
using * by fast
have "⋀i. {y ∈ space M. max 0 (s i y) ≠ 0} ⊆ {y ∈ space M. s i y ≠ 0}"
unfolding max_def by force
moreover have "⋀i. {y ∈ space M. s i y ≠ 0} ∈ sets M"
using * by measurable
ultimately have "⋀i. emeasure M {y ∈ space M. max 0 (s i y) ≠ 0} ≤ emeasure M {y ∈ space M. s i y ≠ 0}"
by (rule emeasure_mono)
hence **:"⋀i. emeasure M {y ∈ space M. max 0 (s i y) ≠ 0} ≠ ∞"
using *(2) by (auto intro: order.strict_trans1 simp add: top.not_eq_extremum)
have "⋀x. x ∈ space M ⟹ (λi. max 0 (s i x)) ⇢ max 0 (f x)"
using *(3) tendsto_max by blast
moreover have "⋀x i. x ∈ space M ⟹ norm (max 0 (s i x)) ≤ norm (2 *⇩R f x)"
using *(4) unfolding max_def by auto
ultimately have tendsto: "(λi. integral⇧L M (λx. max 0 (s i x))) ⇢ integral⇧L M (λ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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assume "simple_function M h" "emeasure M {y ∈ space M. h y ≠ 0} ≠ ∞" "⋀x. x ∈ space M ⟶ h x ≥ 0"
hence *: "integral⇧L M h ≥ 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 ≠ {} ⟹ y ≥ 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 "… = integral⇧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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "AE x in M. f x ≤ g x"
shows "integral⇧L M f ≤ integral⇧L M g"
using integral_nonneg_AE_banach[of "λx. g x - f x"] assms Bochner_Integration.integral_diff[OF assms(1,2)] by force
lemma integral_mono_banach:
fixes f g :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "⋀x. x ∈ space M ⟹ f x ≤ g x"
shows "integral⇧L M f ≤ integral⇧L M g"
using integral_mono_AE_banach assms by blast
subsection ‹Auxiliary Lemmas for Set Integrals›
lemma nn_set_integral_eq_set_integral:
assumes [measurable]:"integrable M f"
and "AE x ∈ A in M. 0 ≤ f x" "A ∈ sets M"
shows "(∫⇧+x∈A. f x ∂M) = (∫ x ∈ A. f x ∂M)"
proof-
have "(∫⇧+x. indicator A x *⇩R f x ∂M) = (∫ x ∈ A. f x ∂M)"
unfolding set_lebesgue_integral_def
using assms(2) by (intro nn_integral_eq_integral[of _ "λx. indicat_real A x *⇩R f x"], blast intro: assms integrable_mult_indicator, fastforce)
moreover have "(∫⇧+x. indicator A x *⇩R f x ∂M) = (∫⇧+x∈A. f x ∂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 ⇒ 'b::{banach, second_countable_topology}"
assumes "Ω ∩ space M ∈ sets M"
shows "set_lebesgue_integral (restrict_space M Ω) A f = set_lebesgue_integral M A (λx. indicator Ω x *⇩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 ∈ sets M" "emeasure M A ≠ ∞"
shows "set_lebesgue_integral M A (λ_. c) = measure M A *⇩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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "set_integrable M A f" "set_integrable M A g"
"⋀x. x ∈ A ⟹ f x ≤ g x"
shows "(LINT x:A|M. f x) ≤ (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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "set_integrable M A f" "set_integrable M A g" "AE x∈A in M. f x ≤ g x"
shows "set_lebesgue_integral M A f ≤ 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 "λx. indicator A x *⇩R f x" "λx. indicator A x *⇩R g x"], simp add: indicator_def)
subsection ‹Integrability and Measurability of the Diameter›
context
fixes s :: "nat ⇒ 'a ⇒ 'b :: {second_countable_topology, banach}" and M
assumes bounded: "⋀x. x ∈ space M ⟹ bounded (range (λi. s i x))"
begin
lemma borel_measurable_diameter:
assumes [measurable]: "⋀i. (s i) ∈ borel_measurable M"
shows "(λx. diameter {s i x |i. n ≤ i}) ∈ borel_measurable M"
proof -
have "{s i x |i. N ≤ i} ≠ {}" for x N by blast
hence diameter_SUP: "diameter {s i x |i. N ≤ i} = (SUP (i, j) ∈ {N..} × {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 ≤ i} × {s i x |i. n ≤ i}) = ((λ(i, j). dist (s i x) (s j x)) ` ({n..} × {n..}))" for x by fast
hence *: "(λx. diameter {s i x |i. n ≤ i}) = (λx. Sup ((λ(i, j). dist (s i x) (s j x)) ` ({n..} × {n..})))" using diameter_SUP by (simp add: case_prod_beta')
have "bounded ((λ(i, j). dist (s i x) (s j x)) ` ({n..} × {n..}))" if "x ∈ space M" for x by (rule bounded_imp_dist_bounded[OF bounded, OF that])
hence bdd: "bdd_above ((λ(i, j). dist (s i x) (s j x)) ` ({n..} × {n..}))" if "x ∈ space M" for x using that bounded_imp_bdd_above by presburger
have "fst p ∈ borel_measurable M" "snd p ∈ borel_measurable M" if "p ∈ s ` {n..} × s ` {n..}" for p using that by fastforce+
hence "(λx. fst p x - snd p x) ∈ borel_measurable M" if "p ∈ s ` {n..} × s ` {n..}" for p using that borel_measurable_diff by simp
hence "(λx. case p of (f, g) ⇒ dist (f x) (g x)) ∈ borel_measurable M" if "p ∈ s ` {n..} × s ` {n..}" for p unfolding dist_norm using that by measurable
moreover have "countable (s ` {n..} × 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 ⇒ real"
assumes "integrable M f"
and [measurable]: "⋀i. (s i) ∈ borel_measurable M"
and "⋀x i. x ∈ space M ⟹ norm (s i x) ≤ f x"
shows "integrable M (λx. diameter {s i x |i. n ≤ i})"
proof -
have "{s i x |i. N ≤ i} ≠ {}" for x N by blast
hence diameter_SUP: "diameter {s i x |i. N ≤ i} = (SUP (i, j) ∈ {N..} × {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 ∈ space M"
let ?S = "(λ(i, j). dist (s i x) (s j x)) ` ({n..} × {n..})"
have "case_prod dist ` ({s i x |i. n ≤ i} × {s i x |i. n ≤ i}) = (λ(i, j). dist (s i x) (s j x)) ` ({n..} × {n..})" by fast
hence *: "diameter {s i x |i. n ≤ 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 ≤ Sup ?S" by (auto intro!: cSup_upper2 x bounded_imp_bdd_above)
have "dist (s i x) (s j x) ≤ 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 "∀c ∈ ?S. c ≤ 2 * f x" by force
hence "Sup ?S ≤ 2 * f x" by (intro cSup_least, auto)
hence "norm (Sup ?S) ≤ 2 * norm (f x)" using Sup_S_nonneg by auto
also have "… = norm (2 *⇩R f x)" by simp
finally have "norm (diameter {s i x |i. n ≤ i}) ≤ norm (2 *⇩R f x)" unfolding * .
}
hence "AE x in M. norm (diameter {s i x |i. n ≤ i}) ≤ norm (2 *⇩R f x)" by blast
thus "integrable M (λx. diameter {s i x |i. n ≤ i})" using borel_measurable_diameter by (intro Bochner_Integration.integrable_bound[OF assms(1)[THEN integrable_scaleR_right[of 2]]], measurable)
qed
end
subsection ‹Averaging Theorem›
text ‹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.›
text ‹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})›
lemma balls_countable_basis:
obtains D :: "'a :: {metric_space, second_countable_topology} set"
where "topological_basis (case_prod ball ` (D × (ℚ ∩ {0<..})))"
and "countable D"
and "D ≠ {}"
proof -
obtain D :: "'a set" where dense_subset: "countable D" "D ≠ {}" "⟦open U; U ≠ {}⟧ ⟹ ∃y ∈ D. y ∈ U" for U using countable_dense_exists by blast
have "topological_basis (case_prod ball ` (D × (ℚ ∩ {0<..})))"
proof (intro topological_basis_iff[THEN iffD2], fast, clarify)
fix U and x :: 'a assume asm: "open U" "x ∈ U"
obtain e where e: "e > 0" "ball x e ⊆ U" using asm openE by blast
obtain y where y: "y ∈ D" "y ∈ 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 ∈ ℚ ∩ {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 ∈ ball y r" using r y by (simp add: dist_commute)
hence "ball y r ⊆ U" using r by (intro order_trans[OF _ e(2)], simp, metric)
moreover have "ball y r ∈ (case_prod ball ` (D × (ℚ ∩ {0<..})))" using y(1) r by force
ultimately show "∃B'∈(case_prod ball ` (D × (ℚ ∩ {0<..}))). x ∈ B' ∧ B' ⊆ U" using * by meson
qed
thus ?thesis using that dense_subset by blast
qed
context sigma_finite_measure
begin
text ‹To show statements concerning ‹σ›-finite measure spaces, one usually shows the statement for finite measure spaces and uses a limiting argument to show it for the ‹σ›-finite case.
The following induction scheme formalizes this.›
lemma sigma_finite_measure_induct[case_names finite_measure, consumes 0]:
assumes "⋀(N :: 'a measure) Ω. finite_measure N
⟹ N = restrict_space M Ω
⟹ Ω ∈ sets M
⟹ emeasure N Ω ≠ ∞
⟹ emeasure N Ω ≠ 0
⟹ 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 Ω" "Ω ∈ sets M" "emeasure N Ω ≠ ∞" for N Ω using that by (cases "emeasure N Ω = 0", auto intro: emeasure_0_AE assms(1))
obtain A :: "nat ⇒ 'a set" where A: "range A ⊆ sets M" "(⋃i. A i) = space M" and emeasure_finite: "emeasure M (A i) ≠ ∞" 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 ∈ A i ∩ space M. Q x} = {x ∈ space M. Q x} ∩ (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 ∈ A i. ¬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 ∈ A i. ¬ Q x} = 0" by (subst emeasure_restrict_space[symmetric], auto)
}
hence "emeasure M (⋃i. {x ∈ A i. ¬ Q x}) = 0" by (intro emeasure_UN_eq_0, auto)
moreover have "(⋃i. {x ∈ A i. ¬ Q x}) = {x ∈ space M. ¬ Q x}" using A by auto
ultimately show ?thesis by (intro AE_iff_measurable[THEN iffD2], auto)
qed
text ‹Real Functional Analysis - Lang›
text ‹The Averaging Theorem allows us to make statements concerning how a function behaves almost everywhere, depending on its behaviour on average.›
lemma averaging_theorem:
fixes f::"_ ⇒ 'b::{second_countable_topology, banach}"
assumes [measurable]: "integrable M f"
and closed: "closed S"
and "⋀A. A ∈ sets M ⟹ measure M A > 0 ⟹ (1 / measure M A) *⇩R set_lebesgue_integral M A f ∈ S"
shows "AE x in M. f x ∈ S"
proof (induct rule: sigma_finite_measure_induct)
case (finite_measure N Ω)
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) *⇩R set_lebesgue_integral N A f ∈ S" if "A ∈ sets N" "measure N A > 0" for A
proof -
have *: "A ∈ sets M" using that by (simp add: sets_restrict_space_iff finite_measure)
have "A = A ∩ Ω" 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 × (ℚ ∩ {0<..})))" and countable_D: "countable D" using balls_countable_basis by blast
have countable_balls: "countable (case_prod ball ` (D × (ℚ ∩ {0<..})))" using countable_rat countable_D by blast
obtain B where B_balls: "B ⊆ case_prod ball ` (D × (ℚ ∩ {0<..}))" "⋃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 ∪ {{}})"
have "B ∪ {{}} ≠ {}" by simp
have range_b: "range b = B ∪ {{}}" 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 ∪ {{}}" i] by force
have Union_range_b: "⋃(range b) = -S" using B_balls range_b by simp
{
fix v r assume ball_in_Compl: "ball v r ⊆ -S"
define A where "A = f -` ball v r ∩ space N"
have dist_less: "dist (f x) v < r" if "x ∈ A" for x using that unfolding A_def vimage_def by (simp add: dist_commute)
hence AE_less: "AE x ∈ A in N. norm (f x - v) < r" by (auto simp add: dist_norm)
have *: "A ∈ 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) *⇩R set_lebesgue_integral N A f - v
= (1 / measure N A) *⇩R set_lebesgue_integral N A (λ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 (∫x∈A. (f x - v)∂N) ≤ (∫x∈A. norm (f x - v)∂N)"
using * by (auto intro!: integral_norm_bound[of N "λx. indicator A x *⇩R (f x - v)", THEN order_trans] integrable_mult_indicator integrable simp add: set_lebesgue_integral_def)
ultimately have "norm ((1 / measure N A) *⇩R set_lebesgue_integral N A f - v)
≤ set_lebesgue_integral N A (λx. norm (f x - v)) / measure N A" using asm by (auto intro: divide_right_mono)
also have "… < set_lebesgue_integral N A (λ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 "… = r" using * measure_pos by (simp add: set_integral_const)
finally have "dist ((1 / measure N A) *⇩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' ∈ B"
hence ball_subset_Compl: "b' ⊆ -S" and ball_radius_pos: "∃v ∈ D. ∃r>0. b' = ball v r" using B_balls by (blast, fast)
}
note ** = this
hence "emeasure N (f -` b i ∩ space N) = 0" for i by (cases "b i = {}", simp) (metis UnE singletonD * range_b[THEN eq_refl, THEN range_subsetD])
hence "emeasure N (⋃i. f -` b i ∩ space N) = 0" using open_b by (intro emeasure_UN_eq_0) fastforce+
moreover have "(⋃i. f -` b i ∩ space N) = f -` (⋃(range b)) ∩ space N" by blast
ultimately have "emeasure N (f -` (-S) ∩ space N) = 0" using Union_range_b by argo
hence "AE x in N. f x ∉ -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 ⇒ 'b::{second_countable_topology, banach}"
assumes "integrable M f"
and density_0: "⋀A. A ∈ sets M ⟹ 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 ‹The following lemma shows that densities are unique in Banach spaces.›
lemma density_unique_banach:
fixes f f'::"'a ⇒ 'b::{second_countable_topology, banach}"
assumes "integrable M f" "integrable M f'"
and density_eq: "⋀A. A ∈ sets M ⟹ 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 ∈ sets M"
hence "LINT x|M. indicat_real A x *⇩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::"_ ⇒ 'b::{second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f"
and "⋀A. A ∈ sets M ⟹ set_lebesgue_integral M A f ≥ 0"
shows "AE x in M. f x ≥ 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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 ≤ f x"
shows "integral⇧L M f = 0 ⟷ (AE x in M. f x = 0)"
proof
assume *: "integral⇧L M f = 0"
{
fix A assume asm: "A ∈ sets M"
have "0 ≤ integral⇧L M (λx. indicator A x *⇩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 "… ≤ integral⇧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 ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "integral⇧L M f = integral⇧L M g" "AE x in M. f x ≤ g x"
shows "AE x in M. f x = g x"
proof -
define h where "h = (λ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