(*  Title:      HOL/Probability/Lebesgue_Integration.thy

    Author:     Johannes Hölzl, TU München

    Author:     Armin Heller, TU München

*)

header {*Lebesgue Integration*}

theory Lebesgue_Integration

  imports Measure_Space Borel_Space

begin

lemma indicator_less_ereal[simp]:

  "indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"

  by (simp add: indicator_def not_le)

section "Simple function"

text {*

Our simple functions are not restricted to positive real numbers. Instead

they are just functions with a finite range and are measurable when singleton

sets are measurable.

*}

definition "simple_function M g \<longleftrightarrow>

    finite (g ` space M) \<and>

    (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"

lemma simple_functionD:

  assumes "simple_function M g"

  shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M"

proof -

  show "finite (g ` space M)"

    using assms unfolding simple_function_def by auto

  have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto

  also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto

  finally show "g -` X \<inter> space M \<in> sets M" using assms

    by (auto simp del: UN_simps simp: simple_function_def)

qed

lemma measurable_simple_function[measurable_dest]:

  "simple_function M f \<Longrightarrow> f \<in> measurable M (count_space UNIV)"

  unfolding simple_function_def measurable_def

proof safe

  fix A assume "finite (f ` space M)" "\<forall>x\<in>f ` space M. f -` {x} \<inter> space M \<in> sets M"

  then have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) \<in> sets M"

    by (intro sets.finite_UN) auto

  also have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) = f -` A \<inter> space M"

    by (auto split: split_if_asm)

  finally show "f -` A \<inter> space M \<in> sets M" .

qed simp

lemma borel_measurable_simple_function:

  "simple_function M f \<Longrightarrow> f \<in> borel_measurable M"

  by (auto dest!: measurable_simple_function simp: measurable_def)

lemma simple_function_measurable2[intro]:

  assumes "simple_function M f" "simple_function M g"

  shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"

proof -

  have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"

    by auto

  then show ?thesis using assms[THEN simple_functionD(2)] by auto

qed

lemma simple_function_indicator_representation:

  fixes f ::"'a \<Rightarrow> ereal"

  assumes f: "simple_function M f" and x: "x \<in> space M"

  shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"

  (is "?l = ?r")

proof -

  have "?r = (\<Sum>y \<in> f ` space M.

    (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"

    by (auto intro!: setsum_cong2)

  also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"

    using assms by (auto dest: simple_functionD simp: setsum_delta)

  also have "... = f x" using x by (auto simp: indicator_def)

  finally show ?thesis by auto

qed

lemma simple_function_notspace:

  "simple_function M (\<lambda>x. h x * indicator (- space M) x::ereal)" (is "simple_function M ?h")

proof -

  have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto

  hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)

  have "?h -` {0} \<inter> space M = space M" by auto

  thus ?thesis unfolding simple_function_def by auto

qed

lemma simple_function_cong:

  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"

  shows "simple_function M f \<longleftrightarrow> simple_function M g"

proof -

  have "f ` space M = g ` space M"

    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"

    using assms by (auto intro!: image_eqI)

  thus ?thesis unfolding simple_function_def using assms by simp

qed

lemma simple_function_cong_algebra:

  assumes "sets N = sets M" "space N = space M"

  shows "simple_function M f \<longleftrightarrow> simple_function N f"

  unfolding simple_function_def assms ..

lemma simple_function_borel_measurable:

  fixes f :: "'a \<Rightarrow> 'x::{t2_space}"

  assumes "f \<in> borel_measurable M" and "finite (f ` space M)"

  shows "simple_function M f"

  using assms unfolding simple_function_def

  by (auto intro: borel_measurable_vimage)

lemma simple_function_eq_measurable:

  fixes f :: "'a \<Rightarrow> ereal"

  shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> measurable M (count_space UNIV)"

  using simple_function_borel_measurable[of f] measurable_simple_function[of M f]

  by (fastforce simp: simple_function_def)

lemma simple_function_const[intro, simp]:

  "simple_function M (\<lambda>x. c)"

  by (auto intro: finite_subset simp: simple_function_def)

lemma simple_function_compose[intro, simp]:

  assumes "simple_function M f"

  shows "simple_function M (g \<circ> f)"

  unfolding simple_function_def

proof safe

  show "finite ((g \<circ> f) ` space M)"

    using assms unfolding simple_function_def by (auto simp: image_comp [symmetric])

