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"
            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
      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"
      by (simp add: U'_def fun_eq_iff)
    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
        by (simp add: indicator_def[abs_def])
    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}"
    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"

  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 (simp add: sum.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!: 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

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: sum.distrib[symmetric] scaleR_add_right)
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"
  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_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"
   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_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
    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 flip: ennreal_plus)
      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_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)"
  unfolding diff_conv_add_uminus
  by (intro has_bochner_integral_add has_bochner_integral_minus)

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

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)
           (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 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)"
  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_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]
    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!: 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"
    (‹(‹indent=1 notation=‹binder integral››∫(2 _./ _)/ ∂_)› [60,61] 110)
syntax_consts
  "_lebesgue_integral" == lebesgue_integral
translations
  "∫ x. f ∂M" == "CONST lebesgue_integral M (λx. f)"

syntax
  "_ascii_lebesgue_integral" :: "pttrn ⇒ 'a measure ⇒ real ⇒ real"
    (‹(‹indent=3 notation=‹mixfix LINT››LINT (1_)/|(_)./ _)› [0,110,60] 60)
syntax_consts
  "_ascii_lebesgue_integral" == lebesgue_integral
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"
  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"
  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_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)"
        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 (in finite_measure) square_integrable_imp_integrable:
  fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, real_normed_div_algebra}"
  assumes [measurable]: "f ∈ borel_measurable M"
  assumes "integrable M (λx. f x ^ 2)"
  shows   "integrable M f"
proof -
  have less_top: "emeasure M (space M) < top"
    using finite_emeasure_space by (meson top.not_eq_extremum)
  have "nn_integral M (λx. norm (f x)) ^ 2 ≤
        nn_integral M (λx. norm (f x) ^ 2) * emeasure M (space M)"
    using Cauchy_Schwarz_nn_integral[of "λx. norm (f x)" M "λ_. 1"]
    by (simp add: ennreal_power)
  also have "… < ∞"
    using assms(2) less_top
    by (subst (asm) integrable_iff_bounded) (auto simp: norm_power ennreal_mult_less_top)
  finally have "nn_integral M (λx. norm (f x)) < ∞"
    by (simp add: power_less_top_ennreal)
  thus ?thesis
    by (simp add: integrable_iff_bounded)
qed

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
  by (smt (verit) AE_cong ennreal_le_iff nn_integral_mono_AE norm_ge_zero order_less_subst2 linorder_not_le order_less_le_trans)


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)

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 (metis (no_types, lifting) Int_iff indicator_simps integral_cong)
  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_aux:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  assumes f: "integrable M f" and 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 g"
  unfolding integrable_iff_bounded
proof
  have fmeas: "f ∈ borel_measurable M" "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞"
    using f integrable_iff_bounded by auto
  then show "g ∈ borel_measurable M"
    using measurable_discrete_difference[where X=X]
    by (smt (verit) UNIV_I X eq sets space_borel)
  have "AE x in M. x ∉ X"
    using AE_discrete_difference X null sets by blast
  with fmeas show "(∫⇧+ x. ennreal (norm (g x)) ∂M) < ∞"
    by (metis (mono_tags, lifting) AE_I2 AE_mp eq nn_integral_cong_AE)
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"
  by (metis X eq integrable_discrete_difference_aux null sets)

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 "countable X"
  assumes "⋀x. x ∈ X ⟹ emeasure M {x} = 0"
  assumes "⋀x. x ∈ X ⟹ {x} ∈ sets M"
  assumes "⋀x. x ∈ space M ⟹ x ∉ X ⟹ f x = g x"
  shows "has_bochner_integral M f x ⟷ has_bochner_integral M g x"
  by (metis assms has_bochner_integral_iff integrable_discrete_difference integral_discrete_difference)

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 (metis LIMSEQ_le_const2 ennreal_leI tendsto_norm)
    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 [simp]:
  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 integrable_mult_right_iff [simp]:
  fixes f :: "'a ⇒ real"
  shows "integrable M (λx. f x * c) ⟷ c = 0 ∨ integrable M f"
  using integrable_mult_left_iff [of M c f] by (simp add: mult.commute)

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)
          (simp_all, fastforce)
      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)
  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

