section ‹Bochner Integration for Vector-Valued Functions›
theory Bochner_Integration
imports Finite_Product_Measure
begin
text ‹
In the following development of the Bochner integral we use second countable topologies instead
of separable spaces. A second countable topology is also separable.
›
lemma borel_measurable_implies_sequence_metric:
fixes f :: "'a ⇒ 'b :: {metric_space, second_countable_topology}"
assumes [measurable]: "f ∈ borel_measurable M"
shows "∃F. (∀i. simple_function M (F i)) ∧ (∀x∈space M. (λi. F i x) ⇢ f x) ∧
(∀i. ∀x∈space M. dist (F i x) z ≤ 2 * dist (f x) z)"
proof -
obtain D :: "'b set" where "countable D" and D: "⋀X. open X ⟹ X ≠ {} ⟹ ∃d∈D. d ∈ X"
by (erule countable_dense_setE)
def e ≡ "from_nat_into D"
{ fix n x
obtain d where "d ∈ D" and d: "d ∈ ball x (1 / Suc n)"
using D[of "ball x (1 / Suc n)"] by auto
from ‹d ∈ D› D[of UNIV] ‹countable D› obtain i where "d = e i"
unfolding e_def by (auto dest: from_nat_into_surj)
with d have "∃i. dist x (e i) < 1 / Suc n"
by auto }
note e = this
def A ≡ "λm n. {x∈space M. dist (f x) (e n) < 1 / (Suc m) ∧ 1 / (Suc m) ≤ dist (f x) z}"
def B ≡ "λm. disjointed (A m)"
def m ≡ "λN x. Max {m::nat. m ≤ N ∧ x ∈ (⋃n≤N. B m n)}"
def F ≡ "λN::nat. λx. if (∃m≤N. x ∈ (⋃n≤N. B m n)) ∧ (∃n≤N. x ∈ B (m N x) n)
then e (LEAST n. x ∈ B (m N x) n) else z"
have B_imp_A[intro, simp]: "⋀x m n. x ∈ B m n ⟹ x ∈ A m n"
using disjointed_subset[of "A m" for m] unfolding B_def by auto
{ fix m
have "⋀n. A m n ∈ sets M"
by (auto simp: A_def)
then have "⋀n. B m n ∈ sets M"
using sets.range_disjointed_sets[of "A m" M] by (auto simp: B_def) }
note this[measurable]
{ fix N i x assume "∃m≤N. x ∈ (⋃n≤N. B m n)"
then have "m N x ∈ {m::nat. m ≤ N ∧ x ∈ (⋃n≤N. B m n)}"
unfolding m_def by (intro Max_in) auto
then have "m N x ≤ N" "∃n≤N. x ∈ B (m N x) n"
by auto }
note m = this
{ fix j N i x assume "j ≤ N" "i ≤ N" "x ∈ B j i"
then have "j ≤ m N x"
unfolding m_def by (intro Max_ge) auto }
note m_upper = this
show ?thesis
unfolding simple_function_def
proof (safe intro!: exI[of _ F])
have [measurable]: "⋀i. F i ∈ borel_measurable M"
unfolding F_def m_def by measurable
show "⋀x i. F i -` {x} ∩ space M ∈ sets M"
by measurable
{ fix i
{ fix n x assume "x ∈ B (m i x) n"
then have "(LEAST n. x ∈ B (m i x) n) ≤ n"
by (intro Least_le)
also assume "n ≤ i"
finally have "(LEAST n. x ∈ B (m i x) n) ≤ i" . }
then have "F i ` space M ⊆ {z} ∪ e ` {.. i}"
by (auto simp: F_def)
then show "finite (F i ` space M)"
by (rule finite_subset) auto }
{ fix N i n x assume "i ≤ N" "n ≤ N" "x ∈ B i n"
then have 1: "∃m≤N. x ∈ (⋃n≤N. B m n)" by auto
from m[OF this] obtain n where n: "m N x ≤ N" "n ≤ N" "x ∈ B (m N x) n" by auto
moreover
def L ≡ "LEAST n. x ∈ B (m N x) n"
have "dist (f x) (e L) < 1 / Suc (m N x)"
proof -
have "x ∈ B (m N x) L"
using n(3) unfolding L_def by (rule LeastI)
then have "x ∈ A (m N x) L"
by auto
then show ?thesis
unfolding A_def by simp
qed
ultimately have "dist (f x) (F N x) < 1 / Suc (m N x)"
by (auto simp add: F_def L_def) }
note * = this
fix x assume "x ∈ space M"
show "(λi. F i x) ⇢ f x"
proof cases
assume "f x = z"
then have "⋀i n. x ∉ A i n"
unfolding A_def by auto
then have "⋀i. F i x = z"
by (auto simp: F_def)
then show ?thesis
using ‹f x = z› by auto
next
assume "f x ≠ z"
show ?thesis
proof (rule tendstoI)
fix e :: real assume "0 < e"
with ‹f x ≠ z› obtain n where "1 / Suc n < e" "1 / Suc n < dist (f x) z"
by (metis dist_nz order_less_trans neq_iff nat_approx_posE)
with ‹x∈space M› ‹f x ≠ z› have "x ∈ (⋃i. B n i)"
unfolding A_def B_def UN_disjointed_eq using e by auto
then obtain i where i: "x ∈ B n i" by auto
show "eventually (λi. dist (F i x) (f x) < e) sequentially"
using eventually_ge_at_top[of "max n i"]
proof eventually_elim
fix j assume j: "max n i ≤ j"
with i have "dist (f x) (F j x) < 1 / Suc (m j x)"
by (intro *[OF _ _ i]) auto
also have "… ≤ 1 / Suc n"
using j m_upper[OF _ _ i]
by (auto simp: field_simps)
also note ‹1 / Suc n < e›
finally show "dist (F j x) (f x) < e"
by (simp add: less_imp_le dist_commute)
qed
qed
qed
fix i
{ fix n m assume "x ∈ A n m"
then have "dist (e m) (f x) + dist (f x) z ≤ 2 * dist (f x) z"
unfolding A_def by (auto simp: dist_commute)
also have "dist (e m) z ≤ dist (e m) (f x) + dist (f x) z"
by (rule dist_triangle)
finally (xtrans) have "dist (e m) z ≤ 2 * dist (f x) z" . }
then show "dist (F i x) z ≤ 2 * dist (f x) z"
unfolding F_def
apply auto
apply (rule LeastI2)
apply auto
done
qed
qed
lemma
fixes f :: "'a ⇒ 'b::semiring_1" assumes "finite A"
shows setsum_mult_indicator[simp]: "(∑x ∈ A. f x * indicator (B x) (g x)) = (∑x∈{x∈A. g x ∈ B x}. f x)"
and setsum_indicator_mult[simp]: "(∑x ∈ A. indicator (B x) (g x) * f x) = (∑x∈{x∈A. g x ∈ B x}. f x)"
unfolding indicator_def
using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm)
lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
fixes P :: "('a ⇒ real) ⇒ bool"
assumes u: "u ∈ borel_measurable M" "⋀x. 0 ≤ u x"
assumes set: "⋀A. A ∈ sets M ⟹ P (indicator A)"
assumes mult: "⋀u c. 0 ≤ c ⟹ u ∈ borel_measurable M ⟹ (⋀x. 0 ≤ u x) ⟹ P u ⟹ P (λx. c * u x)"
assumes add: "⋀u v. u ∈ borel_measurable M ⟹ (⋀x. 0 ≤ u x) ⟹ P u ⟹ v ∈ borel_measurable M ⟹ (⋀x. 0 ≤ v x) ⟹ (⋀x. x ∈ space M ⟹ u x = 0 ∨ v x = 0) ⟹ P v ⟹ P (λx. v x + u x)"
assumes seq: "⋀U. (⋀i. U i ∈ borel_measurable M) ⟹ (⋀i x. 0 ≤ U i x) ⟹ (⋀i. P (U i)) ⟹ incseq U ⟹ (⋀x. x ∈ space M ⟹ (λi. U i x) ⇢ u x) ⟹ P u"
shows "P u"
proof -
have "(λx. ennreal (u x)) ∈ borel_measurable M" using u by auto
from borel_measurable_implies_simple_function_sequence'[OF this]
obtain U where U: "⋀i. simple_function M (U i)" "incseq U" "⋀i x. U i x < top" and
sup: "⋀x. (SUP i. U i x) = ennreal (u x)"
by blast
def U' ≡ "λi x. indicator (space M) x * enn2real (U i x)"
then have U'_sf[measurable]: "⋀i. simple_function M (U' i)"
using U by (auto intro!: simple_function_compose1[where g=enn2real])
show "P u"
proof (rule seq)
show U': "U' i ∈ borel_measurable M" "⋀x. 0 ≤ U' i x" for i
using U by (auto
intro: borel_measurable_simple_function
intro!: borel_measurable_enn2real borel_measurable_times
simp: U'_def zero_le_mult_iff enn2real_nonneg)
show "incseq U'"
using U(2,3)
by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)
fix x assume x: "x ∈ space M"
have "(λi. U i x) ⇢ (SUP i. U i x)"
using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def)
moreover have "(λi. U i x) = (λi. ennreal (U' i x))"
using x U(3) by (auto simp: fun_eq_iff U'_def image_iff eq_commute)
moreover have "(SUP i. U i x) = ennreal (u x)"
using sup u(2) by (simp add: max_def)
ultimately show "(λi. U' i x) ⇢ u x"
using u U' by simp
next
fix i
have "U' i ` space M ⊆ enn2real ` (U i ` space M)" "finite (U i ` space M)"
unfolding U'_def using U(1) by (auto dest: simple_functionD)
then have fin: "finite (U' i ` space M)"
by (metis finite_subset finite_imageI)
moreover have "⋀z. {y. U' i z = y ∧ y ∈ U' i ` space M ∧ z ∈ space M} = (if z ∈ space M then {U' i z} else {})"
by auto
ultimately have U': "(λz. ∑y∈U' i`space M. y * indicator {x∈space M. U' i x = y} z) = U' i"
by (simp add: U'_def fun_eq_iff)
have "⋀x. x ∈ U' i ` space M ⟹ 0 ≤ x"
by (auto simp: U'_def enn2real_nonneg)
with fin have "P (λz. ∑y∈U' i`space M. y * indicator {x∈space M. U' i x = y} z)"
proof induct
case empty from set[of "{}"] show ?case
by (simp add: indicator_def[abs_def])
next
case (insert x F)
then show ?case
by (auto intro!: add mult set setsum_nonneg split: split_indicator split_indicator_asm
simp del: setsum_mult_indicator simp: setsum_nonneg_eq_0_iff)
qed
with U' show "P (U' i)" by simp
qed
qed
lemma scaleR_cong_right:
fixes x :: "'a :: real_vector"
shows "(x ≠ 0 ⟹ r = p) ⟹ r *⇩R x = p *⇩R x"
by (cases "x = 0") auto
inductive simple_bochner_integrable :: "'a measure ⇒ ('a ⇒ 'b::real_vector) ⇒ bool" for M f where
"simple_function M f ⟹ emeasure M {y∈space M. f y ≠ 0} ≠ ∞ ⟹
simple_bochner_integrable M f"
lemma simple_bochner_integrable_compose2:
assumes p_0: "p 0 0 = 0"
shows "simple_bochner_integrable M f ⟹ simple_bochner_integrable M g ⟹
simple_bochner_integrable M (λx. p (f x) (g x))"
proof (safe intro!: simple_bochner_integrable.intros elim!: simple_bochner_integrable.cases del: notI)
assume sf: "simple_function M f" "simple_function M g"
then show "simple_function M (λx. p (f x) (g x))"
by (rule simple_function_compose2)
from sf have [measurable]:
"f ∈ measurable M (count_space UNIV)"
"g ∈ measurable M (count_space UNIV)"
by (auto intro: measurable_simple_function)
assume fin: "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞" "emeasure M {y ∈ space M. g y ≠ 0} ≠ ∞"
have "emeasure M {x∈space M. p (f x) (g x) ≠ 0} ≤
emeasure M ({x∈space M. f x ≠ 0} ∪ {x∈space M. g x ≠ 0})"
by (intro emeasure_mono) (auto simp: p_0)
also have "… ≤ emeasure M {x∈space M. f x ≠ 0} + emeasure M {x∈space M. g x ≠ 0}"
by (intro emeasure_subadditive) auto
finally show "emeasure M {y ∈ space M. p (f y) (g y) ≠ 0} ≠ ∞"
using fin by (auto simp: top_unique)
qed
lemma simple_function_finite_support:
assumes f: "simple_function M f" and fin: "(∫⇧+x. f x ∂M) < ∞" and nn: "⋀x. 0 ≤ f x"
shows "emeasure M {x∈space M. f x ≠ 0} ≠ ∞"
proof cases
from f have meas[measurable]: "f ∈ borel_measurable M"
by (rule borel_measurable_simple_function)
assume non_empty: "∃x∈space M. f x ≠ 0"
def m ≡ "Min (f`space M - {0})"
have "m ∈ f`space M - {0}"
unfolding m_def using f non_empty by (intro Min_in) (auto simp: simple_function_def)
then have m: "0 < m"
using nn by (auto simp: less_le)
from m have "m * emeasure M {x∈space M. 0 ≠ f x} =
(∫⇧+x. m * indicator {x∈space M. 0 ≠ f x} x ∂M)"
using f by (intro nn_integral_cmult_indicator[symmetric]) auto
also have "… ≤ (∫⇧+x. f x ∂M)"
using AE_space
proof (intro nn_integral_mono_AE, eventually_elim)
fix x assume "x ∈ space M"
with nn show "m * indicator {x ∈ space M. 0 ≠ f x} x ≤ f x"
using f by (auto split: split_indicator simp: simple_function_def m_def)
qed
also note ‹… < ∞›
finally show ?thesis
using m by (auto simp: ennreal_mult_less_top)
next
assume "¬ (∃x∈space M. f x ≠ 0)"
with nn have *: "{x∈space M. f x ≠ 0} = {}"
by auto
show ?thesis unfolding * by simp
qed
lemma simple_bochner_integrableI_bounded:
assumes f: "simple_function M f" and fin: "(∫⇧+x. norm (f x) ∂M) < ∞"
shows "simple_bochner_integrable M f"
proof
have "emeasure M {y ∈ space M. ennreal (norm (f y)) ≠ 0} ≠ ∞"
proof (rule simple_function_finite_support)
show "simple_function M (λx. ennreal (norm (f x)))"
using f by (rule simple_function_compose1)
show "(∫⇧+ y. ennreal (norm (f y)) ∂M) < ∞" by fact
qed simp
then show "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞" by simp
qed fact
definition simple_bochner_integral :: "'a measure ⇒ ('a ⇒ 'b::real_vector) ⇒ 'b" where
"simple_bochner_integral M f = (∑y∈f`space M. measure M {x∈space M. f x = y} *⇩R y)"
lemma simple_bochner_integral_partition:
assumes f: "simple_bochner_integrable M f" and g: "simple_function M g"
assumes sub: "⋀x y. x ∈ space M ⟹ y ∈ space M ⟹ g x = g y ⟹ f x = f y"
assumes v: "⋀x. x ∈ space M ⟹ f x = v (g x)"
shows "simple_bochner_integral M f = (∑y∈g ` space M. measure M {x∈space M. g x = y} *⇩R v y)"
(is "_ = ?r")
proof -
from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
by (auto simp: simple_function_def elim: simple_bochner_integrable.cases)
from f have [measurable]: "f ∈ measurable M (count_space UNIV)"
by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
from g have [measurable]: "g ∈ measurable M (count_space UNIV)"
by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
{ fix y assume "y ∈ space M"
then have "f ` space M ∩ {i. ∃x∈space M. i = f x ∧ g y = g x} = {v (g y)}"
by (auto cong: sub simp: v[symmetric]) }
note eq = this
have "simple_bochner_integral M f =
(∑y∈f`space M. (∑z∈g`space M.
if ∃x∈space M. y = f x ∧ z = g x then measure M {x∈space M. g x = z} else 0) *⇩R y)"
unfolding simple_bochner_integral_def
proof (safe intro!: setsum.cong scaleR_cong_right)
fix y assume y: "y ∈ space M" "f y ≠ 0"
have [simp]: "g ` space M ∩ {z. ∃x∈space M. f y = f x ∧ z = g x} =
{z. ∃x∈space M. f y = f x ∧ z = g x}"
by auto
have eq:"{x ∈ space M. f x = f y} =
(⋃i∈{z. ∃x∈space M. f y = f x ∧ z = g x}. {x ∈ space M. g x = i})"
by (auto simp: eq_commute cong: sub rev_conj_cong)
have "finite (g`space M)" by simp
then have "finite {z. ∃x∈space M. f y = f x ∧ z = g x}"
by (rule rev_finite_subset) auto
moreover
{ fix x assume "x ∈ space M" "f x = f y"
then have "x ∈ space M" "f x ≠ 0"
using y by auto
then have "emeasure M {y ∈ space M. g y = g x} ≤ emeasure M {y ∈ space M. f y ≠ 0}"
by (auto intro!: emeasure_mono cong: sub)
then have "emeasure M {xa ∈ space M. g xa = g x} < ∞"
using f by (auto simp: simple_bochner_integrable.simps less_top) }
ultimately
show "measure M {x ∈ space M. f x = f y} =
(∑z∈g ` space M. if ∃x∈space M. f y = f x ∧ z = g x then measure M {x ∈ space M. g x = z} else 0)"
apply (simp add: setsum.If_cases eq)
apply (subst measure_finite_Union[symmetric])
apply (auto simp: disjoint_family_on_def less_top)
done
qed
also have "… = (∑y∈f`space M. (∑z∈g`space M.
if ∃x∈space M. y = f x ∧ z = g x then measure M {x∈space M. g x = z} *⇩R y else 0))"
by (auto intro!: setsum.cong simp: scaleR_setsum_left)
also have "… = ?r"
by (subst setsum.commute)
(auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq)
finally show "simple_bochner_integral M f = ?r" .
qed
lemma simple_bochner_integral_add:
assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
shows "simple_bochner_integral M (λx. f x + g x) =
simple_bochner_integral M f + simple_bochner_integral M g"
proof -
from f g have "simple_bochner_integral M (λx. f x + g x) =
(∑y∈(λx. (f x, g x)) ` space M. measure M {x ∈ space M. (f x, g x) = y} *⇩R (fst y + snd y))"
by (intro simple_bochner_integral_partition)
(auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
moreover from f g have "simple_bochner_integral M f =
(∑y∈(λx. (f x, g x)) ` space M. measure M {x ∈ space M. (f x, g x) = y} *⇩R fst y)"
by (intro simple_bochner_integral_partition)
(auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
moreover from f g have "simple_bochner_integral M g =
(∑y∈(λx. (f x, g x)) ` space M. measure M {x ∈ space M. (f x, g x) = y} *⇩R snd y)"
by (intro simple_bochner_integral_partition)
(auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
ultimately show ?thesis
by (simp add: setsum.distrib[symmetric] scaleR_add_right)
qed
lemma (in linear) simple_bochner_integral_linear:
assumes g: "simple_bochner_integrable M g"
shows "simple_bochner_integral M (λx. f (g x)) = f (simple_bochner_integral M g)"
proof -
from g have "simple_bochner_integral M (λx. f (g x)) =
(∑y∈g ` space M. measure M {x ∈ space M. g x = y} *⇩R f y)"
by (intro simple_bochner_integral_partition)
(auto simp: simple_bochner_integrable_compose2[where p="λx y. f x"] zero
elim: simple_bochner_integrable.cases)
also have "… = f (simple_bochner_integral M g)"
by (simp add: simple_bochner_integral_def setsum scaleR)
finally show ?thesis .
qed
lemma simple_bochner_integral_minus:
assumes f: "simple_bochner_integrable M f"
shows "simple_bochner_integral M (λx. - f x) = - simple_bochner_integral M f"
proof -
interpret linear uminus by unfold_locales auto
from f show ?thesis
by (rule simple_bochner_integral_linear)
qed
lemma simple_bochner_integral_diff:
assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
shows "simple_bochner_integral M (λx. f x - g x) =
simple_bochner_integral M f - simple_bochner_integral M g"
unfolding diff_conv_add_uminus using f g
by (subst simple_bochner_integral_add)
(auto simp: simple_bochner_integral_minus simple_bochner_integrable_compose2[where p="λx y. - y"])
lemma simple_bochner_integral_norm_bound:
assumes f: "simple_bochner_integrable M f"
shows "norm (simple_bochner_integral M f) ≤ simple_bochner_integral M (λx. norm (f x))"
proof -
have "norm (simple_bochner_integral M f) ≤
(∑y∈f ` space M. norm (measure M {x ∈ space M. f x = y} *⇩R y))"
unfolding simple_bochner_integral_def by (rule norm_setsum)
also have "… = (∑y∈f ` space M. measure M {x ∈ space M. f x = y} *⇩R norm y)"
by simp
also have "… = simple_bochner_integral M (λx. norm (f x))"
using f
by (intro simple_bochner_integral_partition[symmetric])
(auto intro: f simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
finally show ?thesis .
qed
lemma simple_bochner_integral_nonneg[simp]:
fixes f :: "'a ⇒ real"
shows "(⋀x. 0 ≤ f x) ⟹ 0 ≤ simple_bochner_integral M f"
by (simp add: setsum_nonneg simple_bochner_integral_def)
lemma simple_bochner_integral_eq_nn_integral:
assumes f: "simple_bochner_integrable M f" "⋀x. 0 ≤ f x"
shows "simple_bochner_integral M f = (∫⇧+x. f x ∂M)"
proof -
{ fix x y z have "(x ≠ 0 ⟹ y = z) ⟹ ennreal x * y = ennreal x * z"
by (cases "x = 0") (auto simp: zero_ennreal_def[symmetric]) }
note ennreal_cong_mult = this
have [measurable]: "f ∈ borel_measurable M"
using f(1) by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
{ fix y assume y: "y ∈ space M" "f y ≠ 0"
have "ennreal (measure M {x ∈ space M. f x = f y}) = emeasure M {x ∈ space M. f x = f y}"
proof (rule emeasure_eq_ennreal_measure[symmetric])
have "emeasure M {x ∈ space M. f x = f y} ≤ emeasure M {x ∈ space M. f x ≠ 0}"
using y by (intro emeasure_mono) auto
with f show "emeasure M {x ∈ space M. f x = f y} ≠ top"
by (auto simp: simple_bochner_integrable.simps top_unique)
qed
moreover have "{x ∈ space M. f x = f y} = (λx. ennreal (f x)) -` {ennreal (f y)} ∩ space M"
using f by auto
ultimately have "ennreal (measure M {x ∈ space M. f x = f y}) =
emeasure M ((λx. ennreal (f x)) -` {ennreal (f y)} ∩ space M)" by simp }
with f have "simple_bochner_integral M f = (∫⇧Sx. f x ∂M)"
unfolding simple_integral_def
by (subst simple_bochner_integral_partition[OF f(1), where g="λx. ennreal (f x)" and v=enn2real])
(auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
intro!: setsum.cong ennreal_cong_mult
simp: setsum_ennreal[symmetric] ac_simps ennreal_mult
simp del: setsum_ennreal)
also have "… = (∫⇧+x. f x ∂M)"
using f
by (intro nn_integral_eq_simple_integral[symmetric])
(auto simp: simple_function_compose1 simple_bochner_integrable.simps)
finally show ?thesis .
qed
lemma simple_bochner_integral_bounded:
fixes f :: "'a ⇒ 'b::{real_normed_vector, second_countable_topology}"
assumes f[measurable]: "f ∈ borel_measurable M"
assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t"
shows "ennreal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) ≤
(∫⇧+ x. norm (f x - s x) ∂M) + (∫⇧+ x. norm (f x - t x) ∂M)"
(is "ennreal (norm (?s - ?t)) ≤ ?S + ?T")
proof -
have [measurable]: "s ∈ borel_measurable M" "t ∈ borel_measurable M"
using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (λx. s x - t x))"
using s t by (subst simple_bochner_integral_diff) auto
also have "… ≤ simple_bochner_integral M (λx. norm (s x - t x))"
using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t
by (auto intro!: simple_bochner_integral_norm_bound)
also have "… = (∫⇧+x. norm (s x - t x) ∂M)"
using simple_bochner_integrable_compose2[of "λx y. norm (x - y)" M "s" "t"] s t
by (auto intro!: simple_bochner_integral_eq_nn_integral)
also have "… ≤ (∫⇧+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) ∂M)"
by (auto intro!: nn_integral_mono simp: ennreal_plus[symmetric] simp del: ennreal_plus)
(metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
norm_minus_commute norm_triangle_ineq4 order_refl)
also have "… = ?S + ?T"
by (rule nn_integral_add) auto
finally show ?thesis .
qed
inductive has_bochner_integral :: "'a measure ⇒ ('a ⇒ 'b) ⇒ 'b::{real_normed_vector, second_countable_topology} ⇒ bool"
for M f x where
"f ∈ borel_measurable M ⟹
(⋀i. simple_bochner_integrable M (s i)) ⟹
(λi. ∫⇧+x. norm (f x - s i x) ∂M) ⇢ 0 ⟹
(λi. simple_bochner_integral M (s i)) ⇢ x ⟹
has_bochner_integral M f x"
lemma has_bochner_integral_cong:
assumes "M = N" "⋀x. x ∈ space N ⟹ f x = g x" "x = y"
shows "has_bochner_integral M f x ⟷ has_bochner_integral N g y"
unfolding has_bochner_integral.simps assms(1,3)
using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
lemma has_bochner_integral_cong_AE:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (AE x in M. f x = g x) ⟹
has_bochner_integral M f x ⟷ has_bochner_integral M g x"
unfolding has_bochner_integral.simps
by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="λx. x ⇢ 0"]
nn_integral_cong_AE)
auto
lemma borel_measurable_has_bochner_integral:
"has_bochner_integral M f x ⟹ f ∈ borel_measurable M"
by (rule has_bochner_integral.cases)
lemma borel_measurable_has_bochner_integral'[measurable_dest]:
"has_bochner_integral M f x ⟹ g ∈ measurable N M ⟹ (λx. f (g x)) ∈ borel_measurable N"
using borel_measurable_has_bochner_integral[measurable] by measurable
lemma has_bochner_integral_simple_bochner_integrable:
"simple_bochner_integrable M f ⟹ has_bochner_integral M f (simple_bochner_integral M f)"
by (rule has_bochner_integral.intros[where s="λ_. f"])
(auto intro: borel_measurable_simple_function
elim: simple_bochner_integrable.cases
simp: zero_ennreal_def[symmetric])
lemma has_bochner_integral_real_indicator:
assumes [measurable]: "A ∈ sets M" and A: "emeasure M A < ∞"
shows "has_bochner_integral M (indicator A) (measure M A)"
proof -
have sbi: "simple_bochner_integrable M (indicator A::'a ⇒ real)"
proof
have "{y ∈ space M. (indicator A y::real) ≠ 0} = A"
using sets.sets_into_space[OF ‹A∈sets M›] by (auto split: split_indicator)
then show "emeasure M {y ∈ space M. (indicator A y::real) ≠ 0} ≠ ∞"
using A by auto
qed (rule simple_function_indicator assms)+
moreover have "simple_bochner_integral M (indicator A) = measure M A"
using simple_bochner_integral_eq_nn_integral[OF sbi] A
by (simp add: ennreal_indicator emeasure_eq_ennreal_measure)
ultimately show ?thesis
by (metis has_bochner_integral_simple_bochner_integrable)
qed
lemma has_bochner_integral_add[intro]:
"has_bochner_integral M f x ⟹ has_bochner_integral M g y ⟹
has_bochner_integral M (λx. f x + g x) (x + y)"
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
fix sf sg
assume f_sf: "(λi. ∫⇧+ x. norm (f x - sf i x) ∂M) ⇢ 0"
assume g_sg: "(λi. ∫⇧+ x. norm (g x - sg i x) ∂M) ⇢ 0"
assume sf: "∀i. simple_bochner_integrable M (sf i)"
and sg: "∀i. simple_bochner_integrable M (sg i)"
then have [measurable]: "⋀i. sf i ∈ borel_measurable M" "⋀i. sg i ∈ borel_measurable M"
by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
assume [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
show "⋀i. simple_bochner_integrable M (λx. sf i x + sg i x)"
using sf sg by (simp add: simple_bochner_integrable_compose2)
show "(λi. ∫⇧+ x. (norm (f x + g x - (sf i x + sg i x))) ∂M) ⇢ 0"
(is "?f ⇢ 0")
proof (rule tendsto_sandwich)
show "eventually (λn. 0 ≤ ?f n) sequentially" "(λ_. 0) ⇢ 0"
by auto
show "eventually (λi. ?f i ≤ (∫⇧+ x. (norm (f x - sf i x)) ∂M) + ∫⇧+ x. (norm (g x - sg i x)) ∂M) sequentially"
(is "eventually (λi. ?f i ≤ ?g i) sequentially")
proof (intro always_eventually allI)
fix i have "?f i ≤ (∫⇧+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) ∂M)"
by (auto intro!: nn_integral_mono norm_diff_triangle_ineq
simp del: ennreal_plus simp add: ennreal_plus[symmetric])
also have "… = ?g i"
by (intro nn_integral_add) auto
finally show "?f i ≤ ?g i" .
qed
show "?g ⇢ 0"
using tendsto_add[OF f_sf g_sg] by simp
qed
qed (auto simp: simple_bochner_integral_add tendsto_add)
lemma has_bochner_integral_bounded_linear:
assumes "bounded_linear T"
shows "has_bochner_integral M f x ⟹ has_bochner_integral M (λx. T (f x)) (T x)"
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
interpret T: bounded_linear T by fact
have [measurable]: "T ∈ borel_measurable borel"
by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id)
assume [measurable]: "f ∈ borel_measurable M"
then show "(λx. T (f x)) ∈ borel_measurable M"
by auto
fix s assume f_s: "(λi. ∫⇧+ x. norm (f x - s i x) ∂M) ⇢ 0"
assume s: "∀i. simple_bochner_integrable M (s i)"
then show "⋀i. simple_bochner_integrable M (λx. T (s i x))"
by (auto intro: simple_bochner_integrable_compose2 T.zero)
have [measurable]: "⋀i. s i ∈ borel_measurable M"
using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
obtain K where K: "K > 0" "⋀x i. norm (T (f x) - T (s i x)) ≤ norm (f x - s i x) * K"
using T.pos_bounded by (auto simp: T.diff[symmetric])
show "(λi. ∫⇧+ x. norm (T (f x) - T (s i x)) ∂M) ⇢ 0"
(is "?f ⇢ 0")
proof (rule tendsto_sandwich)
show "eventually (λn. 0 ≤ ?f n) sequentially" "(λ_. 0) ⇢ 0"
by auto
show "eventually (λi. ?f i ≤ K * (∫⇧+ x. norm (f x - s i x) ∂M)) sequentially"
(is "eventually (λi. ?f i ≤ ?g i) sequentially")
proof (intro always_eventually allI)
fix i have "?f i ≤ (∫⇧+ x. ennreal K * norm (f x - s i x) ∂M)"
using K by (intro nn_integral_mono) (auto simp: ac_simps ennreal_mult[symmetric])
also have "… = ?g i"
using K by (intro nn_integral_cmult) auto
finally show "?f i ≤ ?g i" .
qed
show "?g ⇢ 0"
using ennreal_tendsto_cmult[OF _ f_s] by simp
qed
assume "(λi. simple_bochner_integral M (s i)) ⇢ x"
with s show "(λi. simple_bochner_integral M (λx. T (s i x))) ⇢ T x"
by (auto intro!: T.tendsto simp: T.simple_bochner_integral_linear)
qed
lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (λx. 0) 0"
by (auto intro!: has_bochner_integral.intros[where s="λ_ _. 0"]
simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps
simple_bochner_integral_def image_constant_conv)
lemma has_bochner_integral_scaleR_left[intro]:
"(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. f x *⇩R c) (x *⇩R c)"
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left])
lemma has_bochner_integral_scaleR_right[intro]:
"(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. c *⇩R f x) (c *⇩R x)"
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right])
lemma has_bochner_integral_mult_left[intro]:
fixes c :: "_::{real_normed_algebra,second_countable_topology}"
shows "(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. f x * c) (x * c)"
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left])
lemma has_bochner_integral_mult_right[intro]:
fixes c :: "_::{real_normed_algebra,second_countable_topology}"
shows "(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. c * f x) (c * x)"
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right])
lemmas has_bochner_integral_divide =
has_bochner_integral_bounded_linear[OF bounded_linear_divide]
lemma has_bochner_integral_divide_zero[intro]:
fixes c :: "_::{real_normed_field, field, second_countable_topology}"
shows "(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. f x / c) (x / c)"
using has_bochner_integral_divide by (cases "c = 0") auto
lemma has_bochner_integral_inner_left[intro]:
"(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. f x ∙ c) (x ∙ c)"
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left])
lemma has_bochner_integral_inner_right[intro]:
"(c ≠ 0 ⟹ has_bochner_integral M f x) ⟹ has_bochner_integral M (λx. c ∙ f x) (c ∙ x)"
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right])
lemmas has_bochner_integral_minus =
has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
lemmas has_bochner_integral_Re =
has_bochner_integral_bounded_linear[OF bounded_linear_Re]
lemmas has_bochner_integral_Im =
has_bochner_integral_bounded_linear[OF bounded_linear_Im]
lemmas has_bochner_integral_cnj =
has_bochner_integral_bounded_linear[OF bounded_linear_cnj]
lemmas has_bochner_integral_of_real =
has_bochner_integral_bounded_linear[OF bounded_linear_of_real]
lemmas has_bochner_integral_fst =
has_bochner_integral_bounded_linear[OF bounded_linear_fst]
lemmas has_bochner_integral_snd =
has_bochner_integral_bounded_linear[OF bounded_linear_snd]
lemma has_bochner_integral_indicator:
"A ∈ sets M ⟹ emeasure M A < ∞ ⟹
has_bochner_integral M (λx. indicator A x *⇩R c) (measure M A *⇩R c)"
by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator)
lemma has_bochner_integral_diff:
"has_bochner_integral M f x ⟹ has_bochner_integral M g y ⟹
has_bochner_integral M (λx. f x - g x) (x - y)"
unfolding diff_conv_add_uminus
by (intro has_bochner_integral_add has_bochner_integral_minus)
lemma has_bochner_integral_setsum:
"(⋀i. i ∈ I ⟹ has_bochner_integral M (f i) (x i)) ⟹
has_bochner_integral M (λx. ∑i∈I. f i x) (∑i∈I. x i)"
by (induct I rule: infinite_finite_induct) auto
lemma has_bochner_integral_implies_finite_norm:
"has_bochner_integral M f x ⟹ (∫⇧+x. norm (f x) ∂M) < ∞"
proof (elim has_bochner_integral.cases)
fix s v
assume [measurable]: "f ∈ borel_measurable M" and s: "⋀i. simple_bochner_integrable M (s i)" and
lim_0: "(λi. ∫⇧+ x. ennreal (norm (f x - s i x)) ∂M) ⇢ 0"
from order_tendstoD[OF lim_0, of "∞"]
obtain i where f_s_fin: "(∫⇧+ x. ennreal (norm (f x - s i x)) ∂M) < ∞"
by (auto simp: eventually_sequentially)
have [measurable]: "⋀i. s i ∈ borel_measurable M"
using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
def m ≡ "if space M = {} then 0 else Max ((λx. norm (s i x))`space M)"
have "finite (s i ` space M)"
using s by (auto simp: simple_function_def simple_bochner_integrable.simps)
then have "finite (norm ` s i ` space M)"
by (rule finite_imageI)
then have "⋀x. x ∈ space M ⟹ norm (s i x) ≤ m" "0 ≤ m"
by (auto simp: m_def image_comp comp_def Max_ge_iff)
then have "(∫⇧+x. norm (s i x) ∂M) ≤ (∫⇧+x. ennreal m * indicator {x∈space M. s i x ≠ 0} x ∂M)"
by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
also have "… < ∞"
using s by (subst nn_integral_cmult_indicator) (auto simp: ‹0 ≤ m› simple_bochner_integrable.simps ennreal_mult_less_top less_top)
finally have s_fin: "(∫⇧+x. norm (s i x) ∂M) < ∞" .
have "(∫⇧+ x. norm (f x) ∂M) ≤ (∫⇧+ x. ennreal (norm (f x - s i x)) + ennreal (norm (s i x)) ∂M)"
by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
(metis add.commute norm_triangle_sub)
also have "… = (∫⇧+x. norm (f x - s i x) ∂M) + (∫⇧+x. norm (s i x) ∂M)"
by (rule nn_integral_add) auto
also have "… < ∞"
using s_fin f_s_fin by auto
finally show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞" .
qed
lemma has_bochner_integral_norm_bound:
assumes i: "has_bochner_integral M f x"
shows "norm x ≤ (∫⇧+x. norm (f x) ∂M)"
using assms proof
fix s assume
x: "(λi. simple_bochner_integral M (s i)) ⇢ x" (is "?s ⇢ x") and
s[simp]: "⋀i. simple_bochner_integrable M (s i)" and
lim: "(λi. ∫⇧+ x. ennreal (norm (f x - s i x)) ∂M) ⇢ 0" and
f[measurable]: "f ∈ borel_measurable M"
have [measurable]: "⋀i. s i ∈ borel_measurable M"
using s by (auto simp: simple_bochner_integrable.simps intro: borel_measurable_simple_function)
show "norm x ≤ (∫⇧+x. norm (f x) ∂M)"
proof (rule LIMSEQ_le)
show "(λi. ennreal (norm (?s i))) ⇢ norm x"
using x by (auto simp: tendsto_ennreal_iff intro: tendsto_intros)
show "∃N. ∀n≥N. norm (?s n) ≤ (∫⇧+x. norm (f x - s n x) ∂M) + (∫⇧+x. norm (f x) ∂M)"
(is "∃N. ∀n≥N. _ ≤ ?t n")
proof (intro exI allI impI)
fix n
have "ennreal (norm (?s n)) ≤ simple_bochner_integral M (λx. norm (s n x))"
by (auto intro!: simple_bochner_integral_norm_bound)
also have "… = (∫⇧+x. norm (s n x) ∂M)"
by (intro simple_bochner_integral_eq_nn_integral)
(auto intro: s simple_bochner_integrable_compose2)
also have "… ≤ (∫⇧+x. ennreal (norm (f x - s n x)) + norm (f x) ∂M)"
by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
(metis add.commute norm_minus_commute norm_triangle_sub)
also have "… = ?t n"
by (rule nn_integral_add) auto
finally show "norm (?s n) ≤ ?t n" .
qed
have "?t ⇢ 0 + (∫⇧+ x. ennreal (norm (f x)) ∂M)"
using has_bochner_integral_implies_finite_norm[OF i]
by (intro tendsto_add tendsto_const lim)
then show "?t ⇢ ∫⇧+ x. ennreal (norm (f x)) ∂M"
by simp
qed
qed
lemma has_bochner_integral_eq:
"has_bochner_integral M f x ⟹ has_bochner_integral M f y ⟹ x = y"
proof (elim has_bochner_integral.cases)
assume f[measurable]: "f ∈ borel_measurable M"
fix s t
assume "(λi. ∫⇧+ x. norm (f x - s i x) ∂M) ⇢ 0" (is "?S ⇢ 0")
assume "(λi. ∫⇧+ x. norm (f x - t i x) ∂M) ⇢ 0" (is "?T ⇢ 0")
assume s: "⋀i. simple_bochner_integrable M (s i)"
assume t: "⋀i. simple_bochner_integrable M (t i)"
have [measurable]: "⋀i. s i ∈ borel_measurable M" "⋀i. t i ∈ borel_measurable M"
using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
let ?s = "λi. simple_bochner_integral M (s i)"
let ?t = "λi. simple_bochner_integral M (t i)"
assume "?s ⇢ x" "?t ⇢ y"
then have "(λi. norm (?s i - ?t i)) ⇢ norm (x - y)"
by (intro tendsto_intros)
moreover
have "(λi. ennreal (norm (?s i - ?t i))) ⇢ ennreal 0"
proof (rule tendsto_sandwich)
show "eventually (λi. 0 ≤ ennreal (norm (?s i - ?t i))) sequentially" "(λ_. 0) ⇢ ennreal 0"
by auto
show "eventually (λi. norm (?s i - ?t i) ≤ ?S i + ?T i) sequentially"
by (intro always_eventually allI simple_bochner_integral_bounded s t f)
show "(λi. ?S i + ?T i) ⇢ ennreal 0"
using tendsto_add[OF ‹?S ⇢ 0› ‹?T ⇢ 0›] by simp
qed
then have "(λi. norm (?s i - ?t i)) ⇢ 0"
by (simp add: ennreal_0[symmetric] del: ennreal_0)
ultimately have "norm (x - y) = 0"
by (rule LIMSEQ_unique)
then show "x = y" by simp
qed
lemma has_bochner_integralI_AE:
assumes f: "has_bochner_integral M f x"
and g: "g ∈ borel_measurable M"
and ae: "AE x in M. f x = g x"
shows "has_bochner_integral M g x"
using f
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
fix s assume "(λi. ∫⇧+ x. ennreal (norm (f x - s i x)) ∂M) ⇢ 0"
also have "(λi. ∫⇧+ x. ennreal (norm (f x - s i x)) ∂M) = (λi. ∫⇧+ x. ennreal (norm (g x - s i x)) ∂M)"
using ae
by (intro ext nn_integral_cong_AE, eventually_elim) simp
finally show "(λi. ∫⇧+ x. ennreal (norm (g x - s i x)) ∂M) ⇢ 0" .
qed (auto intro: g)
lemma has_bochner_integral_eq_AE:
assumes f: "has_bochner_integral M f x"
and g: "has_bochner_integral M g y"
and ae: "AE x in M. f x = g x"
shows "x = y"
proof -
from assms have "has_bochner_integral M g x"
by (auto intro: has_bochner_integralI_AE)
from this g show "x = y"
by (rule has_bochner_integral_eq)
qed
lemma simple_bochner_integrable_restrict_space:
fixes f :: "_ ⇒ 'b::real_normed_vector"
assumes Ω: "Ω ∩ space M ∈ sets M"
shows "simple_bochner_integrable (restrict_space M Ω) f ⟷
simple_bochner_integrable M (λx. indicator Ω x *⇩R f x)"
by (simp add: simple_bochner_integrable.simps space_restrict_space
simple_function_restrict_space[OF Ω] emeasure_restrict_space[OF Ω] Collect_restrict
indicator_eq_0_iff conj_ac)
lemma simple_bochner_integral_restrict_space:
fixes f :: "_ ⇒ 'b::real_normed_vector"
assumes Ω: "Ω ∩ space M ∈ sets M"
assumes f: "simple_bochner_integrable (restrict_space M Ω) f"
shows "simple_bochner_integral (restrict_space M Ω) f =
simple_bochner_integral M (λx. indicator Ω x *⇩R f x)"
proof -
have "finite ((λx. indicator Ω x *⇩R f x)`space M)"
using f simple_bochner_integrable_restrict_space[OF Ω, of f]
by (simp add: simple_bochner_integrable.simps simple_function_def)
then show ?thesis
by (auto simp: space_restrict_space measure_restrict_space[OF Ω(1)] le_infI2
simple_bochner_integral_def Collect_restrict
split: split_indicator split_indicator_asm
intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure])
qed
context
notes [[inductive_internals]]
begin
inductive integrable for M f where
"has_bochner_integral M f x ⟹ integrable M f"
end
definition lebesgue_integral ("integral⇧L") where
"integral⇧L M f = (if ∃x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
syntax
"_lebesgue_integral" :: "pttrn ⇒ real ⇒ 'a measure ⇒ real" ("∫((2 _./ _)/ ∂_)" [60,61] 110)
translations
"∫ x. f ∂M" == "CONST lebesgue_integral M (λx. f)"
syntax
"_ascii_lebesgue_integral" :: "pttrn ⇒ 'a measure ⇒ real ⇒ real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
translations
"LINT x|M. f" == "CONST lebesgue_integral M (λx. f)"
lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x ⟹ integral⇧L M f = x"
by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
lemma has_bochner_integral_integrable:
"integrable M f ⟹ has_bochner_integral M f (integral⇧L M f)"
by (auto simp: has_bochner_integral_integral_eq integrable.simps)
lemma has_bochner_integral_iff:
"has_bochner_integral M f x ⟷ integrable M f ∧ integral⇧L M f = x"
by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros)
lemma simple_bochner_integrable_eq_integral:
"simple_bochner_integrable M f ⟹ simple_bochner_integral M f = integral⇧L M f"
using has_bochner_integral_simple_bochner_integrable[of M f]
by (simp add: has_bochner_integral_integral_eq)
lemma not_integrable_integral_eq: "¬ integrable M f ⟹ integral⇧L M f = 0"
unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])
lemma integral_eq_cases:
"integrable M f ⟷ integrable N g ⟹
(integrable M f ⟹ integrable N g ⟹ integral⇧L M f = integral⇧L N g) ⟹
integral⇧L M f = integral⇧L N g"
by (metis not_integrable_integral_eq)
lemma borel_measurable_integrable[measurable_dest]: "integrable M f ⟹ f ∈ borel_measurable M"
by (auto elim: integrable.cases has_bochner_integral.cases)
lemma borel_measurable_integrable'[measurable_dest]:
"integrable M f ⟹ g ∈ measurable N M ⟹ (λx. f (g x)) ∈ borel_measurable N"
using borel_measurable_integrable[measurable] by measurable
lemma integrable_cong:
"M = N ⟹ (⋀x. x ∈ space N ⟹ f x = g x) ⟹ integrable M f ⟷ integrable N g"
using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
lemma integrable_cong_AE:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ AE x in M. f x = g x ⟹
integrable M f ⟷ integrable M g"
unfolding integrable.simps
by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)
lemma integral_cong:
"M = N ⟹ (⋀x. x ∈ space N ⟹ f x = g x) ⟹ integral⇧L M f = integral⇧L N g"
using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
lemma integral_cong_AE:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ AE x in M. f x = g x ⟹
integral⇧L M f = integral⇧L M g"
unfolding lebesgue_integral_def
by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)
lemma integrable_add[simp, intro]: "integrable M f ⟹ integrable M g ⟹ integrable M (λx. f x + g x)"
by (auto simp: integrable.simps)
lemma integrable_zero[simp, intro]: "integrable M (λx. 0)"
by (metis has_bochner_integral_zero integrable.simps)
lemma integrable_setsum[simp, intro]: "(⋀i. i ∈ I ⟹ integrable M (f i)) ⟹ integrable M (λx. ∑i∈I. f i x)"
by (metis has_bochner_integral_setsum integrable.simps)
lemma integrable_indicator[simp, intro]: "A ∈ sets M ⟹ emeasure M A < ∞ ⟹
integrable M (λx. indicator A x *⇩R c)"
by (metis has_bochner_integral_indicator integrable.simps)
lemma integrable_real_indicator[simp, intro]: "A ∈ sets M ⟹ emeasure M A < ∞ ⟹
integrable M (indicator A :: 'a ⇒ real)"
by (metis has_bochner_integral_real_indicator integrable.simps)
lemma integrable_diff[simp, intro]: "integrable M f ⟹ integrable M g ⟹ integrable M (λx. f x - g x)"
by (auto simp: integrable.simps intro: has_bochner_integral_diff)
lemma integrable_bounded_linear: "bounded_linear T ⟹ integrable M f ⟹ integrable M (λx. T (f x))"
by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)
lemma integrable_scaleR_left[simp, intro]: "(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. f x *⇩R c)"
unfolding integrable.simps by fastforce
lemma integrable_scaleR_right[simp, intro]: "(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. c *⇩R f x)"
unfolding integrable.simps by fastforce
lemma integrable_mult_left[simp, intro]:
fixes c :: "_::{real_normed_algebra,second_countable_topology}"
shows "(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. f x * c)"
unfolding integrable.simps by fastforce
lemma integrable_mult_right[simp, intro]:
fixes c :: "_::{real_normed_algebra,second_countable_topology}"
shows "(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. c * f x)"
unfolding integrable.simps by fastforce
lemma integrable_divide_zero[simp, intro]:
fixes c :: "_::{real_normed_field, field, second_countable_topology}"
shows "(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. f x / c)"
unfolding integrable.simps by fastforce
lemma integrable_inner_left[simp, intro]:
"(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. f x ∙ c)"
unfolding integrable.simps by fastforce
lemma integrable_inner_right[simp, intro]:
"(c ≠ 0 ⟹ integrable M f) ⟹ integrable M (λx. c ∙ f x)"
unfolding integrable.simps by fastforce
lemmas integrable_minus[simp, intro] =
integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
lemmas integrable_divide[simp, intro] =
integrable_bounded_linear[OF bounded_linear_divide]
lemmas integrable_Re[simp, intro] =
integrable_bounded_linear[OF bounded_linear_Re]
lemmas integrable_Im[simp, intro] =
integrable_bounded_linear[OF bounded_linear_Im]
lemmas integrable_cnj[simp, intro] =
integrable_bounded_linear[OF bounded_linear_cnj]
lemmas integrable_of_real[simp, intro] =
integrable_bounded_linear[OF bounded_linear_of_real]
lemmas integrable_fst[simp, intro] =
integrable_bounded_linear[OF bounded_linear_fst]
lemmas integrable_snd[simp, intro] =
integrable_bounded_linear[OF bounded_linear_snd]
lemma integral_zero[simp]: "integral⇧L M (λx. 0) = 0"
by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)
lemma integral_add[simp]: "integrable M f ⟹ integrable M g ⟹
integral⇧L M (λx. f x + g x) = integral⇧L M f + integral⇧L M g"
by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable)
lemma integral_diff[simp]: "integrable M f ⟹ integrable M g ⟹
integral⇧L M (λx. f x - g x) = integral⇧L M f - integral⇧L M g"
by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
lemma integral_setsum: "(⋀i. i ∈ I ⟹ integrable M (f i)) ⟹
integral⇧L M (λx. ∑i∈I. f i x) = (∑i∈I. integral⇧L M (f i))"
by (intro has_bochner_integral_integral_eq has_bochner_integral_setsum has_bochner_integral_integrable)
lemma integral_setsum'[simp]: "(⋀i. i ∈ I =simp=> integrable M (f i)) ⟹
integral⇧L M (λx. ∑i∈I. f i x) = (∑i∈I. integral⇧L M (f i))"
unfolding simp_implies_def by (rule integral_setsum)
lemma integral_bounded_linear: "bounded_linear T ⟹ integrable M f ⟹
integral⇧L M (λx. T (f x)) = T (integral⇧L M f)"
by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
lemma integral_bounded_linear':
assumes T: "bounded_linear T" and T': "bounded_linear T'"
assumes *: "¬ (∀x. T x = 0) ⟹ (∀x. T' (T x) = x)"
shows "integral⇧L M (λx. T (f x)) = T (integral⇧L M f)"
proof cases
assume "(∀x. T x = 0)" then show ?thesis
by simp
next
assume **: "¬ (∀x. T x = 0)"
show ?thesis
proof cases
assume "integrable M f" with T show ?thesis
by (rule integral_bounded_linear)
next
assume not: "¬ integrable M f"
moreover have "¬ integrable M (λx. T (f x))"
proof
assume "integrable M (λx. T (f x))"
from integrable_bounded_linear[OF T' this] not *[OF **]
show False
by auto
qed
ultimately show ?thesis
using T by (simp add: not_integrable_integral_eq linear_simps)
qed
qed
lemma integral_scaleR_left[simp]: "(c ≠ 0 ⟹ integrable M f) ⟹ (∫ x. f x *⇩R c ∂M) = integral⇧L M f *⇩R c"
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
lemma integral_scaleR_right[simp]: "(∫ x. c *⇩R f x ∂M) = c *⇩R integral⇧L M f"
by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp
lemma integral_mult_left[simp]:
fixes c :: "_::{real_normed_algebra,second_countable_topology}"
shows "(c ≠ 0 ⟹ integrable M f) ⟹ (∫ x. f x * c ∂M) = integral⇧L M f * c"
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)
lemma integral_mult_right[simp]:
fixes c :: "_::{real_normed_algebra,second_countable_topology}"
shows "(c ≠ 0 ⟹ integrable M f) ⟹ (∫ x. c * f x ∂M) = c * integral⇧L M f"
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
lemma integral_mult_left_zero[simp]:
fixes c :: "_::{real_normed_field,second_countable_topology}"
shows "(∫ x. f x * c ∂M) = integral⇧L M f * c"
by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp
lemma integral_mult_right_zero[simp]:
fixes c :: "_::{real_normed_field,second_countable_topology}"
shows "(∫ x. c * f x ∂M) = c * integral⇧L M f"
by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp
lemma integral_inner_left[simp]: "(c ≠ 0 ⟹ integrable M f) ⟹ (∫ x. f x ∙ c ∂M) = integral⇧L M f ∙ c"
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
lemma integral_inner_right[simp]: "(c ≠ 0 ⟹ integrable M f) ⟹ (∫ x. c ∙ f x ∂M) = c ∙ integral⇧L M f"
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
lemma integral_divide_zero[simp]:
fixes c :: "_::{real_normed_field, field, second_countable_topology}"
shows "integral⇧L M (λx. f x / c) = integral⇧L M f / c"
by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
lemma integral_minus[simp]: "integral⇧L M (λx. - f x) = - integral⇧L M f"
by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp
lemma integral_complex_of_real[simp]: "integral⇧L M (λx. complex_of_real (f x)) = of_real (integral⇧L M f)"
by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp
lemma integral_cnj[simp]: "integral⇧L M (λx. cnj (f x)) = cnj (integral⇧L M f)"
by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp
lemmas integral_divide[simp] =
integral_bounded_linear[OF bounded_linear_divide]
lemmas integral_Re[simp] =
integral_bounded_linear[OF bounded_linear_Re]
lemmas integral_Im[simp] =
integral_bounded_linear[OF bounded_linear_Im]
lemmas integral_of_real[simp] =
integral_bounded_linear[OF bounded_linear_of_real]
lemmas integral_fst[simp] =
integral_bounded_linear[OF bounded_linear_fst]
lemmas integral_snd[simp] =
integral_bounded_linear[OF bounded_linear_snd]
lemma integral_norm_bound_ennreal:
"integrable M f ⟹ norm (integral⇧L M f) ≤ (∫⇧+x. norm (f x) ∂M)"
by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)
lemma integrableI_sequence:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes f[measurable]: "f ∈ borel_measurable M"
assumes s: "⋀i. simple_bochner_integrable M (s i)"
assumes lim: "(λi. ∫⇧+x. norm (f x - s i x) ∂M) ⇢ 0" (is "?S ⇢ 0")
shows "integrable M f"
proof -
let ?s = "λn. simple_bochner_integral M (s n)"
have "∃x. ?s ⇢ x"
unfolding convergent_eq_cauchy
proof (rule metric_CauchyI)
fix e :: real assume "0 < e"
then have "0 < ennreal (e / 2)" by auto
from order_tendstoD(2)[OF lim this]
obtain M where M: "⋀n. M ≤ n ⟹ ?S n < e / 2"
by (auto simp: eventually_sequentially)
show "∃M. ∀m≥M. ∀n≥M. dist (?s m) (?s n) < e"
proof (intro exI allI impI)
fix m n assume m: "M ≤ m" and n: "M ≤ n"
have "?S n ≠ ∞"
using M[OF n] by auto
have "norm (?s n - ?s m) ≤ ?S n + ?S m"
by (intro simple_bochner_integral_bounded s f)
also have "… < ennreal (e / 2) + e / 2"
by (intro add_strict_mono M n m)
also have "… = e" using ‹0<e› by (simp del: ennreal_plus add: ennreal_plus[symmetric])
finally show "dist (?s n) (?s m) < e"
using ‹0<e› by (simp add: dist_norm ennreal_less_iff)
qed
qed
then obtain x where "?s ⇢ x" ..
show ?thesis
by (rule, rule) fact+
qed
lemma nn_integral_dominated_convergence_norm:
fixes u' :: "_ ⇒ _::{real_normed_vector, second_countable_topology}"
assumes [measurable]:
"⋀i. u i ∈ borel_measurable M" "u' ∈ borel_measurable M" "w ∈ borel_measurable M"
and bound: "⋀j. AE x in M. norm (u j x) ≤ w x"
and w: "(∫⇧+x. w x ∂M) < ∞"
and u': "AE x in M. (λi. u i x) ⇢ u' x"
shows "(λi. (∫⇧+x. norm (u' x - u i x) ∂M)) ⇢ 0"
proof -
have "AE x in M. ∀j. norm (u j x) ≤ w x"
unfolding AE_all_countable by rule fact
with u' have bnd: "AE x in M. ∀j. norm (u' x - u j x) ≤ 2 * w x"
proof (eventually_elim, intro allI)
fix i x assume "(λi. u i x) ⇢ u' x" "∀j. norm (u j x) ≤ w x" "∀j. norm (u j x) ≤ w x"
then have "norm (u' x) ≤ w x" "norm (u i x) ≤ w x"
by (auto intro: LIMSEQ_le_const2 tendsto_norm)
then have "norm (u' x) + norm (u i x) ≤ 2 * w x"
by simp
also have "norm (u' x - u i x) ≤ norm (u' x) + norm (u i x)"
by (rule norm_triangle_ineq4)
finally (xtrans) show "norm (u' x - u i x) ≤ 2 * w x" .
qed
have w_nonneg: "AE x in M. 0 ≤ w x"
using bound[of 0] by (auto intro: order_trans[OF norm_ge_zero])
have "(λi. (∫⇧+x. norm (u' x - u i x) ∂M)) ⇢ (∫⇧+x. 0 ∂M)"
proof (rule nn_integral_dominated_convergence)
show "(∫⇧+x. 2 * w x ∂M) < ∞"
by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) (insert w_nonneg, auto simp: ennreal_mult )
show "AE x in M. (λi. ennreal (norm (u' x - u i x))) ⇢ 0"
using u'
proof eventually_elim
fix x assume "(λi. u i x) ⇢ u' x"
from tendsto_diff[OF tendsto_const[of "u' x"] this]
show "(λi. ennreal (norm (u' x - u i x))) ⇢ 0"
by (simp add: tendsto_norm_zero_iff ennreal_0[symmetric] del: ennreal_0)
qed
qed (insert bnd w_nonneg, auto)
then show ?thesis by simp
qed
lemma integrableI_bounded:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes f[measurable]: "f ∈ borel_measurable M" and fin: "(∫⇧+x. norm (f x) ∂M) < ∞"
shows "integrable M f"
proof -
from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
s: "⋀i. simple_function M (s i)" and
pointwise: "⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x" and
bound: "⋀i x. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)"
by simp metis
show ?thesis
proof (rule integrableI_sequence)
{ fix i
have "(∫⇧+x. norm (s i x) ∂M) ≤ (∫⇧+x. ennreal (2 * norm (f x)) ∂M)"
by (intro nn_integral_mono) (simp add: bound)
also have "… = 2 * (∫⇧+x. ennreal (norm (f x)) ∂M)"
by (simp add: ennreal_mult nn_integral_cmult)
also have "… < top"
using fin by (simp add: ennreal_mult_less_top)
finally have "(∫⇧+x. norm (s i x) ∂M) < ∞"
by simp }
note fin_s = this
show "⋀i. simple_bochner_integrable M (s i)"
by (rule simple_bochner_integrableI_bounded) fact+
show "(λi. ∫⇧+ x. ennreal (norm (f x - s i x)) ∂M) ⇢ 0"
proof (rule nn_integral_dominated_convergence_norm)
show "⋀j. AE x in M. norm (s j x) ≤ 2 * norm (f x)"
using bound by auto
show "⋀i. s i ∈ borel_measurable M" "(λx. 2 * norm (f x)) ∈ borel_measurable M"
using s by (auto intro: borel_measurable_simple_function)
show "(∫⇧+ x. ennreal (2 * norm (f x)) ∂M) < ∞"
using fin by (simp add: nn_integral_cmult ennreal_mult ennreal_mult_less_top)
show "AE x in M. (λi. s i x) ⇢ f x"
using pointwise by auto
qed fact
qed fact
qed
lemma integrableI_bounded_set:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "A ∈ sets M" "f ∈ borel_measurable M"
assumes finite: "emeasure M A < ∞"
and bnd: "AE x in M. x ∈ A ⟶ norm (f x) ≤ B"
and null: "AE x in M. x ∉ A ⟶ f x = 0"
shows "integrable M f"
proof (rule integrableI_bounded)
{ fix x :: 'b have "norm x ≤ B ⟹ 0 ≤ B"
using norm_ge_zero[of x] by arith }
with bnd null have "(∫⇧+ x. ennreal (norm (f x)) ∂M) ≤ (∫⇧+ x. ennreal (max 0 B) * indicator A x ∂M)"
by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
also have "… < ∞"
using finite by (subst nn_integral_cmult_indicator) (auto simp: ennreal_mult_less_top)
finally show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞" .
qed simp
lemma integrableI_bounded_set_indicator:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "A ∈ sets M ⟹ f ∈ borel_measurable M ⟹
emeasure M A < ∞ ⟹ (AE x in M. x ∈ A ⟶ norm (f x) ≤ B) ⟹
integrable M (λx. indicator A x *⇩R f x)"
by (rule integrableI_bounded_set[where A=A]) auto
lemma integrableI_nonneg:
fixes f :: "'a ⇒ real"
assumes "f ∈ borel_measurable M" "AE x in M. 0 ≤ f x" "(∫⇧+x. f x ∂M) < ∞"
shows "integrable M f"
proof -
have "(∫⇧+x. norm (f x) ∂M) = (∫⇧+x. f x ∂M)"
using assms by (intro nn_integral_cong_AE) auto
then show ?thesis
using assms by (intro integrableI_bounded) auto
qed
lemma integrable_iff_bounded:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "integrable M f ⟷ f ∈ borel_measurable M ∧ (∫⇧+x. norm (f x) ∂M) < ∞"
using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f]
unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto
lemma integrable_bound:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
and g :: "'a ⇒ 'c::{banach, second_countable_topology}"
shows "integrable M f ⟹ g ∈ borel_measurable M ⟹ (AE x in M. norm (g x) ≤ norm (f x)) ⟹
integrable M g"
unfolding integrable_iff_bounded
proof safe
assume "f ∈ borel_measurable M" "g ∈ borel_measurable M"
assume "AE x in M. norm (g x) ≤ norm (f x)"
then have "(∫⇧+ x. ennreal (norm (g x)) ∂M) ≤ (∫⇧+ x. ennreal (norm (f x)) ∂M)"
by (intro nn_integral_mono_AE) auto
also assume "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞"
finally show "(∫⇧+ x. ennreal (norm (g x)) ∂M) < ∞" .
qed
lemma integrable_mult_indicator:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "A ∈ sets M ⟹ integrable M f ⟹ integrable M (λx. indicator A x *⇩R f x)"
by (rule integrable_bound[of M f]) (auto split: split_indicator)
lemma integrable_real_mult_indicator:
fixes f :: "'a ⇒ real"
shows "A ∈ sets M ⟹ integrable M f ⟹ integrable M (λx. f x * indicator A x)"
using integrable_mult_indicator[of A M f] by (simp add: mult_ac)
lemma integrable_abs[simp, intro]:
fixes f :: "'a ⇒ real"
assumes [measurable]: "integrable M f" shows "integrable M (λx. ¦f x¦)"
using assms by (rule integrable_bound) auto
lemma integrable_norm[simp, intro]:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "integrable M f" shows "integrable M (λx. norm (f x))"
using assms by (rule integrable_bound) auto
lemma integrable_norm_cancel:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "integrable M (λx. norm (f x))" "f ∈ borel_measurable M" shows "integrable M f"
using assms by (rule integrable_bound) auto
lemma integrable_norm_iff:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "f ∈ borel_measurable M ⟹ integrable M (λx. norm (f x)) ⟷ integrable M f"
by (auto intro: integrable_norm_cancel)
lemma integrable_abs_cancel:
fixes f :: "'a ⇒ real"
assumes [measurable]: "integrable M (λx. ¦f x¦)" "f ∈ borel_measurable M" shows "integrable M f"
using assms by (rule integrable_bound) auto
lemma integrable_abs_iff:
fixes f :: "'a ⇒ real"
shows "f ∈ borel_measurable M ⟹ integrable M (λx. ¦f x¦) ⟷ integrable M f"
by (auto intro: integrable_abs_cancel)
lemma integrable_max[simp, intro]:
fixes f :: "'a ⇒ real"
assumes fg[measurable]: "integrable M f" "integrable M g"
shows "integrable M (λx. max (f x) (g x))"
using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
by (rule integrable_bound) auto
lemma integrable_min[simp, intro]:
fixes f :: "'a ⇒ real"
assumes fg[measurable]: "integrable M f" "integrable M g"
shows "integrable M (λx. min (f x) (g x))"
using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
by (rule integrable_bound) auto
lemma integral_minus_iff[simp]:
"integrable M (λx. - f x ::'a::{banach, second_countable_topology}) ⟷ integrable M f"
unfolding integrable_iff_bounded
by (auto intro: borel_measurable_uminus[of "λx. - f x" M, simplified])
lemma integrable_indicator_iff:
"integrable M (indicator A::_ ⇒ real) ⟷ A ∩ space M ∈ sets M ∧ emeasure M (A ∩ space M) < ∞"
by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator nn_integral_indicator'
cong: conj_cong)
lemma integral_indicator[simp]: "integral⇧L M (indicator A) = measure M (A ∩ space M)"
proof cases
assume *: "A ∩ space M ∈ sets M ∧ emeasure M (A ∩ space M) < ∞"
have "integral⇧L M (indicator A) = integral⇧L M (indicator (A ∩ space M))"
by (intro integral_cong) (auto split: split_indicator)
also have "… = measure M (A ∩ space M)"
using * by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator) auto
finally show ?thesis .
next
assume *: "¬ (A ∩ space M ∈ sets M ∧ emeasure M (A ∩ space M) < ∞)"
have "integral⇧L M (indicator A) = integral⇧L M (indicator (A ∩ space M) :: _ ⇒ real)"
by (intro integral_cong) (auto split: split_indicator)
also have "… = 0"
using * by (subst not_integrable_integral_eq) (auto simp: integrable_indicator_iff)
also have "… = measure M (A ∩ space M)"
using * by (auto simp: measure_def emeasure_notin_sets not_less top_unique)
finally show ?thesis .
qed
lemma integrable_discrete_difference:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes X: "countable X"
assumes null: "⋀x. x ∈ X ⟹ emeasure M {x} = 0"
assumes sets: "⋀x. x ∈ X ⟹ {x} ∈ sets M"
assumes eq: "⋀x. x ∈ space M ⟹ x ∉ X ⟹ f x = g x"
shows "integrable M f ⟷ integrable M g"
unfolding integrable_iff_bounded
proof (rule conj_cong)
{ assume "f ∈ borel_measurable M" then have "g ∈ borel_measurable M"
by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
moreover
{ assume "g ∈ borel_measurable M" then have "f ∈ borel_measurable M"
by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
ultimately show "f ∈ borel_measurable M ⟷ g ∈ borel_measurable M" ..
next
have "AE x in M. x ∉ X"
by (rule AE_discrete_difference) fact+
then have "(∫⇧+ x. norm (f x) ∂M) = (∫⇧+ x. norm (g x) ∂M)"
by (intro nn_integral_cong_AE) (auto simp: eq)
then show "(∫⇧+ x. norm (f x) ∂M) < ∞ ⟷ (∫⇧+ x. norm (g x) ∂M) < ∞"
by simp
qed
lemma integral_discrete_difference:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes X: "countable X"
assumes null: "⋀x. x ∈ X ⟹ emeasure M {x} = 0"
assumes sets: "⋀x. x ∈ X ⟹ {x} ∈ sets M"
assumes eq: "⋀x. x ∈ space M ⟹ x ∉ X ⟹ f x = g x"
shows "integral⇧L M f = integral⇧L M g"
proof (rule integral_eq_cases)
show eq: "integrable M f ⟷ integrable M g"
by (rule integrable_discrete_difference[where X=X]) fact+
assume f: "integrable M f"
show "integral⇧L M f = integral⇧L M g"
proof (rule integral_cong_AE)
show "f ∈ borel_measurable M" "g ∈ borel_measurable M"
using f eq by (auto intro: borel_measurable_integrable)
have "AE x in M. x ∉ X"
by (rule AE_discrete_difference) fact+
with AE_space show "AE x in M. f x = g x"
by eventually_elim fact
qed
qed
lemma has_bochner_integral_discrete_difference:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes X: "countable X"
assumes null: "⋀x. x ∈ X ⟹ emeasure M {x} = 0"
assumes sets: "⋀x. x ∈ X ⟹ {x} ∈ sets M"
assumes eq: "⋀x. x ∈ space M ⟹ x ∉ X ⟹ f x = g x"
shows "has_bochner_integral M f x ⟷ has_bochner_integral M g x"
using integrable_discrete_difference[of X M f g, OF assms]
using integral_discrete_difference[of X M f g, OF assms]
by (metis has_bochner_integral_iff)
lemma
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
assumes "f ∈ borel_measurable M" "⋀i. s i ∈ borel_measurable M" "integrable M w"
assumes lim: "AE x in M. (λi. s i x) ⇢ f x"
assumes bound: "⋀i. AE x in M. norm (s i x) ≤ w x"
shows integrable_dominated_convergence: "integrable M f"
and integrable_dominated_convergence2: "⋀i. integrable M (s i)"
and integral_dominated_convergence: "(λi. integral⇧L M (s i)) ⇢ integral⇧L M f"
proof -
have w_nonneg: "AE x in M. 0 ≤ w x"
using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
then have "(∫⇧+x. w x ∂M) = (∫⇧+x. norm (w x) ∂M)"
by (intro nn_integral_cong_AE) auto
with ‹integrable M w› have w: "w ∈ borel_measurable M" "(∫⇧+x. w x ∂M) < ∞"
unfolding integrable_iff_bounded by auto
show int_s: "⋀i. integrable M (s i)"
unfolding integrable_iff_bounded
proof
fix i
have "(∫⇧+ x. ennreal (norm (s i x)) ∂M) ≤ (∫⇧+x. w x ∂M)"
using bound[of i] w_nonneg by (intro nn_integral_mono_AE) auto
with w show "(∫⇧+ x. ennreal (norm (s i x)) ∂M) < ∞" by auto
qed fact
have all_bound: "AE x in M. ∀i. norm (s i x) ≤ w x"
using bound unfolding AE_all_countable by auto
show int_f: "integrable M f"
unfolding integrable_iff_bounded
proof
have "(∫⇧+ x. ennreal (norm (f x)) ∂M) ≤ (∫⇧+x. w x ∂M)"
using all_bound lim w_nonneg
proof (intro nn_integral_mono_AE, eventually_elim)
fix x assume "∀i. norm (s i x) ≤ w x" "(λi. s i x) ⇢ f x" "0 ≤ w x"
then show "ennreal (norm (f x)) ≤ ennreal (w x)"
by (intro LIMSEQ_le_const2[where X="λi. ennreal (norm (s i x))"]) (auto intro: tendsto_intros)
qed
with w show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞" by auto
qed fact
have "(λn. ennreal (norm (integral⇧L M (s n) - integral⇧L M f))) ⇢ ennreal 0" (is "?d ⇢ ennreal 0")
proof (rule tendsto_sandwich)
show "eventually (λn. ennreal 0 ≤ ?d n) sequentially" "(λ_. ennreal 0) ⇢ ennreal 0" by auto
show "eventually (λn. ?d n ≤ (∫⇧+x. norm (s n x - f x) ∂M)) sequentially"
proof (intro always_eventually allI)
fix n
have "?d n = norm (integral⇧L M (λx. s n x - f x))"
using int_f int_s by simp
also have "… ≤ (∫⇧+x. norm (s n x - f x) ∂M)"
by (intro int_f int_s integrable_diff integral_norm_bound_ennreal)
finally show "?d n ≤ (∫⇧+x. norm (s n x - f x) ∂M)" .
qed
show "(λn. ∫⇧+x. norm (s n x - f x) ∂M) ⇢ ennreal 0"
unfolding ennreal_0
apply (subst norm_minus_commute)
proof (rule nn_integral_dominated_convergence_norm[where w=w])
show "⋀n. s n ∈ borel_measurable M"
using int_s unfolding integrable_iff_bounded by auto
qed fact+
qed
then have "(λn. integral⇧L M (s n) - integral⇧L M f) ⇢ 0"
by (simp add: tendsto_norm_zero_iff del: ennreal_0)
from tendsto_add[OF this tendsto_const[of "integral⇧L M f"]]
show "(λi. integral⇧L M (s i)) ⇢ integral⇧L M f" by simp
qed
context
fixes s :: "real ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
and f :: "'a ⇒ 'b" and M
assumes "f ∈ borel_measurable M" "⋀t. s t ∈ borel_measurable M" "integrable M w"
assumes lim: "AE x in M. ((λi. s i x) ⤏ f x) at_top"
assumes bound: "∀⇩F i in at_top. AE x in M. norm (s i x) ≤ w x"
begin
lemma integral_dominated_convergence_at_top: "((λt. integral⇧L M (s t)) ⤏ integral⇧L M f) at_top"
proof (rule tendsto_at_topI_sequentially)
fix X :: "nat ⇒ real" assume X: "filterlim X at_top sequentially"
from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
obtain N where w: "⋀n. N ≤ n ⟹ AE x in M. norm (s (X n) x) ≤ w x"
by (auto simp: eventually_sequentially)
show "(λn. integral⇧L M (s (X n))) ⇢ integral⇧L M f"
proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
show "AE x in M. norm (s (X (n + N)) x) ≤ w x" for n
by (rule w) auto
show "AE x in M. (λn. s (X (n + N)) x) ⇢ f x"
using lim
proof eventually_elim
fix x assume "((λi. s i x) ⤏ f x) at_top"
then show "(λn. s (X (n + N)) x) ⇢ f x"
by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
qed
qed fact+
qed
lemma integrable_dominated_convergence_at_top: "integrable M f"
proof -
from bound obtain N where w: "⋀n. N ≤ n ⟹ AE x in M. norm (s n x) ≤ w x"
by (auto simp: eventually_at_top_linorder)
show ?thesis
proof (rule integrable_dominated_convergence)
show "AE x in M. norm (s (N + i) x) ≤ w x" for i :: nat
by (intro w) auto
show "AE x in M. (λi. s (N + real i) x) ⇢ f x"
using lim
proof eventually_elim
fix x assume "((λi. s i x) ⤏ f x) at_top"
then show "(λn. s (N + n) x) ⇢ f x"
by (rule filterlim_compose)
(auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially)
qed
qed fact+
qed
end
lemma integrable_mult_left_iff:
fixes f :: "'a ⇒ real"
shows "integrable M (λx. c * f x) ⟷ c = 0 ∨ integrable M f"
using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "λx. c * f x"]
by (cases "c = 0") auto
lemma integrableI_nn_integral_finite:
assumes [measurable]: "f ∈ borel_measurable M"
and nonneg: "AE x in M. 0 ≤ f x"
and finite: "(∫⇧+x. f x ∂M) = ennreal x"
shows "integrable M f"
proof (rule integrableI_bounded)
have "(∫⇧+ x. ennreal (norm (f x)) ∂M) = (∫⇧+ x. ennreal (f x) ∂M)"
using nonneg by (intro nn_integral_cong_AE) auto
with finite show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞"
by auto
qed simp
lemma integral_nonneg_AE:
fixes f :: "'a ⇒ real"
assumes nonneg: "AE x in M. 0 ≤ f x"
shows "0 ≤ integral⇧L M f"
proof cases
assume f: "integrable M f"
then have [measurable]: "f ∈ M →⇩M borel"
by auto
have "(λx. max 0 (f x)) ∈ M →⇩M borel" "⋀x. 0 ≤ max 0 (f x)" "integrable M (λx. max 0 (f x))"
using f by auto
from this have "0 ≤ integral⇧L M (λx. max 0 (f x))"
proof (induction rule: borel_measurable_induct_real)
case (add f g)
then have "integrable M f" "integrable M g"
by (auto intro!: integrable_bound[OF add.prems])
with add show ?case
by (simp add: nn_integral_add)
next
case (seq U)
show ?case
proof (rule LIMSEQ_le_const)
have U_le: "x ∈ space M ⟹ U i x ≤ max 0 (f x)" for x i
using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
with seq nonneg show "(λi. integral⇧L M (U i)) ⇢ LINT x|M. max 0 (f x)"
by (intro integral_dominated_convergence) auto
have "integrable M (U i)" for i
using seq.prems by (rule integrable_bound) (insert U_le seq, auto)
with seq show "∃N. ∀n≥N. 0 ≤ integral⇧L M (U n)"
by auto
qed
qed (auto simp: measure_nonneg integrable_mult_left_iff)
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_nonneg[simp]:
fixes f :: "'a ⇒ real"
shows "(⋀x. x ∈ space M ⟹ 0 ≤ f x) ⟹ 0 ≤ integral⇧L M f"
by (intro integral_nonneg_AE) auto
lemma nn_integral_eq_integral:
assumes f: "integrable M f"
assumes nonneg: "AE x in M. 0 ≤ f x"
shows "(∫⇧+ x. f x ∂M) = integral⇧L M f"
proof -
{ fix f :: "'a ⇒ real" assume f: "f ∈ borel_measurable M" "⋀x. 0 ≤ f x" "integrable M f"
then have "(∫⇧+ x. f x ∂M) = integral⇧L M f"
proof (induct rule: borel_measurable_induct_real)
case (set A) then show ?case
by (simp add: integrable_indicator_iff ennreal_indicator emeasure_eq_ennreal_measure)
next
case (mult f c) then show ?case
by (auto simp add: integrable_mult_left_iff nn_integral_cmult ennreal_mult integral_nonneg_AE)
next
case (add g f)
then have "integrable M f" "integrable M g"
by (auto intro!: integrable_bound[OF add.prems])
with add show ?case
by (simp add: nn_integral_add integral_nonneg_AE)
next
case (seq U)
show ?case
proof (rule LIMSEQ_unique)
have U_le_f: "x ∈ space M ⟹ U i x ≤ f x" for x i
using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
have int_U: "⋀i. integrable M (U i)"
using seq f U_le_f by (intro integrable_bound[OF f(3)]) auto
from U_le_f seq have "(λi. integral⇧L M (U i)) ⇢ integral⇧L M f"
by (intro integral_dominated_convergence) auto
then show "(λi. ennreal (integral⇧L M (U i))) ⇢ ennreal (integral⇧L M f)"
using seq f int_U by (simp add: f integral_nonneg_AE)
have "(λi. ∫⇧+ x. U i x ∂M) ⇢ ∫⇧+ x. f x ∂M"
using seq U_le_f f
by (intro nn_integral_dominated_convergence[where w=f]) (auto simp: integrable_iff_bounded)
then show "(λi. ∫x. U i x ∂M) ⇢ ∫⇧+x. f x ∂M"
using seq int_U by simp
qed
qed }
from this[of "λx. max 0 (f x)"] assms have "(∫⇧+ x. max 0 (f x) ∂M) = integral⇧L M (λx. max 0 (f x))"
by simp
also have "… = integral⇧L M f"
using assms by (auto intro!: integral_cong_AE simp: integral_nonneg_AE)
also have "(∫⇧+ x. max 0 (f x) ∂M) = (∫⇧+ x. f x ∂M)"
using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
finally show ?thesis .
qed
lemma
fixes f :: "_ ⇒ _ ⇒ 'a :: {banach, second_countable_topology}"
assumes integrable[measurable]: "⋀i. integrable M (f i)"
and summable: "AE x in M. summable (λi. norm (f i x))"
and sums: "summable (λi. (∫x. norm (f i x) ∂M))"
shows integrable_suminf: "integrable M (λx. (∑i. f i x))" (is "integrable M ?S")
and sums_integral: "(λi. integral⇧L M (f i)) sums (∫x. (∑i. f i x) ∂M)" (is "?f sums ?x")
and integral_suminf: "(∫x. (∑i. f i x) ∂M) = (∑i. integral⇧L M (f i))"
and summable_integral: "summable (λi. integral⇧L M (f i))"
proof -
have 1: "integrable M (λx. ∑i. norm (f i x))"
proof (rule integrableI_bounded)
have "(∫⇧+ x. ennreal (norm (∑i. norm (f i x))) ∂M) = (∫⇧+ x. (∑i. ennreal (norm (f i x))) ∂M)"
apply (intro nn_integral_cong_AE)
using summable
apply eventually_elim
apply (simp add: suminf_nonneg ennreal_suminf_neq_top)
done
also have "… = (∑i. ∫⇧+ x. norm (f i x) ∂M)"
by (intro nn_integral_suminf) auto
also have "… = (∑i. ennreal (∫x. norm (f i x) ∂M))"
by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
finally show "(∫⇧+ x. ennreal (norm (∑i. norm (f i x))) ∂M) < ∞"
by (simp add: sums ennreal_suminf_neq_top less_top[symmetric] integral_nonneg_AE)
qed simp
have 2: "AE x in M. (λn. ∑i<n. f i x) ⇢ (∑i. f i x)"
using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
have 3: "⋀j. AE x in M. norm (∑i<j. f i x) ≤ (∑i. norm (f i x))"
using summable
proof eventually_elim
fix j x assume [simp]: "summable (λi. norm (f i x))"
have "norm (∑i<j. f i x) ≤ (∑i<j. norm (f i x))" by (rule norm_setsum)
also have "… ≤ (∑i. norm (f i x))"
using setsum_le_suminf[of "λi. norm (f i x)"] unfolding sums_iff by auto
finally show "norm (∑i<j. f i x) ≤ (∑i. norm (f i x))" by simp
qed
note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
note int = integral_dominated_convergence[OF _ _ 1 2 3]
show "integrable M ?S"
by (rule ibl) measurable
show "?f sums ?x" unfolding sums_def
using int by (simp add: integrable)
then show "?x = suminf ?f" "summable ?f"
unfolding sums_iff by auto
qed
lemma integral_norm_bound:
fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
shows "integrable M f ⟹ norm (integral⇧L M f) ≤ (∫x. norm (f x) ∂M)"
using nn_integral_eq_integral[of M "λx. norm (f x)"]
using integral_norm_bound_ennreal[of M f] by (simp add: integral_nonneg_AE)
lemma integral_eq_nn_integral:
assumes [measurable]: "f ∈ borel_measurable M"
assumes nonneg: "AE x in M. 0 ≤ f x"
shows "integral⇧L M f = enn2real (∫⇧+ x. ennreal (f x) ∂M)"
proof cases
assume *: "(∫⇧+ x. ennreal (f x) ∂M) = ∞"
also have "(∫⇧+ x. ennreal (f x) ∂M) = (∫⇧+ x. ennreal (norm (f x)) ∂M)"
using nonneg by (intro nn_integral_cong_AE) auto
finally have "¬ integrable M f"
by (auto simp: integrable_iff_bounded)
then show ?thesis
by (simp add: * not_integrable_integral_eq)
next
assume "(∫⇧+ x. ennreal (f x) ∂M) ≠ ∞"
then have "integrable M f"
by (cases "∫⇧+ x. ennreal (f x) ∂M" rule: ennreal_cases)
(auto intro!: integrableI_nn_integral_finite assms)
from nn_integral_eq_integral[OF this] nonneg show ?thesis
by (simp add: integral_nonneg_AE)
qed
lemma enn2real_nn_integral_eq_integral:
assumes eq: "AE x in M. f x = ennreal (g x)" and nn: "AE x in M. 0 ≤ g x"
and fin: "(∫⇧+x. f x ∂M) < top"
and [measurable]: "g ∈ M →⇩M borel"
shows "enn2real (∫⇧+x. f x ∂M) = (∫x. g x ∂M)"
proof -
have "ennreal (enn2real (∫⇧+x. f x ∂M)) = (∫⇧+x. f x ∂M)"
using fin by (intro ennreal_enn2real) auto
also have "… = (∫⇧+x. g x ∂M)"
using eq by (rule nn_integral_cong_AE)
also have "… = (∫x. g x ∂M)"
proof (rule nn_integral_eq_integral)
show "integrable M g"
proof (rule integrableI_bounded)
have "(∫⇧+ x. ennreal (norm (g x)) ∂M) = (∫⇧+ x. f x ∂M)"
using eq nn by (auto intro!: nn_integral_cong_AE elim!: eventually_elim2)
also note fin
finally show "(∫⇧+ x. ennreal (norm (g x)) ∂M) < ∞"
by simp
qed simp
qed fact
finally show ?thesis
using nn by (simp add: integral_nonneg_AE)
qed
lemma has_bochner_integral_nn_integral:
assumes "f ∈ borel_measurable M" "AE x in M. 0 ≤ f x" "0 ≤ x"
assumes "(∫⇧+x. f x ∂M) = ennreal x"
shows "has_bochner_integral M f x"
unfolding has_bochner_integral_iff
using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
lemma integrableI_simple_bochner_integrable:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "simple_bochner_integrable M f ⟹ integrable M f"
by (intro integrableI_sequence[where s="λ_. f"] borel_measurable_simple_function)
(auto simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps)
lemma integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "integrable M f"
assumes base: "⋀A c. A ∈ sets M ⟹ emeasure M A < ∞ ⟹ P (λx. indicator A x *⇩R c)"
assumes add: "⋀f g. integrable M f ⟹ P f ⟹ integrable M g ⟹ P g ⟹ P (λx. f x + g x)"
assumes lim: "⋀f s. (⋀i. integrable M (s i)) ⟹ (⋀i. P (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)) ⟹ integrable M f ⟹ P f"
shows "P f"
proof -
from ‹integrable M f› have f: "f ∈ borel_measurable M" "(∫⇧+x. norm (f x) ∂M) < ∞"
unfolding integrable_iff_bounded by auto
from borel_measurable_implies_sequence_metric[OF f(1)]
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)"
unfolding norm_conv_dist by metis
{ fix f A
have [simp]: "P (λx. 0)"
using base[of "{}" undefined] by simp
have "(⋀i::'b. i ∈ A ⟹ integrable M (f i::'a ⇒ 'b)) ⟹
(⋀i. i ∈ A ⟹ P (f i)) ⟹ P (λx. ∑i∈A. f i x)"
by (induct A rule: infinite_finite_induct) (auto intro!: add) }
note setsum = this
def s' ≡ "λi z. indicator (space M) z *⇩R s i z"
then have s'_eq_s: "⋀i x. x ∈ space M ⟹ s' i x = s i x"
by simp
have sf[measurable]: "⋀i. simple_function M (s' i)"
unfolding s'_def using s(1)
by (intro simple_function_compose2[where h="op *⇩R"] simple_function_indicator) auto
{ fix i
have "⋀z. {y. s' i z = y ∧ y ∈ s' i ` space M ∧ y ≠ 0 ∧ z ∈ space M} =
(if z ∈ space M ∧ s' i z ≠ 0 then {s' i z} else {})"
by (auto simp add: s'_def split: split_indicator)
then have "⋀z. s' i = (λz. ∑y∈s' i`space M - {0}. indicator {x∈space M. s' i x = y} z *⇩R y)"
using sf by (auto simp: fun_eq_iff simple_function_def s'_def) }
note s'_eq = this
show "P f"
proof (rule lim)
fix i
have "(∫⇧+x. norm (s' i x) ∂M) ≤ (∫⇧+x. ennreal (2 * norm (f x)) ∂M)"
using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
also have "… < ∞"
using f by (simp add: nn_integral_cmult ennreal_mult_less_top ennreal_mult)
finally have sbi: "simple_bochner_integrable M (s' i)"
using sf by (intro simple_bochner_integrableI_bounded) auto
then show "integrable M (s' i)"
by (rule integrableI_simple_bochner_integrable)
{ fix x assume"x ∈ space M" "s' i x ≠ 0"
then have "emeasure M {y ∈ space M. s' i y = s' i x} ≤ emeasure M {y ∈ space M. s' i y ≠ 0}"
by (intro emeasure_mono) auto
also have "… < ∞"
using sbi by (auto elim: simple_bochner_integrable.cases simp: less_top)
finally have "emeasure M {y ∈ space M. s' i y = s' i x} ≠ ∞" by simp }
then show "P (s' i)"
by (subst s'_eq) (auto intro!: setsum base simp: less_top)
fix x assume "x ∈ space M" with s show "(λi. s' i x) ⇢ f x"
by (simp add: s'_eq_s)
show "norm (s' i x) ≤ 2 * norm (f x)"
using ‹x ∈ space M› s by (simp add: s'_eq_s)
qed fact
qed
lemma integral_eq_zero_AE:
"(AE x in M. f x = 0) ⟹ integral⇧L M f = 0"
using integral_cong_AE[of f M "λ_. 0"]
by (cases "integrable M f") (simp_all add: not_integrable_integral_eq)
lemma integral_nonneg_eq_0_iff_AE:
fixes f :: "_ ⇒ real"
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"
then have "integral⇧N M f = 0"
using nn_integral_eq_integral[OF f nonneg] by simp
then have "AE x in M. ennreal (f x) ≤ 0"
by (simp add: nn_integral_0_iff_AE)
with nonneg show "AE x in M. f x = 0"
by auto
qed (auto simp add: integral_eq_zero_AE)
lemma integral_mono_AE:
fixes f :: "'a ⇒ real"
assumes "integrable M f" "integrable M g" "AE x in M. f x ≤ g x"
shows "integral⇧L M f ≤ integral⇧L M g"
proof -
have "0 ≤ integral⇧L M (λx. g x - f x)"
using assms by (intro integral_nonneg_AE integrable_diff assms) auto
also have "… = integral⇧L M g - integral⇧L M f"
by (intro integral_diff assms)
finally show ?thesis by simp
qed
lemma integral_mono:
fixes f :: "'a ⇒ real"
shows "integrable M f ⟹ integrable M g ⟹ (⋀x. x ∈ space M ⟹ f x ≤ g x) ⟹
integral⇧L M f ≤ integral⇧L M g"
by (intro integral_mono_AE) auto
lemma (in finite_measure) integrable_measure:
assumes I: "disjoint_family_on X I" "countable I"
shows "integrable (count_space I) (λi. measure M (X i))"
proof -
have "(∫⇧+i. measure M (X i) ∂count_space I) = (∫⇧+i. measure M (if X i ∈ sets M then X i else {}) ∂count_space I)"
by (auto intro!: nn_integral_cong measure_notin_sets)
also have "… = measure M (⋃i∈I. if X i ∈ sets M then X i else {})"
using I unfolding emeasure_eq_measure[symmetric]
by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
finally show ?thesis
by (auto intro!: integrableI_bounded)
qed
lemma integrableI_real_bounded:
assumes f: "f ∈ borel_measurable M" and ae: "AE x in M. 0 ≤ f x" and fin: "integral⇧N M f < ∞"
shows "integrable M f"
proof (rule integrableI_bounded)
have "(∫⇧+ x. ennreal (norm (f x)) ∂M) = ∫⇧+ x. ennreal (f x) ∂M"
using ae by (auto intro: nn_integral_cong_AE)
also note fin
finally show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞" .
qed fact
lemma integral_real_bounded:
assumes "0 ≤ r" "integral⇧N M f ≤ ennreal r"
shows "integral⇧L M f ≤ r"
proof cases
assume [simp]: "integrable M f"
have "integral⇧L M (λx. max 0 (f x)) = integral⇧N M (λx. max 0 (f x))"
by (intro nn_integral_eq_integral[symmetric]) auto
also have "… = integral⇧N M f"
by (intro nn_integral_cong) (simp add: max_def ennreal_neg)
also have "… ≤ r"
by fact
finally have "integral⇧L M (λx. max 0 (f x)) ≤ r"
using ‹0 ≤ r› by simp
moreover have "integral⇧L M f ≤ integral⇧L M (λx. max 0 (f x))"
by (rule integral_mono_AE) auto
ultimately show ?thesis
by simp
next
assume "¬ integrable M f" then show ?thesis
using ‹0 ≤ r› by (simp add: not_integrable_integral_eq)
qed
subsection ‹Restricted measure spaces›
lemma integrable_restrict_space:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes Ω[simp]: "Ω ∩ space M ∈ sets M"
shows "integrable (restrict_space M Ω) f ⟷ integrable M (λx. indicator Ω x *⇩R f x)"
unfolding integrable_iff_bounded
borel_measurable_restrict_space_iff[OF Ω]
nn_integral_restrict_space[OF Ω]
by (simp add: ac_simps ennreal_indicator ennreal_mult)
lemma integral_restrict_space:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes Ω[simp]: "Ω ∩ space M ∈ sets M"
shows "integral⇧L (restrict_space M Ω) f = integral⇧L M (λx. indicator Ω x *⇩R f x)"
proof (rule integral_eq_cases)
assume "integrable (restrict_space M Ω) f"
then show ?thesis
proof induct
case (base A c) then show ?case
by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
emeasure_restrict_space Int_absorb1 measure_restrict_space)
next
case (add g f) then show ?case
by (simp add: scaleR_add_right integrable_restrict_space)
next
case (lim f s)
show ?case
proof (rule LIMSEQ_unique)
show "(λi. integral⇧L (restrict_space M Ω) (s i)) ⇢ integral⇧L (restrict_space M Ω) f"
using lim by (intro integral_dominated_convergence[where w="λx. 2 * norm (f x)"]) simp_all
show "(λi. integral⇧L (restrict_space M Ω) (s i)) ⇢ (∫ x. indicator Ω x *⇩R f x ∂M)"
unfolding lim
using lim
by (intro integral_dominated_convergence[where w="λx. 2 * norm (indicator Ω x *⇩R f x)"])
(auto simp add: space_restrict_space integrable_restrict_space simp del: norm_scaleR
split: split_indicator)
qed
qed
qed (simp add: integrable_restrict_space)
lemma integral_empty:
assumes "space M = {}"
shows "integral⇧L M f = 0"
proof -
have "(∫ x. f x ∂M) = (∫ x. 0 ∂M)"
by(rule integral_cong)(simp_all add: assms)
thus ?thesis by simp
qed
subsection ‹Measure spaces with an associated density›
lemma integrable_density:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and g :: "'a ⇒ real"
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
and nn: "AE x in M. 0 ≤ g x"
shows "integrable (density M g) f ⟷ integrable M (λx. g x *⇩R f x)"
unfolding integrable_iff_bounded using nn
apply (simp add: nn_integral_density less_top[symmetric])
apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
apply (auto simp: ennreal_mult)
done
lemma integral_density:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and g :: "'a ⇒ real"
assumes f: "f ∈ borel_measurable M"
and g[measurable]: "g ∈ borel_measurable M" "AE x in M. 0 ≤ g x"
shows "integral⇧L (density M g) f = integral⇧L M (λx. g x *⇩R f x)"
proof (rule integral_eq_cases)
assume "integrable (density M g) f"
then show ?thesis
proof induct
case (base A c)
then have [measurable]: "A ∈ sets M" by auto
have int: "integrable M (λx. g x * indicator A x)"
using g base integrable_density[of "indicator A :: 'a ⇒ real" M g] by simp
then have "integral⇧L M (λx. g x * indicator A x) = (∫⇧+ x. ennreal (g x * indicator A x) ∂M)"
using g by (subst nn_integral_eq_integral) auto
also have "… = (∫⇧+ x. ennreal (g x) * indicator A x ∂M)"
by (intro nn_integral_cong) (auto split: split_indicator)
also have "… = emeasure (density M g) A"
by (rule emeasure_density[symmetric]) auto
also have "… = ennreal (measure (density M g) A)"
using base by (auto intro: emeasure_eq_ennreal_measure)
also have "… = integral⇧L (density M g) (indicator A)"
using base by simp
finally show ?case
using base g
apply (simp add: int integral_nonneg_AE)
apply (subst (asm) ennreal_inj)
apply (auto intro!: integral_nonneg_AE)
done
next
case (add f h)
then have [measurable]: "f ∈ borel_measurable M" "h ∈ borel_measurable M"
by (auto dest!: borel_measurable_integrable)
from add g show ?case
by (simp add: scaleR_add_right integrable_density)
next
case (lim f s)
have [measurable]: "f ∈ borel_measurable M" "⋀i. s i ∈ borel_measurable M"
using lim(1,5)[THEN borel_measurable_integrable] by auto
show ?case
proof (rule LIMSEQ_unique)
show "(λi. integral⇧L M (λx. g x *⇩R s i x)) ⇢ integral⇧L M (λx. g x *⇩R f x)"
proof (rule integral_dominated_convergence)
show "integrable M (λx. 2 * norm (g x *⇩R f x))"
by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
show "AE x in M. (λi. g x *⇩R s i x) ⇢ g x *⇩R f x"
using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M])
show "⋀i. AE x in M. norm (g x *⇩R s i x) ≤ 2 * norm (g x *⇩R f x)"
using lim(4) g by (auto intro!: AE_I2[of M] mult_left_mono simp: field_simps)
qed auto
show "(λi. integral⇧L M (λx. g x *⇩R s i x)) ⇢ integral⇧L (density M g) f"
unfolding lim(2)[symmetric]
by (rule integral_dominated_convergence[where w="λx. 2 * norm (f x)"])
(insert lim(3-5), auto)
qed
qed
qed (simp add: f g integrable_density)
lemma
fixes g :: "'a ⇒ real"
assumes "f ∈ borel_measurable M" "AE x in M. 0 ≤ f x" "g ∈ borel_measurable M"
shows integral_real_density: "integral⇧L (density M f) g = (∫ x. f x * g x ∂M)"
and integrable_real_density: "integrable (density M f) g ⟷ integrable M (λx. f x * g x)"
using assms integral_density[of g M f] integrable_density[of g M f] by auto
lemma has_bochner_integral_density:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and g :: "'a ⇒ real"
shows "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (AE x in M. 0 ≤ g x) ⟹
has_bochner_integral M (λx. g x *⇩R f x) x ⟹ has_bochner_integral (density M g) f x"
by (simp add: has_bochner_integral_iff integrable_density integral_density)
subsection ‹Distributions›
lemma integrable_distr_eq:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "g ∈ measurable M N" "f ∈ borel_measurable N"
shows "integrable (distr M N g) f ⟷ integrable M (λx. f (g x))"
unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
lemma integrable_distr:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "T ∈ measurable M M' ⟹ integrable (distr M M' T) f ⟹ integrable M (λx. f (T x))"
by (subst integrable_distr_eq[symmetric, where g=T])
(auto dest: borel_measurable_integrable)
lemma integral_distr:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes g[measurable]: "g ∈ measurable M N" and f: "f ∈ borel_measurable N"
shows "integral⇧L (distr M N g) f = integral⇧L M (λx. f (g x))"
proof (rule integral_eq_cases)
assume "integrable (distr M N g) f"
then show ?thesis
proof induct
case (base A c)
then have [measurable]: "A ∈ sets N" by auto
from base have int: "integrable (distr M N g) (λa. indicator A a *⇩R c)"
by (intro integrable_indicator)
have "integral⇧L (distr M N g) (λa. indicator A a *⇩R c) = measure (distr M N g) A *⇩R c"
using base by auto
also have "… = measure M (g -` A ∩ space M) *⇩R c"
by (subst measure_distr) auto
also have "… = integral⇧L M (λa. indicator (g -` A ∩ space M) a *⇩R c)"
using base by (auto simp: emeasure_distr)
also have "… = integral⇧L M (λa. indicator A (g a) *⇩R c)"
using int base by (intro integral_cong_AE) (auto simp: emeasure_distr split: split_indicator)
finally show ?case .
next
case (add f h)
then have [measurable]: "f ∈ borel_measurable N" "h ∈ borel_measurable N"
by (auto dest!: borel_measurable_integrable)
from add g show ?case
by (simp add: scaleR_add_right integrable_distr_eq)
next
case (lim f s)
have [measurable]: "f ∈ borel_measurable N" "⋀i. s i ∈ borel_measurable N"
using lim(1,5)[THEN borel_measurable_integrable] by auto
show ?case
proof (rule LIMSEQ_unique)
show "(λi. integral⇧L M (λx. s i (g x))) ⇢ integral⇧L M (λx. f (g x))"
proof (rule integral_dominated_convergence)
show "integrable M (λx. 2 * norm (f (g x)))"
using lim by (auto simp: integrable_distr_eq)
show "AE x in M. (λi. s i (g x)) ⇢ f (g x)"
using lim(3) g[THEN measurable_space] by auto
show "⋀i. AE x in M. norm (s i (g x)) ≤ 2 * norm (f (g x))"
using lim(4) g[THEN measurable_space] by auto
qed auto
show "(λi. integral⇧L M (λx. s i (g x))) ⇢ integral⇧L (distr M N g) f"
unfolding lim(2)[symmetric]
by (rule integral_dominated_convergence[where w="λx. 2 * norm (f x)"])
(insert lim(3-5), auto)
qed
qed
qed (simp add: f g integrable_distr_eq)
lemma has_bochner_integral_distr:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "f ∈ borel_measurable N ⟹ g ∈ measurable M N ⟹
has_bochner_integral M (λx. f (g x)) x ⟹ has_bochner_integral (distr M N g) f x"
by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
subsection ‹Lebesgue integration on @{const count_space}›
lemma integrable_count_space:
fixes f :: "'a ⇒ 'b::{banach,second_countable_topology}"
shows "finite X ⟹ integrable (count_space X) f"
by (auto simp: nn_integral_count_space integrable_iff_bounded)
lemma measure_count_space[simp]:
"B ⊆ A ⟹ finite B ⟹ measure (count_space A) B = card B"
unfolding measure_def by (subst emeasure_count_space ) auto
lemma lebesgue_integral_count_space_finite_support:
assumes f: "finite {a∈A. f a ≠ 0}"
shows "(∫x. f x ∂count_space A) = (∑a | a ∈ A ∧ f a ≠ 0. f a)"
proof -
have eq: "⋀x. x ∈ A ⟹ (∑a | x = a ∧ a ∈ A ∧ f a ≠ 0. f a) = (∑x∈{x}. f x)"
by (intro setsum.mono_neutral_cong_left) auto
have "(∫x. f x ∂count_space A) = (∫x. (∑a | a ∈ A ∧ f a ≠ 0. indicator {a} x *⇩R f a) ∂count_space A)"
by (intro integral_cong refl) (simp add: f eq)
also have "… = (∑a | a ∈ A ∧ f a ≠ 0. measure (count_space A) {a} *⇩R f a)"
by (subst integral_setsum) (auto intro!: setsum.cong)
finally show ?thesis
by auto
qed
lemma lebesgue_integral_count_space_finite: "finite A ⟹ (∫x. f x ∂count_space A) = (∑a∈A. f a)"
by (subst lebesgue_integral_count_space_finite_support)
(auto intro!: setsum.mono_neutral_cong_left)
lemma integrable_count_space_nat_iff:
fixes f :: "nat ⇒ _::{banach,second_countable_topology}"
shows "integrable (count_space UNIV) f ⟷ summable (λx. norm (f x))"
by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat ennreal_suminf_neq_top
intro: summable_suminf_not_top)
lemma sums_integral_count_space_nat:
fixes f :: "nat ⇒ _::{banach,second_countable_topology}"
assumes *: "integrable (count_space UNIV) f"
shows "f sums (integral⇧L (count_space UNIV) f)"
proof -
let ?f = "λn i. indicator {n} i *⇩R f i"
have f': "⋀n i. ?f n i = indicator {n} i *⇩R f n"
by (auto simp: fun_eq_iff split: split_indicator)
have "(λi. ∫n. ?f i n ∂count_space UNIV) sums ∫ n. (∑i. ?f i n) ∂count_space UNIV"
proof (rule sums_integral)
show "⋀i. integrable (count_space UNIV) (?f i)"
using * by (intro integrable_mult_indicator) auto
show "AE n in count_space UNIV. summable (λi. norm (?f i n))"
using summable_finite[of "{n}" "λi. norm (?f i n)" for n] by simp
show "summable (λi. ∫ n. norm (?f i n) ∂count_space UNIV)"
using * by (subst f') (simp add: integrable_count_space_nat_iff)
qed
also have "(∫ n. (∑i. ?f i n) ∂count_space UNIV) = (∫n. f n ∂count_space UNIV)"
using suminf_finite[of "{n}" "λi. ?f i n" for n] by (auto intro!: integral_cong)
also have "(λi. ∫n. ?f i n ∂count_space UNIV) = f"
by (subst f') simp
finally show ?thesis .
qed
lemma integral_count_space_nat:
fixes f :: "nat ⇒ _::{banach,second_countable_topology}"
shows "integrable (count_space UNIV) f ⟹ integral⇧L (count_space UNIV) f = (∑x. f x)"
using sums_integral_count_space_nat by (rule sums_unique)
subsection ‹Point measure›
lemma lebesgue_integral_point_measure_finite:
fixes g :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "finite A ⟹ (⋀a. a ∈ A ⟹ 0 ≤ f a) ⟹
integral⇧L (point_measure A f) g = (∑a∈A. f a *⇩R g a)"
by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def)
lemma integrable_point_measure_finite:
fixes g :: "'a ⇒ 'b::{banach, second_countable_topology}" and f :: "'a ⇒ real"
shows "finite A ⟹ integrable (point_measure A f) g"
unfolding point_measure_def
apply (subst density_cong[where f'="λx. ennreal (max 0 (f x))"])
apply (auto split: split_max simp: ennreal_neg)
apply (subst integrable_density)
apply (auto simp: AE_count_space integrable_count_space)
done
subsection ‹Lebesgue integration on @{const null_measure}›
lemma has_bochner_integral_null_measure_iff[iff]:
"has_bochner_integral (null_measure M) f 0 ⟷ f ∈ borel_measurable M"
by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
intro!: exI[of _ "λn x. 0"] simple_bochner_integrable.intros)
lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f ⟷ f ∈ borel_measurable M"
by (auto simp add: integrable.simps)
lemma integral_null_measure[simp]: "integral⇧L (null_measure M) f = 0"
by (cases "integrable (null_measure M) f")
(auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
subsection ‹Legacy lemmas for the real-valued Lebesgue integral›
lemma real_lebesgue_integral_def:
assumes f[measurable]: "integrable M f"
shows "integral⇧L M f = enn2real (∫⇧+x. f x ∂M) - enn2real (∫⇧+x. ennreal (- f x) ∂M)"
proof -
have "integral⇧L M f = integral⇧L M (λx. max 0 (f x) - max 0 (- f x))"
by (auto intro!: arg_cong[where f="integral⇧L M"])
also have "… = integral⇧L M (λx. max 0 (f x)) - integral⇧L M (λx. max 0 (- f x))"
by (intro integral_diff integrable_max integrable_minus integrable_zero f)
also have "integral⇧L M (λx. max 0 (f x)) = enn2real (∫⇧+x. ennreal (f x) ∂M)"
by (subst integral_eq_nn_integral) (auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: max_def ennreal_neg)
also have "integral⇧L M (λx. max 0 (- f x)) = enn2real (∫⇧+x. ennreal (- f x) ∂M)"
by (subst integral_eq_nn_integral) (auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: max_def ennreal_neg)
finally show ?thesis .
qed
lemma real_integrable_def:
"integrable M f ⟷ f ∈ borel_measurable M ∧
(∫⇧+ x. ennreal (f x) ∂M) ≠ ∞ ∧ (∫⇧+ x. ennreal (- f x) ∂M) ≠ ∞"
unfolding integrable_iff_bounded
proof (safe del: notI)
assume *: "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞"
have "(∫⇧+ x. ennreal (f x) ∂M) ≤ (∫⇧+ x. ennreal (norm (f x)) ∂M)"
by (intro nn_integral_mono) auto
also note *
finally show "(∫⇧+ x. ennreal (f x) ∂M) ≠ ∞"
by simp
have "(∫⇧+ x. ennreal (- f x) ∂M) ≤ (∫⇧+ x. ennreal (norm (f x)) ∂M)"
by (intro nn_integral_mono) auto
also note *
finally show "(∫⇧+ x. ennreal (- f x) ∂M) ≠ ∞"
by simp
next
assume [measurable]: "f ∈ borel_measurable M"
assume fin: "(∫⇧+ x. ennreal (f x) ∂M) ≠ ∞" "(∫⇧+ x. ennreal (- f x) ∂M) ≠ ∞"
have "(∫⇧+ x. norm (f x) ∂M) = (∫⇧+ x. ennreal (f x) + ennreal (- f x) ∂M)"
by (intro nn_integral_cong) (auto simp: abs_real_def ennreal_neg)
also have"… = (∫⇧+ x. ennreal (f x) ∂M) + (∫⇧+ x. ennreal (- f x) ∂M)"
by (intro nn_integral_add) auto
also have "… < ∞"
using fin by (auto simp: less_top)
finally show "(∫⇧+ x. norm (f x) ∂M) < ∞" .
qed
lemma integrableD[dest]:
assumes "integrable M f"
shows "f ∈ borel_measurable M" "(∫⇧+ x. ennreal (f x) ∂M) ≠ ∞" "(∫⇧+ x. ennreal (- f x) ∂M) ≠ ∞"
using assms unfolding real_integrable_def by auto
lemma integrableE:
assumes "integrable M f"
obtains r q where
"(∫⇧+x. ennreal (f x)∂M) = ennreal r"
"(∫⇧+x. ennreal (-f x)∂M) = ennreal q"
"f ∈ borel_measurable M" "integral⇧L M f = r - q"
using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
by (cases rule: ennreal2_cases[of "(∫⇧+x. ennreal (-f x)∂M)" "(∫⇧+x. ennreal (f x)∂M)"]) auto
lemma integral_monotone_convergence_nonneg:
fixes f :: "nat ⇒ 'a ⇒ real"
assumes i: "⋀i. integrable M (f i)" and mono: "AE x in M. mono (λn. f n x)"
and pos: "⋀i. AE x in M. 0 ≤ f i x"
and lim: "AE x in M. (λi. f i x) ⇢ u x"
and ilim: "(λi. integral⇧L M (f i)) ⇢ x"
and u: "u ∈ borel_measurable M"
shows "integrable M u"
and "integral⇧L M u = x"
proof -
have nn: "AE x in M. ∀i. 0 ≤ f i x"
using pos unfolding AE_all_countable by auto
with lim have u_nn: "AE x in M. 0 ≤ u x"
by eventually_elim (auto intro: LIMSEQ_le_const)
have [simp]: "0 ≤ x"
by (intro LIMSEQ_le_const[OF ilim] allI exI impI integral_nonneg_AE pos)
have "(∫⇧+ x. ennreal (u x) ∂M) = (SUP n. (∫⇧+ x. ennreal (f n x) ∂M))"
proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
fix i
from mono nn show "AE x in M. ennreal (f i x) ≤ ennreal (f (Suc i) x)"
by eventually_elim (auto simp: mono_def)
show "(λx. ennreal (f i x)) ∈ borel_measurable M"
using i by auto
next
show "(∫⇧+ x. ennreal (u x) ∂M) = ∫⇧+ x. (SUP i. ennreal (f i x)) ∂M"
apply (rule nn_integral_cong_AE)
using lim mono nn u_nn
apply eventually_elim
apply (simp add: LIMSEQ_unique[OF _ LIMSEQ_SUP] incseq_def)
done
qed
also have "… = ennreal x"
using mono i nn unfolding nn_integral_eq_integral[OF i pos]
by (subst LIMSEQ_unique[OF LIMSEQ_SUP]) (auto simp: mono_def integral_nonneg_AE pos intro!: integral_mono_AE ilim)
finally have "(∫⇧+ x. ennreal (u x) ∂M) = ennreal x" .
moreover have "(∫⇧+ x. ennreal (- u x) ∂M) = 0"
using u u_nn by (subst nn_integral_0_iff_AE) (auto simp add: ennreal_neg)
ultimately show "integrable M u" "integral⇧L M u = x"
by (auto simp: real_integrable_def real_lebesgue_integral_def u)
qed
lemma
fixes f :: "nat ⇒ 'a ⇒ real"
assumes f: "⋀i. integrable M (f i)" and mono: "AE x in M. mono (λn. f n x)"
and lim: "AE x in M. (λi. f i x) ⇢ u x"
and ilim: "(λi. integral⇧L M (f i)) ⇢ x"
and u: "u ∈ borel_measurable M"
shows integrable_monotone_convergence: "integrable M u"
and integral_monotone_convergence: "integral⇧L M u = x"
and has_bochner_integral_monotone_convergence: "has_bochner_integral M u x"
proof -
have 1: "⋀i. integrable M (λx. f i x - f 0 x)"
using f by auto
have 2: "AE x in M. mono (λn. f n x - f 0 x)"
using mono by (auto simp: mono_def le_fun_def)
have 3: "⋀n. AE x in M. 0 ≤ f n x - f 0 x"
using mono by (auto simp: field_simps mono_def le_fun_def)
have 4: "AE x in M. (λi. f i x - f 0 x) ⇢ u x - f 0 x"
using lim by (auto intro!: tendsto_diff)
have 5: "(λi. (∫x. f i x - f 0 x ∂M)) ⇢ x - integral⇧L M (f 0)"
using f ilim by (auto intro!: tendsto_diff)
have 6: "(λx. u x - f 0 x) ∈ borel_measurable M"
using f[of 0] u by auto
note diff = integral_monotone_convergence_nonneg[OF 1 2 3 4 5 6]
have "integrable M (λx. (u x - f 0 x) + f 0 x)"
using diff(1) f by (rule integrable_add)
with diff(2) f show "integrable M u" "integral⇧L M u = x"
by auto
then show "has_bochner_integral M u x"
by (metis has_bochner_integral_integrable)
qed
lemma integral_norm_eq_0_iff:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes f[measurable]: "integrable M f"
shows "(∫x. norm (f x) ∂M) = 0 ⟷ emeasure M {x∈space M. f x ≠ 0} = 0"
proof -
have "(∫⇧+x. norm (f x) ∂M) = (∫x. norm (f x) ∂M)"
using f by (intro nn_integral_eq_integral integrable_norm) auto
then have "(∫x. norm (f x) ∂M) = 0 ⟷ (∫⇧+x. norm (f x) ∂M) = 0"
by simp
also have "… ⟷ emeasure M {x∈space M. ennreal (norm (f x)) ≠ 0} = 0"
by (intro nn_integral_0_iff) auto
finally show ?thesis
by simp
qed
lemma integral_0_iff:
fixes f :: "'a ⇒ real"
shows "integrable M f ⟹ (∫x. ¦f x¦ ∂M) = 0 ⟷ emeasure M {x∈space M. f x ≠ 0} = 0"
using integral_norm_eq_0_iff[of M f] by simp
lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (λx. a)"
using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong add: less_top[symmetric])
lemma lebesgue_integral_const[simp]:
fixes a :: "'a :: {banach, second_countable_topology}"
shows "(∫x. a ∂M) = measure M (space M) *⇩R a"
proof -
{ assume "emeasure M (space M) = ∞" "a ≠ 0"
then have ?thesis
by (auto simp add: not_integrable_integral_eq ennreal_mult_less_top measure_def integrable_iff_bounded) }
moreover
{ assume "a = 0" then have ?thesis by simp }
moreover
{ assume "emeasure M (space M) ≠ ∞"
interpret finite_measure M
proof qed fact
have "(∫x. a ∂M) = (∫x. indicator (space M) x *⇩R a ∂M)"
by (intro integral_cong) auto
also have "… = measure M (space M) *⇩R a"
by (simp add: less_top[symmetric])
finally have ?thesis . }
ultimately show ?thesis by blast
qed
lemma (in finite_measure) integrable_const_bound:
fixes f :: "'a ⇒ 'b::{banach,second_countable_topology}"
shows "AE x in M. norm (f x) ≤ B ⟹ f ∈ borel_measurable M ⟹ integrable M f"
apply (rule integrable_bound[OF integrable_const[of B], of f])
apply assumption
apply (cases "0 ≤ B")
apply auto
done
lemma integral_indicator_finite_real:
fixes f :: "'a ⇒ real"
assumes [simp]: "finite A"
assumes [measurable]: "⋀a. a ∈ A ⟹ {a} ∈ sets M"
assumes finite: "⋀a. a ∈ A ⟹ emeasure M {a} < ∞"
shows "(∫x. f x * indicator A x ∂M) = (∑a∈A. f a * measure M {a})"
proof -
have "(∫x. f x * indicator A x ∂M) = (∫x. (∑a∈A. f a * indicator {a} x) ∂M)"
proof (intro integral_cong refl)
fix x show "f x * indicator A x = (∑a∈A. f a * indicator {a} x)"
by (auto split: split_indicator simp: eq_commute[of x] cong: conj_cong)
qed
also have "… = (∑a∈A. f a * measure M {a})"
using finite by (subst integral_setsum) (auto simp add: integrable_mult_left_iff)
finally show ?thesis .
qed
lemma (in finite_measure) ennreal_integral_real:
assumes [measurable]: "f ∈ borel_measurable M"
assumes ae: "AE x in M. f x ≤ ennreal B" "0 ≤ B"
shows "ennreal (∫x. enn2real (f x) ∂M) = (∫⇧+x. f x ∂M)"
proof (subst nn_integral_eq_integral[symmetric])
show "integrable M (λx. enn2real (f x))"
using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI enn2real_nonneg)
show "(∫⇧+ x. ennreal (enn2real (f x)) ∂M) = integral⇧N M f"
using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
qed (auto simp: enn2real_nonneg)
lemma (in finite_measure) integral_less_AE:
fixes X Y :: "'a ⇒ real"
assumes int: "integrable M X" "integrable M Y"
assumes A: "(emeasure M) A ≠ 0" "A ∈ sets M" "AE x in M. x ∈ A ⟶ X x ≠ Y x"
assumes gt: "AE x in M. X x ≤ Y x"
shows "integral⇧L M X < integral⇧L M Y"
proof -
have "integral⇧L M X ≤ integral⇧L M Y"
using gt int by (intro integral_mono_AE) auto
moreover
have "integral⇧L M X ≠ integral⇧L M Y"
proof
assume eq: "integral⇧L M X = integral⇧L M Y"
have "integral⇧L M (λx. ¦Y x - X x¦) = integral⇧L M (λx. Y x - X x)"
using gt int by (intro integral_cong_AE) auto
also have "… = 0"
using eq int by simp
finally have "(emeasure M) {x ∈ space M. Y x - X x ≠ 0} = 0"
using int by (simp add: integral_0_iff)
moreover
have "(∫⇧+x. indicator A x ∂M) ≤ (∫⇧+x. indicator {x ∈ space M. Y x - X x ≠ 0} x ∂M)"
using A by (intro nn_integral_mono_AE) auto
then have "(emeasure M) A ≤ (emeasure M) {x ∈ space M. Y x - X x ≠ 0}"
using int A by (simp add: integrable_def)
ultimately have "emeasure M A = 0"
by simp
with ‹(emeasure M) A ≠ 0› show False by auto
qed
ultimately show ?thesis by auto
qed
lemma (in finite_measure) integral_less_AE_space:
fixes X Y :: "'a ⇒ real"
assumes int: "integrable M X" "integrable M Y"
assumes gt: "AE x in M. X x < Y x" "emeasure M (space M) ≠ 0"
shows "integral⇧L M X < integral⇧L M Y"
using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
lemma tendsto_integral_at_top:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}"
assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
shows "((λy. ∫ x. indicator {.. y} x *⇩R f x ∂M) ⤏ ∫ x. f x ∂M) at_top"
proof (rule tendsto_at_topI_sequentially)
fix X :: "nat ⇒ real" assume "filterlim X at_top sequentially"
show "(λn. ∫x. indicator {..X n} x *⇩R f x ∂M) ⇢ integral⇧L M f"
proof (rule integral_dominated_convergence)
show "integrable M (λx. norm (f x))"
by (rule integrable_norm) fact
show "AE x in M. (λn. indicator {..X n} x *⇩R f x) ⇢ 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 {..X n} x *⇩R f x) ⇢ f x"
by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {..X n} x *⇩R f x) ≤ norm (f x)"
by (auto split: split_indicator)
qed auto
qed
lemma
fixes f :: "real ⇒ real"
assumes M: "sets M = sets borel"
assumes nonneg: "AE x in M. 0 ≤ f x"
assumes borel: "f ∈ borel_measurable borel"
assumes int: "⋀y. integrable M (λx. f x * indicator {.. y} x)"
assumes conv: "((λy. ∫ x. f x * indicator {.. y} x ∂M) ⤏ x) at_top"
shows has_bochner_integral_monotone_convergence_at_top: "has_bochner_integral M f x"
and integrable_monotone_convergence_at_top: "integrable M f"
and integral_monotone_convergence_at_top:"integral⇧L M f = x"
proof -
from nonneg have "AE x in M. mono (λn::nat. f x * indicator {..real n} x)"
by (auto split: split_indicator intro!: monoI)
{ fix x have "eventually (λn. f x * indicator {..real n} x = f x) sequentially"
by (rule eventually_sequentiallyI[of "nat ⌈x⌉"])
(auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
from filterlim_cong[OF refl refl this]
have "AE x in M. (λi. f x * indicator {..real i} x) ⇢ f x"
by simp
have "(λi. ∫ x. f x * indicator {..real i} x ∂M) ⇢ x"
using conv filterlim_real_sequentially by (rule filterlim_compose)
have M_measure[simp]: "borel_measurable M = borel_measurable borel"
using M by (simp add: sets_eq_imp_space_eq measurable_def)
have "f ∈ borel_measurable M"
using borel by simp
show "has_bochner_integral M f x"
by (rule has_bochner_integral_monotone_convergence) fact+
then show "integrable M f" "integral⇧L M f = x"
by (auto simp: _has_bochner_integral_iff)
qed
subsection ‹Product measure›
lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]: "case_prod f ∈ borel_measurable (N ⨂⇩M M)"
shows "Measurable.pred N (λx. integrable M (f x))"
proof -
have [simp]: "⋀x. x ∈ space N ⟹ integrable M (f x) ⟷ (∫⇧+y. norm (f x y) ∂M) < ∞"
unfolding integrable_iff_bounded by simp
show ?thesis
by (simp cong: measurable_cong)
qed
lemma Collect_subset [simp]: "{x∈A. P x} ⊆ A" by auto
lemma (in sigma_finite_measure) measurable_measure[measurable (raw)]:
"(⋀x. x ∈ space N ⟹ A x ⊆ space M) ⟹
{x ∈ space (N ⨂⇩M M). snd x ∈ A (fst x)} ∈ sets (N ⨂⇩M M) ⟹
(λx. measure M (A x)) ∈ borel_measurable N"
unfolding measure_def by (intro measurable_emeasure borel_measurable_enn2real) auto
lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "case_prod f ∈ borel_measurable (N ⨂⇩M M)"
shows "(λx. ∫y. f x y ∂M) ∈ borel_measurable N"
proof -
from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
then have s: "⋀i. simple_function (N ⨂⇩M M) (s i)"
"⋀x y. x ∈ space N ⟹ y ∈ space M ⟹ (λi. s i (x, y)) ⇢ f x y"
"⋀i x y. x ∈ space N ⟹ y ∈ space M ⟹ norm (s i (x, y)) ≤ 2 * norm (f x y)"
by (auto simp: space_pair_measure)
have [measurable]: "⋀i. s i ∈ borel_measurable (N ⨂⇩M M)"
by (rule borel_measurable_simple_function) fact
have "⋀i. s i ∈ measurable (N ⨂⇩M M) (count_space UNIV)"
by (rule measurable_simple_function) fact
def f' ≡ "λi x. if integrable M (f x) then simple_bochner_integral M (λy. s i (x, y)) else 0"
{ fix i x assume "x ∈ space N"
then have "simple_bochner_integral M (λy. s i (x, y)) =
(∑z∈s i ` (space N × space M). measure M {y ∈ space M. s i (x, y) = z} *⇩R z)"
using s(1)[THEN simple_functionD(1)]
unfolding simple_bochner_integral_def
by (intro setsum.mono_neutral_cong_left)
(auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
note eq = this
show ?thesis
proof (rule borel_measurable_LIMSEQ_metric)
fix i show "f' i ∈ borel_measurable N"
unfolding f'_def by (simp_all add: eq cong: measurable_cong if_cong)
next
fix x assume x: "x ∈ space N"
{ assume int_f: "integrable M (f x)"
have int_2f: "integrable M (λy. 2 * norm (f x y))"
by (intro integrable_norm integrable_mult_right int_f)
have "(λi. integral⇧L M (λy. s i (x, y))) ⇢ integral⇧L M (f x)"
proof (rule integral_dominated_convergence)
from int_f show "f x ∈ borel_measurable M" by auto
show "⋀i. (λy. s i (x, y)) ∈ borel_measurable M"
using x by simp
show "AE xa in M. (λi. s i (x, xa)) ⇢ f x xa"
using x s(2) by auto
show "⋀i. AE xa in M. norm (s i (x, xa)) ≤ 2 * norm (f x xa)"
using x s(3) by auto
qed fact
moreover
{ fix i
have "simple_bochner_integrable M (λy. s i (x, y))"
proof (rule simple_bochner_integrableI_bounded)
have "(λy. s i (x, y)) ` space M ⊆ s i ` (space N × space M)"
using x by auto
then show "simple_function M (λy. s i (x, y))"
using simple_functionD(1)[OF s(1), of i] x
by (intro simple_function_borel_measurable)
(auto simp: space_pair_measure dest: finite_subset)
have "(∫⇧+ y. ennreal (norm (s i (x, y))) ∂M) ≤ (∫⇧+ y. 2 * norm (f x y) ∂M)"
using x s by (intro nn_integral_mono) auto
also have "(∫⇧+ y. 2 * norm (f x y) ∂M) < ∞"
using int_2f by (simp add: integrable_iff_bounded)
finally show "(∫⇧+ xa. ennreal (norm (s i (x, xa))) ∂M) < ∞" .
qed
then have "integral⇧L M (λy. s i (x, y)) = simple_bochner_integral M (λy. s i (x, y))"
by (rule simple_bochner_integrable_eq_integral[symmetric]) }
ultimately have "(λi. simple_bochner_integral M (λy. s i (x, y))) ⇢ integral⇧L M (f x)"
by simp }
then
show "(λi. f' i x) ⇢ integral⇧L M (f x)"
unfolding f'_def
by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
qed
qed
lemma (in pair_sigma_finite) integrable_product_swap:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "integrable (M1 ⨂⇩M M2) f"
shows "integrable (M2 ⨂⇩M M1) (λ(x,y). f (y,x))"
proof -
interpret Q: pair_sigma_finite M2 M1 ..
have *: "(λ(x,y). f (y,x)) = (λx. f (case x of (x,y)⇒(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis unfolding *
by (rule integrable_distr[OF measurable_pair_swap'])
(simp add: distr_pair_swap[symmetric] assms)
qed
lemma (in pair_sigma_finite) integrable_product_swap_iff:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
shows "integrable (M2 ⨂⇩M M1) (λ(x,y). f (y,x)) ⟷ integrable (M1 ⨂⇩M M2) f"
proof -
interpret Q: pair_sigma_finite M2 M1 ..
from Q.integrable_product_swap[of "λ(x,y). f (y,x)"] integrable_product_swap[of f]
show ?thesis by auto
qed
lemma (in pair_sigma_finite) integral_product_swap:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f: "f ∈ borel_measurable (M1 ⨂⇩M M2)"
shows "(∫(x,y). f (y,x) ∂(M2 ⨂⇩M M1)) = integral⇧L (M1 ⨂⇩M M2) f"
proof -
have *: "(λ(x,y). f (y,x)) = (λx. f (case x of (x,y)⇒(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis unfolding *
by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
qed
lemma (in pair_sigma_finite) Fubini_integrable:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M2)"
and integ1: "integrable M1 (λx. ∫ y. norm (f (x, y)) ∂M2)"
and integ2: "AE x in M1. integrable M2 (λy. f (x, y))"
shows "integrable (M1 ⨂⇩M M2) f"
proof (rule integrableI_bounded)
have "(∫⇧+ p. norm (f p) ∂(M1 ⨂⇩M M2)) = (∫⇧+ x. (∫⇧+ y. norm (f (x, y)) ∂M2) ∂M1)"
by (simp add: M2.nn_integral_fst [symmetric])
also have "… = (∫⇧+ x. ¦∫y. norm (f (x, y)) ∂M2¦ ∂M1)"
apply (intro nn_integral_cong_AE)
using integ2
proof eventually_elim
fix x assume "integrable M2 (λy. f (x, y))"
then have f: "integrable M2 (λy. norm (f (x, y)))"
by simp
then have "(∫⇧+y. ennreal (norm (f (x, y))) ∂M2) = ennreal (LINT y|M2. norm (f (x, y)))"
by (rule nn_integral_eq_integral) simp
also have "… = ennreal ¦LINT y|M2. norm (f (x, y))¦"
using f by simp
finally show "(∫⇧+y. ennreal (norm (f (x, y))) ∂M2) = ennreal ¦LINT y|M2. norm (f (x, y))¦" .
qed
also have "… < ∞"
using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
finally show "(∫⇧+ p. norm (f p) ∂(M1 ⨂⇩M M2)) < ∞" .
qed fact
lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
assumes A: "A ∈ sets (M1 ⨂⇩M M2)" and finite: "emeasure (M1 ⨂⇩M M2) A < ∞"
shows "AE x in M1. emeasure M2 {y∈space M2. (x, y) ∈ A} < ∞"
proof -
from M2.emeasure_pair_measure_alt[OF A] finite
have "(∫⇧+ x. emeasure M2 (Pair x -` A) ∂M1) ≠ ∞"
by simp
then have "AE x in M1. emeasure M2 (Pair x -` A) ≠ ∞"
by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
moreover have "⋀x. x ∈ space M1 ⟹ Pair x -` A = {y∈space M2. (x, y) ∈ A}"
using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
ultimately show ?thesis by (auto simp: less_top)
qed
lemma (in pair_sigma_finite) AE_integrable_fst':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "integrable (M1 ⨂⇩M M2) f"
shows "AE x in M1. integrable M2 (λy. f (x, y))"
proof -
have "(∫⇧+x. (∫⇧+y. norm (f (x, y)) ∂M2) ∂M1) = (∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M2))"
by (rule M2.nn_integral_fst) simp
also have "(∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M2)) ≠ ∞"
using f unfolding integrable_iff_bounded by simp
finally have "AE x in M1. (∫⇧+y. norm (f (x, y)) ∂M2) ≠ ∞"
by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
(auto simp: measurable_split_conv)
with AE_space show ?thesis
by eventually_elim
(auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top)
qed
lemma (in pair_sigma_finite) integrable_fst':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "integrable (M1 ⨂⇩M M2) f"
shows "integrable M1 (λx. ∫y. f (x, y) ∂M2)"
unfolding integrable_iff_bounded
proof
show "(λx. ∫ y. f (x, y) ∂M2) ∈ borel_measurable M1"
by (rule M2.borel_measurable_lebesgue_integral) simp
have "(∫⇧+ x. ennreal (norm (∫ y. f (x, y) ∂M2)) ∂M1) ≤ (∫⇧+x. (∫⇧+y. norm (f (x, y)) ∂M2) ∂M1)"
using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ennreal)
also have "(∫⇧+x. (∫⇧+y. norm (f (x, y)) ∂M2) ∂M1) = (∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M2))"
by (rule M2.nn_integral_fst) simp
also have "(∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M2)) < ∞"
using f unfolding integrable_iff_bounded by simp
finally show "(∫⇧+ x. ennreal (norm (∫ y. f (x, y) ∂M2)) ∂M1) < ∞" .
qed
lemma (in pair_sigma_finite) integral_fst':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f: "integrable (M1 ⨂⇩M M2) f"
shows "(∫x. (∫y. f (x, y) ∂M2) ∂M1) = integral⇧L (M1 ⨂⇩M M2) f"
using f proof induct
case (base A c)
have A[measurable]: "A ∈ sets (M1 ⨂⇩M M2)" by fact
have eq: "⋀x y. x ∈ space M1 ⟹ indicator A (x, y) = indicator {y∈space M2. (x, y) ∈ A} y"
using sets.sets_into_space[OF A] by (auto split: split_indicator simp: space_pair_measure)
have int_A: "integrable (M1 ⨂⇩M M2) (indicator A :: _ ⇒ real)"
using base by (rule integrable_real_indicator)
have "(∫ x. ∫ y. indicator A (x, y) *⇩R c ∂M2 ∂M1) = (∫x. measure M2 {y∈space M2. (x, y) ∈ A} *⇩R c ∂M1)"
proof (intro integral_cong_AE, simp, simp)
from AE_integrable_fst'[OF int_A] AE_space
show "AE x in M1. (∫y. indicator A (x, y) *⇩R c ∂M2) = measure M2 {y∈space M2. (x, y) ∈ A} *⇩R c"
by eventually_elim (simp add: eq integrable_indicator_iff)
qed
also have "… = measure (M1 ⨂⇩M M2) A *⇩R c"
proof (subst integral_scaleR_left)
have "(∫⇧+x. ennreal (measure M2 {y ∈ space M2. (x, y) ∈ A}) ∂M1) =
(∫⇧+x. emeasure M2 {y ∈ space M2. (x, y) ∈ A} ∂M1)"
using emeasure_pair_measure_finite[OF base]
by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ennreal_measure)
also have "… = emeasure (M1 ⨂⇩M M2) A"
using sets.sets_into_space[OF A]
by (subst M2.emeasure_pair_measure_alt)
(auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
finally have *: "(∫⇧+x. ennreal (measure M2 {y ∈ space M2. (x, y) ∈ A}) ∂M1) = emeasure (M1 ⨂⇩M M2) A" .
from base * show "integrable M1 (λx. measure M2 {y ∈ space M2. (x, y) ∈ A})"
by (simp add: integrable_iff_bounded)
then have "(∫x. measure M2 {y ∈ space M2. (x, y) ∈ A} ∂M1) =
(∫⇧+x. ennreal (measure M2 {y ∈ space M2. (x, y) ∈ A}) ∂M1)"
by (rule nn_integral_eq_integral[symmetric]) simp
also note *
finally show "(∫x. measure M2 {y ∈ space M2. (x, y) ∈ A} ∂M1) *⇩R c = measure (M1 ⨂⇩M M2) A *⇩R c"
using base by (simp add: emeasure_eq_ennreal_measure)
qed
also have "… = (∫ a. indicator A a *⇩R c ∂(M1 ⨂⇩M M2))"
using base by simp
finally show ?case .
next
case (add f g)
then have [measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M2)" "g ∈ borel_measurable (M1 ⨂⇩M M2)"
by auto
have "(∫ x. ∫ y. f (x, y) + g (x, y) ∂M2 ∂M1) =
(∫ x. (∫ y. f (x, y) ∂M2) + (∫ y. g (x, y) ∂M2) ∂M1)"
apply (rule integral_cong_AE)
apply simp_all
using AE_integrable_fst'[OF add(1)] AE_integrable_fst'[OF add(3)]
apply eventually_elim
apply simp
done
also have "… = (∫ x. f x ∂(M1 ⨂⇩M M2)) + (∫ x. g x ∂(M1 ⨂⇩M M2))"
using integrable_fst'[OF add(1)] integrable_fst'[OF add(3)] add(2,4) by simp
finally show ?case
using add by simp
next
case (lim f s)
then have [measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M2)" "⋀i. s i ∈ borel_measurable (M1 ⨂⇩M M2)"
by auto
show ?case
proof (rule LIMSEQ_unique)
show "(λi. integral⇧L (M1 ⨂⇩M M2) (s i)) ⇢ integral⇧L (M1 ⨂⇩M M2) f"
proof (rule integral_dominated_convergence)
show "integrable (M1 ⨂⇩M M2) (λx. 2 * norm (f x))"
using lim(5) by auto
qed (insert lim, auto)
have "(λi. ∫ x. ∫ y. s i (x, y) ∂M2 ∂M1) ⇢ ∫ x. ∫ y. f (x, y) ∂M2 ∂M1"
proof (rule integral_dominated_convergence)
have "AE x in M1. ∀i. integrable M2 (λy. s i (x, y))"
unfolding AE_all_countable using AE_integrable_fst'[OF lim(1)] ..
with AE_space AE_integrable_fst'[OF lim(5)]
show "AE x in M1. (λi. ∫ y. s i (x, y) ∂M2) ⇢ ∫ y. f (x, y) ∂M2"
proof eventually_elim
fix x assume x: "x ∈ space M1" and
s: "∀i. integrable M2 (λy. s i (x, y))" and f: "integrable M2 (λy. f (x, y))"
show "(λi. ∫ y. s i (x, y) ∂M2) ⇢ ∫ y. f (x, y) ∂M2"
proof (rule integral_dominated_convergence)
show "integrable M2 (λy. 2 * norm (f (x, y)))"
using f by auto
show "AE xa in M2. (λi. s i (x, xa)) ⇢ f (x, xa)"
using x lim(3) by (auto simp: space_pair_measure)
show "⋀i. AE xa in M2. norm (s i (x, xa)) ≤ 2 * norm (f (x, xa))"
using x lim(4) by (auto simp: space_pair_measure)
qed (insert x, measurable)
qed
show "integrable M1 (λx. (∫ y. 2 * norm (f (x, y)) ∂M2))"
by (intro integrable_mult_right integrable_norm integrable_fst' lim)
fix i show "AE x in M1. norm (∫ y. s i (x, y) ∂M2) ≤ (∫ y. 2 * norm (f (x, y)) ∂M2)"
using AE_space AE_integrable_fst'[OF lim(1), of i] AE_integrable_fst'[OF lim(5)]
proof eventually_elim
fix x assume x: "x ∈ space M1"
and s: "integrable M2 (λy. s i (x, y))" and f: "integrable M2 (λy. f (x, y))"
from s have "norm (∫ y. s i (x, y) ∂M2) ≤ (∫⇧+y. norm (s i (x, y)) ∂M2)"
by (rule integral_norm_bound_ennreal)
also have "… ≤ (∫⇧+y. 2 * norm (f (x, y)) ∂M2)"
using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
also have "… = (∫y. 2 * norm (f (x, y)) ∂M2)"
using f by (intro nn_integral_eq_integral) auto
finally show "norm (∫ y. s i (x, y) ∂M2) ≤ (∫ y. 2 * norm (f (x, y)) ∂M2)"
by simp
qed
qed simp_all
then show "(λi. integral⇧L (M1 ⨂⇩M M2) (s i)) ⇢ ∫ x. ∫ y. f (x, y) ∂M2 ∂M1"
using lim by simp
qed
qed
lemma (in pair_sigma_finite)
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes f: "integrable (M1 ⨂⇩M M2) (case_prod f)"
shows AE_integrable_fst: "AE x in M1. integrable M2 (λy. f x y)" (is "?AE")
and integrable_fst: "integrable M1 (λx. ∫y. f x y ∂M2)" (is "?INT")
and integral_fst: "(∫x. (∫y. f x y ∂M2) ∂M1) = integral⇧L (M1 ⨂⇩M M2) (λ(x, y). f x y)" (is "?EQ")
using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto
lemma (in pair_sigma_finite)
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "integrable (M1 ⨂⇩M M2) (case_prod f)"
shows AE_integrable_snd: "AE y in M2. integrable M1 (λx. f x y)" (is "?AE")
and integrable_snd: "integrable M2 (λy. ∫x. f x y ∂M1)" (is "?INT")
and integral_snd: "(∫y. (∫x. f x y ∂M1) ∂M2) = integral⇧L (M1 ⨂⇩M M2) (case_prod f)" (is "?EQ")
proof -
interpret Q: pair_sigma_finite M2 M1 ..
have Q_int: "integrable (M2 ⨂⇩M M1) (λ(x, y). f y x)"
using f unfolding integrable_product_swap_iff[symmetric] by simp
show ?AE using Q.AE_integrable_fst'[OF Q_int] by simp
show ?INT using Q.integrable_fst'[OF Q_int] by simp
show ?EQ using Q.integral_fst'[OF Q_int]
using integral_product_swap[of "case_prod f"] by simp
qed
lemma (in pair_sigma_finite) Fubini_integral:
fixes f :: "_ ⇒ _ ⇒ _ :: {banach, second_countable_topology}"
assumes f: "integrable (M1 ⨂⇩M M2) (case_prod f)"
shows "(∫y. (∫x. f x y ∂M1) ∂M2) = (∫x. (∫y. f x y ∂M2) ∂M1)"
unfolding integral_snd[OF assms] integral_fst[OF assms] ..
lemma (in product_sigma_finite) product_integral_singleton:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
shows "f ∈ borel_measurable (M i) ⟹ (∫x. f (x i) ∂Pi⇩M {i} M) = integral⇧L (M i) f"
apply (subst distr_singleton[symmetric])
apply (subst integral_distr)
apply simp_all
done
lemma (in product_sigma_finite) product_integral_fold:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes IJ[simp]: "I ∩ J = {}" and fin: "finite I" "finite J"
and f: "integrable (Pi⇩M (I ∪ J) M) f"
shows "integral⇧L (Pi⇩M (I ∪ J) M) f = (∫x. (∫y. f (merge I J (x, y)) ∂Pi⇩M J M) ∂Pi⇩M I M)"
proof -
interpret I: finite_product_sigma_finite M I by standard fact
interpret J: finite_product_sigma_finite M J by standard fact
have "finite (I ∪ J)" using fin by auto
interpret IJ: finite_product_sigma_finite M "I ∪ J" by standard fact
interpret P: pair_sigma_finite "Pi⇩M I M" "Pi⇩M J M" ..
let ?M = "merge I J"
let ?f = "λx. f (?M x)"
from f have f_borel: "f ∈ borel_measurable (Pi⇩M (I ∪ J) M)"
by auto
have P_borel: "(λx. f (merge I J x)) ∈ borel_measurable (Pi⇩M I M ⨂⇩M Pi⇩M J M)"
using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
have f_int: "integrable (Pi⇩M I M ⨂⇩M Pi⇩M J M) ?f"
by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
show ?thesis
apply (subst distr_merge[symmetric, OF IJ fin])
apply (subst integral_distr[OF measurable_merge f_borel])
apply (subst P.integral_fst'[symmetric, OF f_int])
apply simp
done
qed
lemma (in product_sigma_finite) product_integral_insert:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes I: "finite I" "i ∉ I"
and f: "integrable (Pi⇩M (insert i I) M) f"
shows "integral⇧L (Pi⇩M (insert i I) M) f = (∫x. (∫y. f (x(i:=y)) ∂M i) ∂Pi⇩M I M)"
proof -
have "integral⇧L (Pi⇩M (insert i I) M) f = integral⇧L (Pi⇩M (I ∪ {i}) M) f"
by simp
also have "… = (∫x. (∫y. f (merge I {i} (x,y)) ∂Pi⇩M {i} M) ∂Pi⇩M I M)"
using f I by (intro product_integral_fold) auto
also have "… = (∫x. (∫y. f (x(i := y)) ∂M i) ∂Pi⇩M I M)"
proof (rule integral_cong[OF refl], subst product_integral_singleton[symmetric])
fix x assume x: "x ∈ space (Pi⇩M I M)"
have f_borel: "f ∈ borel_measurable (Pi⇩M (insert i I) M)"
using f by auto
show "(λy. f (x(i := y))) ∈ borel_measurable (M i)"
using measurable_comp[OF measurable_component_update f_borel, OF x ‹i ∉ I›]
unfolding comp_def .
from x I show "(∫ y. f (merge I {i} (x,y)) ∂Pi⇩M {i} M) = (∫ xa. f (x(i := xa i)) ∂Pi⇩M {i} M)"
by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
qed
finally show ?thesis .
qed
lemma (in product_sigma_finite) product_integrable_setprod:
fixes f :: "'i ⇒ 'a ⇒ _::{real_normed_field,banach,second_countable_topology}"
assumes [simp]: "finite I" and integrable: "⋀i. i ∈ I ⟹ integrable (M i) (f i)"
shows "integrable (Pi⇩M I M) (λx. (∏i∈I. f i (x i)))" (is "integrable _ ?f")
proof (unfold integrable_iff_bounded, intro conjI)
interpret finite_product_sigma_finite M I by standard fact
show "?f ∈ borel_measurable (Pi⇩M I M)"
using assms by simp
have "(∫⇧+ x. ennreal (norm (∏i∈I. f i (x i))) ∂Pi⇩M I M) =
(∫⇧+ x. (∏i∈I. ennreal (norm (f i (x i)))) ∂Pi⇩M I M)"
by (simp add: setprod_norm setprod_ennreal)
also have "… = (∏i∈I. ∫⇧+ x. ennreal (norm (f i x)) ∂M i)"
using assms by (intro product_nn_integral_setprod) auto
also have "… < ∞"
using integrable by (simp add: less_top[symmetric] ennreal_setprod_eq_top integrable_iff_bounded)
finally show "(∫⇧+ x. ennreal (norm (∏i∈I. f i (x i))) ∂Pi⇩M I M) < ∞" .
qed
lemma (in product_sigma_finite) product_integral_setprod:
fixes f :: "'i ⇒ 'a ⇒ _::{real_normed_field,banach,second_countable_topology}"
assumes "finite I" and integrable: "⋀i. i ∈ I ⟹ integrable (M i) (f i)"
shows "(∫x. (∏i∈I. f i (x i)) ∂Pi⇩M I M) = (∏i∈I. integral⇧L (M i) (f i))"
using assms proof induct
case empty
interpret finite_measure "Pi⇩M {} M"
by rule (simp add: space_PiM)
show ?case by (simp add: space_PiM measure_def)
next
case (insert i I)
then have iI: "finite (insert i I)" by auto
then have prod: "⋀J. J ⊆ insert i I ⟹
integrable (Pi⇩M J M) (λx. (∏i∈J. f i (x i)))"
by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
interpret I: finite_product_sigma_finite M I by standard fact
have *: "⋀x y. (∏j∈I. f j (if j = i then y else x j)) = (∏j∈I. f j (x j))"
using ‹i ∉ I› by (auto intro!: setprod.cong)
show ?case
unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
by (simp add: * insert prod subset_insertI)
qed
lemma integrable_subalgebra:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes borel: "f ∈ borel_measurable N"
and N: "sets N ⊆ sets M" "space N = space M" "⋀A. A ∈ sets N ⟹ emeasure N A = emeasure M A"
shows "integrable N f ⟷ integrable M f" (is ?P)
proof -
have "f ∈ borel_measurable M"
using assms by (auto simp: measurable_def)
with assms show ?thesis
using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
qed
lemma integral_subalgebra:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes borel: "f ∈ borel_measurable N"
and N: "sets N ⊆ sets M" "space N = space M" "⋀A. A ∈ sets N ⟹ emeasure N A = emeasure M A"
shows "integral⇧L N f = integral⇧L M f"
proof cases
assume "integrable N f"
then show ?thesis
proof induct
case base with assms show ?case by (auto simp: subset_eq measure_def)
next
case (add f g)
then have "(∫ a. f a + g a ∂N) = integral⇧L M f + integral⇧L M g"
by simp
also have "… = (∫ a. f a + g a ∂M)"
using add integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of g] by simp
finally show ?case .
next
case (lim f s)
then have M: "⋀i. integrable M (s i)" "integrable M f"
using integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of "s i" for i] by simp_all
show ?case
proof (intro LIMSEQ_unique)
show "(λi. integral⇧L N (s i)) ⇢ integral⇧L N f"
apply (rule integral_dominated_convergence[where w="λx. 2 * norm (f x)"])
using lim
apply auto
done
show "(λi. integral⇧L N (s i)) ⇢ integral⇧L M f"
unfolding lim
apply (rule integral_dominated_convergence[where w="λx. 2 * norm (f x)"])
using lim M N(2)
apply auto
done
qed
qed
qed (simp add: not_integrable_integral_eq integrable_subalgebra[OF assms])
hide_const (open) simple_bochner_integral
hide_const (open) simple_bochner_integrable
end