Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 133 kB

Quellcode-Bibliothek Nonnegative_Lebesgue_Integration.thy Sprache: Isabelle

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

section \<open>Lebesgue Integration for Nonnegative Functions\<close>

theory Nonnegative_Lebesgue_Integration
  imports Measure_Space Borel_Space
begin

subsection\<^marker>\<open>tag unimportant\<close> \<open>Approximating functions\<close>

lemma AE_upper_bound_inf_ennreal:
  fixes F G::"'a \ ennreal"
  assumes "\e. (e::real) > 0 \ AE x in M. F x \ G x + e"
  shows "AE x in M. F x \ G x"
proof -
  have "AE x in M. \n::nat. F x \ G x + ennreal (1 / Suc n)"
    using assms by (auto simp: AE_all_countable)
  then show ?thesis
  proof (eventually_elim)
    fix x assume x: "\n::nat. F x \ G x + ennreal (1 / Suc n)"
    show "F x \ G x"
    proof (rule ennreal_le_epsilon)
      fix e :: real assume "0 < e"
      then obtain n where n: "1 / Suc n < e"
        by (blast elim: nat_approx_posE)
      have "F x \ G x + 1 / Suc n"
        using x by simp
      also have "\ \ G x + e"
        using n by (intro add_mono ennreal_leI) auto
      finally show "F x \ G x + ennreal e" .
    qed
  qed
qed

lemma AE_upper_bound_inf:
  fixes F G::"'a \ real"
  assumes "\e. e > 0 \ AE x in M. F x \ G x + e"
  shows "AE x in M. F x \ G x"