next

  fix x assume "x \<in> space M"

  let ?G = "g -` {g (f x)} \<inter> (f`space M)"

  have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M =

    (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto

  show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"

    using assms unfolding simple_function_def *

    by (rule_tac sets.finite_UN) auto

qed

lemma simple_function_indicator[intro, simp]:

  assumes "A \<in> sets M"

  shows "simple_function M (indicator A)"

proof -

  have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")

    by (auto simp: indicator_def)

  hence "finite ?S" by (rule finite_subset) simp

  moreover have "- A \<inter> space M = space M - A" by auto

  ultimately show ?thesis unfolding simple_function_def

    using assms by (auto simp: indicator_def [abs_def])

qed

lemma simple_function_Pair[intro, simp]:

  assumes "simple_function M f"

  assumes "simple_function M g"

  shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p")

  unfolding simple_function_def

proof safe

  show "finite (?p ` space M)"

    using assms unfolding simple_function_def

    by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto

next

  fix x assume "x \<in> space M"

  have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M =

      (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"

    by auto

  with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M"

    using assms unfolding simple_function_def by auto

qed

lemma simple_function_compose1:

  assumes "simple_function M f"

  shows "simple_function M (\<lambda>x. g (f x))"

  using simple_function_compose[OF assms, of g]

  by (simp add: comp_def)

lemma simple_function_compose2:

  assumes "simple_function M f" and "simple_function M g"

  shows "simple_function M (\<lambda>x. h (f x) (g x))"

proof -

  have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"

    using assms by auto

  thus ?thesis by (simp_all add: comp_def)

qed

lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]

  and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]

  and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]

  and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]

  and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]

  and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]

  and simple_function_max[intro, simp] = simple_function_compose2[where h=max]

lemma simple_function_setsum[intro, simp]:

  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"

  shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)"

proof cases

  assume "finite P" from this assms show ?thesis by induct auto

qed auto

lemma simple_function_ereal[intro, simp]: 

  fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"

  shows "simple_function M (\<lambda>x. ereal (f x))"

  by (auto intro!: simple_function_compose1[OF sf])

lemma simple_function_real_of_nat[intro, simp]: 

  fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"

  shows "simple_function M (\<lambda>x. real (f x))"

  by (auto intro!: simple_function_compose1[OF sf])

lemma borel_measurable_implies_simple_function_sequence:

  fixes u :: "'a \<Rightarrow> ereal"

  assumes u: "u \<in> borel_measurable M"

  shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>

             (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"

proof -

  def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)"

  { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def

    proof (split split_if, intro conjI impI)

      assume "\<not> real j \<le> u x"

      then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"

         by (cases "u x") (auto intro!: natfloor_mono)

      moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"

        by (intro real_natfloor_le) auto

      ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"

        unfolding real_of_nat_le_iff by auto

    qed auto }

  note f_upper = this

  have real_f:

    "\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))"

    unfolding f_def by auto

  let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"

  show ?thesis

  proof (intro exI[of _ ?g] conjI allI ballI)

    fix i

    have "simple_function M (\<lambda>x. real (f x i))"

    proof (intro simple_function_borel_measurable)

      show "(\<lambda>x. real (f x i)) \<in> borel_measurable M"

        using u by (auto simp: real_f)

      have "(\<lambda>x. real (f x i))`space M \<subseteq> real`{..i*2^i}"

        using f_upper[of _ i] by auto

      then show "finite ((\<lambda>x. real (f x i))`space M)"

        by (rule finite_subset) auto

    qed

    then show "simple_function M (?g i)"

      by (auto intro: simple_function_ereal simple_function_div)

  next

    show "incseq ?g"

    proof (intro incseq_ereal incseq_SucI le_funI)

      fix x and i :: nat

      have "f x i * 2 \<le> f x (Suc i)" unfolding f_def

      proof ((split split_if)+, intro conjI impI)

        assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"

        then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)"

          by (cases "u x") (auto intro!: le_natfloor)

      next

        assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x"

        then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i"

          by (cases "u x") auto

      next

        assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"

        have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2"

          by simp

        also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"

        proof cases

          assume "0 \<le> u x" then show ?thesis

            by (intro le_mult_natfloor) 

        next

          assume "\<not> 0 \<le> u x" then show ?thesis

            by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)

        qed

        also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)"

          by (simp add: ac_simps)

        finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" .

      qed simp

      then show "?g i x \<le> ?g (Suc i) x"

        by (auto simp: field_simps)

    qed

  next

    fix x show "(SUP i. ?g i x) = max 0 (u x)"

    proof (rule SUP_eqI)

      fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def

        by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg

                                     mult_nonpos_nonneg)

    next

      fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"

      have "\<And>i. 0 \<le> ?g i x" by auto

      from order_trans[OF this *] have "0 \<le> y" by simp

      show "max 0 (u x) \<le> y"

      proof (cases y)

        case (real r)

        with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)

        from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)

        then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)

        then guess p .. note ux = this

        obtain m :: nat where m: "p < real m" using reals_Archimedean2 ..

        have "p \<le> r"

        proof (rule ccontr)

          assume "\<not> p \<le> r"

          with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"]

          obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)

          then have "r * 2^max N m < p * 2^max N m - 1" by simp

          moreover

          have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"

            using *[of "max N m"] m unfolding real_f using ux

            by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)

          then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"

            by (metis real_natfloor_gt_diff_one less_le_trans)

          ultimately show False by auto

        qed

        then show "max 0 (u x) \<le> y" using real ux by simp

      qed (insert `0 \<le> y`, auto)

    qed

  qed auto