proposition 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: 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 nn_integral_eq_integrable:
  assumes "f ∈ M →⇩M borel" "AE x in M. 0 ≤ f x" and "0 ≤ x"
  shows "(∫⇧+x. f x ∂M) = ennreal x ⟷ (integrable M f ∧ integral⇧L M f = x)"
  by (metis assms ennreal_inj integrableI_nn_integral_finite integral_nonneg_AE nn_integral_eq_integral)

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. summable (λi. norm (f i x)) ⟹
         ennreal (norm (∑i. norm (f i x))) = (∑i. ennreal (norm (f i x)))"
      by (simp add: suminf_nonneg ennreal_suminf_neq_top)
  then have "(∫⇧+ x. ennreal (norm (∑i. norm (f i x))) ∂M) = (∫⇧+ x. (∑i. ennreal (norm (f i x))) ∂M)"
      using local.summable by (intro nn_integral_cong_AE) auto
    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_sum)
    also have "… ≤ (∑i. norm (f i x))"
      using sum_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

proposition integral_norm_bound [simp]:
  fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
  shows "norm (integral⇧L M f) ≤ (∫x. norm (f x) ∂M)"
proof (cases "integrable M f")
  case True then show ?thesis
    using nn_integral_eq_integral[of M "λx. norm (f x)"] integral_norm_bound_ennreal[of M f]
    by (simp add: integral_nonneg_AE)
next
  case False
  then have "norm (integral⇧L M f) = 0" by (simp add: not_integrable_integral_eq)
  moreover have "(∫x. norm (f x) ∂M) ≥ 0" by auto
  ultimately show ?thesis by simp
qed

proposition integral_abs_bound [simp]:
  fixes f :: "'a ⇒ real" shows "abs (∫x. f x ∂M) ≤ (∫x. ¦f x¦ ∂M)"
using integral_norm_bound[of M f] by auto

lemma integral_eq_nn_integral:
  assumes "f ∈ borel_measurable M"
  assumes "AE x in M. 0 ≤ f x"
  shows "integral⇧L M f = enn2real (∫⇧+ x. ennreal (f x) ∂M)"
  by (metis assms enn2real_ennreal enn2real_top infinity_ennreal_def integrableI_nonneg integral_nonneg_AE
      less_top nn_integral_eq_integral not_integrable_integral_eq)

lemma enn2real_nn_integral_eq_integral:
  assumes "AE x in M. f x = ennreal (g x)" and nn: "AE x in M. 0 ≤ g x"
    and "g ∈ M →⇩M borel"
  shows "enn2real (∫⇧+x. f x ∂M) = (∫x. g x ∂M)"
  by (metis assms integral_eq_nn_integral nn nn_integral_cong_AE)

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"
  by (metis assms has_bochner_integral_iff nn_integral_eq_integrable)

lemma integrableI_simple_bochner_integrable:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  shows "simple_bochner_integrable M f ⟹ integrable M f"
  using has_bochner_integral_simple_bochner_integrable integrable.intros by blast