proof -
  have "AE x in M. F x \ G x + 1/real (n+1)" for n::nat
    by (rule assms, auto)
  then have "AE x in M. \n::nat \ UNIV. F x \ G x + 1/real (n+1)"
    by (rule AE_ball_countable', auto)
  moreover
  {
    fix x assume i: "\n::nat \ UNIV. F x \ G x + 1/real (n+1)"
    have "(\n. G x + 1/real (n+1)) \ G x + 0"
      by (rule tendsto_add, simp, rule LIMSEQ_ignore_initial_segment[OF lim_1_over_n, of 1])
    then have "F x \ G x" using i LIMSEQ_le_const by fastforce
  }
  ultimately show ?thesis by auto
qed

lemma not_AE_zero_ennreal_E:
  fixes f::"'a \ ennreal"
  assumes "\ (AE x in M. f x = 0)" and [measurable]: "f \ borel_measurable M"
  shows "\A\sets M. \e::real>0. emeasure M A > 0 \ (\x \ A. f x \ e)"
proof -
  { assume "\ (\e::real>0. {x \ space M. f x \ e} \ null_sets M)"
    then have "0 < e \ AE x in M. f x \ e" for e :: real
      by (auto simp: not_le less_imp_le dest!: AE_not_in)
    then have "AE x in M. f x \ 0"
      by (intro AE_upper_bound_inf_ennreal[where G="\_. 0"]) simp
    then have False
      using assms by auto }
  then obtain e::real where e: "e > 0" "{x \ space M. f x \ e} \ null_sets M" by auto
  define A where "A = {x \ space M. f x \ e}"
  have 1 [measurable]: "A \ sets M" unfolding A_def by auto
  have 2: "emeasure M A > 0"
    using e(2) A_def \<open>A \<in> sets M\<close> by auto
  have 3: "\x. x \ A \ f x \ e" unfolding A_def by auto
  show ?thesis using e(1) 1 2 3 by blast
qed

lemma not_AE_zero_E:
  fixes f::"'a \ real"
  assumes "AE x in M. f x \ 0"
          "\(AE x in M. f x = 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 -
  have "\e. e > 0 \ {x \ space M. f x \ e} \ null_sets M"
  proof (rule ccontr)
    assume *: "\(\e. e > 0 \ {x \ space M. f x \ e} \ null_sets M)"
    {
      fix e::real assume "e > 0"
      then have "{x \ space M. f x \ e} \ null_sets M" using * by blast
      then have "AE x in M. x \ {x \ space M. f x \ e}" using AE_not_in by blast
      then have "AE x in M. f x \ e" by auto
    }
    then have "AE x in M. f x \ 0" by (rule AE_upper_bound_inf, auto)
    then have "AE x in M. f x = 0" using assms(1) by auto
    then show False using assms(2) by auto
  qed
  then obtain e where e: "e>0" "{x \ space M. f x \ e} \ null_sets M" by auto
  define A where "A = {x \ space M. f x \ e}"
  have 1 [measurable]: "A \ sets M" unfolding A_def by auto
  have 2: "emeasure M A > 0"
    using e(2) A_def \<open>A \<in> sets M\<close> by auto
  have 3: "\x. x \ A \ f x \ e" unfolding A_def by auto
  show ?thesis
    using e(1) 1 2 3 by blast
qed

subsection "Simple function"

text \<open>

Our simple functions are not restricted to nonnegative real numbers. Instead
they are just functions with a finite range and are measurable when singleton
sets are measurable.

\<close>

definition\<^marker>\<open>tag important\<close> "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 \ space M \ sets M"
proof -
  show "finite (g ` space M)"
    using assms unfolding simple_function_def by auto
  have "g -` X \ space M = g -` (X \ g`space M) \ space M" by auto
  also have "\ = (\x\X \ g`space M. g-`{x} \ space M)" by auto
  finally show "g -` X \ space M \ 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 \ f \ measurable M (count_space UNIV)"
  unfolding simple_function_def measurable_def
proof safe
  fix A assume "finite (f ` space M)" "\x\f ` space M. f -` {x} \ space M \ sets M"
  then have "(\x\f ` space M. if x \ A then f -` {x} \ space M else {}) \ sets M"
    by (intro sets.finite_UN) auto
  also have "(\x\f ` space M. if x \ A then f -` {x} \ space M else {}) = f -` A \ space M"
    by (auto split: if_split_asm)
  finally show "f -` A \ space M \ sets M" .
qed simp

lemma borel_measurable_simple_function:
  "simple_function M f \ f \ 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 \ g -` B \ space M \ sets M"
proof -
  have "f -` A \ g -` B \ space M = (f -` A \ space M) \ (g -` B \ space M)"
    by auto
  then show ?thesis using assms[THEN simple_functionD(2)] by auto
qed

lemma simple_function_indicator_representation:
  fixes f ::"'a \ ennreal"
  assumes f: "simple_function M f" and x: "x \ space M"
  shows "f x = (\y \ f ` space M. y * indicator (f -` {y} \ space M) x)"
  (is "?l = ?r")
proof -
  have "?r = (\y \ f ` space M.
    (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
    by (auto intro!: sum.cong)
  also have "... = f x * indicator (f -` {f x} \ space M) x"
    using assms by (auto dest: simple_functionD)
  also have "... = f x" using x by (auto simp: indicator_def)
  finally show ?thesis by auto
qed

lemma simple_function_notspace:
  "simple_function M (\x. h x * indicator (- space M) x::ennreal)" (is "simple_function M ?h")
proof -
  have "?h ` space M \ {0}" unfolding indicator_def by auto
  hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
  have "?h -` {0} \ space M = space M" by auto
  thus ?thesis unfolding simple_function_def by (auto simp add: image_constant_conv)
qed

lemma simple_function_cong:
  assumes "\t. t \ space M \ f t = g t"
  shows "simple_function M f \ simple_function M g"
proof -
  have "\x. f -` {x} \ space M = g -` {x} \ space M"
    using assms by auto
  with assms show ?thesis
    by (simp add: simple_function_def cong: image_cong)
qed

lemma simple_function_cong_algebra:
  assumes "sets N = sets M" "space N = space M"
  shows "simple_function M f \ simple_function N f"
  unfolding simple_function_def assms ..

lemma simple_function_borel_measurable:
  fixes f :: "'a \ 'x::{t2_space}"
  assumes "f \ 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_iff_borel_measurable:
  fixes f :: "'a \ 'x::{t2_space}"
  shows "simple_function M f \ finite (f ` space M) \ f \ borel_measurable M"
  by (metis borel_measurable_simple_function simple_functionD(1) simple_function_borel_measurable)

lemma simple_function_eq_measurable:
  "simple_function M f \ finite (f`space M) \ f \ measurable M (count_space UNIV)"
  using measurable_simple_function[of M f] by (fastforce simp: simple_function_def)

lemma simple_function_const[intro, simp]:
  "simple_function M (\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 \ f)"
  unfolding simple_function_def
proof safe
  show "finite ((g \ f) ` space M)"
    using assms unfolding simple_function_def image_comp [symmetric] by auto
next
  fix x assume "x \ space M"
  let ?G = "g -` {g (f x)} \ (f`space M)"
  have *: "(g \ f) -` {(g \ f) x} \ space M =
    (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
  show "(g \ f) -` {(g \ f) x} \ space M \ sets M"
    using assms unfolding simple_function_def *
    by (rule_tac sets.finite_UN) auto
qed

lemma simple_function_indicator[intro, simp]:
  assumes "A \ sets M"
  shows "simple_function M (indicator A)"
proof -
  have "indicator A ` space M \ {0, 1}" (is "?S \ _")
    by (auto simp: indicator_def)
  hence "finite ?S" by (rule finite_subset) simp
  moreover have "- A \ 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 (\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 \ g`space M"]) auto
next
  fix x assume "x \ space M"
  have "(\x. (f x, g x)) -` {(f x, g x)} \ space M =
      (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"
    by auto
  with \<open>x \<in> space M\<close> 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 (\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 (\x. h (f x) (g x))"
proof -
  have "simple_function M ((\(x, y). h x y) \ (\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="(+)"]
  and simple_function_diff[intro, simp] = simple_function_compose2[where h="(-)"]
  and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
  and simple_function_mult[intro, simp] = simple_function_compose2[where h="(*)"]
  and simple_function_div[intro, simp] = simple_function_compose2[where h="(/)"]
  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_sum[intro, simp]:
  assumes "\i. i \ P \ simple_function M (f i)"
  shows "simple_function M (\x. \i\P. f i x)"
proof cases
  assume "finite P" from this assms show ?thesis by induct auto
qed auto

lemma simple_function_ennreal[intro, simp]:
  fixes f g :: "'a \ real" assumes sf: "simple_function M f"
  shows "simple_function M (\x. ennreal (f x))"
  by (rule simple_function_compose1[OF sf])

lemma simple_function_real_of_nat[intro, simp]:
  fixes f g :: "'a \ nat" assumes sf: "simple_function M f"
  shows "simple_function M (\x. real (f x))"
  by (rule simple_function_compose1[OF sf])

lemma\<^marker>\<open>tag important\<close> borel_measurable_implies_simple_function_sequence:
  fixes u :: "'a \ ennreal"
  assumes u[measurable]: "u \ borel_measurable M"
  shows "\f. incseq f \ (\i. (\x. f i x < top) \ simple_function M (f i)) \ u = (SUP i. f i)"
proof -
  define f where [abs_def]:
    "f i x = real_of_int (floor (enn2real (min i (u x)) * 2^i)) / 2^i" for i x

  have [simp]: "0 \ f i x" for i x
    by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg enn2real_nonneg)

  have *: "2^n * real_of_int x = real_of_int (2^n * x)" for n x
    by simp

  have "real_of_int \real i * 2 ^ i\ = real_of_int \i * 2 ^ i\" for i
    by (intro arg_cong[where f=real_of_int]) simp
  then have [simp]: "real_of_int \real i * 2 ^ i\ = i * 2 ^ i" for i
    unfolding floor_of_nat by simp

  have "incseq f"
  proof (intro monoI le_funI)
    fix m n :: nat and x assume "m \ n"
    moreover
    { fix d :: nat
      have "\2^d::real\ * \2^m * enn2real (min (of_nat m) (u x))\ \
        \<lfloor>2^d * (2^m * enn2real (min (of_nat m) (u x)))\<rfloor>"
        by (rule le_mult_floor) (auto)
      also have "\ \ \2^d * (2^m * enn2real (min (of_nat d + of_nat m) (u x)))\"
        by (intro floor_mono mult_mono enn2real_mono min.mono)
           (auto simp: min_less_iff_disj of_nat_less_top)
      finally have "f m x \ f (m + d) x"
        unfolding f_def
        by (auto simp: field_simps power_add * simp del: of_int_mult) }
    ultimately show "f m x \ f n x"
      by (auto simp add: le_iff_add)
  qed
  then have inc_f: "incseq (\i. ennreal (f i x))" for x
    by (auto simp: incseq_def le_fun_def)
  then have "incseq (\i x. ennreal (f i x))"
    by (auto simp: incseq_def le_fun_def)
  moreover
  have "simple_function M (f i)" for i
  proof (rule simple_function_borel_measurable)
    have "\enn2real (min (of_nat i) (u x)) * 2 ^ i\ \ \int i * 2 ^ i\" for x
      by (cases "u x" rule: ennreal_cases)
         (auto split: split_min intro!: floor_mono)
    then have "f i ` space M \ (\n. real_of_int n / 2^i) ` {0 .. of_nat i * 2^i}"
      unfolding floor_of_int by (auto simp: f_def intro!: imageI)
    then show "finite (f i ` space M)"
      by (rule finite_subset) auto
    show "f i \ borel_measurable M"
      unfolding f_def enn2real_def by measurable
  qed
  moreover
  { fix x
    have "(SUP i. ennreal (f i x)) = u x"
    proof (cases "u x" rule: ennreal_cases)
      case top then show ?thesis
        by (simp add: f_def inf_min[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric]
                      ennreal_SUP_of_nat_eq_top)
    next
      case (real r)
      obtain n where "r \ of_nat n" using real_arch_simple by auto
      then have min_eq_r: "\\<^sub>F x in sequentially. min (real x) r = r"
        by (auto simp: eventually_sequentially intro!: exI[of _ n] split: split_min)

      have "(\i. real_of_int \min (real i) r * 2^i\ / 2^i) \ r"
      proof (rule tendsto_sandwich)
        show "(\n. r - (1/2)^n) \ r"
          by (auto intro!: tendsto_eq_intros LIMSEQ_power_zero)
        show "\\<^sub>F n in sequentially. real_of_int \min (real n) r * 2 ^ n\ / 2 ^ n \ r"
          using min_eq_r by eventually_elim (auto simp: field_simps)
        have *: "r * (2 ^ n * 2 ^ n) \ 2^n + 2^n * real_of_int \r * 2 ^ n\" for n
          using real_of_int_floor_ge_diff_one[of "r * 2^n", THEN mult_left_mono, of "2^n"]
          by (auto simp: field_simps)
        show "\\<^sub>F n in sequentially. r - (1/2)^n \ real_of_int \min (real n) r * 2 ^ n\ / 2 ^ n"
          using min_eq_r by eventually_elim (insert *, auto simp: field_simps)
      qed auto
      then have "(\i. ennreal (f i x)) \ ennreal r"
        by (simp add: real f_def ennreal_of_nat_eq_real_of_nat min_ennreal)
      from LIMSEQ_unique[OF LIMSEQ_SUP[OF inc_f] this]
      show ?thesis
        by (simp add: real)
    qed }
  ultimately show ?thesis
    by (intro exI [of _ "\i x. ennreal (f i x)"]) (auto simp add: image_comp)
qed

lemma borel_measurable_implies_simple_function_sequence':
  fixes u :: "'a \ ennreal"
  assumes u: "u \ borel_measurable M"
  obtains f where
    "\i. simple_function M (f i)" "incseq f" "\i x. f i x < top" "\x. (SUP i. f i x) = u x"
  using borel_measurable_implies_simple_function_sequence [OF u]
  by (metis SUP_apply)

lemma\<^marker>\<open>tag important\<close> simple_function_induct
    [consumes 1, case_names cong set mult add, induct set: simple_function]:
  fixes u :: "'a \ ennreal"
  assumes u: "simple_function M u"
  assumes cong: "\f g. simple_function M f \ simple_function M g \ (AE x in M. f x = g x) \ P f \ P g"
  assumes set: "\A. A \ sets M \ P (indicator A)"
  assumes mult: "\u c. P u \ P (\x. c * u x)"
  assumes add: "\u v. P u \ P v \ P (\x. v x + u x)"
  shows "P u"
proof (rule cong)
  from AE_space show "AE x in M. (\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x"
  proof eventually_elim
    fix x assume x: "x \ space M"
    from simple_function_indicator_representation[OF u x]
    show "(\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x" ..
  qed
next
  from u have "finite (u ` space M)"
    unfolding simple_function_def by auto
  then show "P (\x. \y\u ` space M. y * indicator (u -` {y} \ 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 (\x. (\y\u ` space M. y * indicator (u -` {y} \ 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 1, case_names cong set mult add]:
  fixes u :: "'a \ ennreal"
  assumes u: "simple_function M u"
  assumes cong: "\f g. simple_function M f \ simple_function M g \ (\x. x \ space M \ f x = g x) \ P f \ P g"
  assumes set: "\A. A \ sets M \ P (indicator A)"
  assumes mult: "\u c. simple_function M u \ P u \ P (\x. c * u x)"
  assumes add: "\u v. simple_function M u \ P u \ simple_function M v \ (\x. x \ space M \ u x = 0 \ v x = 0) \ P v \ P (\x. v x + u x)"
  shows "P u"
proof -
  show ?thesis
  proof (rule cong)
    fix x assume x: "x \ space M"
    from simple_function_indicator_representation[OF u x]
    show "(\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x" ..
  next
    show "simple_function M (\x. (\y\u ` space M. y * indicator (u -` {y} \ space M) x))"
      apply (subst simple_function_cong)
      apply (rule simple_function_indicator_representation[symmetric])
      apply (auto intro: u)
      done
  next
    from u have "finite (u ` space M)"
      unfolding simple_function_def by auto
    then show "P (\x. \y\u ` space M. y * indicator (u -` {y} \ space M) x)"
    proof induct
      case empty show ?case
        using set[of "{}"] by (simp add: indicator_def[abs_def])
    next
      case (insert x S)
      { fix z have "(\y\S. y * indicator (u -` {y} \ space M) z) = 0 \
          x * indicator (u -` {x} \<inter> space M) z = 0"
          using insert by (subst sum_eq_0_iff) (auto simp: indicator_def) }
      note disj = this
      from insert show ?case
        by (auto intro!: add mult set simple_functionD u simple_function_sum disj)
    qed
  qed fact
qed

lemma\<^marker>\<open>tag important\<close> borel_measurable_induct
    [consumes 1, case_names cong set mult add seq, induct set: borel_measurable]:
  fixes u :: "'a \ ennreal"
  assumes u: "u \ borel_measurable M"
  assumes cong: "\f g. f \ borel_measurable M \ g \ borel_measurable M \ (\x. x \ space M \ f x = g x) \ P g \ P f"
  assumes set: "\A. A \ sets M \ P (indicator A)"
  assumes mult': "\u c. c < top \ u \ borel_measurable M \ (\x. x \ space M \ u x < top) \ P u \ P (\x. c * u x)"
  assumes add: "\u v. u \ borel_measurable M\ (\x. x \ space M \ u x < top) \ P u \ v \ borel_measurable M \ (\x. x \ space M \ v x < top) \ (\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. x \ space M \ U i x < top) \ (\i. P (U i)) \ incseq U \ u = (SUP i. U i) \ P (SUP i. U i)"
  shows "P u"
  using u
proof (induct rule: borel_measurable_implies_simple_function_sequence')
  fix U assume U: "\i. simple_function M (U i)" "incseq U" "\i x. U i x < top" and sup: "\x. (SUP i. U i x) = u x"
  have u_eq: "u = (SUP i. U i)"
    using u by (auto simp add: image_comp sup)

  have not_inf: "\x i. x \ space M \ U i x < top"
    using U by (auto simp: image_iff eq_commute)

  from U have "\i. U i \ 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 \<open>simple_function M (U i)\<close> not_inf[of _ i]
    proof (induct rule: simple_function_induct_nn)
      case (mult u c)
      show ?case
      proof cases
        assume "c = 0 \ space M = {} \ (\x\space M. u x = 0)"
        with mult(1) show ?thesis
          by (intro cong[of "\x. c * u x" "indicator {}"] set)
             (auto dest!: borel_measurable_simple_function)
      next
        assume "\ (c = 0 \ space M = {} \ (\x\space M. u x = 0))"
        then obtain x where "space M \ {}" and x: "x \ space M" "u x \ 0" "c \ 0"
          by auto
        with mult(3)[of x] have "c < top"
          by (auto simp: ennreal_mult_less_top)
        then have u_fin: "x' \ space M \ u x' < top" for x'
          using mult(3)[of x'] \c \ 0\ by (auto simp: ennreal_mult_less_top)
        then have "P u"
          by (rule mult)
        with u_fin \<open>c < top\<close> mult(1) show ?thesis
          by (intro mult') (auto dest!: borel_measurable_simple_function)
      qed
    qed (auto intro: cong intro!: set add 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 \ space M \ sets M"
  shows "simple_function M (\x. if x \ A then f x else g x)" (is "simple_function M ?IF")
proof -
  define F where "F x = f -` {x} \ space M" for x
  define G where "G x = g -` {x} \ space M" for x
  show ?thesis unfolding simple_function_def
  proof safe
    have "?IF ` space M \ f ` space M \ 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 \ space M"
    then have *: "?IF -` {?IF x} \ space M = (if x \ 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: if_split_asm simp: G_def F_def)
    have [intro]: "\x. F x \ sets M" "\x. G x \ sets M"
      unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
    show "?IF -` {?IF x} \ space M \ 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\space M. P x} \ sets M"
  shows "simple_function M (\x. if P x then f x else g x)"
proof -
  have "{x\space M. P x} = {x. P x} \ 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 \ 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 \ measurable M M'"
    and f: "simple_function M' f"
  shows "simple_function M (\x. f (T x))"
proof (intro simple_function_def[THEN iffD2] conjI ballI)
  have "(\x. f (T x)) ` space M \ f ` space M'"
    using T unfolding measurable_def by auto
  then show "finite ((\x. f (T x)) ` space M)"
    using f unfolding simple_function_def by (auto intro: finite_subset)
  fix i assume i: "i \ (\x. f (T x)) ` space M"
  then have "i \ f ` space M'"
    using T unfolding measurable_def by auto
  then have "f -` {i} \ space M' \ sets M'"
    using f unfolding simple_function_def by auto
  then have "T -` (f -` {i} \ space M') \ space M \ sets M"
    using T unfolding measurable_def by auto
  also have "T -` (f -` {i} \ space M') \ space M = (\x. f (T x)) -` {i} \ space M"
    using T unfolding measurable_def by auto
  finally show "(\x. f (T x)) -` {i} \ space M \ sets M" .
qed

subsection "Simple integral"

definition\<^marker>\<open>tag important\<close> simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" (\<open>integral\<^sup>S\<close>) where
  "integral\<^sup>S M f = (\x \ f ` space M. x * emeasure M (f -` {x} \ space M))"

syntax
  "_simple_integral" :: "pttrn \ ennreal \ 'a measure \ ennreal"
    (\<open>(\<open>open_block notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>S _. _ \<partial>_)\<close> [60,61] 110)
syntax_consts
  "_simple_integral" == simple_integral
translations
  "\\<^sup>S x. f \M" == "CONST simple_integral M (%x. f)"

lemma simple_integral_cong:
  assumes "\t. t \ space M \ f t = g t"
  shows "integral\<^sup>S M f = integral\<^sup>S M g"
proof -
  have "f ` space M = g ` space M"
    "\x. f -` {x} \ space M = g -` {x} \ space M"
    using assms by (auto intro!: image_eqI)
  thus ?thesis unfolding simple_integral_def by simp
qed

lemma simple_integral_const[simp]:
  "(\\<^sup>Sx. c \M) = c * (emeasure M) (space M)"
proof (cases "space M = {}")
  case True thus ?thesis unfolding simple_integral_def by simp
next
  case False hence "(\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: "\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 "integral\<^sup>S M f = (\y\g ` space M. v y * emeasure M {x\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 \ measurable M (count_space UNIV)" "g \ measurable M (count_space UNIV)"
    by (auto intro: measurable_simple_function)

  { 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 "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!: sum.cong ennreal_mult_left_cong)
    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. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
      by auto
    have eq:"(\i\{z. \x\space M. f y = f x \ z = g x}. {x \ 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. \x\space M. f y = f x \ z = g x}"
      by (rule rev_finite_subset) auto
    then show "emeasure M (f -` {f y} \ 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: sum.If_cases)
      apply (subst sum_emeasure)
      apply (auto simp: disjoint_family_on_def eq)
      done
  qed
  also have "\ = (\y\f`space M. (\z\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!: sum.cong simp: sum_distrib_left)
  also have "\ = ?r"
    by (subst sum.swap)
       (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
  finally show "integral\<^sup>S M f = ?r" .
qed

lemma simple_integral_add[simp]:
  assumes f: "simple_function M f" and "\x. 0 \ f x" and g: "simple_function M g" and "\x. 0 \ g x"
  shows "(\\<^sup>Sx. f x + g x \M) = integral\<^sup>S M f + integral\<^sup>S M g"
proof -
  have "(\\<^sup>Sx. f x + g x \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 "\ = (\y\(\x. (f x, g x))`space M. fst y * emeasure M {x\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!: sum.cong distrib_right simp: sum.distrib[symmetric])
  also have "(\y\(\x. (f x, g x))`space M. fst y * emeasure M {x\space M. (f x, g x) = y}) = (\\<^sup>Sx. f x \M)"
    by (intro simple_function_partition[symmetric]) (auto intro: f g)
  also have "(\y\(\x. (f x, g x))`space M. snd y * emeasure M {x\space M. (f x, g x) = y}) = (\\<^sup>Sx. g x \M)"
    by (intro simple_function_partition[symmetric]) (auto intro: f g)
  finally show ?thesis .
qed

lemma simple_integral_sum[simp]:
  assumes "\i x. i \ P \ 0 \ f i x"
  assumes "\i. i \ P \ simple_function M (f i)"
  shows "(\\<^sup>Sx. (\i\P. f i x) \M) = (\i\P. integral\<^sup>S M (f i))"
proof cases
  assume "finite P"
  from this assms show ?thesis
    by induct (auto)
qed auto

lemma simple_integral_mult[simp]:
  assumes f: "simple_function M f"
  shows "(\\<^sup>Sx. c * f x \M) = c * integral\<^sup>S M f"
proof -
  have "(\\<^sup>Sx. c * f x \M) = (\y\f ` space M. (c * y) * emeasure M {x\space M. f x = y})"
    using f by (intro simple_function_partition) auto
  also have "\ = c * integral\<^sup>S M f"
    using f unfolding simple_integral_def
    by (subst sum_distrib_left) (auto simp: 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 \ g x"
  shows "integral\<^sup>S M f \ integral\<^sup>S M g"
proof -
  let ?\<mu> = "\<lambda>P. emeasure M {x\<in>space M. P x}"
  have "integral\<^sup>S M f = (\y\(\x. (f x, g x))`space M. fst y * ?\ (\x. (f x, g x) = y))"
    using f g by (intro simple_function_partition) auto
  also have "\ \ (\y\(\x. (f x, g x))`space M. snd y * ?\ (\x. (f x, g x) = y))"
  proof (clarsimp intro!: sum_mono)
    fix x assume "x \ space M"
    let ?M = "?\ (\y. f y = f x \ g y = g x)"
    show "f x * ?M \ g x * ?M"
    proof cases
      assume "?M \ 0"
      then have "0 < ?M"
        by (simp add: less_le)
      also have "\ \ ?\ (\y. f x \ g x)"
        using mono by (force intro: emeasure_mono_AE)
      finally have "\ \ f x \ g x"
        by (intro notI) auto
      then show ?thesis
        by (intro mult_right_mono) auto
    qed simp
  qed
  also have "\ = 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: "\ x. x \ space M \ f x \ g x"
  shows "integral\<^sup>S M f \ 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\space M. f x \ 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\space M. f x \ g x} = 0" by fact
  show "{x \ space M. f x \ g x} \ sets M"
    using sf[THEN borel_measurable_simple_function] by auto
qed simp

lemma simple_integral_indicator:
  assumes A: "A \ sets M"
  assumes f: "simple_function M f"
  shows "(\\<^sup>Sx. f x * indicator A x \M) =
    (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))"
proof -
  have eq: "(\x. (f x, indicator A x)) ` space M \ {x. snd x = 1} = (\x. (f x, 1::ennreal))`A"
    using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: if_split_asm)
  have eq2: "\x. f x \ f ` A \ f -` {f x} \ space M \ A = {}"
    by (auto simp: image_iff)

  have "(\\<^sup>Sx. f x * indicator A x \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 "\ = (\y\(\x. (f x, indicator A x::ennreal))`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: if_split_asm intro!: arg_cong2[where f="(*)"] arg_cong2[where f=emeasure] sum.cong)
  also have "\ = (\y\(\x. (f x, 1::ennreal))`A. fst y * emeasure M (f -` {fst y} \ space M \ A))"
    using assms by (subst sum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
  also have "\ = (\y\fst`(\x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \ space M \ A))"
    by (subst sum.reindex [of fst]) (auto simp: inj_on_def)
  also have "\ = (\x \ f ` space M. x * emeasure M (f -` {x} \ space M \ A))"
    using A[THEN sets.sets_into_space]
    by (intro sum.mono_neutral_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2)
  finally show ?thesis .
qed

lemma simple_integral_indicator_only[simp]:
  assumes "A \ sets M"
  shows "integral\<^sup>S M (indicator A) = emeasure M A"
  using simple_integral_indicator[OF assms, of "\x. 1"] sets.sets_into_space[OF assms]
  by (simp_all add: image_constant_conv Int_absorb1 split: if_split_asm)

lemma simple_integral_null_set:
  assumes "simple_function M u" "\x. 0 \ u x" and "N \ null_sets M"
  shows "(\\<^sup>Sx. u x * indicator N x \M) = 0"
proof -
  have "AE x in M. indicator N x = (0 :: ennreal)"
    using \<open>N \<in> null_sets M\<close> by (auto simp: indicator_def intro!: AE_I[of _ _ N])
  then have "(\\<^sup>Sx. u x * indicator N x \M) = (\\<^sup>Sx. 0 \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 \ S" and "S \ sets M"
  shows "integral\<^sup>S M f = (\\<^sup>Sx. f x * indicator S x \M)"
  using assms by (intro simple_integral_cong_AE) auto

lemma simple_integral_cmult_indicator:
  assumes A: "A \ sets M"
  shows "(\\<^sup>Sx. c * indicator A x \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_nonneg:
  assumes f: "simple_function M f" and ae: "AE x in M. 0 \ f x"
  shows "0 \ integral\<^sup>S M f"
proof -
  have "integral\<^sup>S M (\x. 0) \ integral\<^sup>S M f"
    using simple_integral_mono_AE[OF _ f ae] by auto
  then show ?thesis by simp
qed

subsection \<open>Integral on nonnegative functions\<close>

definition\<^marker>\<open>tag important\<close> nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" (\<open>integral\<^sup>N\<close>) where
  "integral\<^sup>N M f = (SUP g \ {g. simple_function M g \ g \ f}. integral\<^sup>S M g)"

syntax
  "_nn_integral" :: "pttrn \ ennreal \ 'a measure \ ennreal" (\(\indent=2 notation=\binder integral\\\\<^sup>+(2 _./ _)/ \_)\ [60,61] 110)
syntax_consts
  "_nn_integral" == nn_integral
translations
  "\\<^sup>+x. f \M" == "CONST nn_integral M (\x. f)"

lemma nn_integral_def_finite:
  "integral\<^sup>N M f = (SUP g \ {g. simple_function M g \ g \ f \ (\x. g x < top)}. integral\<^sup>S M g)"
    (is "_ = Sup (?A ` ?f)")
  unfolding nn_integral_def
proof (safe intro!: antisym SUP_least)
  fix g assume g[measurable]: "simple_function M g" "g \ f"

  show "integral\<^sup>S M g \ Sup (?A ` ?f)"
  proof cases
    assume ae: "AE x in M. g x \ top"
    let ?G = "{x \ space M. g x \ top}"
    have "integral\<^sup>S M g = integral\<^sup>S M (\x. g x * indicator ?G x)"
    proof (rule simple_integral_cong_AE)
      show "AE x in M. g x = g x * indicator ?G x"
        using ae AE_space by eventually_elim auto
    qed (insert g, auto)
    also have "\ \ Sup (?A ` ?f)"
      using g by (intro SUP_upper) (auto simp: le_fun_def less_top split: split_indicator)
    finally show ?thesis .
  next
    assume nAE: "\ (AE x in M. g x \ top)"
    then have "emeasure M {x\space M. g x = top} \ 0" (is "emeasure M ?G \ 0")
      by (subst (asm) AE_iff_measurable[OF _ refl]) auto
    then have "top = (SUP n. (\\<^sup>Sx. of_nat n * indicator ?G x \M))"
      by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric])
    also have "\ \ Sup (?A ` ?f)"
      using g
      by (safe intro!: SUP_least SUP_upper)
         (auto simp: le_fun_def of_nat_less_top top_unique[symmetric] split: split_indicator
               intro: order_trans[of _ "g x" "f x" for x, OF order_trans[of _ top]])
    finally show ?thesis
      by (simp add: top_unique del: SUP_eq_top_iff Sup_eq_top_iff)
  qed
qed (auto intro: SUP_upper)

lemma nn_integral_mono_AE:
  assumes ae: "AE x in M. u x \ v x" shows "integral\<^sup>N M u \ integral\<^sup>N M v"
  unfolding nn_integral_def
proof (safe intro!: SUP_mono)
  fix n assume n: "simple_function M n" "n \ u"
  from ae[THEN AE_E] obtain N
    where N: "{x \ space M. \ u x \ v x} \ N" "emeasure M N = 0" "N \ sets M"
    by auto
  then have ae_N: "AE x in M. x \ N" by (auto intro: AE_not_in)
  let ?n = "\x. n x * indicator (space M - N) x"
  have "AE x in M. n x \ ?n x" "simple_function M ?n"
    using n N ae_N by auto
  moreover
  { fix x have "?n x \ v x"
    proof cases
      assume x: "x \ space M - N"
      with N have "u x \ v x" by auto
      with n(2)[THEN le_funD, of x] x show ?thesis
        by (auto simp: max_def split: if_split_asm)
    qed simp }
  then have "?n \ v" by (auto simp: le_funI)
  moreover have "integral\<^sup>S M n \ integral\<^sup>S M ?n"
    using ae_N N n by (auto intro!: simple_integral_mono_AE)
  ultimately show "\m\{g. simple_function M g \ g \ v}. integral\<^sup>S M n \ integral\<^sup>S M m"
    by force
qed

lemma nn_integral_mono:
  "(\x. x \ space M \ u x \ v x) \ integral\<^sup>N M u \ integral\<^sup>N M v"
  by (auto intro: nn_integral_mono_AE)

lemma mono_nn_integral: "mono F \ mono (\x. integral\<^sup>N M (F x))"
  by (auto simp add: mono_def le_fun_def intro!: nn_integral_mono)

lemma nn_integral_cong_AE:
  "AE x in M. u x = v x \ integral\<^sup>N M u = integral\<^sup>N M v"
  by (auto simp: eq_iff intro!: nn_integral_mono_AE)

lemma nn_integral_cong:
  "(\x. x \ space M \ u x = v x) \ integral\<^sup>N M u = integral\<^sup>N M v"
  by (auto intro: nn_integral_cong_AE)

lemma nn_integral_cong_simp:
  "(\x. x \ space M =simp=> u x = v x) \ integral\<^sup>N M u = integral\<^sup>N M v"
  by (auto intro: nn_integral_cong simp: simp_implies_def)

lemma incseq_nn_integral:
  assumes "incseq f" shows "incseq (\i. integral\<^sup>N M (f i))"
proof -
  have "\i x. f i x \ f (Suc i) x"
    using assms by (auto dest!: incseq_SucD simp: le_fun_def)
  then show ?thesis
    by (auto intro!: incseq_SucI nn_integral_mono)
qed

lemma nn_integral_eq_simple_integral:
  assumes f: "simple_function M f" shows "integral\<^sup>N M f = integral\<^sup>S M f"
proof -
  let ?f = "\x. f x * indicator (space M) x"
  have f': "simple_function M ?f" using f by auto
  have "integral\<^sup>N M ?f \ integral\<^sup>S M ?f" using f'
    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def nn_integral_def)
  moreover have "integral\<^sup>S M ?f \ integral\<^sup>N M ?f"
    unfolding nn_integral_def
    using f' by (auto intro!: SUP_upper)
  ultimately show ?thesis
    by (simp cong: nn_integral_cong simple_integral_cong)
qed

text \<open>Beppo-Levi monotone convergence theorem\<close>
lemma nn_integral_monotone_convergence_SUP:
  assumes f: "incseq f" and [measurable]: "\i. f i \ borel_measurable M"
  shows "(\\<^sup>+ x. (SUP i. f i x) \M) = (SUP i. integral\<^sup>N M (f i))"
proof (rule antisym)
  show "(\\<^sup>+ x. (SUP i. f i x) \M) \ (SUP i. (\\<^sup>+ x. f i x \M))"
    unfolding nn_integral_def_finite[of _ "\x. SUP i. f i x"]
  proof (safe intro!: SUP_least)
    fix u assume sf_u[simp]: "simple_function M u" and
      u: "u \ (\x. SUP i. f i x)" and u_range: "\x. u x < top"
    note sf_u[THEN borel_measurable_simple_function, measurable]
    show "integral\<^sup>S M u \ (SUP j. \\<^sup>+x. f j x \M)"
    proof (rule ennreal_approx_unit)
      fix a :: ennreal assume "a < 1"
      let ?au = "\x. a * u x"

      let ?B = "\c i. {x\space M. ?au x = c \ c \ f i x}"
      have "integral\<^sup>S M ?au = (\c\?au`space M. c * (SUP i. emeasure M (?B c i)))"
        unfolding simple_integral_def
      proof (intro sum.cong ennreal_mult_left_cong refl)
        fix c assume "c \ ?au ` space M" "c \ 0"
        { fix x' assume x': "x' \ space M" "?au x' = c"
          with \<open>c \<noteq> 0\<close> u_range have "?au x' < 1 * u x'"
            by (intro ennreal_mult_strict_right_mono \<open>a < 1\<close>) (auto simp: less_le)
          also have "\ \ (SUP i. f i x')"
            using u by (auto simp: le_fun_def)
          finally have "\i. ?au x' \ f i x'"
            by (auto simp: less_SUP_iff intro: less_imp_le) }
        then have *: "?au -` {c} \ space M = (\i. ?B c i)"
          by auto
        show "emeasure M (?au -` {c} \ space M) = (SUP i. emeasure M (?B c i))"
          unfolding * using f
          by (intro SUP_emeasure_incseq[symmetric])
             (auto simp: incseq_def le_fun_def intro: order_trans)
      qed
      also have "\ = (SUP i. \c\?au`space M. c * emeasure M (?B c i))"
        unfolding SUP_mult_left_ennreal using f
        by (intro ennreal_SUP_sum[symmetric])
           (auto intro!: mult_mono emeasure_mono simp: incseq_def le_fun_def intro: order_trans)
      also have "\ \ (SUP i. integral\<^sup>N M (f i))"
      proof (intro SUP_subset_mono order_refl)
        fix i
        have "(\c\?au`space M. c * emeasure M (?B c i)) =
          (\<integral>\<^sup>Sx. (a * u x) * indicator {x\<in>space M. a * u x \<le> f i x} x \<partial>M)"
          by (subst simple_integral_indicator)
             (auto intro!: sum.cong ennreal_mult_left_cong arg_cong2[where f=emeasure])
        also have "\ = (\\<^sup>+x. (a * u x) * indicator {x\space M. a * u x \ f i x} x \M)"
          by (rule nn_integral_eq_simple_integral[symmetric]) simp
        also have "\ \ (\\<^sup>+x. f i x \M)"
          by (intro nn_integral_mono) (auto split: split_indicator)
        finally show "(\c\?au`space M. c * emeasure M (?B c i)) \ (\\<^sup>+x. f i x \M)" .
      qed
      finally show "a * integral\<^sup>S M u \ (SUP i. integral\<^sup>N M (f i))"
        by simp
    qed
  qed
qed (auto intro!: SUP_least SUP_upper nn_integral_mono)

lemma sup_continuous_nn_integral[order_continuous_intros]:
  assumes f: "\y. sup_continuous (f y)"
  assumes [measurable]: "\x. (\y. f y x) \ borel_measurable M"
  shows "sup_continuous (\x. (\\<^sup>+y. f y x \M))"
  unfolding sup_continuous_def
proof safe
  fix C :: "nat \ 'b" assume C: "incseq C"
  with sup_continuous_mono[OF f] show "(\\<^sup>+ y. f y (Sup (C ` UNIV)) \M) = (SUP i. \\<^sup>+ y. f y (C i) \M)"
    unfolding sup_continuousD[OF f C]
    by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
qed

theorem nn_integral_monotone_convergence_SUP_AE:
  assumes f: "\i. AE x in M. f i x \ f (Suc i) x" "\i. f i \ borel_measurable M"
  shows "(\\<^sup>+ x. (SUP i. f i x) \M) = (SUP i. integral\<^sup>N M (f i))"
proof -
  from f have "AE x in M. \i. f i x \ f (Suc i) x"
    by (simp add: AE_all_countable)
  from this[THEN AE_E] obtain N
    where N: "{x \ space M. \ (\i. f i x \ f (Suc i) x)} \ N" "emeasure M N = 0" "N \ sets M"
    by auto
  let ?f = "\i x. if x \ space M - N then f i x else 0"
  have f_eq: "AE x in M. \i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
  then have "(\\<^sup>+ x. (SUP i. f i x) \M) = (\\<^sup>+ x. (SUP i. ?f i x) \M)"
    by (auto intro!: nn_integral_cong_AE)
  also have "\ = (SUP i. (\\<^sup>+ x. ?f i x \M))"
  proof (rule nn_integral_monotone_convergence_SUP)
    show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
    { fix i show "(\x. if x \ space M - N then f i x else 0) \ borel_measurable M"
        using f N(3) by (intro measurable_If_set) auto }
  qed
  also have "\ = (SUP i. (\\<^sup>+ x. f i x \M))"
    using f_eq by (force intro!: arg_cong[where f = "\f. Sup (range f)"] nn_integral_cong_AE ext)
  finally show ?thesis .
qed

lemma nn_integral_monotone_convergence_simple:
  "incseq f \ (\i. simple_function M (f i)) \ (SUP i. \\<^sup>S x. f i x \M) = (\\<^sup>+x. (SUP i. f i x) \M)"
  using nn_integral_monotone_convergence_SUP[of f M]
  by (simp add: nn_integral_eq_simple_integral[symmetric] borel_measurable_simple_function)

lemma SUP_simple_integral_sequences:
  assumes f: "incseq f" "\i. simple_function M (f i)"
  and g: "incseq g" "\i. simple_function M (g i)"
  and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)"
  shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))"
    (is "Sup (?F ` _) = Sup (?G ` _)")
proof -
  have "(SUP i. integral\<^sup>S M (f i)) = (\\<^sup>+x. (SUP i. f i x) \M)"
    using f by (rule nn_integral_monotone_convergence_simple)
  also have "\ = (\\<^sup>+x. (SUP i. g i x) \M)"
    unfolding eq[THEN nn_integral_cong_AE] ..
  also have "\ = (SUP i. ?G i)"
    using g by (rule nn_integral_monotone_convergence_simple[symmetric])
  finally show ?thesis by simp
qed

lemma nn_integral_const[simp]: "(\\<^sup>+ x. c \M) = c * emeasure M (space M)"
  by (subst nn_integral_eq_simple_integral) auto

lemma nn_integral_linear:
  assumes f: "f \ borel_measurable M" and g: "g \ borel_measurable M"
  shows "(\\<^sup>+ x. a * f x + g x \M) = a * integral\<^sup>N M f + integral\<^sup>N M g"
    (is "integral\<^sup>N M ?L = _")
proof -
  obtain u
    where "\i. simple_function M (u i)" "incseq u" "\i x. u i x < top" "\x. (SUP i. u i x) = f x"
    using borel_measurable_implies_simple_function_sequence' f(1)
    by auto
  note u = nn_integral_monotone_convergence_simple[OF this(2,1)] this

  obtain v where
    "\i. simple_function M (v i)" "incseq v" "\i x. v i x < top" "\x. (SUP i. v i x) = g x"
    using borel_measurable_implies_simple_function_sequence' g(1)
    by auto
  note v = nn_integral_monotone_convergence_simple[OF this(2,1)] this

  let ?L' = "\i x. a * u i x + v i x"

  have "?L \ borel_measurable M" using assms by auto
  from borel_measurable_implies_simple_function_sequence'[OF this]
  obtain l where "\i. simple_function M (l i)" "incseq l" "\i x. l i x < top" "\x. (SUP i. l i x) = a * f x + g x"
    by auto
  note l = nn_integral_monotone_convergence_simple[OF this(2,1)] this

  have inc: "incseq (\i. a * integral\<^sup>S M (u i))" "incseq (\i. integral\<^sup>S M (v i))"
    using u v by (auto simp: incseq_Suc_iff le_fun_def intro!: add_mono mult_left_mono simple_integral_mono)

  have l': "(SUP i. integral\<^sup>S M (l i)) = (SUP i. integral\<^sup>S M (?L' i))"
  proof (rule SUP_simple_integral_sequences[OF l(3,2)])
    show "incseq ?L'" "\i. simple_function M (?L' i)"
      using u v unfolding incseq_Suc_iff le_fun_def
      by (auto intro!: add_mono mult_left_mono)
    { fix x
      have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
        using u(3) v(3) u(4)[of _ x] v(4)[of _ x] unfolding SUP_mult_left_ennreal
        by (auto intro!: ennreal_SUP_add simp: incseq_Suc_iff le_fun_def add_mono mult_left_mono) }
    then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
      unfolding l(5) using u(5) v(5) by (intro AE_I2) auto
  qed
  also have "\ = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))"
    using u(2) v(2) by auto
  finally show ?thesis
    unfolding l(5)[symmetric] l(1)[symmetric]
    by (simp add: ennreal_SUP_add[OF inc] v u SUP_mult_left_ennreal[symmetric])