qed

lemma borel_measurable_implies_simple_function_sequence':

  fixes u :: "'a \<Rightarrow> ereal"

  assumes u: "u \<in> borel_measurable M"

  obtains f where "\<And>i. simple_function M (f i)" "incseq f" "\<And>i. \<infinity> \<notin> range (f i)"

    "\<And>x. (SUP i. f i x) = max 0 (u x)" "\<And>i x. 0 \<le> f i x"

  using borel_measurable_implies_simple_function_sequence[OF u] by auto

lemma simple_function_induct[consumes 1, case_names cong set mult add, induct set: simple_function]:

  fixes u :: "'a \<Rightarrow> ereal"

  assumes u: "simple_function M u"

  assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"

  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"

  assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)"

  assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"

  shows "P u"

proof (rule cong)

  from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x"

  proof eventually_elim

    fix x assume x: "x \<in> space M"

    from simple_function_indicator_representation[OF u x]

    show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" ..

  qed

next

  from u have "finite (u ` space M)"

    unfolding simple_function_def by auto

  then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)"

  proof induct

    case empty show ?case

      using set[of "{}"] by (simp add: indicator_def[abs_def])

  qed (auto intro!: add mult set simple_functionD u)

next

  show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))"

    apply (subst simple_function_cong)

    apply (rule simple_function_indicator_representation[symmetric])

    apply (auto intro: u)

    done

qed fact

lemma simple_function_induct_nn[consumes 2, case_names cong set mult add]:

  fixes u :: "'a \<Rightarrow> ereal"

  assumes u: "simple_function M u" and nn: "\<And>x. 0 \<le> u x"

  assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"

  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"

  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"

  assumes add: "\<And>u v. simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> simple_function M v \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"

  shows "P u"

proof -

  show ?thesis

  proof (rule cong)

    fix x assume x: "x \<in> space M"

    from simple_function_indicator_representation[OF u x]

    show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" ..

  next

    show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))"

      apply (subst simple_function_cong)

      apply (rule simple_function_indicator_representation[symmetric])

      apply (auto intro: u)

      done

  next

    from u nn have "finite (u ` space M)" "\<And>x. x \<in> u ` space M \<Longrightarrow> 0 \<le> x"

      unfolding simple_function_def by auto

    then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)"

    proof induct

      case empty show ?case

        using set[of "{}"] by (simp add: indicator_def[abs_def])

    qed (auto intro!: add mult set simple_functionD u setsum_nonneg

       simple_function_setsum)

  qed fact

qed

lemma borel_measurable_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:

  fixes u :: "'a \<Rightarrow> ereal"

  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"

  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"

  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"

  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"

  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"

  assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow>  (\<And>i x. 0 \<le> U i x) \<Longrightarrow>  (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P (SUP i. U i)"

  shows "P u"

  using u

proof (induct rule: borel_measurable_implies_simple_function_sequence')

  fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and

    sup: "\<And>x. (SUP i. U i x) = max 0 (u x)" and nn: "\<And>i x. 0 \<le> U i x"

  have u_eq: "u = (SUP i. U i)"

    using nn u sup by (auto simp: max_def)

  from U have "\<And>i. U i \<in> borel_measurable M"

    by (simp add: borel_measurable_simple_function)

  show "P u"

    unfolding u_eq

  proof (rule seq)

    fix i show "P (U i)"

      using `simple_function M (U i)` nn

      by (induct rule: simple_function_induct_nn)

         (auto intro: set mult add cong dest!: borel_measurable_simple_function)

  qed fact+

qed

lemma simple_function_If_set:

  assumes sf: "simple_function M f" "simple_function M g" and A: "A \<inter> space M \<in> sets M"

  shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF")

proof -

  def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"

  show ?thesis unfolding simple_function_def

  proof safe

    have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto

    from finite_subset[OF this] assms

    show "finite (?IF ` space M)" unfolding simple_function_def by auto

  next

    fix x assume "x \<in> space M"

    then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A

      then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))

      else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"

      using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)

    have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"

      unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto

    show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto

  qed