proposition 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 sum = this

  define s' where [abs_def]: "s' i z = indicator (space M) z *⇩R s i z" for 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="(*⇩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: 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!: sum 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: 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 integral_norm_bound_integral:
  fixes f :: "'a::euclidean_space ⇒ 'b::{banach,second_countable_topology}"
  assumes "integrable M f" "integrable M g" "⋀x. x ∈ space M ⟹ norm(f x) ≤ g x"
  shows "norm (∫x. f x ∂M) ≤ (∫x. g x ∂M)"
  by (smt (verit, best) assms integrable_norm integral_mono integral_norm_bound)

lemma integral_abs_bound_integral:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes "integrable M f" "integrable M g" "⋀x. x ∈ space M ⟹ ¦f x¦ ≤ g x"
  shows "¦∫x. f x ∂M¦ ≤ (∫x. g x ∂M)"
  by (metis integral_norm_bound_integral assms real_norm_def)

text ‹The next two statements are useful to bound Lebesgue integrals, as they avoid one
integrability assumption. The price to pay is that the upper function has to be nonnegative,
but this is often true and easy to check in computations.›

lemma integral_mono_AE':
  fixes f::"_ ⇒ real"
  assumes "integrable M f" "AE x in M. g x ≤ f x" "AE x in M. 0 ≤ f x"
  shows "(∫x. g x ∂M) ≤ (∫x. f x ∂M)"
  by (metis assms integral_mono_AE integral_nonneg_AE not_integrable_integral_eq)

lemma integral_mono':
  fixes f::"_ ⇒ real"
  assumes "integrable M f" "⋀x. x ∈ space M ⟹ g x ≤ f x" "⋀x. x ∈ space M ⟹ 0 ≤ f x"
  shows "(∫x. g x ∂M) ≤ (∫x. f x ∂M)"
by (rule integral_mono_AE', insert assms, 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 nn_integral_nonneg_infinite:
  fixes f::"'a ⇒ real"
  assumes "f ∈ borel_measurable M" "¬ integrable M f" "AE x in M. f x ≥ 0"
  shows "(∫⇧+x. f x ∂M) = ∞"
  using assms integrableI_nonneg less_top by auto

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

lemma integrable_MIN:
  fixes f:: "_ ⇒ _ ⇒ real"
  shows "⟦ finite I;  I ≠ {}; ⋀i. i ∈ I ⟹ integrable M (f i) ⟧
   ⟹ integrable M (λx. MIN i∈I. f i x)"
  by (induct rule: finite_ne_induct) simp+

lemma integrable_MAX:
  fixes f:: "_ ⇒ _ ⇒ real"
  shows "⟦ finite I;  I ≠ {};  ⋀i. i ∈ I ⟹ integrable M (f i) ⟧
  ⟹ integrable M (λx. MAX i∈I. f i x)"
  by (induct rule: finite_ne_induct) simp+

theorem integral_Markov_inequality:
  assumes [measurable]: "integrable M u" and "AE x in M. 0 ≤ u x" "0 < (c::real)"
  shows "(emeasure M) {x∈space M. u x ≥ c} ≤ (1/c) * (∫x. u x ∂M)"
proof -
  have "(∫⇧+ x. ennreal(u x) * indicator (space M) x ∂M) ≤ (∫⇧+ x. u x ∂M)"
    by (rule nn_integral_mono_AE, auto simp: ‹c>0› less_eq_real_def)
  also have "… = (∫x. u x ∂M)"
    by (rule nn_integral_eq_integral, auto simp: assms)
  finally have *: "(∫⇧+ x. ennreal(u x) * indicator (space M) x ∂M) ≤ (∫x. u x ∂M)"
    by simp

  have "{x ∈ space M. u x ≥ c} = {x ∈ space M. ennreal(1/c) * u x ≥ 1} ∩ (space M)"
    using ‹c>0› by (auto simp: ennreal_mult'[symmetric])
  then have "emeasure M {x ∈ space M. u x ≥ c} = emeasure M ({x ∈ space M. ennreal(1/c) * u x ≥ 1})"
    by simp
  also have "… ≤ ennreal(1/c) * (∫⇧+ x. ennreal(u x) * indicator (space M) x ∂M)"
    by (rule nn_integral_Markov_inequality) (auto simp: assms)
  also have "… ≤ ennreal(1/c) * (∫x. u x ∂M)"
    by (rule mult_left_mono) (use * ‹c > 0› in auto)
  finally show ?thesis
    using ‹0<c› by (simp add: ennreal_mult'[symmetric])
qed

theorem integral_Markov_inequality_measure:
  assumes [measurable]: "integrable M u" and "A ∈ sets M" and "AE x in M. 0 ≤ u x" "0 < (c::real)"
  shows "measure M {x∈space M. u x ≥ c} ≤ (∫x. u x ∂M) / c"
proof -
  have le: "emeasure M {x∈space M. u x ≥ c} ≤ ennreal ((1/c) * (∫x. u x ∂M))"
    by (rule integral_Markov_inequality) (use assms in auto)
  also have "… < top"
    by auto
  finally have "ennreal (measure M {x∈space M. u x ≥ c}) = emeasure M {x∈space M. u x ≥ c}"
    by (intro emeasure_eq_ennreal_measure [symmetric]) auto
  also note le
  finally show ?thesis
    by (simp add: assms divide_nonneg_pos integral_nonneg_AE)
qed

theorem%important (in finite_measure) second_moment_method:
  assumes [measurable]: "f ∈ M →⇩M borel"
  assumes "integrable M (λx. f x ^ 2)"
  defines "μ ≡ lebesgue_integral M f"
  assumes "a > 0"
  shows "measure M {x∈space M. ¦f x¦ ≥ a} ≤ lebesgue_integral M (λx. f x ^ 2) / a⇧2"
proof -
  have integrable: "integrable M f"
    using assms by (blast dest: square_integrable_imp_integrable)
  have "{x∈space M. ¦f x¦ ≥ a} = {x∈space M. f x ^ 2 ≥ a⇧2}"
    using ‹a > 0› by (simp flip: abs_le_square_iff)
  hence "measure M {x∈space M. ¦f x¦ ≥ a} = measure M {x∈space M. f x ^ 2 ≥ a⇧2}"
    by simp
  also have "… ≤ lebesgue_integral M (λx. f x ^ 2) / a⇧2"
    using assms by (intro integral_Markov_inequality_measure) auto
  finally show ?thesis .
qed

lemma integral_ineq_eq_0_then_AE:
  fixes f::"_ ⇒ real"
  assumes "AE x in M. f x ≤ g x" "integrable M f" "integrable M g"
          "(∫x. f x ∂M) = (∫x. g x ∂M)"
  shows "AE x in M. f x = g x"
proof -
  define h where "h = (λx. g x - f x)"
  have "AE x in M. h x = 0"
    apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
    unfolding h_def using assms by auto
  then show ?thesis unfolding h_def by auto
qed

lemma not_AE_zero_int_E:
  fixes f::"'a ⇒ real"
  assumes "AE x in M. f x ≥ 0" "(∫x. f x ∂M) > 0"
      and [measurable]: "f ∈ borel_measurable M"
  shows "∃A e. A ∈ sets M ∧ e>0 ∧ emeasure M A > 0 ∧ (∀x ∈ A. f x ≥ e)"
proof (rule not_AE_zero_E, auto simp: assms)
  assume *: "AE x in M. f x = 0"
  have "(∫x. f x ∂M) = (∫x. 0 ∂M)" 
    by (rule integral_cong_AE, auto simp: *)
  then have "(∫x. f x ∂M) = 0" by simp
  then show False using assms(2) by simp
qed

proposition tendsto_L1_int:
  fixes u :: "_ ⇒ _ ⇒ 'b::{banach, second_countable_topology}"
  assumes [measurable]: "⋀n. integrable M (u n)" "integrable M f"
          and "((λn. (∫⇧+x. norm(u n x - f x) ∂M)) ⤏ 0) F"
  shows "((λn. (∫x. u n x ∂M)) ⤏ (∫x. f x ∂M)) F"
proof -
  have "((λn. norm((∫x. u n x ∂M) - (∫x. f x ∂M))) ⤏ (0::ennreal)) F"
  proof (rule tendsto_sandwich[of "λ_. 0", where ?h = "λn. (∫⇧+x. norm(u n x - f x) ∂M)"], auto simp: assms)
    {
      fix n
      have "(∫x. u n x ∂M) - (∫x. f x ∂M) = (∫x. u n x - f x ∂M)"
        by (simp add: assms)
      then have "norm((∫x. u n x ∂M) - (∫x. f x ∂M)) = norm (∫x. u n x - f x ∂M)"
        by auto
      also have "… ≤ (∫x. norm(u n x - f x) ∂M)"
        by (rule integral_norm_bound)
      finally have "ennreal(norm((∫x. u n x ∂M) - (∫x. f x ∂M))) ≤ (∫x. norm(u n x - f x) ∂M)"
        by simp
      also have "… = (∫⇧+x. norm(u n x - f x) ∂M)"
        by (simp add: assms nn_integral_eq_integral)
      finally have "norm((∫x. u n x ∂M) - (∫x. f x ∂M)) ≤ (∫⇧+x. norm(u n x - f x) ∂M)" 
        by simp
    }
    then show "eventually (λn. norm((∫x. u n x ∂M) - (∫x. f x ∂M)) ≤ (∫⇧+x. norm(u n x - f x) ∂M)) F"
      by auto
  qed
  then have "((λn. norm((∫x. u n x ∂M) - (∫x. f x ∂M))) ⤏ 0) F"
    by (simp flip: ennreal_0)
  then have "((λn. ((∫x. u n x ∂M) - (∫x. f x ∂M))) ⤏ 0) F" 
    using tendsto_norm_zero_iff by blast
  then show ?thesis 
    using Lim_null by auto
qed

text ‹The next lemma asserts that, if a sequence of functions converges in ‹L⇧1›, then
it admits a subsequence that converges almost everywhere.›

proposition tendsto_L1_AE_subseq:
  fixes u :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
  assumes [measurable]: "⋀n. integrable M (u n)"
      and "(λn. (∫x. norm(u n x) ∂M)) ⇢ 0"
  shows "∃r::nat⇒nat. strict_mono r ∧ (AE x in M. (λn. u (r n) x) ⇢ 0)"
proof -
  {
    fix k
    have "eventually (λn. (∫x. norm(u n x) ∂M) < (1/2)^k) sequentially"
      using order_tendstoD(2)[OF assms(2)] by auto
    with eventually_elim2[OF eventually_gt_at_top[of k] this]
    have "∃n>k. (∫x. norm(u n x) ∂M) < (1/2)^k"
      by (metis eventually_False_sequentially)
  }
  then have "∃r. ∀n. True ∧ (r (Suc n) > r n ∧ (∫x. norm(u (r (Suc n)) x) ∂M) < (1/2)^(r n))"
    by (intro dependent_nat_choice, auto)
  then obtain r0 where r0: "strict_mono r0" "⋀n. (∫x. norm(u (r0 (Suc n)) x) ∂M) < (1/2)^(r0 n)"
    by (auto simp: strict_mono_Suc_iff)
  define r where "r = (λn. r0(n+1))"
  have "strict_mono r" unfolding r_def using r0(1) by (simp add: strict_mono_Suc_iff)
  have I: "(∫⇧+x. norm(u (r n) x) ∂M) < ennreal((1/2)^n)" for n
  proof -
    have "r0 n ≥ n" using ‹strict_mono r0› by (simp add: seq_suble)
    have "(1/2::real)^(r0 n) ≤ (1/2)^n" by (rule power_decreasing[OF ‹r0 n ≥ n›], auto)
    then have "(∫x. norm(u (r0 (Suc n)) x) ∂M) < (1/2)^n" 
      using r0(2) less_le_trans by blast
    then have "(∫x. norm(u (r n) x) ∂M) < (1/2)^n" 
      unfolding r_def by auto
    moreover have "(∫⇧+x. norm(u (r n) x) ∂M) = (∫x. norm(u (r n) x) ∂M)"
      by (rule nn_integral_eq_integral, auto simp: integrable_norm[OF assms(1)[of "r n"]])
    ultimately show ?thesis by (auto intro: ennreal_lessI)
  qed

  have "AE x in M. limsup (λn. ennreal (norm(u (r n) x))) ≤ 0"
  proof (rule AE_upper_bound_inf_ennreal)
    fix e::real assume "e > 0"
    define A where "A = (λn. {x ∈ space M. norm(u (r n) x) ≥ e})"
    have A_meas [measurable]: "⋀n. A n ∈ sets M" unfolding A_def by auto
    have A_bound: "emeasure M (A n) < (1/e) * ennreal((1/2)^n)" for n
    proof -
      have *: "indicator (A n) x ≤ (1/e) * ennreal(norm(u (r n) x))" for x
        using ‹0 < e› by (cases "x ∈ A n") (auto simp: A_def ennreal_mult[symmetric])
      have "emeasure M (A n) = (∫⇧+x. indicator (A n) x ∂M)" by auto
      also have "… ≤ (∫⇧+x. (1/e) * ennreal(norm(u (r n) x)) ∂M)"
        by (meson "*" nn_integral_mono)
      also have "… = (1/e) * (∫⇧+x. norm(u (r n) x) ∂M)"
        using ‹e > 0› by (force simp add: intro: nn_integral_cmult)
      also have "… < (1/e) * ennreal((1/2)^n)"
        using I[of n] ‹e > 0› by (intro ennreal_mult_strict_left_mono) auto
      finally show ?thesis by simp
    qed
    have A_fin: "emeasure M (A n) < ∞" for n
      using ‹e > 0› A_bound[of n]
      by (auto simp: ennreal_mult less_top[symmetric])

    have A_sum: "summable (λn. measure M (A n))"
    proof (rule summable_comparison_test')
      have "summable (λn. (1/(2::real))^n)" 
        by (simp add: summable_geometric)
      then show "summable (λn. (1/e) * (1/2)^n)" using summable_mult by blast
      fix n::nat assume "n ≥ 0"
      have "norm(measure M (A n)) = measure M (A n)" by simp
      also have "… = enn2real(emeasure M (A n))" unfolding measure_def by simp
      also have "… < enn2real((1/e) * (1/2)^n)"
        using A_bound[of n] ‹emeasure M (A n) < ∞› ‹0 < e›
        by (auto simp: emeasure_eq_ennreal_measure ennreal_mult[symmetric] ennreal_less_iff)
      also have "… = (1/e) * (1/2)^n"
        using ‹0<e› by auto
      finally show "norm(measure M (A n)) ≤ (1/e) * (1/2)^n" by simp
    qed

    have "AE x in M. eventually (λn. x ∈ space M - A n) sequentially"
      by (rule borel_cantelli_AE1[OF A_meas A_fin A_sum])
    moreover
    {
      fix x assume "eventually (λn. x ∈ space M - A n) sequentially"
      moreover have "norm(u (r n) x) ≤ ennreal e" if "x ∈ space M - A n" for n
        using that unfolding A_def by (auto intro: ennreal_leI)
      ultimately have "eventually (λn. norm(u (r n) x) ≤ ennreal e) sequentially"
        by (simp add: eventually_mono)
      then have "limsup (λn. ennreal (norm(u (r n) x))) ≤ e"
        by (simp add: Limsup_bounded)
    }
    ultimately show "AE x in M. limsup (λn. ennreal (norm(u (r n) x))) ≤ 0 + ennreal e" 
      by auto
  qed
  moreover
  {
    fix x assume x: "limsup (λn. ennreal (norm(u (r n) x))) ≤ 0"
    moreover have "liminf (λn. ennreal (norm(u (r n) x))) ≤ 0"
      by (metis x Liminf_le_Limsup le_zero_eq sequentially_bot)
    ultimately have "(λn. ennreal (norm(u (r n) x))) ⇢ 0"
      using tendsto_Limsup[of sequentially "λn. ennreal (norm(u (r n) x))"] by auto
    then have "(λn. norm(u (r n) x)) ⇢ 0"
      by (simp flip: ennreal_0)
    then have "(λn. u (r n) x) ⇢ 0"
      by (simp add: tendsto_norm_zero_iff)
  }
  ultimately have "AE x in M. (λn. u (r n) x) ⇢ 0" by auto
  then show ?thesis using ‹strict_mono r› by auto
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: 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"
  by (metis AE_I2 assms empty_iff integral_eq_zero_AE)

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="(=)"] 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)"])
           (use lim in 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 (metis integrable_distr_eq integrable_iff_bounded measurable_distr_eq1)

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)"])
           (use lim in 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 sum.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_sum) (auto intro!: sum.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!: sum.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: 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 sums_unique by auto

lemma integrable_bij_count_space:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  assumes g: "bij_betw g A B"
  shows "integrable (count_space A) (λx. f (g x)) ⟷ integrable (count_space B) f"
  unfolding integrable_iff_bounded by (subst nn_integral_bij_count_space[OF g]) auto

lemma integral_bij_count_space:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  assumes g: "bij_betw g A B"
  shows "integral⇧L (count_space A) (λx. f (g x)) = integral⇧L (count_space B) f"
  using g[THEN bij_betw_imp_funcset] distr_bij_count_space [OF g]
  by (metis borel_measurable_count_space integral_distr measurable_count_space_eq1 space_count_space)

lemma has_bochner_integral_count_space_nat:
  fixes f :: "nat ⇒ _::{banach,second_countable_topology}"
  shows "has_bochner_integral (count_space UNIV) f x ⟹ f sums x"
  unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat)

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)

proposition integrable_point_measure_finite:
  fixes g :: "'a ⇒ 'b::{banach, second_countable_topology}" and f :: "'a ⇒ real"
  assumes "finite A"
  shows "integrable (point_measure A f) g"
proof -
  have "integrable (density (count_space A) (λx. ennreal (max 0 (f x)))) g"
    using assms
    by (simp add: integrable_count_space integrable_density )
  then show ?thesis
    by (smt (verit) AE_I2 borel_measurable_count_space density_cong ennreal_neg point_measure_def)
qed

lemma integral_uniform_count_measure:
  assumes "finite A" 
  shows "integral⇧L (uniform_count_measure A) f = sum f A / (card A)"
proof -
  have "integral⇧L (uniform_count_measure A) f = (∑x∈A. f x / card A)" 
    using assms by (simp add: uniform_count_measure_def lebesgue_integral_point_measure_finite)
  with assms show ?thesis
    by (simp add: sum_divide_distrib nn_integral_count_space_finite)
qed

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: 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: integrable.simps)

lemma integral_null_measure[simp]: "integral⇧L (null_measure M) f = 0"
  using integral_norm_bound_ennreal not_integrable_integral_eq by fastforce

subsection ‹Legacy lemmas for the real-valued Lebesgue integral›

theorem 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

theorem 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 "0 ≤ r" "0 ≤ q"
    "(∫⇧+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"
    proof (rule nn_integral_cong_AE)
      show "AE x in M. ennreal (u x) = (SUP i. ennreal (f i x))"
        using lim mono nn u_nn
        by eventually_elim (simp add: LIMSEQ_unique[OF _ LIMSEQ_SUP] incseq_def)
    qed
  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: 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: 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"
  using integrable_bound[OF integrable_const[of B], of f]
  by (smt (verit, ccfv_SIG) eventually_elim2 real_norm_def)

lemma (in finite_measure) integral_bounded_eq_bound_then_AE:
  assumes "AE x in M. f x ≤ (c::real)"
    "integrable M f" "(∫x. f x ∂M) = c * measure M (space M)"
  shows "AE x in M. f x = c"
  using assms  by (intro integral_ineq_eq_0_then_AE) auto

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_sum) (auto)
  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)
  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

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 tendsto_eventually) (auto simp: frequently_def split: split_indicator)
    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 (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

proposition (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]
  obtain s where s: "⋀i. simple_function (N ⨂⇩M M) (s i)"
    and "∀x∈space (N ⨂⇩M M). (λi. s i x) ⇢ (case x of (x, y) ⇒ f x y)"
    and "∀i. ∀x∈space (N ⨂⇩M M). dist (s i x) 0 ≤ 2 * dist (case x of (x, xa) ⇒ f x xa) 0"
    by auto
  then have *:
    "⋀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

  define f' where [abs_def]: "f' i x =
    (if integrable M (f x) then simple_bochner_integral M (λy. s i (x, y)) else 0)" for i x

  { 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[THEN simple_functionD(1)]
      unfolding simple_bochner_integral_def
      by (intro sum.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 * by auto
        show "⋀i. AE xa in M. norm (s i (x, xa)) ≤ 2 * norm (f x xa)"
          using x * 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 * by (intro nn_integral_mono) auto
          also have "(∫⇧+ y. 2 * norm (f x y) ∂M) < ∞"
            using int_2f unfolding integrable_iff_bounded by simp
          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))"
  by (smt (verit) assms distr_pair_swap integrable_cong integrable_distr measurable_pair_swap' prod.case_distrib split_cong)

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"
  by (smt (verit) distr_pair_swap f integral_cong integral_distr measurable_pair_swap' prod.case_distrib split_cong)

theorem (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

proposition (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 "AE x in M1. LINT y|M2. f (x, y) + g (x, y) =
                (LINT y|M2. f (x, y)) + (LINT y|M2. g (x, y))"
    using AE_integrable_fst'[OF add(1)] AE_integrable_fst'[OF add(3)]
    by eventually_elim simp
  then have "(∫ x. ∫ y. f (x, y) + g (x, y) ∂M2 ∂M1) =
    (∫ x. (∫ y. f (x, y) ∂M2) + (∫ y. g (x, y) ∂M2) ∂M1)"
    by (intro integral_cong_AE) auto
  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

proposition (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"
  by (metis (no_types) distr_singleton insert_iff integral_distr measurable_component_singleton)

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)
  have "LINT x|(Pi⇩M I M ⨂⇩M Pi⇩M J M). f (merge I J x) =
        LINT x|Pi⇩M I M. LINT y|Pi⇩M J M. f (merge I J (x, y))"
    by (simp add: P.integral_fst'[symmetric, OF f_int])
  then show ?thesis
    apply (subst distr_merge[symmetric, OF IJ fin])
    by (simp add: integral_distr[OF measurable_merge f_borel])
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_prod:
  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: prod_norm prod_ennreal)
  also have "… = (∏i∈I. ∫⇧+ x. ennreal (norm (f i x)) ∂M i)"
    using assms by (intro product_nn_integral_prod) auto
  also have "… < ∞"
    using integrable by (simp add: less_top[symmetric] ennreal_prod_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_prod:
  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_prod 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!: prod.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 by auto
      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 by auto
    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