qed

lemma nn_integral_cmult: "f \ borel_measurable M \ (\\<^sup>+ x. c * f x \M) = c * integral\<^sup>N M f"
  using nn_integral_linear[of f M "\x. 0" c] by simp

lemma nn_integral_multc: "f \ borel_measurable M \ (\\<^sup>+ x. f x * c \M) = integral\<^sup>N M f * c"
  unfolding mult.commute[of _ c] nn_integral_cmult by simp

lemma nn_integral_divide: "f \ borel_measurable M \ (\\<^sup>+ x. f x / c \M) = (\\<^sup>+ x. f x \M) / c"
   unfolding divide_ennreal_def by (rule nn_integral_multc)

lemma nn_integral_indicator[simp]: "A \ sets M \ (\\<^sup>+ x. indicator A x\M) = (emeasure M) A"
  by (subst nn_integral_eq_simple_integral) (auto simp: simple_integral_indicator)

lemma nn_integral_cmult_indicator: "A \ sets M \ (\\<^sup>+ x. c * indicator A x \M) = c * emeasure M A"
  by (subst nn_integral_eq_simple_integral) (auto)

lemma nn_integral_indicator':
  assumes [measurable]: "A \ space M \ sets M"
  shows "(\\<^sup>+ x. indicator A x \M) = emeasure M (A \ space M)"