qed

lemma simple_function_If:

  assumes sf: "simple_function M f" "simple_function M g" and P: "{x\<in>space M. P x} \<in> sets M"

  shows "simple_function M (\<lambda>x. if P x then f x else g x)"

proof -

  have "{x\<in>space M. P x} = {x. P x} \<inter> space M" by auto

  with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp

qed

lemma simple_function_subalgebra:

  assumes "simple_function N f"

  and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M"

  shows "simple_function M f"

  using assms unfolding simple_function_def by auto

lemma simple_function_comp:

  assumes T: "T \<in> measurable M M'"

    and f: "simple_function M' f"

  shows "simple_function M (\<lambda>x. f (T x))"

proof (intro simple_function_def[THEN iffD2] conjI ballI)

  have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"

    using T unfolding measurable_def by auto

  then show "finite ((\<lambda>x. f (T x)) ` space M)"

    using f unfolding simple_function_def by (auto intro: finite_subset)

  fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"

  then have "i \<in> f ` space M'"

    using T unfolding measurable_def by auto

  then have "f -` {i} \<inter> space M' \<in> sets M'"

    using f unfolding simple_function_def by auto

  then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"

    using T unfolding measurable_def by auto

  also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"

    using T unfolding measurable_def by auto

  finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .

qed

section "Simple integral"

definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>S") where

  "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"

syntax

  "_simple_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110)

translations

  "\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"

lemma simple_integral_cong:

  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"

  shows "integral\<^sup>S M f = integral\<^sup>S M g"

proof -

  have "f ` space M = g ` space M"

    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"

    using assms by (auto intro!: image_eqI)

  thus ?thesis unfolding simple_integral_def by simp

qed

lemma simple_integral_const[simp]:

  "(\<integral>\<^sup>Sx. c \<partial>M) = c * (emeasure M) (space M)"

proof (cases "space M = {}")

  case True thus ?thesis unfolding simple_integral_def by simp

next

  case False hence "(\<lambda>x. c) ` space M = {c}" by auto

  thus ?thesis unfolding simple_integral_def by simp

qed

lemma simple_function_partition:

  assumes f: "simple_function M f" and g: "simple_function M g"

  assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y"

  assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)"

  shows "integral\<^sup>S M f = (\<Sum>y\<in>g ` space M. v y * emeasure M {x\<in>space M. g x = y})"

    (is "_ = ?r")

proof -

  from f g have [simp]: "finite (f`space M)" "finite (g`space M)"

    by (auto simp: simple_function_def)

  from f g have [measurable]: "f \<in> measurable M (count_space UNIV)" "g \<in> measurable M (count_space UNIV)"

    by (auto intro: measurable_simple_function)

  { fix y assume "y \<in> space M"

    then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}"

      by (auto cong: sub simp: v[symmetric]) }

  note eq = this

  have "integral\<^sup>S M f =

    (\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M. 

      if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))"

    unfolding simple_integral_def

  proof (safe intro!: setsum_cong ereal_left_mult_cong)

    fix y assume y: "y \<in> space M" "f y \<noteq> 0"

    have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 

        {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"

      by auto

    have eq:"(\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i}) =

        f -` {f y} \<inter> space M"

      by (auto simp: eq_commute cong: sub rev_conj_cong)

    have "finite (g`space M)" by simp

    then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"

      by (rule rev_finite_subset) auto

    then show "emeasure M (f -` {f y} \<inter> space M) =

      (\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then emeasure M {x \<in> space M. g x = z} else 0)"

      apply (simp add: setsum_cases)

      apply (subst setsum_emeasure)

      apply (auto simp: disjoint_family_on_def eq)

      done

  qed

  also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 

      if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))"

    by (auto intro!: setsum_cong simp: setsum_ereal_right_distrib emeasure_nonneg)

  also have "\<dots> = ?r"

    by (subst setsum_commute)

       (auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq)

  finally show "integral\<^sup>S M f = ?r" .

