# Theory Bochner_Integration

```(*  Title:      HOL/Analysis/Bochner_Integration.thy
Author:     Johannes Hölzl, TU München
*)

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.

›

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

define e where "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

define A where [abs_def]: "A m n =
{x∈space M. dist (f x) (e n) < 1 / (Suc m) ∧ 1 / (Suc m) ≤ dist (f x) z}" for m n
define B where [abs_def]: "B m = disjointed (A m)" for m

define m where [abs_def]: "m N x = Max {m. m ≤ N ∧ x ∈ (⋃n≤N. B m n)}" for N x
define F where [abs_def]: "F N 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)" for N x

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
define L where "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: F_def L_def) }
note * = this

fix x assume "x ∈ space M"
show "(λi. F i x) ⇢ f x"
proof (cases "f x = z")
case True
then have "⋀i n. x ∉ A i n"
unfolding A_def by auto
then show ?thesis
by (metis B_imp_A F_def LIMSEQ_def True dist_self)
next
case False
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"
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
by (smt (verit, ccfv_threshold) LeastI2 B_imp_A dist_eq_0_iff zero_le_dist)
qed
qed

lemma
fixes f :: "'a ⇒ 'b::semiring_1" assumes "finite A"
shows sum_mult_indicator[simp]: "(∑x ∈ A. f x * indicator (B x) (g x)) = (∑x∈{x∈A. g x ∈ B x}. f x)"
and sum_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!: sum.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

define U' where [abs_def]: "U' i x = indicator (space M) x * enn2real (U i x)" for 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'_sf by (auto simp: U'_def borel_measurable_simple_function)
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"
have "⋀x. x ∈ U' i ` space M ⟹ 0 ≤ x"
by (auto simp: U'_def)
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
next
case (insert x F)
from insert.prems have nonneg: "x ≥ 0" "⋀y. y ∈ F ⟹ y ≥ 0"
by simp_all
hence *: "P (λxa. x * indicat_real {x' ∈ space M. U' i x' = x} xa)"
by (intro mult set) auto
have "P (λz. x * indicat_real {x' ∈ space M. U' i x' = x} z +
(∑y∈F. y * indicat_real {x ∈ space M. U' i x = y} z))"
using insert(1-3)
by (intro add * sum_nonneg mult_nonneg_nonneg)
(auto simp: nonneg indicator_def of_bool_def sum_nonneg_eq_0_iff)
thus ?case
using insert.hyps by (subst sum.insert) auto
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 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}"
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"

define m where "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} ≠ ∞"
using simple_function_finite_support simple_function_compose1 f fin by force
then show "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞" by simp
qed fact

definition✐‹tag important› 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)"

proposition 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!: sum.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 (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!: sum.cong simp: scaleR_sum_left)
also have "… = ?r"
by (subst sum.swap)
(auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
finally show "simple_bochner_integral M f = ?r" .
qed

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
qed

lemma simple_bochner_integral_linear:
assumes "linear f"
assumes g: "simple_bochner_integrable M g"
shows "simple_bochner_integral M (λx. f (g x)) = f (simple_bochner_integral M g)"
proof -
interpret linear f by fact
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"]
elim: simple_bochner_integrable.cases)
also have "… = f (simple_bochner_integral M g)"
by (simp add: simple_bochner_integral_def sum scale)
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 -
from linear_uminus 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"
(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_sum)
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 (force simp: simple_bochner_integral_def intro: sum_nonneg)

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 -
have ennreal_cong_mult: "(x ≠ 0 ⟹ y = z) ⟹ ennreal x * y = ennreal x * z" for x y z
by fastforce

have [measurable]: "f ∈ borel_measurable M"
by (meson borel_measurable_simple_function f(1) 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!: sum.cong ennreal_cong_mult
simp: ac_simps ennreal_mult
simp flip: sum_ennreal)
also have "… = (∫⇧+x. f x ∂M)"
using f
by (metis nn_integral_eq_simple_integral simple_bochner_integrable.cases simple_function_compose1)
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 "(-)" 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)"
proof -
have "⋀x. x ∈ space M ⟹
norm (s x - t x) ≤ norm (f x - s x) + norm (f x - t x)"
by (metis dual_order.refl norm_diff_triangle_le norm_minus_commute)
then show ?thesis
by (metis (mono_tags, lifting) ennreal_leI ennreal_plus nn_integral_mono norm_ge_zero)
qed
also have "… = ?S + ?T"
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_simp nn_integral_cong_simp)

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 flip: zero_ennreal_def)

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
ultimately show ?thesis
by (metis has_bochner_integral_simple_bochner_integrable)
qed

"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 flip: ennreal_plus)
also have "… = ?g i"
finally show "?f i ≤ ?g i" .
qed
show "?g ⇢ 0"
using tendsto_add[OF f_sf g_sg] by simp
qed

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_onI 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: simple_bochner_integral_linear T.linear_axioms)
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: 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: 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: 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: 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: 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: 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)"

lemma has_bochner_integral_sum:
"(⋀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

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

define m where "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 flip: ennreal_plus)
also have "… = (∫⇧+x. norm (f x - s i x) ∂M) + (∫⇧+x. norm (s i x) ∂M)"
also have "… < ∞"
using s_fin f_s_fin by auto
finally show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞" .
qed

proposition 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 flip: ennreal_plus)
also have "… = ?t n"
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]
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 flip: 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 "has_bochner_integral M f x" and "has_bochner_integral M g y"
and "AE x in M. f x = g x"
shows "x = y"
by (meson assms has_bochner_integral.simps has_bochner_integral_cong_AE has_bochner_integral_eq)

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)"
simple_function_restrict_space[OF Ω] emeasure_restrict_space[OF Ω] Collect_restrict
indicator_eq_0_iff conj_left_commute)

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]
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!: sum.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✐‹tag important› 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]

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"
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 integrable_cong_AE_imp:
"integrable M g ⟹ f ∈ borel_measurable M ⟹ (AE x in M. g x = f x) ⟹ integrable M f"
using integrable_cong_AE[of f M g] by (auto simp: eq_commute)

lemma integral_cong:
"M = N ⟹ (⋀x. x ∈ space N ⟹ f x = g x) ⟹ integral⇧L M f = integral⇧L N g"
by (simp cong: has_bochner_integral_cong cong del: if_weak_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_sum[simp, intro]: "(⋀i. i ∈ I ⟹ integrable M (f i)) ⟹ integrable M (λx. ∑i∈I. f i x)"
by (metis has_bochner_integral_sum 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"

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_sum: "(⋀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_sum has_bochner_integral_integrable)

lemma integral_sum'[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_sum)

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))"
by (metis (full_types) "*" "**" T' integrable_bounded_linear integrable_cong not)
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 flip: ennreal_plus)
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

proposition 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 flip: ennreal_0)
qed
qed (use bnd w_nonneg in auto)
then show ?thesis by simp
qed

proposition 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)"
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</```