proof -
  have "(\\<^sup>+ x. indicator A x \M) = (\\<^sup>+ x. indicator (A \ space M) x \M)"
    by (intro nn_integral_cong) (simp split: split_indicator)
  also have "\ = emeasure M (A \ space M)"
    by simp
  finally show ?thesis .
qed

lemma nn_integral_indicator_singleton[simp]:
  assumes [measurable]: "{y} \ sets M" shows "(\\<^sup>+x. f x * indicator {y} x \M) = f y * emeasure M {y}"
proof -
  have "(\\<^sup>+x. f x * indicator {y} x \M) = (\\<^sup>+x. f y * indicator {y} x \M)"
    by (auto intro!: nn_integral_cong split: split_indicator)
  then show ?thesis
    by (simp add: nn_integral_cmult)
qed

lemma nn_integral_set_ennreal:
  "(\\<^sup>+x. ennreal (f x) * indicator A x \M) = (\\<^sup>+x. ennreal (f x * indicator A x) \M)"
  by (rule nn_integral_cong) (simp split: split_indicator)

lemma nn_integral_indicator_singleton'[simp]:
  assumes [measurable]: "{y} \ sets M"
  shows "(\\<^sup>+x. ennreal (f x * indicator {y} x) \M) = f y * emeasure M {y}"
  by (subst nn_integral_set_ennreal[symmetric]) (simp)