qed

lemma simple_integral_add[simp]:

  assumes f: "simple_function M f" and "\<And>x. 0 \<le> f x" and g: "simple_function M g" and "\<And>x. 0 \<le> g x"

  shows "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = integral\<^sup>S M f + integral\<^sup>S M g"

proof -

  have "(\<integral>\<^sup>Sx. f x + g x \<partial>M) =

    (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. (fst y + snd y) * emeasure M {x\<in>space M. (f x, g x) = y})"

    by (intro simple_function_partition) (auto intro: f g)

  also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) +

    (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y})"

    using assms(2,4) by (auto intro!: setsum_cong ereal_left_distrib simp: setsum_addf[symmetric])

  also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. f x \<partial>M)"

    by (intro simple_function_partition[symmetric]) (auto intro: f g)

  also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. g x \<partial>M)"

    by (intro simple_function_partition[symmetric]) (auto intro: f g)

  finally show ?thesis .

qed

lemma simple_integral_setsum[simp]:

  assumes "\<And>i x. i \<in> P \<Longrightarrow> 0 \<le> f i x"

  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"

  shows "(\<integral>\<^sup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>S M (f i))"

proof cases

  assume "finite P"

  from this assms show ?thesis

    by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg)

qed auto

lemma simple_integral_mult[simp]:

  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x"

  shows "(\<integral>\<^sup>Sx. c * f x \<partial>M) = c * integral\<^sup>S M f"

proof -

  have "(\<integral>\<^sup>Sx. c * f x \<partial>M) = (\<Sum>y\<in>f ` space M. (c * y) * emeasure M {x\<in>space M. f x = y})"

    using f by (intro simple_function_partition) auto

  also have "\<dots> = c * integral\<^sup>S M f"

    using f unfolding simple_integral_def

    by (subst setsum_ereal_right_distrib) (auto simp: emeasure_nonneg mult_assoc Int_def conj_commute)

  finally show ?thesis .

qed

lemma simple_integral_mono_AE:

  assumes f[measurable]: "simple_function M f" and g[measurable]: "simple_function M g"

  and mono: "AE x in M. f x \<le> g x"

  shows "integral\<^sup>S M f \<le> integral\<^sup>S M g"

proof -

  let ?\<mu> = "\<lambda>P. emeasure M {x\<in>space M. P x}"

  have "integral\<^sup>S M f = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * ?\<mu> (\<lambda>x. (f x, g x) = y))"

    using f g by (intro simple_function_partition) auto

  also have "\<dots> \<le> (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * ?\<mu> (\<lambda>x. (f x, g x) = y))"

  proof (clarsimp intro!: setsum_mono)

    fix x assume "x \<in> space M"

    let ?M = "?\<mu> (\<lambda>y. f y = f x \<and> g y = g x)"

    show "f x * ?M \<le> g x * ?M"

    proof cases

      assume "?M \<noteq> 0"

      then have "0 < ?M"

        by (simp add: less_le emeasure_nonneg)

      also have "\<dots> \<le> ?\<mu> (\<lambda>y. f x \<le> g x)"

        using mono by (intro emeasure_mono_AE) auto

      finally have "\<not> \<not> f x \<le> g x"

        by (intro notI) auto

      then show ?thesis

        by (intro ereal_mult_right_mono) auto

    qed simp

  qed

  also have "\<dots> = integral\<^sup>S M g"

    using f g by (intro simple_function_partition[symmetric]) auto

  finally show ?thesis .

qed

lemma simple_integral_mono:

  assumes "simple_function M f" and "simple_function M g"

  and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"

  shows "integral\<^sup>S M f \<le> integral\<^sup>S M g"

  using assms by (intro simple_integral_mono_AE) auto

lemma simple_integral_cong_AE:

  assumes "simple_function M f" and "simple_function M g"

  and "AE x in M. f x = g x"

  shows "integral\<^sup>S M f = integral\<^sup>S M g"

  using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE)

lemma simple_integral_cong':

  assumes sf: "simple_function M f" "simple_function M g"

  and mea: "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0"

  shows "integral\<^sup>S M f = integral\<^sup>S M g"

proof (intro simple_integral_cong_AE sf AE_I)

  show "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" by fact

  show "{x \<in> space M. f x \<noteq> g x} \<in> sets M"

    using sf[THEN borel_measurable_simple_function] by auto

qed simp

