src/HOL/Probability/Lebesgue_Integration.thy
author hoelzl
Tue Mar 22 18:53:05 2011 +0100 (2011-03-22)
changeset 42066 6db76c88907a
parent 41981 cdf7693bbe08
child 42067 66c8281349ec
permissions -rw-r--r--
generalized Caratheodory from algebra to ring_of_sets
     1 (* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
     2 
     3 header {*Lebesgue Integration*}
     4 
     5 theory Lebesgue_Integration
     6 imports Measure Borel_Space
     7 begin
     8 
     9 lemma extreal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::extreal)"
    10   unfolding indicator_def by auto
    11 
    12 lemma tendsto_real_max:
    13   fixes x y :: real
    14   assumes "(X ---> x) net"
    15   assumes "(Y ---> y) net"
    16   shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
    17 proof -
    18   have *: "\<And>x y :: real. max x y = y + ((x - y) + norm (x - y)) / 2"
    19     by (auto split: split_max simp: field_simps)
    20   show ?thesis
    21     unfolding *
    22     by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto
    23 qed
    24 
    25 lemma (in measure_space) measure_Union:
    26   assumes "finite S" "S \<subseteq> sets M" "\<And>A B. A \<in> S \<Longrightarrow> B \<in> S \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}"
    27   shows "setsum \<mu> S = \<mu> (\<Union>S)"
    28 proof -
    29   have "setsum \<mu> S = \<mu> (\<Union>i\<in>S. i)"
    30     using assms by (intro measure_setsum[OF `finite S`]) (auto simp: disjoint_family_on_def)
    31   also have "\<dots> = \<mu> (\<Union>S)" by (auto intro!: arg_cong[where f=\<mu>])
    32   finally show ?thesis .
    33 qed
    34 
    35 lemma (in sigma_algebra) measurable_sets2[intro]:
    36   assumes "f \<in> measurable M M'" "g \<in> measurable M M''"
    37   and "A \<in> sets M'" "B \<in> sets M''"
    38   shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
    39 proof -
    40   have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
    41     by auto
    42   then show ?thesis using assms by (auto intro: measurable_sets)
    43 qed
    44 
    45 lemma incseq_extreal: "incseq f \<Longrightarrow> incseq (\<lambda>x. extreal (f x))"
    46   unfolding incseq_def by auto
    47 
    48 lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
    49 proof
    50   assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
    51 qed (auto simp: incseq_def)
    52 
    53 lemma borel_measurable_real_floor:
    54   "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
    55   unfolding borel.borel_measurable_iff_ge
    56 proof (intro allI)
    57   fix a :: real
    58   { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
    59       using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
    60       unfolding real_eq_of_int by simp }
    61   then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
    62   then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
    63 qed
    64 
    65 lemma measure_preservingD2:
    66   "f \<in> measure_preserving A B \<Longrightarrow> f \<in> measurable A B"
    67   unfolding measure_preserving_def by auto
    68 
    69 lemma measure_preservingD3:
    70   "f \<in> measure_preserving A B \<Longrightarrow> f \<in> space A \<rightarrow> space B"
    71   unfolding measure_preserving_def measurable_def by auto
    72 
    73 lemma measure_preservingD:
    74   "T \<in> measure_preserving A B \<Longrightarrow> X \<in> sets B \<Longrightarrow> measure A (T -` X \<inter> space A) = measure B X"
    75   unfolding measure_preserving_def by auto
    76 
    77 lemma (in sigma_algebra) borel_measurable_real_natfloor[intro, simp]:
    78   assumes "f \<in> borel_measurable M"
    79   shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
    80 proof -
    81   have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
    82     by (auto simp: max_def natfloor_def)
    83   with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
    84   show ?thesis by (simp add: comp_def)
    85 qed
    86 
    87 lemma (in measure_space) AE_not_in:
    88   assumes N: "N \<in> null_sets" shows "AE x. x \<notin> N"
    89   using N by (rule AE_I') auto
    90 
    91 lemma sums_If_finite:
    92   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    93   assumes finite: "finite {r. P r}"
    94   shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")
    95 proof cases
    96   assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto
    97   thus ?thesis by (simp add: sums_zero)
    98 next
    99   assume not_empty: "{r. P r} \<noteq> {}"
   100   have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"
   101     by (rule series_zero)
   102        (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])
   103   also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"
   104     by (subst setsum_cases)
   105        (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)
   106   finally show ?thesis .
   107 qed
   108 
   109 lemma sums_single:
   110   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   111   shows "(\<lambda>r. if r = i then f r else 0) sums f i"
   112   using sums_If_finite[of "\<lambda>r. r = i" f] by simp
   113 
   114 section "Simple function"
   115 
   116 text {*
   117 
   118 Our simple functions are not restricted to positive real numbers. Instead
   119 they are just functions with a finite range and are measurable when singleton
   120 sets are measurable.
   121 
   122 *}
   123 
   124 definition "simple_function M g \<longleftrightarrow>
   125     finite (g ` space M) \<and>
   126     (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"
   127 
   128 lemma (in sigma_algebra) simple_functionD:
   129   assumes "simple_function M g"
   130   shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M"
   131 proof -
   132   show "finite (g ` space M)"
   133     using assms unfolding simple_function_def by auto
   134   have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
   135   also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
   136   finally show "g -` X \<inter> space M \<in> sets M" using assms
   137     by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def)
   138 qed
   139 
   140 lemma (in sigma_algebra) simple_function_measurable2[intro]:
   141   assumes "simple_function M f" "simple_function M g"
   142   shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
   143 proof -
   144   have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
   145     by auto
   146   then show ?thesis using assms[THEN simple_functionD(2)] by auto
   147 qed
   148 
   149 lemma (in sigma_algebra) simple_function_indicator_representation:
   150   fixes f ::"'a \<Rightarrow> extreal"
   151   assumes f: "simple_function M f" and x: "x \<in> space M"
   152   shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
   153   (is "?l = ?r")
   154 proof -
   155   have "?r = (\<Sum>y \<in> f ` space M.
   156     (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
   157     by (auto intro!: setsum_cong2)
   158   also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
   159     using assms by (auto dest: simple_functionD simp: setsum_delta)
   160   also have "... = f x" using x by (auto simp: indicator_def)
   161   finally show ?thesis by auto
   162 qed
   163 
   164 lemma (in measure_space) simple_function_notspace:
   165   "simple_function M (\<lambda>x. h x * indicator (- space M) x::extreal)" (is "simple_function M ?h")
   166 proof -
   167   have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto
   168   hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
   169   have "?h -` {0} \<inter> space M = space M" by auto
   170   thus ?thesis unfolding simple_function_def by auto
   171 qed
   172 
   173 lemma (in sigma_algebra) simple_function_cong:
   174   assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
   175   shows "simple_function M f \<longleftrightarrow> simple_function M g"
   176 proof -
   177   have "f ` space M = g ` space M"
   178     "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
   179     using assms by (auto intro!: image_eqI)
   180   thus ?thesis unfolding simple_function_def using assms by simp
   181 qed
   182 
   183 lemma (in sigma_algebra) simple_function_cong_algebra:
   184   assumes "sets N = sets M" "space N = space M"
   185   shows "simple_function M f \<longleftrightarrow> simple_function N f"
   186   unfolding simple_function_def assms ..
   187 
   188 lemma (in sigma_algebra) borel_measurable_simple_function:
   189   assumes "simple_function M f"
   190   shows "f \<in> borel_measurable M"
   191 proof (rule borel_measurableI)
   192   fix S
   193   let ?I = "f ` (f -` S \<inter> space M)"
   194   have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto
   195   have "finite ?I"
   196     using assms unfolding simple_function_def
   197     using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
   198   hence "?U \<in> sets M"
   199     apply (rule finite_UN)
   200     using assms unfolding simple_function_def by auto
   201   thus "f -` S \<inter> space M \<in> sets M" unfolding * .
   202 qed
   203 
   204 lemma (in sigma_algebra) simple_function_borel_measurable:
   205   fixes f :: "'a \<Rightarrow> 'x::{t2_space}"
   206   assumes "f \<in> borel_measurable M" and "finite (f ` space M)"
   207   shows "simple_function M f"
   208   using assms unfolding simple_function_def
   209   by (auto intro: borel_measurable_vimage)
   210 
   211 lemma (in sigma_algebra) simple_function_eq_borel_measurable:
   212   fixes f :: "'a \<Rightarrow> extreal"
   213   shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M"
   214   using simple_function_borel_measurable[of f]
   215     borel_measurable_simple_function[of f]
   216   by (fastsimp simp: simple_function_def)
   217 
   218 lemma (in sigma_algebra) simple_function_const[intro, simp]:
   219   "simple_function M (\<lambda>x. c)"
   220   by (auto intro: finite_subset simp: simple_function_def)
   221 lemma (in sigma_algebra) simple_function_compose[intro, simp]:
   222   assumes "simple_function M f"
   223   shows "simple_function M (g \<circ> f)"
   224   unfolding simple_function_def
   225 proof safe
   226   show "finite ((g \<circ> f) ` space M)"
   227     using assms unfolding simple_function_def by (auto simp: image_compose)
   228 next
   229   fix x assume "x \<in> space M"
   230   let ?G = "g -` {g (f x)} \<inter> (f`space M)"
   231   have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M =
   232     (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
   233   show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
   234     using assms unfolding simple_function_def *
   235     by (rule_tac finite_UN) (auto intro!: finite_UN)
   236 qed
   237 
   238 lemma (in sigma_algebra) simple_function_indicator[intro, simp]:
   239   assumes "A \<in> sets M"
   240   shows "simple_function M (indicator A)"
   241 proof -
   242   have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")
   243     by (auto simp: indicator_def)
   244   hence "finite ?S" by (rule finite_subset) simp
   245   moreover have "- A \<inter> space M = space M - A" by auto
   246   ultimately show ?thesis unfolding simple_function_def
   247     using assms by (auto simp: indicator_def_raw)
   248 qed
   249 
   250 lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
   251   assumes "simple_function M f"
   252   assumes "simple_function M g"
   253   shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p")
   254   unfolding simple_function_def
   255 proof safe
   256   show "finite (?p ` space M)"
   257     using assms unfolding simple_function_def
   258     by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto
   259 next
   260   fix x assume "x \<in> space M"
   261   have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M =
   262       (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"
   263     by auto
   264   with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M"
   265     using assms unfolding simple_function_def by auto
   266 qed
   267 
   268 lemma (in sigma_algebra) simple_function_compose1:
   269   assumes "simple_function M f"
   270   shows "simple_function M (\<lambda>x. g (f x))"
   271   using simple_function_compose[OF assms, of g]
   272   by (simp add: comp_def)
   273 
   274 lemma (in sigma_algebra) simple_function_compose2:
   275   assumes "simple_function M f" and "simple_function M g"
   276   shows "simple_function M (\<lambda>x. h (f x) (g x))"
   277 proof -
   278   have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"
   279     using assms by auto
   280   thus ?thesis by (simp_all add: comp_def)
   281 qed
   282 
   283 lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]
   284   and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]
   285   and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
   286   and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]
   287   and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]
   288   and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
   289   and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
   290 
   291 lemma (in sigma_algebra) simple_function_setsum[intro, simp]:
   292   assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"
   293   shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)"
   294 proof cases
   295   assume "finite P" from this assms show ?thesis by induct auto
   296 qed auto
   297 
   298 lemma (in sigma_algebra)
   299   fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"
   300   shows simple_function_extreal[intro, simp]: "simple_function M (\<lambda>x. extreal (f x))"
   301   by (auto intro!: simple_function_compose1[OF sf])
   302 
   303 lemma (in sigma_algebra)
   304   fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
   305   shows simple_function_real_of_nat[intro, simp]: "simple_function M (\<lambda>x. real (f x))"
   306   by (auto intro!: simple_function_compose1[OF sf])
   307 
   308 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
   309   fixes u :: "'a \<Rightarrow> extreal"
   310   assumes u: "u \<in> borel_measurable M"
   311   shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
   312              (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
   313 proof -
   314   def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)"
   315   { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
   316     proof (split split_if, intro conjI impI)
   317       assume "\<not> real j \<le> u x"
   318       then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
   319          by (cases "u x") (auto intro!: natfloor_mono simp: mult_nonneg_nonneg)
   320       moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
   321         by (intro real_natfloor_le) (auto simp: mult_nonneg_nonneg)
   322       ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
   323         unfolding real_of_nat_le_iff by auto
   324     qed auto }
   325   note f_upper = this
   326 
   327   have real_f:
   328     "\<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)))"
   329     unfolding f_def by auto
   330 
   331   let "?g j x" = "real (f x j) / 2^j :: extreal"
   332   show ?thesis
   333   proof (intro exI[of _ ?g] conjI allI ballI)
   334     fix i
   335     have "simple_function M (\<lambda>x. real (f x i))"
   336     proof (intro simple_function_borel_measurable)
   337       show "(\<lambda>x. real (f x i)) \<in> borel_measurable M"
   338         using u by (auto intro!: measurable_If simp: real_f)
   339       have "(\<lambda>x. real (f x i))`space M \<subseteq> real`{..i*2^i}"
   340         using f_upper[of _ i] by auto
   341       then show "finite ((\<lambda>x. real (f x i))`space M)"
   342         by (rule finite_subset) auto
   343     qed
   344     then show "simple_function M (?g i)"
   345       by (auto intro: simple_function_extreal simple_function_div)
   346   next
   347     show "incseq ?g"
   348     proof (intro incseq_extreal incseq_SucI le_funI)
   349       fix x and i :: nat
   350       have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
   351       proof ((split split_if)+, intro conjI impI)
   352         assume "extreal (real i) \<le> u x" "\<not> extreal (real (Suc i)) \<le> u x"
   353         then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)"
   354           by (cases "u x") (auto intro!: le_natfloor)
   355       next
   356         assume "\<not> extreal (real i) \<le> u x" "extreal (real (Suc i)) \<le> u x"
   357         then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i"
   358           by (cases "u x") auto
   359       next
   360         assume "\<not> extreal (real i) \<le> u x" "\<not> extreal (real (Suc i)) \<le> u x"
   361         have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2"
   362           by simp
   363         also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
   364         proof cases
   365           assume "0 \<le> u x" then show ?thesis
   366             by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg)
   367         next
   368           assume "\<not> 0 \<le> u x" then show ?thesis
   369             by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)
   370         qed
   371         also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)"
   372           by (simp add: ac_simps)
   373         finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" .
   374       qed simp
   375       then show "?g i x \<le> ?g (Suc i) x"
   376         by (auto simp: field_simps)
   377     qed
   378   next
   379     fix x show "(SUP i. ?g i x) = max 0 (u x)"
   380     proof (rule extreal_SUPI)
   381       fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
   382         by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
   383                                      mult_nonpos_nonneg mult_nonneg_nonneg)
   384     next
   385       fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
   386       have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
   387       from order_trans[OF this *] have "0 \<le> y" by simp
   388       show "max 0 (u x) \<le> y"
   389       proof (cases y)
   390         case (real r)
   391         with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
   392         from real_arch_lt[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
   393         then have "\<exists>p. max 0 (u x) = extreal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
   394         then guess p .. note ux = this
   395         obtain m :: nat where m: "p < real m" using real_arch_lt ..
   396         have "p \<le> r"
   397         proof (rule ccontr)
   398           assume "\<not> p \<le> r"
   399           with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"]
   400           obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: inverse_eq_divide field_simps)
   401           then have "r * 2^max N m < p * 2^max N m - 1" by simp
   402           moreover
   403           have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
   404             using *[of "max N m"] m unfolding real_f using ux
   405             by (cases "0 \<le> u x") (simp_all add: max_def mult_nonneg_nonneg split: split_if_asm)
   406           then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
   407             by (metis real_natfloor_gt_diff_one less_le_trans)
   408           ultimately show False by auto
   409         qed
   410         then show "max 0 (u x) \<le> y" using real ux by simp
   411       qed (insert `0 \<le> y`, auto)
   412     qed
   413   qed (auto simp: divide_nonneg_pos)
   414 qed
   415 
   416 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence':
   417   fixes u :: "'a \<Rightarrow> extreal"
   418   assumes u: "u \<in> borel_measurable M"
   419   obtains f where "\<And>i. simple_function M (f i)" "incseq f" "\<And>i. \<infinity> \<notin> range (f i)"
   420     "\<And>x. (SUP i. f i x) = max 0 (u x)" "\<And>i x. 0 \<le> f i x"
   421   using borel_measurable_implies_simple_function_sequence[OF u] by auto
   422 
   423 lemma (in sigma_algebra) simple_function_If_set:
   424   assumes sf: "simple_function M f" "simple_function M g" and A: "A \<inter> space M \<in> sets M"
   425   shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF")
   426 proof -
   427   def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
   428   show ?thesis unfolding simple_function_def
   429   proof safe
   430     have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
   431     from finite_subset[OF this] assms
   432     show "finite (?IF ` space M)" unfolding simple_function_def by auto
   433   next
   434     fix x assume "x \<in> space M"
   435     then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
   436       then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
   437       else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
   438       using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
   439     have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
   440       unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
   441     show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
   442   qed
   443 qed
   444 
   445 lemma (in sigma_algebra) simple_function_If:
   446   assumes sf: "simple_function M f" "simple_function M g" and P: "{x\<in>space M. P x} \<in> sets M"
   447   shows "simple_function M (\<lambda>x. if P x then f x else g x)"
   448 proof -
   449   have "{x\<in>space M. P x} = {x. P x} \<inter> space M" by auto
   450   with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp
   451 qed
   452 
   453 lemma (in measure_space) simple_function_restricted:
   454   fixes f :: "'a \<Rightarrow> extreal" assumes "A \<in> sets M"
   455   shows "simple_function (restricted_space A) f \<longleftrightarrow> simple_function M (\<lambda>x. f x * indicator A x)"
   456     (is "simple_function ?R f \<longleftrightarrow> simple_function M ?f")
   457 proof -
   458   interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
   459   have f: "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
   460   proof cases
   461     assume "A = space M"
   462     then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
   463     then show ?thesis by simp
   464   next
   465     assume "A \<noteq> space M"
   466     then obtain x where x: "x \<in> space M" "x \<notin> A"
   467       using sets_into_space `A \<in> sets M` by auto
   468     have *: "?f`space M = f`A \<union> {0}"
   469     proof (auto simp add: image_iff)
   470       show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0"
   471         using x by (auto intro!: bexI[of _ x])
   472     next
   473       fix x assume "x \<in> A"
   474       then show "\<exists>y\<in>space M. f x = f y * indicator A y"
   475         using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x])
   476     next
   477       fix x
   478       assume "indicator A x \<noteq> (0::extreal)"
   479       then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm)
   480       moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y"
   481       ultimately show "f x = 0" by auto
   482     qed
   483     then show ?thesis by auto
   484   qed
   485   then show ?thesis
   486     unfolding simple_function_eq_borel_measurable
   487       R.simple_function_eq_borel_measurable
   488     unfolding borel_measurable_restricted[OF `A \<in> sets M`]
   489     using assms(1)[THEN sets_into_space]
   490     by (auto simp: indicator_def)
   491 qed
   492 
   493 lemma (in sigma_algebra) simple_function_subalgebra:
   494   assumes "simple_function N f"
   495   and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M"
   496   shows "simple_function M f"
   497   using assms unfolding simple_function_def by auto
   498 
   499 lemma (in measure_space) simple_function_vimage:
   500   assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
   501     and f: "simple_function M' f"
   502   shows "simple_function M (\<lambda>x. f (T x))"
   503 proof (intro simple_function_def[THEN iffD2] conjI ballI)
   504   interpret T: sigma_algebra M' by fact
   505   have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
   506     using T unfolding measurable_def by auto
   507   then show "finite ((\<lambda>x. f (T x)) ` space M)"
   508     using f unfolding simple_function_def by (auto intro: finite_subset)
   509   fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
   510   then have "i \<in> f ` space M'"
   511     using T unfolding measurable_def by auto
   512   then have "f -` {i} \<inter> space M' \<in> sets M'"
   513     using f unfolding simple_function_def by auto
   514   then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
   515     using T unfolding measurable_def by auto
   516   also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
   517     using T unfolding measurable_def by auto
   518   finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
   519 qed
   520 
   521 section "Simple integral"
   522 
   523 definition simple_integral_def:
   524   "integral\<^isup>S M f = (\<Sum>x \<in> f ` space M. x * measure M (f -` {x} \<inter> space M))"
   525 
   526 syntax
   527   "_simple_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> extreal) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> extreal" ("\<integral>\<^isup>S _. _ \<partial>_" [60,61] 110)
   528 
   529 translations
   530   "\<integral>\<^isup>S x. f \<partial>M" == "CONST integral\<^isup>S M (%x. f)"
   531 
   532 lemma (in measure_space) simple_integral_cong:
   533   assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
   534   shows "integral\<^isup>S M f = integral\<^isup>S M g"
   535 proof -
   536   have "f ` space M = g ` space M"
   537     "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
   538     using assms by (auto intro!: image_eqI)
   539   thus ?thesis unfolding simple_integral_def by simp
   540 qed
   541 
   542 lemma (in measure_space) simple_integral_cong_measure:
   543   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
   544     and "simple_function M f"
   545   shows "integral\<^isup>S N f = integral\<^isup>S M f"
   546 proof -
   547   interpret v: measure_space N
   548     by (rule measure_space_cong) fact+
   549   from simple_functionD[OF `simple_function M f`] assms show ?thesis
   550     by (auto intro!: setsum_cong simp: simple_integral_def)
   551 qed
   552 
   553 lemma (in measure_space) simple_integral_const[simp]:
   554   "(\<integral>\<^isup>Sx. c \<partial>M) = c * \<mu> (space M)"
   555 proof (cases "space M = {}")
   556   case True thus ?thesis unfolding simple_integral_def by simp
   557 next
   558   case False hence "(\<lambda>x. c) ` space M = {c}" by auto
   559   thus ?thesis unfolding simple_integral_def by simp
   560 qed
   561 
   562 lemma (in measure_space) simple_function_partition:
   563   assumes f: "simple_function M f" and g: "simple_function M g"
   564   shows "integral\<^isup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
   565     (is "_ = setsum _ (?p ` space M)")
   566 proof-
   567   let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
   568   let ?SIGMA = "Sigma (f`space M) ?sub"
   569 
   570   have [intro]:
   571     "finite (f ` space M)"
   572     "finite (g ` space M)"
   573     using assms unfolding simple_function_def by simp_all
   574 
   575   { fix A
   576     have "?p ` (A \<inter> space M) \<subseteq>
   577       (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
   578       by auto
   579     hence "finite (?p ` (A \<inter> space M))"
   580       by (rule finite_subset) auto }
   581   note this[intro, simp]
   582   note sets = simple_function_measurable2[OF f g]
   583 
   584   { fix x assume "x \<in> space M"
   585     have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
   586     with sets have "\<mu> (f -` {f x} \<inter> space M) = setsum \<mu> (?sub (f x))"
   587       by (subst measure_Union) auto }
   588   hence "integral\<^isup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)"
   589     unfolding simple_integral_def using f sets
   590     by (subst setsum_Sigma[symmetric])
   591        (auto intro!: setsum_cong setsum_extreal_right_distrib)
   592   also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)"
   593   proof -
   594     have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
   595     have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
   596       = (\<lambda>x. (f x, ?p x)) ` space M"
   597     proof safe
   598       fix x assume "x \<in> space M"
   599       thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
   600         by (auto intro!: image_eqI[of _ _ "?p x"])
   601     qed auto
   602     thus ?thesis
   603       apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
   604       apply (rule_tac x="xa" in image_eqI)
   605       by simp_all
   606   qed
   607   finally show ?thesis .
   608 qed
   609 
   610 lemma (in measure_space) simple_integral_add[simp]:
   611   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"
   612   shows "(\<integral>\<^isup>Sx. f x + g x \<partial>M) = integral\<^isup>S M f + integral\<^isup>S M g"
   613 proof -
   614   { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
   615     assume "x \<in> space M"
   616     hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}"
   617         "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S"
   618       by auto }
   619   with assms show ?thesis
   620     unfolding
   621       simple_function_partition[OF simple_function_add[OF f g] simple_function_Pair[OF f g]]
   622       simple_function_partition[OF f g]
   623       simple_function_partition[OF g f]
   624     by (subst (3) Int_commute)
   625        (auto simp add: extreal_left_distrib setsum_addf[symmetric] intro!: setsum_cong)
   626 qed
   627 
   628 lemma (in measure_space) simple_integral_setsum[simp]:
   629   assumes "\<And>i x. i \<in> P \<Longrightarrow> 0 \<le> f i x"
   630   assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"
   631   shows "(\<integral>\<^isup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>S M (f i))"
   632 proof cases
   633   assume "finite P"
   634   from this assms show ?thesis
   635     by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg)
   636 qed auto
   637 
   638 lemma (in measure_space) simple_integral_mult[simp]:
   639   assumes f: "simple_function M f" "\<And>x. 0 \<le> f x"
   640   shows "(\<integral>\<^isup>Sx. c * f x \<partial>M) = c * integral\<^isup>S M f"
   641 proof -
   642   note mult = simple_function_mult[OF simple_function_const[of c] f(1)]
   643   { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
   644     assume "x \<in> space M"
   645     hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"
   646       by auto }
   647   with assms show ?thesis
   648     unfolding simple_function_partition[OF mult f(1)]
   649               simple_function_partition[OF f(1) mult]
   650     by (subst setsum_extreal_right_distrib)
   651        (auto intro!: extreal_0_le_mult setsum_cong simp: mult_assoc)
   652 qed
   653 
   654 lemma (in measure_space) simple_integral_mono_AE:
   655   assumes f: "simple_function M f" and g: "simple_function M g"
   656   and mono: "AE x. f x \<le> g x"
   657   shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
   658 proof -
   659   let "?S x" = "(g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
   660   have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x"
   661     "\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto
   662   show ?thesis
   663     unfolding *
   664       simple_function_partition[OF f g]
   665       simple_function_partition[OF g f]
   666   proof (safe intro!: setsum_mono)
   667     fix x assume "x \<in> space M"
   668     then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto
   669     show "the_elem (f`?S x) * \<mu> (?S x) \<le> the_elem (g`?S x) * \<mu> (?S x)"
   670     proof (cases "f x \<le> g x")
   671       case True then show ?thesis
   672         using * assms(1,2)[THEN simple_functionD(2)]
   673         by (auto intro!: extreal_mult_right_mono)
   674     next
   675       case False
   676       obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "\<mu> N = 0"
   677         using mono by (auto elim!: AE_E)
   678       have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
   679       moreover have "?S x \<in> sets M" using assms
   680         by (rule_tac Int) (auto intro!: simple_functionD)
   681       ultimately have "\<mu> (?S x) \<le> \<mu> N"
   682         using `N \<in> sets M` by (auto intro!: measure_mono)
   683       moreover have "0 \<le> \<mu> (?S x)"
   684         using assms(1,2)[THEN simple_functionD(2)] by auto
   685       ultimately have "\<mu> (?S x) = 0" using `\<mu> N = 0` by auto
   686       then show ?thesis by simp
   687     qed
   688   qed
   689 qed
   690 
   691 lemma (in measure_space) simple_integral_mono:
   692   assumes "simple_function M f" and "simple_function M g"
   693   and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
   694   shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
   695   using assms by (intro simple_integral_mono_AE) auto
   696 
   697 lemma (in measure_space) simple_integral_cong_AE:
   698   assumes "simple_function M f" and "simple_function M g"
   699   and "AE x. f x = g x"
   700   shows "integral\<^isup>S M f = integral\<^isup>S M g"
   701   using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE)
   702 
   703 lemma (in measure_space) simple_integral_cong':
   704   assumes sf: "simple_function M f" "simple_function M g"
   705   and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"
   706   shows "integral\<^isup>S M f = integral\<^isup>S M g"
   707 proof (intro simple_integral_cong_AE sf AE_I)
   708   show "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" by fact
   709   show "{x \<in> space M. f x \<noteq> g x} \<in> sets M"
   710     using sf[THEN borel_measurable_simple_function] by auto
   711 qed simp
   712 
   713 lemma (in measure_space) simple_integral_indicator:
   714   assumes "A \<in> sets M"
   715   assumes "simple_function M f"
   716   shows "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) =
   717     (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
   718 proof cases
   719   assume "A = space M"
   720   moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = integral\<^isup>S M f"
   721     by (auto intro!: simple_integral_cong)
   722   moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
   723   ultimately show ?thesis by (simp add: simple_integral_def)
   724 next
   725   assume "A \<noteq> space M"
   726   then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
   727   have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
   728   proof safe
   729     fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
   730   next
   731     fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
   732       using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
   733   next
   734     show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
   735   qed
   736   have *: "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) =
   737     (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
   738     unfolding simple_integral_def I
   739   proof (rule setsum_mono_zero_cong_left)
   740     show "finite (f ` space M \<union> {0})"
   741       using assms(2) unfolding simple_function_def by auto
   742     show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
   743       using sets_into_space[OF assms(1)] by auto
   744     have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
   745       by (auto simp: image_iff)
   746     thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
   747       i * \<mu> (f -` {i} \<inter> space M \<inter> A) = 0" by auto
   748   next
   749     fix x assume "x \<in> f`A \<union> {0}"
   750     hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A"
   751       by (auto simp: indicator_def split: split_if_asm)
   752     thus "x * \<mu> (?I -` {x} \<inter> space M) =
   753       x * \<mu> (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all
   754   qed
   755   show ?thesis unfolding *
   756     using assms(2) unfolding simple_function_def
   757     by (auto intro!: setsum_mono_zero_cong_right)
   758 qed
   759 
   760 lemma (in measure_space) simple_integral_indicator_only[simp]:
   761   assumes "A \<in> sets M"
   762   shows "integral\<^isup>S M (indicator A) = \<mu> A"
   763 proof cases
   764   assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
   765   thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
   766 next
   767   assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::extreal}" by auto
   768   thus ?thesis
   769     using simple_integral_indicator[OF assms simple_function_const[of 1]]
   770     using sets_into_space[OF assms]
   771     by (auto intro!: arg_cong[where f="\<mu>"])
   772 qed
   773 
   774 lemma (in measure_space) simple_integral_null_set:
   775   assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets"
   776   shows "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = 0"
   777 proof -
   778   have "AE x. indicator N x = (0 :: extreal)"
   779     using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
   780   then have "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^isup>Sx. 0 \<partial>M)"
   781     using assms apply (intro simple_integral_cong_AE) by auto
   782   then show ?thesis by simp
   783 qed
   784 
   785 lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
   786   assumes sf: "simple_function M f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
   787   shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)"
   788   using assms by (intro simple_integral_cong_AE) auto
   789 
   790 lemma (in measure_space) simple_integral_restricted:
   791   assumes "A \<in> sets M"
   792   assumes sf: "simple_function M (\<lambda>x. f x * indicator A x)"
   793   shows "integral\<^isup>S (restricted_space A) f = (\<integral>\<^isup>Sx. f x * indicator A x \<partial>M)"
   794     (is "_ = integral\<^isup>S M ?f")
   795   unfolding simple_integral_def
   796 proof (simp, safe intro!: setsum_mono_zero_cong_left)
   797   from sf show "finite (?f ` space M)"
   798     unfolding simple_function_def by auto
   799 next
   800   fix x assume "x \<in> A"
   801   then show "f x \<in> ?f ` space M"
   802     using sets_into_space `A \<in> sets M` by (auto intro!: image_eqI[of _ _ x])
   803 next
   804   fix x assume "x \<in> space M" "?f x \<notin> f`A"
   805   then have "x \<notin> A" by (auto simp: image_iff)
   806   then show "?f x * \<mu> (?f -` {?f x} \<inter> space M) = 0" by simp
   807 next
   808   fix x assume "x \<in> A"
   809   then have "f x \<noteq> 0 \<Longrightarrow>
   810     f -` {f x} \<inter> A = ?f -` {f x} \<inter> space M"
   811     using `A \<in> sets M` sets_into_space
   812     by (auto simp: indicator_def split: split_if_asm)
   813   then show "f x * \<mu> (f -` {f x} \<inter> A) =
   814     f x * \<mu> (?f -` {f x} \<inter> space M)"
   815     unfolding extreal_mult_cancel_left by auto
   816 qed
   817 
   818 lemma (in measure_space) simple_integral_subalgebra:
   819   assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M"
   820   shows "integral\<^isup>S N = integral\<^isup>S M"
   821   unfolding simple_integral_def_raw by simp
   822 
   823 lemma (in measure_space) simple_integral_vimage:
   824   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
   825     and f: "simple_function M' f"
   826   shows "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
   827 proof -
   828   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
   829   show "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
   830     unfolding simple_integral_def
   831   proof (intro setsum_mono_zero_cong_right ballI)
   832     show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
   833       using T unfolding measurable_def measure_preserving_def by auto
   834     show "finite (f ` space M')"
   835       using f unfolding simple_function_def by auto
   836   next
   837     fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
   838     then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
   839     with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
   840     show "i * T.\<mu> (f -` {i} \<inter> space M') = 0" by simp
   841   next
   842     fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
   843     then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
   844       using T unfolding measurable_def measure_preserving_def by auto
   845     with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
   846     show "i * T.\<mu> (f -` {i} \<inter> space M') = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
   847       by auto
   848   qed
   849 qed
   850 
   851 lemma (in measure_space) simple_integral_cmult_indicator:
   852   assumes A: "A \<in> sets M"
   853   shows "(\<integral>\<^isup>Sx. c * indicator A x \<partial>M) = c * \<mu> A"
   854   using simple_integral_mult[OF simple_function_indicator[OF A]]
   855   unfolding simple_integral_indicator_only[OF A] by simp
   856 
   857 lemma (in measure_space) simple_integral_positive:
   858   assumes f: "simple_function M f" and ae: "AE x. 0 \<le> f x"
   859   shows "0 \<le> integral\<^isup>S M f"
   860 proof -
   861   have "integral\<^isup>S M (\<lambda>x. 0) \<le> integral\<^isup>S M f"
   862     using simple_integral_mono_AE[OF _ f ae] by auto
   863   then show ?thesis by simp
   864 qed
   865 
   866 section "Continuous positive integration"
   867 
   868 definition positive_integral_def:
   869   "integral\<^isup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^isup>S M g)"
   870 
   871 syntax
   872   "_positive_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> extreal) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> extreal" ("\<integral>\<^isup>+ _. _ \<partial>_" [60,61] 110)
   873 
   874 translations
   875   "\<integral>\<^isup>+ x. f \<partial>M" == "CONST integral\<^isup>P M (%x. f)"
   876 
   877 lemma (in measure_space) positive_integral_cong_measure:
   878   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
   879   shows "integral\<^isup>P N f = integral\<^isup>P M f"
   880   unfolding positive_integral_def
   881   unfolding simple_function_cong_algebra[OF assms(2,3), symmetric]
   882   using AE_cong_measure[OF assms]
   883   using simple_integral_cong_measure[OF assms]
   884   by (auto intro!: SUP_cong)
   885 
   886 lemma (in measure_space) positive_integral_positive:
   887   "0 \<le> integral\<^isup>P M f"
   888   by (auto intro!: le_SUPI2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
   889 
   890 lemma (in measure_space) positive_integral_def_finite:
   891   "integral\<^isup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^isup>S M g)"
   892     (is "_ = SUPR ?A ?f")
   893   unfolding positive_integral_def
   894 proof (safe intro!: antisym SUP_leI)
   895   fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
   896   let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
   897   note gM = g(1)[THEN borel_measurable_simple_function]
   898   have \<mu>G_pos: "0 \<le> \<mu> ?G" using gM by auto
   899   let "?g y x" = "if g x = \<infinity> then y else max 0 (g x)"
   900   from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
   901     apply (safe intro!: simple_function_max simple_function_If)
   902     apply (force simp: max_def le_fun_def split: split_if_asm)+
   903     done
   904   show "integral\<^isup>S M g \<le> SUPR ?A ?f"
   905   proof cases
   906     have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto
   907     assume "\<mu> ?G = 0"
   908     with gM have "AE x. x \<notin> ?G" by (simp add: AE_iff_null_set)
   909     with gM g show ?thesis
   910       by (intro le_SUPI2[OF g0] simple_integral_mono_AE)
   911          (auto simp: max_def intro!: simple_function_If)
   912   next
   913     assume \<mu>G: "\<mu> ?G \<noteq> 0"
   914     have "SUPR ?A (integral\<^isup>S M) = \<infinity>"
   915     proof (intro SUP_PInfty)
   916       fix n :: nat
   917       let ?y = "extreal (real n) / (if \<mu> ?G = \<infinity> then 1 else \<mu> ?G)"
   918       have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>G \<mu>G_pos by (auto simp: extreal_divide_eq)
   919       then have "?g ?y \<in> ?A" by (rule g_in_A)
   920       have "real n \<le> ?y * \<mu> ?G"
   921         using \<mu>G \<mu>G_pos by (cases "\<mu> ?G") (auto simp: field_simps)
   922       also have "\<dots> = (\<integral>\<^isup>Sx. ?y * indicator ?G x \<partial>M)"
   923         using `0 \<le> ?y` `?g ?y \<in> ?A` gM
   924         by (subst simple_integral_cmult_indicator) auto
   925       also have "\<dots> \<le> integral\<^isup>S M (?g ?y)" using `?g ?y \<in> ?A` gM
   926         by (intro simple_integral_mono) auto
   927       finally show "\<exists>i\<in>?A. real n \<le> integral\<^isup>S M i"
   928         using `?g ?y \<in> ?A` by blast
   929     qed
   930     then show ?thesis by simp
   931   qed
   932 qed (auto intro: le_SUPI)
   933 
   934 lemma (in measure_space) positive_integral_mono_AE:
   935   assumes ae: "AE x. u x \<le> v x" shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
   936   unfolding positive_integral_def
   937 proof (safe intro!: SUP_mono)
   938   fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
   939   from ae[THEN AE_E] guess N . note N = this
   940   then have ae_N: "AE x. x \<notin> N" by (auto intro: AE_not_in)
   941   let "?n x" = "n x * indicator (space M - N) x"
   942   have "AE x. n x \<le> ?n x" "simple_function M ?n"
   943     using n N ae_N by auto
   944   moreover
   945   { fix x have "?n x \<le> max 0 (v x)"
   946     proof cases
   947       assume x: "x \<in> space M - N"
   948       with N have "u x \<le> v x" by auto
   949       with n(2)[THEN le_funD, of x] x show ?thesis
   950         by (auto simp: max_def split: split_if_asm)
   951     qed simp }
   952   then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI)
   953   moreover have "integral\<^isup>S M n \<le> integral\<^isup>S M ?n"
   954     using ae_N N n by (auto intro!: simple_integral_mono_AE)
   955   ultimately show "\<exists>m\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> v}. integral\<^isup>S M n \<le> integral\<^isup>S M m"
   956     by force
   957 qed
   958 
   959 lemma (in measure_space) positive_integral_mono:
   960   "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^isup>P M u \<le> integral\<^isup>P M v"
   961   by (auto intro: positive_integral_mono_AE)
   962 
   963 lemma (in measure_space) positive_integral_cong_AE:
   964   "AE x. u x = v x \<Longrightarrow> integral\<^isup>P M u = integral\<^isup>P M v"
   965   by (auto simp: eq_iff intro!: positive_integral_mono_AE)
   966 
   967 lemma (in measure_space) positive_integral_cong:
   968   "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^isup>P M u = integral\<^isup>P M v"
   969   by (auto intro: positive_integral_cong_AE)
   970 
   971 lemma (in measure_space) positive_integral_eq_simple_integral:
   972   assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
   973 proof -
   974   let "?f x" = "f x * indicator (space M) x"
   975   have f': "simple_function M ?f" using f by auto
   976   with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
   977     by (auto simp: fun_eq_iff max_def split: split_indicator)
   978   have "integral\<^isup>P M ?f \<le> integral\<^isup>S M ?f" using f'
   979     by (force intro!: SUP_leI simple_integral_mono simp: le_fun_def positive_integral_def)
   980   moreover have "integral\<^isup>S M ?f \<le> integral\<^isup>P M ?f"
   981     unfolding positive_integral_def
   982     using f' by (auto intro!: le_SUPI)
   983   ultimately show ?thesis
   984     by (simp cong: positive_integral_cong simple_integral_cong)
   985 qed
   986 
   987 lemma (in measure_space) positive_integral_eq_simple_integral_AE:
   988   assumes f: "simple_function M f" "AE x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
   989 proof -
   990   have "AE x. f x = max 0 (f x)" using f by (auto split: split_max)
   991   with f have "integral\<^isup>P M f = integral\<^isup>S M (\<lambda>x. max 0 (f x))"
   992     by (simp cong: positive_integral_cong_AE simple_integral_cong_AE
   993              add: positive_integral_eq_simple_integral)
   994   with assms show ?thesis
   995     by (auto intro!: simple_integral_cong_AE split: split_max)
   996 qed
   997 
   998 lemma (in measure_space) positive_integral_SUP_approx:
   999   assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
  1000   and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"
  1001   shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S")
  1002 proof (rule extreal_le_mult_one_interval)
  1003   have "0 \<le> (SUP i. integral\<^isup>P M (f i))"
  1004     using f(3) by (auto intro!: le_SUPI2 positive_integral_positive)
  1005   then show "(SUP i. integral\<^isup>P M (f i)) \<noteq> -\<infinity>" by auto
  1006   have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
  1007     using u(3) by auto
  1008   fix a :: extreal assume "0 < a" "a < 1"
  1009   hence "a \<noteq> 0" by auto
  1010   let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
  1011   have B: "\<And>i. ?B i \<in> sets M"
  1012     using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
  1013 
  1014   let "?uB i x" = "u x * indicator (?B i) x"
  1015 
  1016   { fix i have "?B i \<subseteq> ?B (Suc i)"
  1017     proof safe
  1018       fix i x assume "a * u x \<le> f i x"
  1019       also have "\<dots> \<le> f (Suc i) x"
  1020         using `incseq f`[THEN incseq_SucD] unfolding le_fun_def by auto
  1021       finally show "a * u x \<le> f (Suc i) x" .
  1022     qed }
  1023   note B_mono = this
  1024 
  1025   note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
  1026 
  1027   let "?B' i n" = "(u -` {i} \<inter> space M) \<inter> ?B n"
  1028   have measure_conv: "\<And>i. \<mu> (u -` {i} \<inter> space M) = (SUP n. \<mu> (?B' i n))"
  1029   proof -
  1030     fix i
  1031     have 1: "range (?B' i) \<subseteq> sets M" using B_u by auto
  1032     have 2: "incseq (?B' i)" using B_mono by (auto intro!: incseq_SucI)
  1033     have "(\<Union>n. ?B' i n) = u -` {i} \<inter> space M"
  1034     proof safe
  1035       fix x i assume x: "x \<in> space M"
  1036       show "x \<in> (\<Union>i. ?B' (u x) i)"
  1037       proof cases
  1038         assume "u x = 0" thus ?thesis using `x \<in> space M` f(3) by simp
  1039       next
  1040         assume "u x \<noteq> 0"
  1041         with `a < 1` u_range[OF `x \<in> space M`]
  1042         have "a * u x < 1 * u x"
  1043           by (intro extreal_mult_strict_right_mono) (auto simp: image_iff)
  1044         also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUPR_apply)
  1045         finally obtain i where "a * u x < f i x" unfolding SUPR_def
  1046           by (auto simp add: less_Sup_iff)
  1047         hence "a * u x \<le> f i x" by auto
  1048         thus ?thesis using `x \<in> space M` by auto
  1049       qed
  1050     qed
  1051     then show "?thesis i" using continuity_from_below[OF 1 2] by simp
  1052   qed
  1053 
  1054   have "integral\<^isup>S M u = (SUP i. integral\<^isup>S M (?uB i))"
  1055     unfolding simple_integral_indicator[OF B `simple_function M u`]
  1056   proof (subst SUPR_extreal_setsum, safe)
  1057     fix x n assume "x \<in> space M"
  1058     with u_range show "incseq (\<lambda>i. u x * \<mu> (?B' (u x) i))" "\<And>i. 0 \<le> u x * \<mu> (?B' (u x) i)"
  1059       using B_mono B_u by (auto intro!: measure_mono extreal_mult_left_mono incseq_SucI simp: extreal_zero_le_0_iff)
  1060   next
  1061     show "integral\<^isup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (?B' i n))"
  1062       using measure_conv u_range B_u unfolding simple_integral_def
  1063       by (auto intro!: setsum_cong SUPR_extreal_cmult[symmetric])
  1064   qed
  1065   moreover
  1066   have "a * (SUP i. integral\<^isup>S M (?uB i)) \<le> ?S"
  1067     apply (subst SUPR_extreal_cmult[symmetric])
  1068   proof (safe intro!: SUP_mono bexI)
  1069     fix i
  1070     have "a * integral\<^isup>S M (?uB i) = (\<integral>\<^isup>Sx. a * ?uB i x \<partial>M)"
  1071       using B `simple_function M u` u_range
  1072       by (subst simple_integral_mult) (auto split: split_indicator)
  1073     also have "\<dots> \<le> integral\<^isup>P M (f i)"
  1074     proof -
  1075       have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto
  1076       show ?thesis using f(3) * u_range `0 < a`
  1077         by (subst positive_integral_eq_simple_integral[symmetric])
  1078            (auto intro!: positive_integral_mono split: split_indicator)
  1079     qed
  1080     finally show "a * integral\<^isup>S M (?uB i) \<le> integral\<^isup>P M (f i)"
  1081       by auto
  1082   next
  1083     fix i show "0 \<le> \<integral>\<^isup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range
  1084       by (intro simple_integral_positive) (auto split: split_indicator)
  1085   qed (insert `0 < a`, auto)
  1086   ultimately show "a * integral\<^isup>S M u \<le> ?S" by simp
  1087 qed
  1088 
  1089 lemma (in measure_space) incseq_positive_integral:
  1090   assumes "incseq f" shows "incseq (\<lambda>i. integral\<^isup>P M (f i))"
  1091 proof -
  1092   have "\<And>i x. f i x \<le> f (Suc i) x"
  1093     using assms by (auto dest!: incseq_SucD simp: le_fun_def)
  1094   then show ?thesis
  1095     by (auto intro!: incseq_SucI positive_integral_mono)
  1096 qed
  1097 
  1098 text {* Beppo-Levi monotone convergence theorem *}
  1099 lemma (in measure_space) positive_integral_monotone_convergence_SUP:
  1100   assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
  1101   shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
  1102 proof (rule antisym)
  1103   show "(SUP j. integral\<^isup>P M (f j)) \<le> (\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M)"
  1104     by (auto intro!: SUP_leI le_SUPI positive_integral_mono)
  1105 next
  1106   show "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^isup>P M (f j))"
  1107     unfolding positive_integral_def_finite[of "\<lambda>x. SUP i. f i x"]
  1108   proof (safe intro!: SUP_leI)
  1109     fix g assume g: "simple_function M g"
  1110       and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
  1111     moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
  1112       using f by (auto intro!: le_SUPI2)
  1113     ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
  1114       by (intro  positive_integral_SUP_approx[OF f g _ g'])
  1115          (auto simp: le_fun_def max_def SUPR_apply)
  1116   qed
  1117 qed
  1118 
  1119 lemma (in measure_space) positive_integral_monotone_convergence_SUP_AE:
  1120   assumes f: "\<And>i. AE x. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M"
  1121   shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
  1122 proof -
  1123   from f have "AE x. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
  1124     by (simp add: AE_all_countable)
  1125   from this[THEN AE_E] guess N . note N = this
  1126   let "?f i x" = "if x \<in> space M - N then f i x else 0"
  1127   have f_eq: "AE x. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ N])
  1128   then have "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^isup>+ x. (SUP i. ?f i x) \<partial>M)"
  1129     by (auto intro!: positive_integral_cong_AE)
  1130   also have "\<dots> = (SUP i. (\<integral>\<^isup>+ x. ?f i x \<partial>M))"
  1131   proof (rule positive_integral_monotone_convergence_SUP)
  1132     show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
  1133     { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
  1134         using f N(3) by (intro measurable_If_set) auto
  1135       fix x show "0 \<le> ?f i x"
  1136         using N(1) by auto }
  1137   qed
  1138   also have "\<dots> = (SUP i. (\<integral>\<^isup>+ x. f i x \<partial>M))"
  1139     using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext)
  1140   finally show ?thesis .
  1141 qed
  1142 
  1143 lemma (in measure_space) positive_integral_monotone_convergence_SUP_AE_incseq:
  1144   assumes f: "incseq f" "\<And>i. AE x. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M"
  1145   shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
  1146   using f[unfolded incseq_Suc_iff le_fun_def]
  1147   by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])
  1148      auto
  1149 
  1150 lemma (in measure_space) positive_integral_monotone_convergence_simple:
  1151   assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
  1152   shows "(SUP i. integral\<^isup>S M (f i)) = (\<integral>\<^isup>+x. (SUP i. f i x) \<partial>M)"
  1153   using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
  1154     f(3)[THEN borel_measurable_simple_function] f(2)]
  1155   by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext)
  1156 
  1157 lemma positive_integral_max_0:
  1158   "(\<integral>\<^isup>+x. max 0 (f x) \<partial>M) = integral\<^isup>P M f"
  1159   by (simp add: le_fun_def positive_integral_def)
  1160 
  1161 lemma (in measure_space) positive_integral_cong_pos:
  1162   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
  1163   shows "integral\<^isup>P M f = integral\<^isup>P M g"
  1164 proof -
  1165   have "integral\<^isup>P M (\<lambda>x. max 0 (f x)) = integral\<^isup>P M (\<lambda>x. max 0 (g x))"
  1166   proof (intro positive_integral_cong)
  1167     fix x assume "x \<in> space M"
  1168     from assms[OF this] show "max 0 (f x) = max 0 (g x)"
  1169       by (auto split: split_max)
  1170   qed
  1171   then show ?thesis by (simp add: positive_integral_max_0)
  1172 qed
  1173 
  1174 lemma (in measure_space) SUP_simple_integral_sequences:
  1175   assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
  1176   and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)"
  1177   and eq: "AE x. (SUP i. f i x) = (SUP i. g i x)"
  1178   shows "(SUP i. integral\<^isup>S M (f i)) = (SUP i. integral\<^isup>S M (g i))"
  1179     (is "SUPR _ ?F = SUPR _ ?G")
  1180 proof -
  1181   have "(SUP i. integral\<^isup>S M (f i)) = (\<integral>\<^isup>+x. (SUP i. f i x) \<partial>M)"
  1182     using f by (rule positive_integral_monotone_convergence_simple)
  1183   also have "\<dots> = (\<integral>\<^isup>+x. (SUP i. g i x) \<partial>M)"
  1184     unfolding eq[THEN positive_integral_cong_AE] ..
  1185   also have "\<dots> = (SUP i. ?G i)"
  1186     using g by (rule positive_integral_monotone_convergence_simple[symmetric])
  1187   finally show ?thesis by simp
  1188 qed
  1189 
  1190 lemma (in measure_space) positive_integral_const[simp]:
  1191   "0 \<le> c \<Longrightarrow> (\<integral>\<^isup>+ x. c \<partial>M) = c * \<mu> (space M)"
  1192   by (subst positive_integral_eq_simple_integral) auto
  1193 
  1194 lemma (in measure_space) positive_integral_vimage:
  1195   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
  1196   and f: "f \<in> borel_measurable M'"
  1197   shows "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
  1198 proof -
  1199   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
  1200   from T.borel_measurable_implies_simple_function_sequence'[OF f]
  1201   guess f' . note f' = this
  1202   let "?f i x" = "f' i (T x)"
  1203   have inc: "incseq ?f" using f' by (force simp: le_fun_def incseq_def)
  1204   have sup: "\<And>x. (SUP i. ?f i x) = max 0 (f (T x))"
  1205     using f'(4) .
  1206   have sf: "\<And>i. simple_function M (\<lambda>x. f' i (T x))"
  1207     using simple_function_vimage[OF T(1) measure_preservingD2[OF T(2)] f'(1)] .
  1208   show "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
  1209     using
  1210       T.positive_integral_monotone_convergence_simple[OF f'(2,5,1)]
  1211       positive_integral_monotone_convergence_simple[OF inc f'(5) sf]
  1212     by (simp add: positive_integral_max_0 simple_integral_vimage[OF T f'(1)] f')
  1213 qed
  1214 
  1215 lemma (in measure_space) positive_integral_linear:
  1216   assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
  1217   and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
  1218   shows "(\<integral>\<^isup>+ x. a * f x + g x \<partial>M) = a * integral\<^isup>P M f + integral\<^isup>P M g"
  1219     (is "integral\<^isup>P M ?L = _")
  1220 proof -
  1221   from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
  1222   note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
  1223   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
  1224   note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
  1225   let "?L' i x" = "a * u i x + v i x"
  1226 
  1227   have "?L \<in> borel_measurable M" using assms by auto
  1228   from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
  1229   note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
  1230 
  1231   have inc: "incseq (\<lambda>i. a * integral\<^isup>S M (u i))" "incseq (\<lambda>i. integral\<^isup>S M (v i))"
  1232     using u v `0 \<le> a`
  1233     by (auto simp: incseq_Suc_iff le_fun_def
  1234              intro!: add_mono extreal_mult_left_mono simple_integral_mono)
  1235   have pos: "\<And>i. 0 \<le> integral\<^isup>S M (u i)" "\<And>i. 0 \<le> integral\<^isup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^isup>S M (u i)"
  1236     using u v `0 \<le> a` by (auto simp: simple_integral_positive)
  1237   { fix i from pos[of i] have "a * integral\<^isup>S M (u i) \<noteq> -\<infinity>" "integral\<^isup>S M (v i) \<noteq> -\<infinity>"
  1238       by (auto split: split_if_asm) }
  1239   note not_MInf = this
  1240 
  1241   have l': "(SUP i. integral\<^isup>S M (l i)) = (SUP i. integral\<^isup>S M (?L' i))"
  1242   proof (rule SUP_simple_integral_sequences[OF l(3,6,2)])
  1243     show "incseq ?L'" "\<And>i x. 0 \<le> ?L' i x" "\<And>i. simple_function M (?L' i)"
  1244       using u v  `0 \<le> a` unfolding incseq_Suc_iff le_fun_def
  1245       by (auto intro!: add_mono extreal_mult_left_mono extreal_add_nonneg_nonneg)
  1246     { fix x
  1247       { fix i have "a * u i x \<noteq> -\<infinity>" "v i x \<noteq> -\<infinity>" "u i x \<noteq> -\<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x]
  1248           by auto }
  1249       then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
  1250         using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
  1251         by (subst SUPR_extreal_cmult[symmetric, OF u(6) `0 \<le> a`])
  1252            (auto intro!: SUPR_extreal_add
  1253                  simp: incseq_Suc_iff le_fun_def add_mono extreal_mult_left_mono extreal_add_nonneg_nonneg) }
  1254     then show "AE x. (SUP i. l i x) = (SUP i. ?L' i x)"
  1255       unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
  1256       by (intro AE_I2) (auto split: split_max simp add: extreal_add_nonneg_nonneg)
  1257   qed
  1258   also have "\<dots> = (SUP i. a * integral\<^isup>S M (u i) + integral\<^isup>S M (v i))"
  1259     using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPR UNIV"] ext)
  1260   finally have "(\<integral>\<^isup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^isup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^isup>+x. max 0 (g x) \<partial>M)"
  1261     unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
  1262     unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
  1263     apply (subst SUPR_extreal_cmult[symmetric, OF pos(1) `0 \<le> a`])
  1264     apply (subst SUPR_extreal_add[symmetric, OF inc not_MInf]) .
  1265   then show ?thesis by (simp add: positive_integral_max_0)
  1266 qed
  1267 
  1268 lemma (in measure_space) positive_integral_cmult:
  1269   assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x" "0 \<le> c"
  1270   shows "(\<integral>\<^isup>+ x. c * f x \<partial>M) = c * integral\<^isup>P M f"
  1271 proof -
  1272   have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c`
  1273     by (auto split: split_max simp: extreal_zero_le_0_iff)
  1274   have "(\<integral>\<^isup>+ x. c * f x \<partial>M) = (\<integral>\<^isup>+ x. c * max 0 (f x) \<partial>M)"
  1275     by (simp add: positive_integral_max_0)
  1276   then show ?thesis
  1277     using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" "\<lambda>x. 0"] f
  1278     by (auto simp: positive_integral_max_0)
  1279 qed
  1280 
  1281 lemma (in measure_space) positive_integral_multc:
  1282   assumes "f \<in> borel_measurable M" "AE x. 0 \<le> f x" "0 \<le> c"
  1283   shows "(\<integral>\<^isup>+ x. f x * c \<partial>M) = integral\<^isup>P M f * c"
  1284   unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
  1285 
  1286 lemma (in measure_space) positive_integral_indicator[simp]:
  1287   "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x\<partial>M) = \<mu> A"
  1288   by (subst positive_integral_eq_simple_integral)
  1289      (auto simp: simple_function_indicator simple_integral_indicator)
  1290 
  1291 lemma (in measure_space) positive_integral_cmult_indicator:
  1292   "0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x \<partial>M) = c * \<mu> A"
  1293   by (subst positive_integral_eq_simple_integral)
  1294      (auto simp: simple_function_indicator simple_integral_indicator)
  1295 
  1296 lemma (in measure_space) positive_integral_add:
  1297   assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x"
  1298   and g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
  1299   shows "(\<integral>\<^isup>+ x. f x + g x \<partial>M) = integral\<^isup>P M f + integral\<^isup>P M g"
  1300 proof -
  1301   have ae: "AE x. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
  1302     using assms by (auto split: split_max simp: extreal_add_nonneg_nonneg)
  1303   have "(\<integral>\<^isup>+ x. f x + g x \<partial>M) = (\<integral>\<^isup>+ x. max 0 (f x + g x) \<partial>M)"
  1304     by (simp add: positive_integral_max_0)
  1305   also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"
  1306     unfolding ae[THEN positive_integral_cong_AE] ..
  1307   also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (f x) \<partial>M) + (\<integral>\<^isup>+ x. max 0 (g x) \<partial>M)"
  1308     using positive_integral_linear[of "\<lambda>x. max 0 (f x)" 1 "\<lambda>x. max 0 (g x)"] f g
  1309     by auto
  1310   finally show ?thesis
  1311     by (simp add: positive_integral_max_0)
  1312 qed
  1313 
  1314 lemma (in measure_space) positive_integral_setsum:
  1315   assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" "\<And>i. i\<in>P \<Longrightarrow> AE x. 0 \<le> f i x"
  1316   shows "(\<integral>\<^isup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>P M (f i))"
  1317 proof cases
  1318   assume f: "finite P"
  1319   from assms have "AE x. \<forall>i\<in>P. 0 \<le> f i x" unfolding AE_finite_all[OF f] by auto
  1320   from f this assms(1) show ?thesis
  1321   proof induct
  1322     case (insert i P)
  1323     then have "f i \<in> borel_measurable M" "AE x. 0 \<le> f i x"
  1324       "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x. 0 \<le> (\<Sum>i\<in>P. f i x)"
  1325       by (auto intro!: borel_measurable_extreal_setsum setsum_nonneg)
  1326     from positive_integral_add[OF this]
  1327     show ?case using insert by auto
  1328   qed simp
  1329 qed simp
  1330 
  1331 lemma (in measure_space) positive_integral_Markov_inequality:
  1332   assumes u: "u \<in> borel_measurable M" "AE x. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c" "c \<noteq> \<infinity>"
  1333   shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
  1334     (is "\<mu> ?A \<le> _ * ?PI")
  1335 proof -
  1336   have "?A \<in> sets M"
  1337     using `A \<in> sets M` u by auto
  1338   hence "\<mu> ?A = (\<integral>\<^isup>+ x. indicator ?A x \<partial>M)"
  1339     using positive_integral_indicator by simp
  1340   also have "\<dots> \<le> (\<integral>\<^isup>+ x. c * (u x * indicator A x) \<partial>M)" using u c
  1341     by (auto intro!: positive_integral_mono_AE
  1342       simp: indicator_def extreal_zero_le_0_iff)
  1343   also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
  1344     using assms
  1345     by (auto intro!: positive_integral_cmult borel_measurable_indicator simp: extreal_zero_le_0_iff)
  1346   finally show ?thesis .
  1347 qed
  1348 
  1349 lemma (in measure_space) positive_integral_noteq_infinite:
  1350   assumes g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
  1351   and "integral\<^isup>P M g \<noteq> \<infinity>"
  1352   shows "AE x. g x \<noteq> \<infinity>"
  1353 proof (rule ccontr)
  1354   assume c: "\<not> (AE x. g x \<noteq> \<infinity>)"
  1355   have "\<mu> {x\<in>space M. g x = \<infinity>} \<noteq> 0"
  1356     using c g by (simp add: AE_iff_null_set)
  1357   moreover have "0 \<le> \<mu> {x\<in>space M. g x = \<infinity>}" using g by (auto intro: measurable_sets)
  1358   ultimately have "0 < \<mu> {x\<in>space M. g x = \<infinity>}" by auto
  1359   then have "\<infinity> = \<infinity> * \<mu> {x\<in>space M. g x = \<infinity>}" by auto
  1360   also have "\<dots> \<le> (\<integral>\<^isup>+x. \<infinity> * indicator {x\<in>space M. g x = \<infinity>} x \<partial>M)"
  1361     using g by (subst positive_integral_cmult_indicator) auto
  1362   also have "\<dots> \<le> integral\<^isup>P M g"
  1363     using assms by (auto intro!: positive_integral_mono_AE simp: indicator_def)
  1364   finally show False using `integral\<^isup>P M g \<noteq> \<infinity>` by auto
  1365 qed
  1366 
  1367 lemma (in measure_space) positive_integral_diff:
  1368   assumes f: "f \<in> borel_measurable M"
  1369   and g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
  1370   and fin: "integral\<^isup>P M g \<noteq> \<infinity>"
  1371   and mono: "AE x. g x \<le> f x"
  1372   shows "(\<integral>\<^isup>+ x. f x - g x \<partial>M) = integral\<^isup>P M f - integral\<^isup>P M g"
  1373 proof -
  1374   have diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" "AE x. 0 \<le> f x - g x"
  1375     using assms by (auto intro: extreal_diff_positive)
  1376   have pos_f: "AE x. 0 \<le> f x" using mono g by auto
  1377   { fix a b :: extreal assume "0 \<le> a" "a \<noteq> \<infinity>" "0 \<le> b" "a \<le> b" then have "b - a + a = b"
  1378       by (cases rule: extreal2_cases[of a b]) auto }
  1379   note * = this
  1380   then have "AE x. f x = f x - g x + g x"
  1381     using mono positive_integral_noteq_infinite[OF g fin] assms by auto
  1382   then have **: "integral\<^isup>P M f = (\<integral>\<^isup>+x. f x - g x \<partial>M) + integral\<^isup>P M g"
  1383     unfolding positive_integral_add[OF diff g, symmetric]
  1384     by (rule positive_integral_cong_AE)
  1385   show ?thesis unfolding **
  1386     using fin positive_integral_positive[of g]
  1387     by (cases rule: extreal2_cases[of "\<integral>\<^isup>+ x. f x - g x \<partial>M" "integral\<^isup>P M g"]) auto
  1388 qed
  1389 
  1390 lemma (in measure_space) positive_integral_suminf:
  1391   assumes f: "\<And>i. f i \<in> borel_measurable M" "\<And>i. AE x. 0 \<le> f i x"
  1392   shows "(\<integral>\<^isup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^isup>P M (f i))"
  1393 proof -
  1394   have all_pos: "AE x. \<forall>i. 0 \<le> f i x"
  1395     using assms by (auto simp: AE_all_countable)
  1396   have "(\<Sum>i. integral\<^isup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^isup>P M (f i))"
  1397     using positive_integral_positive by (rule suminf_extreal_eq_SUPR)
  1398   also have "\<dots> = (SUP n. \<integral>\<^isup>+x. (\<Sum>i<n. f i x) \<partial>M)"
  1399     unfolding positive_integral_setsum[OF f] ..
  1400   also have "\<dots> = \<integral>\<^isup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
  1401     by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
  1402        (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
  1403   also have "\<dots> = \<integral>\<^isup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
  1404     by (intro positive_integral_cong_AE) (auto simp: suminf_extreal_eq_SUPR)
  1405   finally show ?thesis by simp
  1406 qed
  1407 
  1408 text {* Fatou's lemma: convergence theorem on limes inferior *}
  1409 lemma (in measure_space) positive_integral_lim_INF:
  1410   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> extreal"
  1411   assumes u: "\<And>i. u i \<in> borel_measurable M" "\<And>i. AE x. 0 \<le> u i x"
  1412   shows "(\<integral>\<^isup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
  1413 proof -
  1414   have pos: "AE x. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
  1415   have "(\<integral>\<^isup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
  1416     (SUP n. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>M)"
  1417     unfolding liminf_SUPR_INFI using pos u
  1418     by (intro positive_integral_monotone_convergence_SUP_AE)
  1419        (elim AE_mp, auto intro!: AE_I2 intro: le_INFI INF_subset)
  1420   also have "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
  1421     unfolding liminf_SUPR_INFI
  1422     by (auto intro!: SUP_mono exI le_INFI positive_integral_mono INF_leI)
  1423   finally show ?thesis .
  1424 qed
  1425 
  1426 lemma (in measure_space) measure_space_density:
  1427   assumes u: "u \<in> borel_measurable M" "AE x. 0 \<le> u x"
  1428     and M'[simp]: "M' = (M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)\<rparr>)"
  1429   shows "measure_space M'"
  1430 proof -
  1431   interpret M': sigma_algebra M' by (intro sigma_algebra_cong) auto
  1432   show ?thesis
  1433   proof
  1434     have pos: "\<And>A. AE x. 0 \<le> u x * indicator A x"
  1435       using u by (auto simp: extreal_zero_le_0_iff)
  1436     then show "positive M' (measure M')" unfolding M'
  1437       using u(1) by (auto simp: positive_def intro!: positive_integral_positive)
  1438     show "countably_additive M' (measure M')"
  1439     proof (intro countably_additiveI)
  1440       fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M'"
  1441       then have *: "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M"
  1442         using u by (auto intro: borel_measurable_indicator)
  1443       assume disj: "disjoint_family A"
  1444       have "(\<Sum>n. measure M' (A n)) = (\<integral>\<^isup>+ x. (\<Sum>n. u x * indicator (A n) x) \<partial>M)"
  1445         unfolding M' using u(1) *
  1446         by (simp add: positive_integral_suminf[OF _ pos, symmetric])
  1447       also have "\<dots> = (\<integral>\<^isup>+ x. u x * (\<Sum>n. indicator (A n) x) \<partial>M)" using u
  1448         by (intro positive_integral_cong_AE)
  1449            (elim AE_mp, auto intro!: AE_I2 suminf_cmult_extreal)
  1450       also have "\<dots> = (\<integral>\<^isup>+ x. u x * indicator (\<Union>n. A n) x \<partial>M)"
  1451         unfolding suminf_indicator[OF disj] ..
  1452       finally show "(\<Sum>n. measure M' (A n)) = measure M' (\<Union>x. A x)"
  1453         unfolding M' by simp
  1454     qed
  1455   qed
  1456 qed
  1457 
  1458 lemma (in measure_space) positive_integral_null_set:
  1459   assumes "N \<in> null_sets" shows "(\<integral>\<^isup>+ x. u x * indicator N x \<partial>M) = 0"
  1460 proof -
  1461   have "(\<integral>\<^isup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)"
  1462   proof (intro positive_integral_cong_AE AE_I)
  1463     show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
  1464       by (auto simp: indicator_def)
  1465     show "\<mu> N = 0" "N \<in> sets M"
  1466       using assms by auto
  1467   qed
  1468   then show ?thesis by simp
  1469 qed
  1470 
  1471 lemma (in measure_space) positive_integral_translated_density:
  1472   assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x"
  1473   assumes g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
  1474     and M': "M' = (M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)\<rparr>)"
  1475   shows "integral\<^isup>P M' g = (\<integral>\<^isup>+ x. f x * g x \<partial>M)"
  1476 proof -
  1477   from measure_space_density[OF f M']
  1478   interpret T: measure_space M' .
  1479   have borel[simp]:
  1480     "borel_measurable M' = borel_measurable M"
  1481     "simple_function M' = simple_function M"
  1482     unfolding measurable_def simple_function_def_raw by (auto simp: M')
  1483   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
  1484   note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
  1485   note G'(2)[simp]
  1486   { fix P have "AE x. P x \<Longrightarrow> AE x in M'. P x"
  1487       using positive_integral_null_set[of _ f]
  1488       unfolding T.almost_everywhere_def almost_everywhere_def
  1489       by (auto simp: M') }
  1490   note ac = this
  1491   from G(4) g(2) have G_M': "AE x in M'. (SUP i. G i x) = g x"
  1492     by (auto intro!: ac split: split_max)
  1493   { fix i
  1494     let "?I y x" = "indicator (G i -` {y} \<inter> space M) x"
  1495     { fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"
  1496       then have [simp]: "G i ` space M \<inter> {y. G i x = y \<and> x \<in> space M} = {G i x}" by auto
  1497       from * G' G have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * (\<Sum>y\<in>G i`space M. (y * ?I y x))"
  1498         by (subst setsum_extreal_right_distrib) (auto simp: ac_simps)
  1499       also have "\<dots> = f x * G i x"
  1500         by (simp add: indicator_def if_distrib setsum_cases)
  1501       finally have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * G i x" . }
  1502     note to_singleton = this
  1503     have "integral\<^isup>P M' (G i) = integral\<^isup>S M' (G i)"
  1504       using G T.positive_integral_eq_simple_integral by simp
  1505     also have "\<dots> = (\<Sum>y\<in>G i`space M. y * (\<integral>\<^isup>+x. f x * ?I y x \<partial>M))"
  1506       unfolding simple_integral_def M' by simp
  1507     also have "\<dots> = (\<Sum>y\<in>G i`space M. (\<integral>\<^isup>+x. y * (f x * ?I y x) \<partial>M))"
  1508       using f G' G by (auto intro!: setsum_cong positive_integral_cmult[symmetric])
  1509     also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) \<partial>M)"
  1510       using f G' G by (auto intro!: positive_integral_setsum[symmetric])
  1511     finally have "integral\<^isup>P M' (G i) = (\<integral>\<^isup>+x. f x * G i x \<partial>M)"
  1512       using f g G' to_singleton by (auto intro!: positive_integral_cong_AE) }
  1513   note [simp] = this
  1514   have "integral\<^isup>P M' g = (SUP i. integral\<^isup>P M' (G i))" using G'(1) G_M'(1) G
  1515     using T.positive_integral_monotone_convergence_SUP[symmetric, OF `incseq G`]
  1516     by (simp cong: T.positive_integral_cong_AE)
  1517   also have "\<dots> = (SUP i. (\<integral>\<^isup>+x. f x * G i x \<partial>M))" by simp
  1518   also have "\<dots> = (\<integral>\<^isup>+x. (SUP i. f x * G i x) \<partial>M)"
  1519     using f G' G(2)[THEN incseq_SucD] G
  1520     by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
  1521        (auto simp: extreal_mult_left_mono le_fun_def extreal_zero_le_0_iff)
  1522   also have "\<dots> = (\<integral>\<^isup>+x. f x * g x \<partial>M)" using f G' G g
  1523     by (intro positive_integral_cong_AE)
  1524        (auto simp add: SUPR_extreal_cmult split: split_max)
  1525   finally show "integral\<^isup>P M' g = (\<integral>\<^isup>+x. f x * g x \<partial>M)" .
  1526 qed
  1527 
  1528 lemma (in measure_space) positive_integral_0_iff:
  1529   assumes u: "u \<in> borel_measurable M" and pos: "AE x. 0 \<le> u x"
  1530   shows "integral\<^isup>P M u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0"
  1531     (is "_ \<longleftrightarrow> \<mu> ?A = 0")
  1532 proof -
  1533   have u_eq: "(\<integral>\<^isup>+ x. u x * indicator ?A x \<partial>M) = integral\<^isup>P M u"
  1534     by (auto intro!: positive_integral_cong simp: indicator_def)
  1535   show ?thesis
  1536   proof
  1537     assume "\<mu> ?A = 0"
  1538     with positive_integral_null_set[of ?A u] u
  1539     show "integral\<^isup>P M u = 0" by (simp add: u_eq)
  1540   next
  1541     { fix r :: extreal and n :: nat assume gt_1: "1 \<le> real n * r"
  1542       then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_extreal_def)
  1543       then have "0 \<le> r" by (auto simp add: extreal_zero_less_0_iff) }
  1544     note gt_1 = this
  1545     assume *: "integral\<^isup>P M u = 0"
  1546     let "?M n" = "{x \<in> space M. 1 \<le> real (n::nat) * u x}"
  1547     have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
  1548     proof -
  1549       { fix n :: nat
  1550         from positive_integral_Markov_inequality[OF u pos, of ?A "extreal (real n)"]
  1551         have "\<mu> (?M n \<inter> ?A) \<le> 0" unfolding u_eq * using u by simp
  1552         moreover have "0 \<le> \<mu> (?M n \<inter> ?A)" using u by auto
  1553         ultimately have "\<mu> (?M n \<inter> ?A) = 0" by auto }
  1554       thus ?thesis by simp
  1555     qed
  1556     also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)"
  1557     proof (safe intro!: continuity_from_below)
  1558       fix n show "?M n \<inter> ?A \<in> sets M"
  1559         using u by (auto intro!: Int)
  1560     next
  1561       show "incseq (\<lambda>n. {x \<in> space M. 1 \<le> real n * u x} \<inter> {x \<in> space M. u x \<noteq> 0})"
  1562       proof (safe intro!: incseq_SucI)
  1563         fix n :: nat and x
  1564         assume *: "1 \<le> real n * u x"
  1565         also from gt_1[OF this] have "real n * u x \<le> real (Suc n) * u x"
  1566           using `0 \<le> u x` by (auto intro!: extreal_mult_right_mono)
  1567         finally show "1 \<le> real (Suc n) * u x" by auto
  1568       qed
  1569     qed
  1570     also have "\<dots> = \<mu> {x\<in>space M. 0 < u x}"
  1571     proof (safe intro!: arg_cong[where f="\<mu>"] dest!: gt_1)
  1572       fix x assume "0 < u x" and [simp, intro]: "x \<in> space M"
  1573       show "x \<in> (\<Union>n. ?M n \<inter> ?A)"
  1574       proof (cases "u x")
  1575         case (real r) with `0 < u x` have "0 < r" by auto
  1576         obtain j :: nat where "1 / r \<le> real j" using real_arch_simple ..
  1577         hence "1 / r * r \<le> real j * r" unfolding mult_le_cancel_right using `0 < r` by auto
  1578         hence "1 \<le> real j * r" using real `0 < r` by auto
  1579         thus ?thesis using `0 < r` real by (auto simp: one_extreal_def)
  1580       qed (insert `0 < u x`, auto)
  1581     qed auto
  1582     finally have "\<mu> {x\<in>space M. 0 < u x} = 0" by simp
  1583     moreover
  1584     from pos have "AE x. \<not> (u x < 0)" by auto
  1585     then have "\<mu> {x\<in>space M. u x < 0} = 0"
  1586       using AE_iff_null_set u by auto
  1587     moreover have "\<mu> {x\<in>space M. u x \<noteq> 0} = \<mu> {x\<in>space M. u x < 0} + \<mu> {x\<in>space M. 0 < u x}"
  1588       using u by (subst measure_additive) (auto intro!: arg_cong[where f=\<mu>])
  1589     ultimately show "\<mu> ?A = 0" by simp
  1590   qed
  1591 qed
  1592 
  1593 lemma (in measure_space) positive_integral_0_iff_AE:
  1594   assumes u: "u \<in> borel_measurable M"
  1595   shows "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. u x \<le> 0)"
  1596 proof -
  1597   have sets: "{x\<in>space M. max 0 (u x) \<noteq> 0} \<in> sets M"
  1598     using u by auto
  1599   from positive_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
  1600   have "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. max 0 (u x) = 0)"
  1601     unfolding positive_integral_max_0
  1602     using AE_iff_null_set[OF sets] u by auto
  1603   also have "\<dots> \<longleftrightarrow> (AE x. u x \<le> 0)" by (auto split: split_max)
  1604   finally show ?thesis .
  1605 qed
  1606 
  1607 lemma (in measure_space) positive_integral_restricted:
  1608   assumes A: "A \<in> sets M"
  1609   shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
  1610     (is "integral\<^isup>P ?R f = integral\<^isup>P M ?f")
  1611 proof -
  1612   interpret R: measure_space ?R
  1613     by (rule restricted_measure_space) fact
  1614   let "?I g x" = "g x * indicator A x :: extreal"
  1615   show ?thesis
  1616     unfolding positive_integral_def
  1617     unfolding simple_function_restricted[OF A]
  1618     unfolding AE_restricted[OF A]
  1619   proof (safe intro!: SUPR_eq)
  1620     fix g assume g: "simple_function M (?I g)" and le: "g \<le> max 0 \<circ> f"
  1621     show "\<exists>j\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> ?I f}.
  1622       integral\<^isup>S (restricted_space A) g \<le> integral\<^isup>S M j"
  1623     proof (safe intro!: bexI[of _ "?I g"])
  1624       show "integral\<^isup>S (restricted_space A) g \<le> integral\<^isup>S M (?I g)"
  1625         using g A by (simp add: simple_integral_restricted)
  1626       show "?I g \<le> max 0 \<circ> ?I f"
  1627         using le by (auto simp: le_fun_def max_def indicator_def split: split_if_asm)
  1628     qed fact
  1629   next
  1630     fix g assume g: "simple_function M g" and le: "g \<le> max 0 \<circ> ?I f"
  1631     show "\<exists>i\<in>{g. simple_function M (?I g) \<and> g \<le> max 0 \<circ> f}.
  1632       integral\<^isup>S M g \<le> integral\<^isup>S (restricted_space A) i"
  1633     proof (safe intro!: bexI[of _ "?I g"])
  1634       show "?I g \<le> max 0 \<circ> f"
  1635         using le by (auto simp: le_fun_def max_def indicator_def split: split_if_asm)
  1636       from le have "\<And>x. g x \<le> ?I (?I g) x"
  1637         by (auto simp: le_fun_def max_def indicator_def split: split_if_asm)
  1638       then show "integral\<^isup>S M g \<le> integral\<^isup>S (restricted_space A) (?I g)"
  1639         using A g by (auto intro!: simple_integral_mono simp: simple_integral_restricted)
  1640       show "simple_function M (?I (?I g))" using g A by auto
  1641     qed
  1642   qed
  1643 qed
  1644 
  1645 lemma (in measure_space) positive_integral_subalgebra:
  1646   assumes f: "f \<in> borel_measurable N" "AE x in N. 0 \<le> f x"
  1647   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A"
  1648   and sa: "sigma_algebra N"
  1649   shows "integral\<^isup>P N f = integral\<^isup>P M f"
  1650 proof -
  1651   interpret N: measure_space N using measure_space_subalgebra[OF sa N] .
  1652   from N.borel_measurable_implies_simple_function_sequence'[OF f(1)] guess fs . note fs = this
  1653   note sf = simple_function_subalgebra[OF fs(1) N(1,2)]
  1654   from N.positive_integral_monotone_convergence_simple[OF fs(2,5,1), symmetric]
  1655   have "integral\<^isup>P N f = (SUP i. \<Sum>x\<in>fs i ` space M. x * N.\<mu> (fs i -` {x} \<inter> space M))"
  1656     unfolding fs(4) positive_integral_max_0
  1657     unfolding simple_integral_def `space N = space M` by simp
  1658   also have "\<dots> = (SUP i. \<Sum>x\<in>fs i ` space M. x * \<mu> (fs i -` {x} \<inter> space M))"
  1659     using N N.simple_functionD(2)[OF fs(1)] unfolding `space N = space M` by auto
  1660   also have "\<dots> = integral\<^isup>P M f"
  1661     using positive_integral_monotone_convergence_simple[OF fs(2,5) sf, symmetric]
  1662     unfolding fs(4) positive_integral_max_0
  1663     unfolding simple_integral_def `space N = space M` by simp
  1664   finally show ?thesis .
  1665 qed
  1666 
  1667 section "Lebesgue Integral"
  1668 
  1669 definition integrable where
  1670   "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
  1671     (\<integral>\<^isup>+ x. extreal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^isup>+ x. extreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1672 
  1673 lemma integrableD[dest]:
  1674   assumes "integrable M f"
  1675   shows "f \<in> borel_measurable M" "(\<integral>\<^isup>+ x. extreal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^isup>+ x. extreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1676   using assms unfolding integrable_def by auto
  1677 
  1678 definition lebesgue_integral_def:
  1679   "integral\<^isup>L M f = real ((\<integral>\<^isup>+ x. extreal (f x) \<partial>M)) - real ((\<integral>\<^isup>+ x. extreal (- f x) \<partial>M))"
  1680 
  1681 syntax
  1682   "_lebesgue_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110)
  1683 
  1684 translations
  1685   "\<integral> x. f \<partial>M" == "CONST integral\<^isup>L M (%x. f)"
  1686 
  1687 lemma (in measure_space) integrableE:
  1688   assumes "integrable M f"
  1689   obtains r q where
  1690     "(\<integral>\<^isup>+x. extreal (f x)\<partial>M) = extreal r"
  1691     "(\<integral>\<^isup>+x. extreal (-f x)\<partial>M) = extreal q"
  1692     "f \<in> borel_measurable M" "integral\<^isup>L M f = r - q"
  1693   using assms unfolding integrable_def lebesgue_integral_def
  1694   using positive_integral_positive[of "\<lambda>x. extreal (f x)"]
  1695   using positive_integral_positive[of "\<lambda>x. extreal (-f x)"]
  1696   by (cases rule: extreal2_cases[of "(\<integral>\<^isup>+x. extreal (-f x)\<partial>M)" "(\<integral>\<^isup>+x. extreal (f x)\<partial>M)"]) auto
  1697 
  1698 lemma (in measure_space) integral_cong:
  1699   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
  1700   shows "integral\<^isup>L M f = integral\<^isup>L M g"
  1701   using assms by (simp cong: positive_integral_cong add: lebesgue_integral_def)
  1702 
  1703 lemma (in measure_space) integral_cong_measure:
  1704   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
  1705   shows "integral\<^isup>L N f = integral\<^isup>L M f"
  1706   by (simp add: positive_integral_cong_measure[OF assms] lebesgue_integral_def)
  1707 
  1708 lemma (in measure_space) integral_cong_AE:
  1709   assumes cong: "AE x. f x = g x"
  1710   shows "integral\<^isup>L M f = integral\<^isup>L M g"
  1711 proof -
  1712   have *: "AE x. extreal (f x) = extreal (g x)"
  1713     "AE x. extreal (- f x) = extreal (- g x)" using cong by auto
  1714   show ?thesis
  1715     unfolding *[THEN positive_integral_cong_AE] lebesgue_integral_def ..
  1716 qed
  1717 
  1718 lemma (in measure_space) integrable_cong:
  1719   "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable M g"
  1720   by (simp cong: positive_integral_cong measurable_cong add: integrable_def)
  1721 
  1722 lemma (in measure_space) integral_eq_positive_integral:
  1723   assumes f: "\<And>x. 0 \<le> f x"
  1724   shows "integral\<^isup>L M f = real (\<integral>\<^isup>+ x. extreal (f x) \<partial>M)"
  1725 proof -
  1726   { fix x have "max 0 (extreal (- f x)) = 0" using f[of x] by (simp split: split_max) }
  1727   then have "0 = (\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>M)" by simp
  1728   also have "\<dots> = (\<integral>\<^isup>+ x. extreal (- f x) \<partial>M)" unfolding positive_integral_max_0 ..
  1729   finally show ?thesis
  1730     unfolding lebesgue_integral_def by simp
  1731 qed
  1732 
  1733 lemma (in measure_space) integral_vimage:
  1734   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
  1735   assumes f: "f \<in> borel_measurable M'"
  1736   shows "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)"
  1737 proof -
  1738   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
  1739   from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
  1740   have borel: "(\<lambda>x. extreal (f x)) \<in> borel_measurable M'" "(\<lambda>x. extreal (- f x)) \<in> borel_measurable M'"
  1741     and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
  1742     using f by (auto simp: comp_def)
  1743   then show ?thesis
  1744     using f unfolding lebesgue_integral_def integrable_def
  1745     by (auto simp: borel[THEN positive_integral_vimage[OF T]])
  1746 qed
  1747 
  1748 lemma (in measure_space) integrable_vimage:
  1749   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
  1750   assumes f: "integrable M' f"
  1751   shows "integrable M (\<lambda>x. f (T x))"
  1752 proof -
  1753   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
  1754   from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
  1755   have borel: "(\<lambda>x. extreal (f x)) \<in> borel_measurable M'" "(\<lambda>x. extreal (- f x)) \<in> borel_measurable M'"
  1756     and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
  1757     using f by (auto simp: comp_def)
  1758   then show ?thesis
  1759     using f unfolding lebesgue_integral_def integrable_def
  1760     by (auto simp: borel[THEN positive_integral_vimage[OF T]])
  1761 qed
  1762 
  1763 lemma (in measure_space) integral_minus[intro, simp]:
  1764   assumes "integrable M f"
  1765   shows "integrable M (\<lambda>x. - f x)" "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
  1766   using assms by (auto simp: integrable_def lebesgue_integral_def)
  1767 
  1768 lemma (in measure_space) integral_of_positive_diff:
  1769   assumes integrable: "integrable M u" "integrable M v"
  1770   and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x"
  1771   shows "integrable M f" and "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
  1772 proof -
  1773   let "?f x" = "max 0 (extreal (f x))"
  1774   let "?mf x" = "max 0 (extreal (- f x))"
  1775   let "?u x" = "max 0 (extreal (u x))"
  1776   let "?v x" = "max 0 (extreal (v x))"
  1777 
  1778   from borel_measurable_diff[of u v] integrable
  1779   have f_borel: "?f \<in> borel_measurable M" and
  1780     mf_borel: "?mf \<in> borel_measurable M" and
  1781     v_borel: "?v \<in> borel_measurable M" and
  1782     u_borel: "?u \<in> borel_measurable M" and
  1783     "f \<in> borel_measurable M"
  1784     by (auto simp: f_def[symmetric] integrable_def)
  1785 
  1786   have "(\<integral>\<^isup>+ x. extreal (u x - v x) \<partial>M) \<le> integral\<^isup>P M ?u"
  1787     using pos by (auto intro!: positive_integral_mono simp: positive_integral_max_0)
  1788   moreover have "(\<integral>\<^isup>+ x. extreal (v x - u x) \<partial>M) \<le> integral\<^isup>P M ?v"
  1789     using pos by (auto intro!: positive_integral_mono simp: positive_integral_max_0)
  1790   ultimately show f: "integrable M f"
  1791     using `integrable M u` `integrable M v` `f \<in> borel_measurable M`
  1792     by (auto simp: integrable_def f_def positive_integral_max_0)
  1793 
  1794   have "\<And>x. ?u x + ?mf x = ?v x + ?f x"
  1795     unfolding f_def using pos by (simp split: split_max)
  1796   then have "(\<integral>\<^isup>+ x. ?u x + ?mf x \<partial>M) = (\<integral>\<^isup>+ x. ?v x + ?f x \<partial>M)" by simp
  1797   then have "real (integral\<^isup>P M ?u + integral\<^isup>P M ?mf) =
  1798       real (integral\<^isup>P M ?v + integral\<^isup>P M ?f)"
  1799     using positive_integral_add[OF u_borel _ mf_borel]
  1800     using positive_integral_add[OF v_borel _ f_borel]
  1801     by auto
  1802   then show "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
  1803     unfolding positive_integral_max_0
  1804     unfolding pos[THEN integral_eq_positive_integral]
  1805     using integrable f by (auto elim!: integrableE)
  1806 qed
  1807 
  1808 lemma (in measure_space) integral_linear:
  1809   assumes "integrable M f" "integrable M g" and "0 \<le> a"
  1810   shows "integrable M (\<lambda>t. a * f t + g t)"
  1811   and "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" (is ?EQ)
  1812 proof -
  1813   let "?f x" = "max 0 (extreal (f x))"
  1814   let "?g x" = "max 0 (extreal (g x))"
  1815   let "?mf x" = "max 0 (extreal (- f x))"
  1816   let "?mg x" = "max 0 (extreal (- g x))"
  1817   let "?p t" = "max 0 (a * f t) + max 0 (g t)"
  1818   let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)"
  1819 
  1820   from assms have linear:
  1821     "(\<integral>\<^isup>+ x. extreal a * ?f x + ?g x \<partial>M) = extreal a * integral\<^isup>P M ?f + integral\<^isup>P M ?g"
  1822     "(\<integral>\<^isup>+ x. extreal a * ?mf x + ?mg x \<partial>M) = extreal a * integral\<^isup>P M ?mf + integral\<^isup>P M ?mg"
  1823     by (auto intro!: positive_integral_linear simp: integrable_def)
  1824 
  1825   have *: "(\<integral>\<^isup>+x. extreal (- ?p x) \<partial>M) = 0" "(\<integral>\<^isup>+x. extreal (- ?n x) \<partial>M) = 0"
  1826     using `0 \<le> a` assms by (auto simp: positive_integral_0_iff_AE integrable_def)
  1827   have **: "\<And>x. extreal a * ?f x + ?g x = max 0 (extreal (?p x))"
  1828            "\<And>x. extreal a * ?mf x + ?mg x = max 0 (extreal (?n x))"
  1829     using `0 \<le> a` by (auto split: split_max simp: zero_le_mult_iff mult_le_0_iff)
  1830 
  1831   have "integrable M ?p" "integrable M ?n"
  1832       "\<And>t. a * f t + g t = ?p t - ?n t" "\<And>t. 0 \<le> ?p t" "\<And>t. 0 \<le> ?n t"
  1833     using linear assms unfolding integrable_def ** *
  1834     by (auto simp: positive_integral_max_0)
  1835   note diff = integral_of_positive_diff[OF this]
  1836 
  1837   show "integrable M (\<lambda>t. a * f t + g t)" by (rule diff)
  1838   from assms linear show ?EQ
  1839     unfolding diff(2) ** positive_integral_max_0
  1840     unfolding lebesgue_integral_def *
  1841     by (auto elim!: integrableE simp: field_simps)
  1842 qed
  1843 
  1844 lemma (in measure_space) integral_add[simp, intro]:
  1845   assumes "integrable M f" "integrable M g"
  1846   shows "integrable M (\<lambda>t. f t + g t)"
  1847   and "(\<integral> t. f t + g t \<partial>M) = integral\<^isup>L M f + integral\<^isup>L M g"
  1848   using assms integral_linear[where a=1] by auto
  1849 
  1850 lemma (in measure_space) integral_zero[simp, intro]:
  1851   shows "integrable M (\<lambda>x. 0)" "(\<integral> x.0 \<partial>M) = 0"
  1852   unfolding integrable_def lebesgue_integral_def
  1853   by (auto simp add: borel_measurable_const)
  1854 
  1855 lemma (in measure_space) integral_cmult[simp, intro]:
  1856   assumes "integrable M f"
  1857   shows "integrable M (\<lambda>t. a * f t)" (is ?P)
  1858   and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I)
  1859 proof -
  1860   have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f"
  1861   proof (cases rule: le_cases)
  1862     assume "0 \<le> a" show ?thesis
  1863       using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
  1864       by (simp add: integral_zero)
  1865   next
  1866     assume "a \<le> 0" hence "0 \<le> - a" by auto
  1867     have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
  1868     show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
  1869         integral_minus(1)[of "\<lambda>t. - a * f t"]
  1870       unfolding * integral_zero by simp
  1871   qed
  1872   thus ?P ?I by auto
  1873 qed
  1874 
  1875 lemma (in measure_space) integral_multc:
  1876   assumes "integrable M f"
  1877   shows "(\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
  1878   unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
  1879 
  1880 lemma (in measure_space) integral_mono_AE:
  1881   assumes fg: "integrable M f" "integrable M g"
  1882   and mono: "AE t. f t \<le> g t"
  1883   shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
  1884 proof -
  1885   have "AE x. extreal (f x) \<le> extreal (g x)"
  1886     using mono by auto
  1887   moreover have "AE x. extreal (- g x) \<le> extreal (- f x)"
  1888     using mono by auto
  1889   ultimately show ?thesis using fg
  1890     by (auto intro!: add_mono positive_integral_mono_AE real_of_extreal_positive_mono
  1891              simp: positive_integral_positive lebesgue_integral_def diff_minus)
  1892 qed
  1893 
  1894 lemma (in measure_space) integral_mono:
  1895   assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
  1896   shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
  1897   using assms by (auto intro: integral_mono_AE)
  1898 
  1899 lemma (in measure_space) integral_diff[simp, intro]:
  1900   assumes f: "integrable M f" and g: "integrable M g"
  1901   shows "integrable M (\<lambda>t. f t - g t)"
  1902   and "(\<integral> t. f t - g t \<partial>M) = integral\<^isup>L M f - integral\<^isup>L M g"
  1903   using integral_add[OF f integral_minus(1)[OF g]]
  1904   unfolding diff_minus integral_minus(2)[OF g]
  1905   by auto
  1906 
  1907 lemma (in measure_space) integral_indicator[simp, intro]:
  1908   assumes "A \<in> sets M" and "\<mu> A \<noteq> \<infinity>"
  1909   shows "integral\<^isup>L M (indicator A) = real (\<mu> A)" (is ?int)
  1910   and "integrable M (indicator A)" (is ?able)
  1911 proof -
  1912   from `A \<in> sets M` have *:
  1913     "\<And>x. extreal (indicator A x) = indicator A x"
  1914     "(\<integral>\<^isup>+x. extreal (- indicator A x) \<partial>M) = 0"
  1915     by (auto split: split_indicator simp: positive_integral_0_iff_AE one_extreal_def)
  1916   show ?int ?able
  1917     using assms unfolding lebesgue_integral_def integrable_def
  1918     by (auto simp: * positive_integral_indicator borel_measurable_indicator)
  1919 qed
  1920 
  1921 lemma (in measure_space) integral_cmul_indicator:
  1922   assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<infinity>"
  1923   shows "integrable M (\<lambda>x. c * indicator A x)" (is ?P)
  1924   and "(\<integral>x. c * indicator A x \<partial>M) = c * real (\<mu> A)" (is ?I)
  1925 proof -
  1926   show ?P
  1927   proof (cases "c = 0")
  1928     case False with assms show ?thesis by simp
  1929   qed simp
  1930 
  1931   show ?I
  1932   proof (cases "c = 0")
  1933     case False with assms show ?thesis by simp
  1934   qed simp
  1935 qed
  1936 
  1937 lemma (in measure_space) integral_setsum[simp, intro]:
  1938   assumes "\<And>n. n \<in> S \<Longrightarrow> integrable M (f n)"
  1939   shows "(\<integral>x. (\<Sum> i \<in> S. f i x) \<partial>M) = (\<Sum> i \<in> S. integral\<^isup>L M (f i))" (is "?int S")
  1940     and "integrable M (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S")
  1941 proof -
  1942   have "?int S \<and> ?I S"
  1943   proof (cases "finite S")
  1944     assume "finite S"
  1945     from this assms show ?thesis by (induct S) simp_all
  1946   qed simp
  1947   thus "?int S" and "?I S" by auto
  1948 qed
  1949 
  1950 lemma (in measure_space) integrable_abs:
  1951   assumes "integrable M f"
  1952   shows "integrable M (\<lambda> x. \<bar>f x\<bar>)"
  1953 proof -
  1954   from assms have *: "(\<integral>\<^isup>+x. extreal (- \<bar>f x\<bar>)\<partial>M) = 0"
  1955     "\<And>x. extreal \<bar>f x\<bar> = max 0 (extreal (f x)) + max 0 (extreal (- f x))"
  1956     by (auto simp: integrable_def positive_integral_0_iff_AE split: split_max)
  1957   with assms show ?thesis
  1958     by (simp add: positive_integral_add positive_integral_max_0 integrable_def)
  1959 qed
  1960 
  1961 lemma (in measure_space) integral_subalgebra:
  1962   assumes borel: "f \<in> borel_measurable N"
  1963   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A" and sa: "sigma_algebra N"
  1964   shows "integrable N f \<longleftrightarrow> integrable M f" (is ?P)
  1965     and "integral\<^isup>L N f = integral\<^isup>L M f" (is ?I)
  1966 proof -
  1967   interpret N: measure_space N using measure_space_subalgebra[OF sa N] .
  1968   have "(\<integral>\<^isup>+ x. max 0 (extreal (f x)) \<partial>N) = (\<integral>\<^isup>+ x. max 0 (extreal (f x)) \<partial>M)"
  1969        "(\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>N) = (\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>M)"
  1970     using borel by (auto intro!: positive_integral_subalgebra N sa)
  1971   moreover have "f \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable N"
  1972     using assms unfolding measurable_def by auto
  1973   ultimately show ?P ?I
  1974     by (auto simp: integrable_def lebesgue_integral_def positive_integral_max_0)
  1975 qed
  1976 
  1977 lemma (in measure_space) integrable_bound:
  1978   assumes "integrable M f"
  1979   and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
  1980     "\<And>x. x \<in> space M \<Longrightarrow> \<bar>g x\<bar> \<le> f x"
  1981   assumes borel: "g \<in> borel_measurable M"
  1982   shows "integrable M g"
  1983 proof -
  1984   have "(\<integral>\<^isup>+ x. extreal (g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. extreal \<bar>g x\<bar> \<partial>M)"
  1985     by (auto intro!: positive_integral_mono)
  1986   also have "\<dots> \<le> (\<integral>\<^isup>+ x. extreal (f x) \<partial>M)"
  1987     using f by (auto intro!: positive_integral_mono)
  1988   also have "\<dots> < \<infinity>"
  1989     using `integrable M f` unfolding integrable_def by auto
  1990   finally have pos: "(\<integral>\<^isup>+ x. extreal (g x) \<partial>M) < \<infinity>" .
  1991 
  1992   have "(\<integral>\<^isup>+ x. extreal (- g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. extreal (\<bar>g x\<bar>) \<partial>M)"
  1993     by (auto intro!: positive_integral_mono)
  1994   also have "\<dots> \<le> (\<integral>\<^isup>+ x. extreal (f x) \<partial>M)"
  1995     using f by (auto intro!: positive_integral_mono)
  1996   also have "\<dots> < \<infinity>"
  1997     using `integrable M f` unfolding integrable_def by auto
  1998   finally have neg: "(\<integral>\<^isup>+ x. extreal (- g x) \<partial>M) < \<infinity>" .
  1999 
  2000   from neg pos borel show ?thesis
  2001     unfolding integrable_def by auto
  2002 qed
  2003 
  2004 lemma (in measure_space) integrable_abs_iff:
  2005   "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda> x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
  2006   by (auto intro!: integrable_bound[where g=f] integrable_abs)
  2007 
  2008 lemma (in measure_space) integrable_max:
  2009   assumes int: "integrable M f" "integrable M g"
  2010   shows "integrable M (\<lambda> x. max (f x) (g x))"
  2011 proof (rule integrable_bound)
  2012   show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
  2013     using int by (simp add: integrable_abs)
  2014   show "(\<lambda>x. max (f x) (g x)) \<in> borel_measurable M"
  2015     using int unfolding integrable_def by auto
  2016 next
  2017   fix x assume "x \<in> space M"
  2018   show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>max (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
  2019     by auto
  2020 qed
  2021 
  2022 lemma (in measure_space) integrable_min:
  2023   assumes int: "integrable M f" "integrable M g"
  2024   shows "integrable M (\<lambda> x. min (f x) (g x))"
  2025 proof (rule integrable_bound)
  2026   show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
  2027     using int by (simp add: integrable_abs)
  2028   show "(\<lambda>x. min (f x) (g x)) \<in> borel_measurable M"
  2029     using int unfolding integrable_def by auto
  2030 next
  2031   fix x assume "x \<in> space M"
  2032   show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>min (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
  2033     by auto
  2034 qed
  2035 
  2036 lemma (in measure_space) integral_triangle_inequality:
  2037   assumes "integrable M f"
  2038   shows "\<bar>integral\<^isup>L M f\<bar> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
  2039 proof -
  2040   have "\<bar>integral\<^isup>L M f\<bar> = max (integral\<^isup>L M f) (- integral\<^isup>L M f)" by auto
  2041   also have "\<dots> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
  2042       using assms integral_minus(2)[of f, symmetric]
  2043       by (auto intro!: integral_mono integrable_abs simp del: integral_minus)
  2044   finally show ?thesis .
  2045 qed
  2046 
  2047 lemma (in measure_space) integral_positive:
  2048   assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
  2049   shows "0 \<le> integral\<^isup>L M f"
  2050 proof -
  2051   have "0 = (\<integral>x. 0 \<partial>M)" by (auto simp: integral_zero)
  2052   also have "\<dots> \<le> integral\<^isup>L M f"
  2053     using assms by (rule integral_mono[OF integral_zero(1)])
  2054   finally show ?thesis .
  2055 qed
  2056 
  2057 lemma (in measure_space) integral_monotone_convergence_pos:
  2058   assumes i: "\<And>i. integrable M (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
  2059   and pos: "\<And>x i. 0 \<le> f i x"
  2060   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
  2061   and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
  2062   shows "integrable M u"
  2063   and "integral\<^isup>L M u = x"
  2064 proof -
  2065   { fix x have "0 \<le> u x"
  2066       using mono pos[of 0 x] incseq_le[OF _ lim, of x 0]
  2067       by (simp add: mono_def incseq_def) }
  2068   note pos_u = this
  2069 
  2070   have SUP_F: "\<And>x. (SUP n. extreal (f n x)) = extreal (u x)"
  2071     unfolding SUP_eq_LIMSEQ[OF mono] by (rule lim)
  2072 
  2073   have borel_f: "\<And>i. (\<lambda>x. extreal (f i x)) \<in> borel_measurable M"
  2074     using i unfolding integrable_def by auto
  2075   hence "(\<lambda>x. SUP i. extreal (f i x)) \<in> borel_measurable M"
  2076     by auto
  2077   hence borel_u: "u \<in> borel_measurable M"
  2078     by (auto simp: borel_measurable_extreal_iff SUP_F)
  2079 
  2080   hence [simp]: "\<And>i. (\<integral>\<^isup>+x. extreal (- f i x) \<partial>M) = 0" "(\<integral>\<^isup>+x. extreal (- u x) \<partial>M) = 0"
  2081     using i borel_u pos pos_u by (auto simp: positive_integral_0_iff_AE integrable_def)
  2082 
  2083   have integral_eq: "\<And>n. (\<integral>\<^isup>+ x. extreal (f n x) \<partial>M) = extreal (integral\<^isup>L M (f n))"
  2084     using i positive_integral_positive by (auto simp: extreal_real lebesgue_integral_def integrable_def)
  2085 
  2086   have pos_integral: "\<And>n. 0 \<le> integral\<^isup>L M (f n)"
  2087     using pos i by (auto simp: integral_positive)
  2088   hence "0 \<le> x"
  2089     using LIMSEQ_le_const[OF ilim, of 0] by auto
  2090 
  2091   from mono pos i have pI: "(\<integral>\<^isup>+ x. extreal (u x) \<partial>M) = (SUP n. (\<integral>\<^isup>+ x. extreal (f n x) \<partial>M))"
  2092     by (auto intro!: positive_integral_monotone_convergence_SUP
  2093       simp: integrable_def incseq_mono incseq_Suc_iff le_fun_def SUP_F[symmetric])
  2094   also have "\<dots> = extreal x" unfolding integral_eq
  2095   proof (rule SUP_eq_LIMSEQ[THEN iffD2])
  2096     show "mono (\<lambda>n. integral\<^isup>L M (f n))"
  2097       using mono i by (auto simp: mono_def intro!: integral_mono)
  2098     show "(\<lambda>n. integral\<^isup>L M (f n)) ----> x" using ilim .
  2099   qed
  2100   finally show  "integrable M u" "integral\<^isup>L M u = x" using borel_u `0 \<le> x`
  2101     unfolding integrable_def lebesgue_integral_def by auto
  2102 qed
  2103 
  2104 lemma (in measure_space) integral_monotone_convergence:
  2105   assumes f: "\<And>i. integrable M (f i)" and "mono f"
  2106   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
  2107   and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
  2108   shows "integrable M u"
  2109   and "integral\<^isup>L M u = x"
  2110 proof -
  2111   have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
  2112       using f by (auto intro!: integral_diff)
  2113   have 2: "\<And>x. mono (\<lambda>n. f n x - f 0 x)" using `mono f`
  2114       unfolding mono_def le_fun_def by auto
  2115   have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
  2116       unfolding mono_def le_fun_def by (auto simp: field_simps)
  2117   have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
  2118     using lim by (auto intro!: LIMSEQ_diff)
  2119   have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)"
  2120     using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
  2121   note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
  2122   have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
  2123     using diff(1) f by (rule integral_add(1))
  2124   with diff(2) f show "integrable M u" "integral\<^isup>L M u = x"
  2125     by (auto simp: integral_diff)
  2126 qed
  2127 
  2128 lemma (in measure_space) integral_0_iff:
  2129   assumes "integrable M f"
  2130   shows "(\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
  2131 proof -
  2132   have *: "(\<integral>\<^isup>+x. extreal (- \<bar>f x\<bar>) \<partial>M) = 0"
  2133     using assms by (auto simp: positive_integral_0_iff_AE integrable_def)
  2134   have "integrable M (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs)
  2135   hence "(\<lambda>x. extreal (\<bar>f x\<bar>)) \<in> borel_measurable M"
  2136     "(\<integral>\<^isup>+ x. extreal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" unfolding integrable_def by auto
  2137   from positive_integral_0_iff[OF this(1)] this(2)
  2138   show ?thesis unfolding lebesgue_integral_def *
  2139     using positive_integral_positive[of "\<lambda>x. extreal \<bar>f x\<bar>"]
  2140     by (auto simp add: real_of_extreal_eq_0)
  2141 qed
  2142 
  2143 lemma (in measure_space) positive_integral_PInf:
  2144   assumes f: "f \<in> borel_measurable M"
  2145   and not_Inf: "integral\<^isup>P M f \<noteq> \<infinity>"
  2146   shows "\<mu> (f -` {\<infinity>} \<inter> space M) = 0"
  2147 proof -
  2148   have "\<infinity> * \<mu> (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^isup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
  2149     using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
  2150   also have "\<dots> \<le> integral\<^isup>P M (\<lambda>x. max 0 (f x))"
  2151     by (auto intro!: positive_integral_mono simp: indicator_def max_def)
  2152   finally have "\<infinity> * \<mu> (f -` {\<infinity>} \<inter> space M) \<le> integral\<^isup>P M f"
  2153     by (simp add: positive_integral_max_0)
  2154   moreover have "0 \<le> \<mu> (f -` {\<infinity>} \<inter> space M)"
  2155     using f by (simp add: measurable_sets)
  2156   ultimately show ?thesis
  2157     using assms by (auto split: split_if_asm)
  2158 qed
  2159 
  2160 lemma (in measure_space) positive_integral_PInf_AE:
  2161   assumes "f \<in> borel_measurable M" "integral\<^isup>P M f \<noteq> \<infinity>" shows "AE x. f x \<noteq> \<infinity>"
  2162 proof (rule AE_I)
  2163   show "\<mu> (f -` {\<infinity>} \<inter> space M) = 0"
  2164     by (rule positive_integral_PInf[OF assms])
  2165   show "f -` {\<infinity>} \<inter> space M \<in> sets M"
  2166     using assms by (auto intro: borel_measurable_vimage)
  2167 qed auto
  2168 
  2169 lemma (in measure_space) simple_integral_PInf:
  2170   assumes "simple_function M f" "\<And>x. 0 \<le> f x"
  2171   and "integral\<^isup>S M f \<noteq> \<infinity>"
  2172   shows "\<mu> (f -` {\<infinity>} \<inter> space M) = 0"
  2173 proof (rule positive_integral_PInf)
  2174   show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
  2175   show "integral\<^isup>P M f \<noteq> \<infinity>"
  2176     using assms by (simp add: positive_integral_eq_simple_integral)
  2177 qed
  2178 
  2179 lemma (in measure_space) integral_real:
  2180   "AE x. \<bar>f x\<bar> \<noteq> \<infinity> \<Longrightarrow> (\<integral>x. real (f x) \<partial>M) = real (integral\<^isup>P M f) - real (integral\<^isup>P M (\<lambda>x. - f x))"
  2181   using assms unfolding lebesgue_integral_def
  2182   by (subst (1 2) positive_integral_cong_AE) (auto simp add: extreal_real)
  2183 
  2184 lemma liminf_extreal_cminus:
  2185   fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
  2186   shows "liminf (\<lambda>x. c - f x) = c - limsup f"
  2187 proof (cases c)
  2188   case PInf then show ?thesis by (simp add: Liminf_const)
  2189 next
  2190   case (real r) then show ?thesis
  2191     unfolding liminf_SUPR_INFI limsup_INFI_SUPR
  2192     apply (subst INFI_extreal_cminus)
  2193     apply auto
  2194     apply (subst SUPR_extreal_cminus)
  2195     apply auto
  2196     done
  2197 qed (insert `c \<noteq> -\<infinity>`, simp)
  2198 
  2199 lemma (in measure_space) integral_dominated_convergence:
  2200   assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
  2201   and w: "integrable M w"
  2202   and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
  2203   shows "integrable M u'"
  2204   and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
  2205   and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
  2206 proof -
  2207   { fix x j assume x: "x \<in> space M"
  2208     from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs)
  2209     from LIMSEQ_le_const2[OF this]
  2210     have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto }
  2211   note u'_bound = this
  2212 
  2213   from u[unfolded integrable_def]
  2214   have u'_borel: "u' \<in> borel_measurable M"
  2215     using u' by (blast intro: borel_measurable_LIMSEQ[of u])
  2216 
  2217   { fix x assume x: "x \<in> space M"
  2218     then have "0 \<le> \<bar>u 0 x\<bar>" by auto
  2219     also have "\<dots> \<le> w x" using bound[OF x] by auto
  2220     finally have "0 \<le> w x" . }
  2221   note w_pos = this
  2222 
  2223   show "integrable M u'"
  2224   proof (rule integrable_bound)
  2225     show "integrable M w" by fact
  2226     show "u' \<in> borel_measurable M" by fact
  2227   next
  2228     fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact
  2229     show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
  2230   qed
  2231 
  2232   let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>"
  2233   have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)"
  2234     using w u `integrable M u'`
  2235     by (auto intro!: integral_add integral_diff integral_cmult integrable_abs)
  2236 
  2237   { fix j x assume x: "x \<in> space M"
  2238     have "\<bar>u j x - u' x\<bar> \<le> \<bar>u j x\<bar> + \<bar>u' x\<bar>" by auto
  2239     also have "\<dots> \<le> w x + w x"
  2240       by (rule add_mono[OF bound[OF x] u'_bound[OF x]])
  2241     finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp }
  2242   note diff_less_2w = this
  2243 
  2244   have PI_diff: "\<And>n. (\<integral>\<^isup>+ x. extreal (?diff n x) \<partial>M) =
  2245     (\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"
  2246     using diff w diff_less_2w w_pos
  2247     by (subst positive_integral_diff[symmetric])
  2248        (auto simp: integrable_def intro!: positive_integral_cong)
  2249 
  2250   have "integrable M (\<lambda>x. 2 * w x)"
  2251     using w by (auto intro: integral_cmult)
  2252   hence I2w_fin: "(\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M) \<noteq> \<infinity>" and
  2253     borel_2w: "(\<lambda>x. extreal (2 * w x)) \<in> borel_measurable M"
  2254     unfolding integrable_def by auto
  2255 
  2256   have "limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M) = 0" (is "limsup ?f = 0")
  2257   proof cases
  2258     assume eq_0: "(\<integral>\<^isup>+ x. max 0 (extreal (2 * w x)) \<partial>M) = 0" (is "?wx = 0")
  2259     { fix n
  2260       have "?f n \<le> ?wx" (is "integral\<^isup>P M ?f' \<le> _")
  2261         using diff_less_2w[of _ n] unfolding positive_integral_max_0
  2262         by (intro positive_integral_mono) auto
  2263       then have "?f n = 0"
  2264         using positive_integral_positive[of ?f'] eq_0 by auto }
  2265     then show ?thesis by (simp add: Limsup_const)
  2266   next
  2267     assume neq_0: "(\<integral>\<^isup>+ x. max 0 (extreal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
  2268     have "0 = limsup (\<lambda>n. 0 :: extreal)" by (simp add: Limsup_const)
  2269     also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"
  2270       by (intro limsup_mono positive_integral_positive)
  2271     finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)" .
  2272     have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (extreal (?diff n x))) \<partial>M)"
  2273     proof (rule positive_integral_cong)
  2274       fix x assume x: "x \<in> space M"
  2275       show "max 0 (extreal (2 * w x)) = liminf (\<lambda>n. max 0 (extreal (?diff n x)))"
  2276         unfolding extreal_max_0
  2277       proof (rule lim_imp_Liminf[symmetric], unfold lim_extreal)
  2278         have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
  2279           using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs)
  2280         then show "(\<lambda>i. max 0 (?diff i x)) ----> max 0 (2 * w x)"
  2281           by (auto intro!: tendsto_real_max simp add: lim_extreal)
  2282       qed (rule trivial_limit_sequentially)
  2283     qed
  2284     also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^isup>+ x. max 0 (extreal (?diff n x)) \<partial>M)"
  2285       using u'_borel w u unfolding integrable_def
  2286       by (intro positive_integral_lim_INF) (auto intro!: positive_integral_lim_INF)
  2287     also have "\<dots> = (\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M) -
  2288         limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"
  2289       unfolding PI_diff positive_integral_max_0
  2290       using positive_integral_positive[of "\<lambda>x. extreal (2 * w x)"]
  2291       by (subst liminf_extreal_cminus) auto
  2292     finally show ?thesis
  2293       using neq_0 I2w_fin positive_integral_positive[of "\<lambda>x. extreal (2 * w x)"] pos
  2294       unfolding positive_integral_max_0
  2295       by (cases rule: extreal2_cases[of "\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M" "limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"])
  2296          auto
  2297   qed
  2298 
  2299   have "liminf ?f \<le> limsup ?f"
  2300     by (intro extreal_Liminf_le_Limsup trivial_limit_sequentially)
  2301   moreover
  2302   { have "0 = liminf (\<lambda>n. 0 :: extreal)" by (simp add: Liminf_const)
  2303     also have "\<dots> \<le> liminf ?f"
  2304       by (intro liminf_mono positive_integral_positive)
  2305     finally have "0 \<le> liminf ?f" . }
  2306   ultimately have liminf_limsup_eq: "liminf ?f = extreal 0" "limsup ?f = extreal 0"
  2307     using `limsup ?f = 0` by auto
  2308   have "\<And>n. (\<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M) = extreal (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)"
  2309     using diff positive_integral_positive
  2310     by (subst integral_eq_positive_integral) (auto simp: extreal_real integrable_def)
  2311   then show ?lim_diff
  2312     using extreal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
  2313     by (simp add: lim_extreal)
  2314 
  2315   show ?lim
  2316   proof (rule LIMSEQ_I)
  2317     fix r :: real assume "0 < r"
  2318     from LIMSEQ_D[OF `?lim_diff` this]
  2319     obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M) < r"
  2320       using diff by (auto simp: integral_positive)
  2321 
  2322     show "\<exists>N. \<forall>n\<ge>N. norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r"
  2323     proof (safe intro!: exI[of _ N])
  2324       fix n assume "N \<le> n"
  2325       have "\<bar>integral\<^isup>L M (u n) - integral\<^isup>L M u'\<bar> = \<bar>(\<integral>x. u n x - u' x \<partial>M)\<bar>"
  2326         using u `integrable M u'` by (auto simp: integral_diff)
  2327       also have "\<dots> \<le> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)" using u `integrable M u'`
  2328         by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff)
  2329       also note N[OF `N \<le> n`]
  2330       finally show "norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r" by simp
  2331     qed
  2332   qed
  2333 qed
  2334 
  2335 lemma (in measure_space) integral_sums:
  2336   assumes borel: "\<And>i. integrable M (f i)"
  2337   and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
  2338   and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
  2339   shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
  2340   and "(\<lambda>i. integral\<^isup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is ?integral)
  2341 proof -
  2342   have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
  2343     using summable unfolding summable_def by auto
  2344   from bchoice[OF this]
  2345   obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
  2346 
  2347   let "?w y" = "if y \<in> space M then w y else 0"
  2348 
  2349   obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
  2350     using sums unfolding summable_def ..
  2351 
  2352   have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)"
  2353     using borel by (auto intro!: integral_setsum)
  2354 
  2355   { fix j x assume [simp]: "x \<in> space M"
  2356     have "\<bar>\<Sum>i = 0..< j. f i x\<bar> \<le> (\<Sum>i = 0..< j. \<bar>f i x\<bar>)" by (rule setsum_abs)
  2357     also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
  2358     finally have "\<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x" by simp }
  2359   note 2 = this
  2360 
  2361   have 3: "integrable M ?w"
  2362   proof (rule integral_monotone_convergence(1))
  2363     let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
  2364     let "?w' n y" = "if y \<in> space M then ?F n y else 0"
  2365     have "\<And>n. integrable M (?F n)"
  2366       using borel by (auto intro!: integral_setsum integrable_abs)
  2367     thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
  2368     show "mono ?w'"
  2369       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
  2370     { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
  2371         using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
  2372     have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
  2373       using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
  2374     from abs_sum
  2375     show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
  2376   qed
  2377 
  2378   from summable[THEN summable_rabs_cancel]
  2379   have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
  2380     by (auto intro: summable_sumr_LIMSEQ_suminf)
  2381 
  2382   note int = integral_dominated_convergence(1,3)[OF 1 2 3 4]
  2383 
  2384   from int show "integrable M ?S" by simp
  2385 
  2386   show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel]
  2387     using int(2) by simp
  2388 qed
  2389 
  2390 section "Lebesgue integration on countable spaces"
  2391 
  2392 lemma (in measure_space) integral_on_countable:
  2393   assumes f: "f \<in> borel_measurable M"
  2394   and bij: "bij_betw enum S (f ` space M)"
  2395   and enum_zero: "enum ` (-S) \<subseteq> {0}"
  2396   and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<infinity>"
  2397   and abs_summable: "summable (\<lambda>r. \<bar>enum r * real (\<mu> (f -` {enum r} \<inter> space M))\<bar>)"
  2398   shows "integrable M f"
  2399   and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral\<^isup>L M f" (is ?sums)
  2400 proof -
  2401   let "?A r" = "f -` {enum r} \<inter> space M"
  2402   let "?F r x" = "enum r * indicator (?A r) x"
  2403   have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral\<^isup>L M (?F r)"
  2404     using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
  2405 
  2406   { fix x assume "x \<in> space M"
  2407     hence "f x \<in> enum ` S" using bij unfolding bij_betw_def by auto
  2408     then obtain i where "i\<in>S" "enum i = f x" by auto
  2409     have F: "\<And>j. ?F j x = (if j = i then f x else 0)"
  2410     proof cases
  2411       fix j assume "j = i"
  2412       thus "?thesis j" using `x \<in> space M` `enum i = f x` by (simp add: indicator_def)
  2413     next
  2414       fix j assume "j \<noteq> i"
  2415       show "?thesis j" using bij `i \<in> S` `j \<noteq> i` `enum i = f x` enum_zero
  2416         by (cases "j \<in> S") (auto simp add: indicator_def bij_betw_def inj_on_def)
  2417     qed
  2418     hence F_abs: "\<And>j. \<bar>if j = i then f x else 0\<bar> = (if j = i then \<bar>f x\<bar> else 0)" by auto
  2419     have "(\<lambda>i. ?F i x) sums f x"
  2420          "(\<lambda>i. \<bar>?F i x\<bar>) sums \<bar>f x\<bar>"
  2421       by (auto intro!: sums_single simp: F F_abs) }
  2422   note F_sums_f = this(1) and F_abs_sums_f = this(2)
  2423 
  2424   have int_f: "integral\<^isup>L M f = (\<integral>x. (\<Sum>r. ?F r x) \<partial>M)" "integrable M f = integrable M (\<lambda>x. \<Sum>r. ?F r x)"
  2425     using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff)
  2426 
  2427   { fix r
  2428     have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x \<partial>M)"
  2429       by (auto simp: indicator_def intro!: integral_cong)
  2430     also have "\<dots> = \<bar>enum r\<bar> * real (\<mu> (?A r))"
  2431       using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
  2432     finally have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = \<bar>enum r * real (\<mu> (?A r))\<bar>"
  2433       using f by (subst (2) abs_mult_pos[symmetric]) (auto intro!: real_of_extreal_pos measurable_sets) }
  2434   note int_abs_F = this
  2435 
  2436   have 1: "\<And>i. integrable M (\<lambda>x. ?F i x)"
  2437     using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
  2438 
  2439   have 2: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>?F i x\<bar>)"
  2440     using F_abs_sums_f unfolding sums_iff by auto
  2441 
  2442   from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
  2443   show ?sums unfolding enum_eq int_f by simp
  2444 
  2445   from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
  2446   show "integrable M f" unfolding int_f by simp
  2447 qed
  2448 
  2449 section "Lebesgue integration on finite space"
  2450 
  2451 lemma (in measure_space) integral_on_finite:
  2452   assumes f: "f \<in> borel_measurable M" and finite: "finite (f`space M)"
  2453   and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<infinity>"
  2454   shows "integrable M f"
  2455   and "(\<integral>x. f x \<partial>M) =
  2456     (\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
  2457 proof -
  2458   let "?A r" = "f -` {r} \<inter> space M"
  2459   let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x"
  2460 
  2461   { fix x assume "x \<in> space M"
  2462     have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)"
  2463       using finite `x \<in> space M` by (simp add: setsum_cases)
  2464     also have "\<dots> = ?S x"
  2465       by (auto intro!: setsum_cong)
  2466     finally have "f x = ?S x" . }
  2467   note f_eq = this
  2468 
  2469   have f_eq_S: "integrable M f \<longleftrightarrow> integrable M ?S" "integral\<^isup>L M f = integral\<^isup>L M ?S"
  2470     by (auto intro!: integrable_cong integral_cong simp only: f_eq)
  2471 
  2472   show "integrable M f" ?integral using fin f f_eq_S
  2473     by (simp_all add: integral_cmul_indicator borel_measurable_vimage)
  2474 qed
  2475 
  2476 lemma (in finite_measure_space) simple_function_finite[simp, intro]: "simple_function M f"
  2477   unfolding simple_function_def using finite_space by auto
  2478 
  2479 lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
  2480   by (auto intro: borel_measurable_simple_function)
  2481 
  2482 lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
  2483   assumes pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
  2484   shows "integral\<^isup>P M f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
  2485 proof -
  2486   have *: "integral\<^isup>P M f = (\<integral>\<^isup>+ x. (\<Sum>y\<in>space M. f y * indicator {y} x) \<partial>M)"
  2487     by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
  2488   show ?thesis unfolding * using borel_measurable_finite[of f] pos
  2489     by (simp add: positive_integral_setsum positive_integral_cmult_indicator)
  2490 qed
  2491 
  2492 lemma (in finite_measure_space) integral_finite_singleton:
  2493   shows "integrable M f"
  2494   and "integral\<^isup>L M f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
  2495 proof -
  2496   have *:
  2497     "(\<integral>\<^isup>+ x. max 0 (extreal (f x)) \<partial>M) = (\<Sum>x \<in> space M. max 0 (extreal (f x)) * \<mu> {x})"
  2498     "(\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>M) = (\<Sum>x \<in> space M. max 0 (extreal (- f x)) * \<mu> {x})"
  2499     by (simp_all add: positive_integral_finite_eq_setsum)
  2500   then show "integrable M f" using finite_space finite_measure
  2501     by (simp add: setsum_Pinfty integrable_def positive_integral_max_0
  2502              split: split_max)
  2503   show ?I using finite_measure *
  2504     apply (simp add: positive_integral_max_0 lebesgue_integral_def)
  2505     apply (subst (1 2) setsum_real_of_extreal[symmetric])
  2506     apply (simp_all split: split_max add: setsum_subtractf[symmetric])
  2507     apply (intro setsum_cong[OF refl])
  2508     apply (simp split: split_max)
  2509     done
  2510 qed
  2511 
  2512 end