lemma nn_integral_add:
  "f \ borel_measurable M \ g \ borel_measurable M \ (\\<^sup>+ x. f x + g x \M) = integral\<^sup>N M f + integral\<^sup>N M g"
  using nn_integral_linear[of f M g 1] by simp

lemma nn_integral_sum:
  "(\i. i \ P \ f i \ borel_measurable M) \ (\\<^sup>+ x. (\i\P. f i x) \M) = (\i\P. integral\<^sup>N M (f i))"
  by (induction P rule: infinite_finite_induct) (auto simp: nn_integral_add)

theorem nn_integral_suminf:
  assumes f: "\i. f i \ borel_measurable M"
  shows "(\\<^sup>+ x. (\i. f i x) \M) = (\i. integral\<^sup>N M (f i))"
proof -
  have all_pos: "AE x in M. \i. 0 \ f i x"
    using assms by (auto simp: AE_all_countable)
  have "(\i. integral\<^sup>N M (f i)) = (SUP n. \iN M (f i))"
    by (rule suminf_eq_SUP)
  also have "\ = (SUP n. \\<^sup>+x. (\iM)"
    unfolding nn_integral_sum[OF f] ..
  also have "\ = \\<^sup>+x. (SUP n. \iM" using f all_pos
    by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
       (elim AE_mp, auto simp: sum_nonneg simp del: sum.lessThan_Suc intro!: AE_I2 sum_mono2)
  also have "\ = \\<^sup>+x. (\i. f i x) \M" using all_pos
    by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP)
  finally show ?thesis by simp