lemma simple_integral_indicator:

  assumes A: "A \<in> sets M"

  assumes f: "simple_function M f"

  shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =

    (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))"

proof -

  have eq: "(\<lambda>x. (f x, indicator A x)) ` space M \<inter> {x. snd x = 1} = (\<lambda>x. (f x, 1::ereal))`A"

    using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: split_if_asm)

  have eq2: "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"

    by (auto simp: image_iff)

  have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =

    (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x))`space M. (fst y * snd y) * emeasure M {x\<in>space M. (f x, indicator A x) = y})"

    using assms by (intro simple_function_partition) auto

  also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ereal))`space M.

    if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"

    by (auto simp: indicator_def split: split_if_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum_cong)

  also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ereal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"

    using assms by (subst setsum_cases) (auto intro!: simple_functionD(1) simp: eq)

  also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ereal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"

    by (subst setsum_reindex[where f=fst]) (auto simp: inj_on_def)

  also have "\<dots> = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))"

    using A[THEN sets.sets_into_space]

    by (intro setsum_mono_zero_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2)

  finally show ?thesis .

qed

lemma simple_integral_indicator_only[simp]:

  assumes "A \<in> sets M"

  shows "integral\<^sup>S M (indicator A) = emeasure M A"

  using simple_integral_indicator[OF assms, of "\<lambda>x. 1"] sets.sets_into_space[OF assms]

  by (simp_all add: image_constant_conv Int_absorb1 split: split_if_asm)

lemma simple_integral_null_set:

  assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets M"

  shows "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = 0"

proof -

  have "AE x in M. indicator N x = (0 :: ereal)"

    using `N \<in> null_sets M` by (auto simp: indicator_def intro!: AE_I[of _ _ N])

  then have "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^sup>Sx. 0 \<partial>M)"

    using assms apply (intro simple_integral_cong_AE) by auto

  then show ?thesis by simp

qed

lemma simple_integral_cong_AE_mult_indicator:

  assumes sf: "simple_function M f" and eq: "AE x in M. x \<in> S" and "S \<in> sets M"

  shows "integral\<^sup>S M f = (\<integral>\<^sup>Sx. f x * indicator S x \<partial>M)"

  using assms by (intro simple_integral_cong_AE) auto

lemma simple_integral_cmult_indicator:

  assumes A: "A \<in> sets M"

  shows "(\<integral>\<^sup>Sx. c * indicator A x \<partial>M) = c * emeasure M A"

  using simple_integral_mult[OF simple_function_indicator[OF A]]

  unfolding simple_integral_indicator_only[OF A] by simp

lemma simple_integral_positive:

  assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x"

  shows "0 \<le> integral\<^sup>S M f"

proof -

  have "integral\<^sup>S M (\<lambda>x. 0) \<le> integral\<^sup>S M f"

    using simple_integral_mono_AE[OF _ f ae] by auto

  then show ?thesis by simp

qed

section "Continuous positive integration"

definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where

  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"

syntax

  "_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)

translations

  "\<integral>\<^sup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)"

lemma positive_integral_positive:

  "0 \<le> integral\<^sup>P M f"

  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)

lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \<noteq> -\<infinity>"

  using positive_integral_positive[of M f] by auto

lemma positive_integral_def_finite:

  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"

    (is "_ = SUPREMUM ?A ?f")

  unfolding positive_integral_def

proof (safe intro!: antisym SUP_least)

  fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"

  let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"

  note gM = g(1)[THEN borel_measurable_simple_function]

  have \<mu>_G_pos: "0 \<le> (emeasure M) ?G" using gM by auto

  let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"

  from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"

    apply (safe intro!: simple_function_max simple_function_If)

    apply (force simp: max_def le_fun_def split: split_if_asm)+

    done

  show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"

  proof cases

    have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto

    assume "(emeasure M) ?G = 0"

    with gM have "AE x in M. x \<notin> ?G"

      by (auto simp add: AE_iff_null intro!: null_setsI)

    with gM g show ?thesis

      by (intro SUP_upper2[OF g0] simple_integral_mono_AE)

         (auto simp: max_def intro!: simple_function_If)

  next

    assume \<mu>_G: "(emeasure M) ?G \<noteq> 0"

    have "SUPREMUM ?A (integral\<^sup>S M) = \<infinity>"

    proof (intro SUP_PInfty)

      fix n :: nat

      let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)"

      have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>_G \<mu>_G_pos by (auto simp: ereal_divide_eq)

      then have "?g ?y \<in> ?A" by (rule g_in_A)

      have "real n \<le> ?y * (emeasure M) ?G"

        using \<mu>_G \<mu>_G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps)

      also have "\<dots> = (\<integral>\<^sup>Sx. ?y * indicator ?G x \<partial>M)"

        using `0 \<le> ?y` `?g ?y \<in> ?A` gM

        by (subst simple_integral_cmult_indicator) auto

      also have "\<dots> \<le> integral\<^sup>S M (?g ?y)" using `?g ?y \<in> ?A` gM

        by (intro simple_integral_mono) auto

      finally show "\<exists>i\<in>?A. real n \<le> integral\<^sup>S M i"

        using `?g ?y \<in> ?A` by blast

    qed

    then show ?thesis by simp

  qed