qed

lemma nn_integral_bound_simple_function:
  assumes bnd: "\x. x \ space M \ f x < \"
  assumes f[measurable]: "simple_function M f"
  assumes supp: "emeasure M {x\space M. f x \ 0} < \"
  shows "nn_integral M f < \"
proof cases
  assume "space M = {}"
  then have "nn_integral M f = (\\<^sup>+x. 0 \M)"
    by (intro nn_integral_cong) auto
  then show ?thesis by simp
next
  assume "space M \ {}"
  with simple_functionD(1)[OF f] bnd have bnd: "0 \ Max (f`space M) \ Max (f`space M) < \"
    by (subst Max_less_iff) (auto simp: Max_ge_iff)

  have "nn_integral M f \ (\\<^sup>+x. Max (f`space M) * indicator {x\space M. f x \ 0} x \M)"
  proof (rule nn_integral_mono)
    fix x assume "x \ space M"
    with f show "f x \ Max (f ` space M) * indicator {x \ space M. f x \ 0} x"
      by (auto split: split_indicator intro!: Max_ge simple_functionD)
  qed
  also have "\ < \"
    using bnd supp by (subst nn_integral_cmult) (auto simp: ennreal_mult_less_top)
  finally show ?thesis .
qed

theorem nn_integral_Markov_inequality:
  assumes u: "(\x. u x * indicator A x) \ borel_measurable M" and "A \ sets M"
  shows "(emeasure M) ({x\A. 1 \ c * u x}) \ c * (\\<^sup>+ x. u x * indicator A x \M)"
    (is "(emeasure M) ?A \ _ * ?PI")