qed (auto intro: SUP_upper)

lemma positive_integral_mono_AE:

  assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>P M u \<le> integral\<^sup>P M v"

  unfolding positive_integral_def

proof (safe intro!: SUP_mono)

  fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"

  from ae[THEN AE_E] guess N . note N = this

  then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in)

  let ?n = "\<lambda>x. n x * indicator (space M - N) x"

  have "AE x in M. n x \<le> ?n x" "simple_function M ?n"

    using n N ae_N by auto

  moreover

  { fix x have "?n x \<le> max 0 (v x)"

    proof cases

      assume x: "x \<in> space M - N"

      with N have "u x \<le> v x" by auto

      with n(2)[THEN le_funD, of x] x show ?thesis

        by (auto simp: max_def split: split_if_asm)

    qed simp }

  then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI)

  moreover have "integral\<^sup>S M n \<le> integral\<^sup>S M ?n"

    using ae_N N n by (auto intro!: simple_integral_mono_AE)

  ultimately show "\<exists>m\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> v}. integral\<^sup>S M n \<le> integral\<^sup>S M m"

    by force

qed

lemma positive_integral_mono:

  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>P M u \<le> integral\<^sup>P M v"

  by (auto intro: positive_integral_mono_AE)

lemma positive_integral_cong_AE:

  "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"

  by (auto simp: eq_iff intro!: positive_integral_mono_AE)

lemma positive_integral_cong:

  "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"

  by (auto intro: positive_integral_cong_AE)

lemma positive_integral_eq_simple_integral:

  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"

proof -

  let ?f = "\<lambda>x. f x * indicator (space M) x"

  have f': "simple_function M ?f" using f by auto

  with f(2) have [simp]: "max 0 \<circ> ?f = ?f"

    by (auto simp: fun_eq_iff max_def split: split_indicator)

  have "integral\<^sup>P M ?f \<le> integral\<^sup>S M ?f" using f'

    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)

  moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>P M ?f"

    unfolding positive_integral_def

    using f' by (auto intro!: SUP_upper)

  ultimately show ?thesis

    by (simp cong: positive_integral_cong simple_integral_cong)

qed

lemma positive_integral_eq_simple_integral_AE:

  assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"

proof -

  have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max)

  with f have "integral\<^sup>P M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"

    by (simp cong: positive_integral_cong_AE simple_integral_cong_AE

             add: positive_integral_eq_simple_integral)

  with assms show ?thesis

    by (auto intro!: simple_integral_cong_AE split: split_max)

qed

lemma positive_integral_SUP_approx:

  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"

  and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"

  shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>P M (f i))" (is "_ \<le> ?S")