proof -
  define u' where "u' = (\<lambda>x. u x * indicator A x)"
  have [measurable]: "u' \ borel_measurable M"
    using u unfolding u'_def .
  have "{x\space M. c * u' x \ 1} \ sets M"
    by measurable
  also have "{x\space M. c * u' x \ 1} = ?A"
    using sets.sets_into_space[OF \<open>A \<in> sets M\<close>] by (auto simp: u'_def indicator_def)
  finally have "(emeasure M) ?A = (\\<^sup>+ x. indicator ?A x \M)"
    using nn_integral_indicator by simp
  also have "\ \ (\\<^sup>+ x. c * (u x * indicator A x) \M)"
    using u by (auto intro!: nn_integral_mono_AE simp: indicator_def)
  also have "\ = c * (\\<^sup>+ x. u x * indicator A x \M)"
    using assms by (auto intro!: nn_integral_cmult)
  finally show ?thesis .
qed

lemma Chernoff_ineq_nn_integral_ge:
  assumes s: "s > 0" and [measurable]: "A \ sets M"
  assumes [measurable]: "(\x. f x * indicator A x) \ borel_measurable M"
  shows   "emeasure M {x\A. f x \ a} \
           ennreal (exp (-s * a)) * nn_integral M (\<lambda>x. ennreal (exp (s * f x)) * indicator A x)"
proof -
  define f' where "f' = (\<lambda>x. f x * indicator A x)"
  have [measurable]: "f' \ borel_measurable M"
    using assms(3) unfolding f'_def by assumption
  have "(\x. ennreal (exp (s * f' x)) * indicator A x) \ borel_measurable M"
    by simp
  also have "(\x. ennreal (exp (s * f' x)) * indicator A x) =
             (\<lambda>x. ennreal (exp (s * f x)) * indicator A x)"
    by (auto simp: f'_def indicator_def fun_eq_iff)
  finally have meas: "\ \ borel_measurable M" .

  have "{x\A. f x \ a} = {x\A. ennreal (exp (-s * a)) * ennreal (exp (s * f x)) \ 1}"
    using s by (auto simp: exp_minus field_simps simp flip: ennreal_mult)
  also have "emeasure M \ \ ennreal (exp (-s * a)) *
               (\<integral>\<^sup>+x. ennreal (exp (s * f x)) * indicator A x \<partial>M)"
    by (intro order.trans[OF nn_integral_Markov_inequality] meas) auto
  finally show ?thesis .
qed

lemma Chernoff_ineq_nn_integral_le:
  assumes s: "s > 0" and [measurable]: "A \ sets M"
  assumes [measurable]: "f \ borel_measurable M"
  shows   "emeasure M {x\A. f x \ a} \
           ennreal (exp (s * a)) * nn_integral M (\<lambda>x. ennreal (exp (-s * f x)) * indicator A x)"
  using Chernoff_ineq_nn_integral_ge[of s A M "\x. -f x" "-a"] assms by simp

lemma nn_integral_noteq_infinite:
  assumes g: "g \ borel_measurable M" and "integral\<^sup>N M g \ \"
  shows "AE x in M. g x \ \"
proof (rule ccontr)
  assume c: "\ (AE x in M. g x \ \)"
  have "(emeasure M) {x\space M. g x = \} \ 0"
    using c g by (auto simp add: AE_iff_null)
  then have "0 < (emeasure M) {x\space M. g x = \}"
    by (auto simp: zero_less_iff_neq_zero)
  then have "\ = \ * (emeasure M) {x\space M. g x = \}"
    by (auto simp: ennreal_top_eq_mult_iff)
  also have "\ \ (\\<^sup>+x. \ * indicator {x\space M. g x = \} x \M)"
    using g by (subst nn_integral_cmult_indicator) auto
  also have "\ \ integral\<^sup>N M g"
    using assms by (auto intro!: nn_integral_mono_AE simp: indicator_def)
  finally show False
    using \<open>integral\<^sup>N M g \<noteq> \<infinity>\<close> by (auto simp: top_unique)
qed

lemma nn_integral_PInf:
  assumes f: "f \ borel_measurable M" and not_Inf: "integral\<^sup>N M f \ \"
  shows "emeasure M (f -` {\} \ space M) = 0"
proof -
  have "\ * emeasure M (f -` {\} \ space M) = (\\<^sup>+ x. \ * indicator (f -` {\} \ space M) x \M)"
    using f by (subst nn_integral_cmult_indicator) (auto simp: measurable_sets)
  also have "\ \ integral\<^sup>N M f"
    by (auto intro!: nn_integral_mono simp: indicator_def)
  finally have "\ * (emeasure M) (f -` {\} \ space M) \ integral\<^sup>N M f"
    by simp
  then show ?thesis
    using assms by (auto simp: ennreal_top_mult top_unique split: if_split_asm)
qed

lemma simple_integral_PInf:
  "simple_function M f \ integral\<^sup>S M f \ \ \ emeasure M (f -` {\} \ space M) = 0"
  by (rule nn_integral_PInf) (auto simp: nn_integral_eq_simple_integral borel_measurable_simple_function)

lemma nn_integral_PInf_AE:
  assumes "f \ borel_measurable M" "integral\<^sup>N M f \ \" shows "AE x in M. f x \ \"
proof (rule AE_I)
  show "(emeasure M) (f -` {\} \ space M) = 0"
    by (rule nn_integral_PInf[OF assms])
  show "f -` {\} \ space M \ sets M"
    using assms by (auto intro: borel_measurable_vimage)
qed auto

lemma nn_integral_diff:
  assumes f: "f \ borel_measurable M"
  and g: "g \ borel_measurable M"
  and fin: "integral\<^sup>N M g \ \"
  and mono: "AE x in M. g x \ f x"
  shows "(\\<^sup>+ x. f x - g x \M) = integral\<^sup>N M f - integral\<^sup>N M g"
proof -
  have diff: "(\x. f x - g x) \ borel_measurable M"
    using assms by auto
  have "AE x in M. f x = f x - g x + g x"
    using diff_add_cancel_ennreal mono nn_integral_noteq_infinite[OF g fin] assms by auto
  then have **: "integral\<^sup>N M f = (\\<^sup>+x. f x - g x \M) + integral\<^sup>N M g"
    unfolding nn_integral_add[OF diff g, symmetric]
    by (rule nn_integral_cong_AE)
  show ?thesis unfolding **
    using fin
    by (cases rule: ennreal2_cases[of "\\<^sup>+ x. f x - g x \M" "integral\<^sup>N M g"]) auto
qed

lemma nn_integral_mult_bounded_inf:
  assumes f: "f \ borel_measurable M" "(\\<^sup>+x. f x \M) < \" and c: "c \ \" and ae: "AE x in M. g x \ c * f x"
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.18Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.