proof (rule ereal_le_mult_one_interval)

  have "0 \<le> (SUP i. integral\<^sup>P M (f i))"

    using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)

  then show "(SUP i. integral\<^sup>P M (f i)) \<noteq> -\<infinity>" by auto

  have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"

    using u(3) by auto

  fix a :: ereal assume "0 < a" "a < 1"

  hence "a \<noteq> 0" by auto

  let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"

  have B: "\<And>i. ?B i \<in> sets M"

    using f `simple_function M u`[THEN borel_measurable_simple_function] by auto

  let ?uB = "\<lambda>i x. u x * indicator (?B i) x"

  { fix i have "?B i \<subseteq> ?B (Suc i)"

    proof safe

      fix i x assume "a * u x \<le> f i x"

      also have "\<dots> \<le> f (Suc i) x"

        using `incseq f`[THEN incseq_SucD] unfolding le_fun_def by auto

      finally show "a * u x \<le> f (Suc i) x" .

    qed }

  note B_mono = this

  note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B]

  let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"

  have measure_conv: "\<And>i. (emeasure M) (u -` {i} \<inter> space M) = (SUP n. (emeasure M) (?B' i n))"

  proof -

    fix i

    have 1: "range (?B' i) \<subseteq> sets M" using B_u by auto

    have 2: "incseq (?B' i)" using B_mono by (auto intro!: incseq_SucI)

    have "(\<Union>n. ?B' i n) = u -` {i} \<inter> space M"

    proof safe

      fix x i assume x: "x \<in> space M"

      show "x \<in> (\<Union>i. ?B' (u x) i)"

      proof cases

        assume "u x = 0" thus ?thesis using `x \<in> space M` f(3) by simp

      next

        assume "u x \<noteq> 0"

        with `a < 1` u_range[OF `x \<in> space M`]

        have "a * u x < 1 * u x"

          by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)

        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)

        finally obtain i where "a * u x < f i x" unfolding SUP_def

          by (auto simp add: less_SUP_iff)

        hence "a * u x \<le> f i x" by auto

        thus ?thesis using `x \<in> space M` by auto

      qed

    qed

    then show "?thesis i" using SUP_emeasure_incseq[OF 1 2] by simp

  qed

  have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB i))"

    unfolding simple_integral_indicator[OF B `simple_function M u`]

  proof (subst SUP_ereal_setsum, safe)

    fix x n assume "x \<in> space M"

    with u_range show "incseq (\<lambda>i. u x * (emeasure M) (?B' (u x) i))" "\<And>i. 0 \<le> u x * (emeasure M) (?B' (u x) i)"

      using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff)

  next

    show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"

      using measure_conv u_range B_u unfolding simple_integral_def

      by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric])

  qed

  moreover

  have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"

    apply (subst SUP_ereal_cmult [symmetric])

  proof (safe intro!: SUP_mono bexI)

    fix i

    have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"

      using B `simple_function M u` u_range

      by (subst simple_integral_mult) (auto split: split_indicator)

    also have "\<dots> \<le> integral\<^sup>P M (f i)"

    proof -

      have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto

      show ?thesis using f(3) * u_range `0 < a`

        by (subst positive_integral_eq_simple_integral[symmetric])

           (auto intro!: positive_integral_mono split: split_indicator)

    qed

    finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>P M (f i)"

      by auto

  next

    fix i show "0 \<le> \<integral>\<^sup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range

      by (intro simple_integral_positive) (auto split: split_indicator)

  qed (insert `0 < a`, auto)

  ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp

qed

lemma incseq_positive_integral:

  assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>P M (f i))"

proof -

  have "\<And>i x. f i x \<le> f (Suc i) x"

    using assms by (auto dest!: incseq_SucD simp: le_fun_def)

  then show ?thesis

    by (auto intro!: incseq_SucI positive_integral_mono)

qed

text {* Beppo-Levi monotone convergence theorem *}

lemma positive_integral_monotone_convergence_SUP:

  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"

  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"

proof (rule antisym)

  show "(SUP j. integral\<^sup>P M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"

    by (auto intro!: SUP_least SUP_upper positive_integral_mono)

next

  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>P M (f j))"

    unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]

  proof (safe intro!: SUP_least)

    fix g assume g: "simple_function M g"

      and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"

    then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"

      using f by (auto intro!: SUP_upper2)

    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"

      by (intro  positive_integral_SUP_approx[OF f g _ g'])

         (auto simp: le_fun_def max_def)

  qed

qed

lemma positive_integral_monotone_convergence_SUP_AE:

  assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M"

  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"

proof -

  from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"

    by (simp add: AE_all_countable)

  from this[THEN AE_E] guess N . note N = this

  let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"

  have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])

  then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"

    by (auto intro!: positive_integral_cong_AE)

  also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))"

  proof (rule positive_integral_monotone_convergence_SUP)

    show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)

    { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"

        using f N(3) by (intro measurable_If_set) auto

      fix x show "0 \<le> ?f i x"

        using N(1) by auto }

  qed

  also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"

    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)

  finally show ?thesis .

qed

lemma positive_integral_monotone_convergence_SUP_AE_incseq:

  assumes f: "incseq f" "\<And>i. AE x in M. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M"

  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"

  using f[unfolded incseq_Suc_iff le_fun_def]

  by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])

     auto

lemma positive_integral_monotone_convergence_simple:

  assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"

  shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"

  using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)

    f(3)[THEN borel_measurable_simple_function] f(2)]

  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)

lemma positive_integral_max_0:

  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"

  by (simp add: le_fun_def positive_integral_def)