src/HOL/Probability/Bochner_Integration.thy
author hoelzl
Thu Jan 22 14:51:08 2015 +0100 (2015-01-22)
changeset 59425 c5e79df8cc21
parent 59357 f366643536cd
child 59452 2538b2c51769
permissions -rw-r--r--
import general thms from Density_Compiler
     1 (*  Title:      HOL/Probability/Bochner_Integration.thy
     2     Author:     Johannes Hölzl, TU München
     3 *)
     4 
     5 section {* Bochner Integration for Vector-Valued Functions *}
     6 
     7 theory Bochner_Integration
     8   imports Finite_Product_Measure
     9 begin
    10 
    11 text {*
    12 
    13 In the following development of the Bochner integral we use second countable topologies instead
    14 of separable spaces. A second countable topology is also separable.
    15 
    16 *}
    17 
    18 lemma borel_measurable_implies_sequence_metric:
    19   fixes f :: "'a \<Rightarrow> 'b :: {metric_space, second_countable_topology}"
    20   assumes [measurable]: "f \<in> borel_measurable M"
    21   shows "\<exists>F. (\<forall>i. simple_function M (F i)) \<and> (\<forall>x\<in>space M. (\<lambda>i. F i x) ----> f x) \<and>
    22     (\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)"
    23 proof -
    24   obtain D :: "'b set" where "countable D" and D: "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
    25     by (erule countable_dense_setE)
    26 
    27   def e \<equiv> "from_nat_into D"
    28   { fix n x
    29     obtain d where "d \<in> D" and d: "d \<in> ball x (1 / Suc n)"
    30       using D[of "ball x (1 / Suc n)"] by auto
    31     from `d \<in> D` D[of UNIV] `countable D` obtain i where "d = e i"
    32       unfolding e_def by (auto dest: from_nat_into_surj)
    33     with d have "\<exists>i. dist x (e i) < 1 / Suc n"
    34       by auto }
    35   note e = this
    36 
    37   def A \<equiv> "\<lambda>m n. {x\<in>space M. dist (f x) (e n) < 1 / (Suc m) \<and> 1 / (Suc m) \<le> dist (f x) z}"
    38   def B \<equiv> "\<lambda>m. disjointed (A m)"
    39   
    40   def m \<equiv> "\<lambda>N x. Max {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}"
    41   def F \<equiv> "\<lambda>N::nat. \<lambda>x. if (\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)) \<and> (\<exists>n\<le>N. x \<in> B (m N x) n) 
    42     then e (LEAST n. x \<in> B (m N x) n) else z"
    43 
    44   have B_imp_A[intro, simp]: "\<And>x m n. x \<in> B m n \<Longrightarrow> x \<in> A m n"
    45     using disjointed_subset[of "A m" for m] unfolding B_def by auto
    46 
    47   { fix m
    48     have "\<And>n. A m n \<in> sets M"
    49       by (auto simp: A_def)
    50     then have "\<And>n. B m n \<in> sets M"
    51       using sets.range_disjointed_sets[of "A m" M] by (auto simp: B_def) }
    52   note this[measurable]
    53 
    54   { fix N i x assume "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)"
    55     then have "m N x \<in> {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}"
    56       unfolding m_def by (intro Max_in) auto
    57     then have "m N x \<le> N" "\<exists>n\<le>N. x \<in> B (m N x) n"
    58       by auto }
    59   note m = this
    60 
    61   { fix j N i x assume "j \<le> N" "i \<le> N" "x \<in> B j i"
    62     then have "j \<le> m N x"
    63       unfolding m_def by (intro Max_ge) auto }
    64   note m_upper = this
    65 
    66   show ?thesis
    67     unfolding simple_function_def
    68   proof (safe intro!: exI[of _ F])
    69     have [measurable]: "\<And>i. F i \<in> borel_measurable M"
    70       unfolding F_def m_def by measurable
    71     show "\<And>x i. F i -` {x} \<inter> space M \<in> sets M"
    72       by measurable
    73 
    74     { fix i
    75       { fix n x assume "x \<in> B (m i x) n"
    76         then have "(LEAST n. x \<in> B (m i x) n) \<le> n"
    77           by (intro Least_le)
    78         also assume "n \<le> i" 
    79         finally have "(LEAST n. x \<in> B (m i x) n) \<le> i" . }
    80       then have "F i ` space M \<subseteq> {z} \<union> e ` {.. i}"
    81         by (auto simp: F_def)
    82       then show "finite (F i ` space M)"
    83         by (rule finite_subset) auto }
    84     
    85     { fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n"
    86       then have 1: "\<exists>m\<le>N. x \<in> (\<Union> n\<le>N. B m n)" by auto
    87       from m[OF this] obtain n where n: "m N x \<le> N" "n \<le> N" "x \<in> B (m N x) n" by auto
    88       moreover
    89       def L \<equiv> "LEAST n. x \<in> B (m N x) n"
    90       have "dist (f x) (e L) < 1 / Suc (m N x)"
    91       proof -
    92         have "x \<in> B (m N x) L"
    93           using n(3) unfolding L_def by (rule LeastI)
    94         then have "x \<in> A (m N x) L"
    95           by auto
    96         then show ?thesis
    97           unfolding A_def by simp
    98       qed
    99       ultimately have "dist (f x) (F N x) < 1 / Suc (m N x)"
   100         by (auto simp add: F_def L_def) }
   101     note * = this
   102 
   103     fix x assume "x \<in> space M"
   104     show "(\<lambda>i. F i x) ----> f x"
   105     proof cases
   106       assume "f x = z"
   107       then have "\<And>i n. x \<notin> A i n"
   108         unfolding A_def by auto
   109       then have "\<And>i. F i x = z"
   110         by (auto simp: F_def)
   111       then show ?thesis
   112         using `f x = z` by auto
   113     next
   114       assume "f x \<noteq> z"
   115 
   116       show ?thesis
   117       proof (rule tendstoI)
   118         fix e :: real assume "0 < e"
   119         with `f x \<noteq> z` obtain n where "1 / Suc n < e" "1 / Suc n < dist (f x) z"
   120           by (metis dist_nz order_less_trans neq_iff nat_approx_posE)
   121         with `x\<in>space M` `f x \<noteq> z` have "x \<in> (\<Union>i. B n i)"
   122           unfolding A_def B_def UN_disjointed_eq using e by auto
   123         then obtain i where i: "x \<in> B n i" by auto
   124 
   125         show "eventually (\<lambda>i. dist (F i x) (f x) < e) sequentially"
   126           using eventually_ge_at_top[of "max n i"]
   127         proof eventually_elim
   128           fix j assume j: "max n i \<le> j"
   129           with i have "dist (f x) (F j x) < 1 / Suc (m j x)"
   130             by (intro *[OF _ _ i]) auto
   131           also have "\<dots> \<le> 1 / Suc n"
   132             using j m_upper[OF _ _ i]
   133             by (auto simp: field_simps)
   134           also note `1 / Suc n < e`
   135           finally show "dist (F j x) (f x) < e"
   136             by (simp add: less_imp_le dist_commute)
   137         qed
   138       qed
   139     qed
   140     fix i 
   141     { fix n m assume "x \<in> A n m"
   142       then have "dist (e m) (f x) + dist (f x) z \<le> 2 * dist (f x) z"
   143         unfolding A_def by (auto simp: dist_commute)
   144       also have "dist (e m) z \<le> dist (e m) (f x) + dist (f x) z"
   145         by (rule dist_triangle)
   146       finally (xtrans) have "dist (e m) z \<le> 2 * dist (f x) z" . }
   147     then show "dist (F i x) z \<le> 2 * dist (f x) z"
   148       unfolding F_def
   149       apply auto
   150       apply (rule LeastI2)
   151       apply auto
   152       done
   153   qed
   154 qed
   155 
   156 lemma real_indicator: "real (indicator A x :: ereal) = indicator A x"
   157   unfolding indicator_def by auto
   158 
   159 lemma split_indicator_asm:
   160   "P (indicator S x) \<longleftrightarrow> \<not> ((x \<in> S \<and> \<not> P 1) \<or> (x \<notin> S \<and> \<not> P 0))"
   161   unfolding indicator_def by auto
   162 
   163 lemma
   164   fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
   165   shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator (B x) (g x)) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
   166   and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator (B x) (g x) * f x) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
   167   unfolding indicator_def
   168   using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm)
   169 
   170 lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
   171   fixes P :: "('a \<Rightarrow> real) \<Rightarrow> bool"
   172   assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
   173   assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
   174   assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
   175   assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
   176   assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. U i x) ----> u x) \<Longrightarrow> P u"
   177   shows "P u"
   178 proof -
   179   have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M" using u by auto
   180   from borel_measurable_implies_simple_function_sequence'[OF this]
   181   obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
   182     sup: "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x"
   183     by blast
   184 
   185   def U' \<equiv> "\<lambda>i x. indicator (space M) x * real (U i x)"
   186   then have U'_sf[measurable]: "\<And>i. simple_function M (U' i)"
   187     using U by (auto intro!: simple_function_compose1[where g=real])
   188 
   189   show "P u"
   190   proof (rule seq)
   191     fix i show "U' i \<in> borel_measurable M" "\<And>x. 0 \<le> U' i x"
   192       using U nn by (auto
   193           intro: borel_measurable_simple_function 
   194           intro!: borel_measurable_real_of_ereal real_of_ereal_pos borel_measurable_times
   195           simp: U'_def zero_le_mult_iff)
   196     show "incseq U'"
   197       using U(2,3) nn
   198       by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def
   199                intro!: real_of_ereal_positive_mono)
   200   next
   201     fix x assume x: "x \<in> space M"
   202     have "(\<lambda>i. U i x) ----> (SUP i. U i x)"
   203       using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def)
   204     moreover have "(\<lambda>i. U i x) = (\<lambda>i. ereal (U' i x))"
   205       using x nn U(3) by (auto simp: fun_eq_iff U'_def ereal_real image_iff eq_commute)
   206     moreover have "(SUP i. U i x) = ereal (u x)"
   207       using sup u(2) by (simp add: max_def)
   208     ultimately show "(\<lambda>i. U' i x) ----> u x" 
   209       by simp
   210   next
   211     fix i
   212     have "U' i ` space M \<subseteq> real ` (U i ` space M)" "finite (U i ` space M)"
   213       unfolding U'_def using U(1) by (auto dest: simple_functionD)
   214     then have fin: "finite (U' i ` space M)"
   215       by (metis finite_subset finite_imageI)
   216     moreover have "\<And>z. {y. U' i z = y \<and> y \<in> U' i ` space M \<and> z \<in> space M} = (if z \<in> space M then {U' i z} else {})"
   217       by auto
   218     ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i"
   219       by (simp add: U'_def fun_eq_iff)
   220     have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
   221       using nn by (auto simp: U'_def real_of_ereal_pos)
   222     with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
   223     proof induct
   224       case empty from set[of "{}"] show ?case
   225         by (simp add: indicator_def[abs_def])
   226     next
   227       case (insert x F)
   228       then show ?case
   229         by (auto intro!: add mult set setsum_nonneg split: split_indicator split_indicator_asm
   230                  simp del: setsum_mult_indicator simp: setsum_nonneg_eq_0_iff )
   231     qed
   232     with U' show "P (U' i)" by simp
   233   qed
   234 qed
   235 
   236 lemma scaleR_cong_right:
   237   fixes x :: "'a :: real_vector"
   238   shows "(x \<noteq> 0 \<Longrightarrow> r = p) \<Longrightarrow> r *\<^sub>R x = p *\<^sub>R x"
   239   by (cases "x = 0") auto
   240 
   241 inductive simple_bochner_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" for M f where
   242   "simple_function M f \<Longrightarrow> emeasure M {y\<in>space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
   243     simple_bochner_integrable M f"
   244 
   245 lemma simple_bochner_integrable_compose2:
   246   assumes p_0: "p 0 0 = 0"
   247   shows "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integrable M g \<Longrightarrow>
   248     simple_bochner_integrable M (\<lambda>x. p (f x) (g x))"
   249 proof (safe intro!: simple_bochner_integrable.intros elim!: simple_bochner_integrable.cases del: notI)
   250   assume sf: "simple_function M f" "simple_function M g"
   251   then show "simple_function M (\<lambda>x. p (f x) (g x))"
   252     by (rule simple_function_compose2)
   253 
   254   from sf have [measurable]:
   255       "f \<in> measurable M (count_space UNIV)"
   256       "g \<in> measurable M (count_space UNIV)"
   257     by (auto intro: measurable_simple_function)
   258 
   259   assume fin: "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" "emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity>"
   260    
   261   have "emeasure M {x\<in>space M. p (f x) (g x) \<noteq> 0} \<le>
   262       emeasure M ({x\<in>space M. f x \<noteq> 0} \<union> {x\<in>space M. g x \<noteq> 0})"
   263     by (intro emeasure_mono) (auto simp: p_0)
   264   also have "\<dots> \<le> emeasure M {x\<in>space M. f x \<noteq> 0} + emeasure M {x\<in>space M. g x \<noteq> 0}"
   265     by (intro emeasure_subadditive) auto
   266   finally show "emeasure M {y \<in> space M. p (f y) (g y) \<noteq> 0} \<noteq> \<infinity>"
   267     using fin by auto
   268 qed
   269 
   270 lemma simple_function_finite_support:
   271   assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" and nn: "\<And>x. 0 \<le> f x"
   272   shows "emeasure M {x\<in>space M. f x \<noteq> 0} \<noteq> \<infinity>"
   273 proof cases
   274   from f have meas[measurable]: "f \<in> borel_measurable M"
   275     by (rule borel_measurable_simple_function)
   276 
   277   assume non_empty: "\<exists>x\<in>space M. f x \<noteq> 0"
   278 
   279   def m \<equiv> "Min (f`space M - {0})"
   280   have "m \<in> f`space M - {0}"
   281     unfolding m_def using f non_empty by (intro Min_in) (auto simp: simple_function_def)
   282   then have m: "0 < m"
   283     using nn by (auto simp: less_le)
   284 
   285   from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} = 
   286     (\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
   287     using f by (intro nn_integral_cmult_indicator[symmetric]) auto
   288   also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
   289     using AE_space
   290   proof (intro nn_integral_mono_AE, eventually_elim)
   291     fix x assume "x \<in> space M"
   292     with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x"
   293       using f by (auto split: split_indicator simp: simple_function_def m_def)
   294   qed
   295   also note `\<dots> < \<infinity>`
   296   finally show ?thesis
   297     using m by auto 
   298 next
   299   assume "\<not> (\<exists>x\<in>space M. f x \<noteq> 0)"
   300   with nn have *: "{x\<in>space M. f x \<noteq> 0} = {}"
   301     by auto
   302   show ?thesis unfolding * by simp
   303 qed
   304 
   305 lemma simple_bochner_integrableI_bounded:
   306   assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   307   shows "simple_bochner_integrable M f"
   308 proof
   309   have "emeasure M {y \<in> space M. ereal (norm (f y)) \<noteq> 0} \<noteq> \<infinity>"
   310   proof (rule simple_function_finite_support)
   311     show "simple_function M (\<lambda>x. ereal (norm (f x)))"
   312       using f by (rule simple_function_compose1)
   313     show "(\<integral>\<^sup>+ y. ereal (norm (f y)) \<partial>M) < \<infinity>" by fact
   314   qed simp
   315   then show "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" by simp
   316 qed fact
   317 
   318 definition simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where
   319   "simple_bochner_integral M f = (\<Sum>y\<in>f`space M. measure M {x\<in>space M. f x = y} *\<^sub>R y)"
   320 
   321 lemma simple_bochner_integral_partition:
   322   assumes f: "simple_bochner_integrable M f" and g: "simple_function M g"
   323   assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y"
   324   assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)"
   325   shows "simple_bochner_integral M f = (\<Sum>y\<in>g ` space M. measure M {x\<in>space M. g x = y} *\<^sub>R v y)"
   326     (is "_ = ?r")
   327 proof -
   328   from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
   329     by (auto simp: simple_function_def elim: simple_bochner_integrable.cases)
   330 
   331   from f have [measurable]: "f \<in> measurable M (count_space UNIV)"
   332     by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
   333 
   334   from g have [measurable]: "g \<in> measurable M (count_space UNIV)"
   335     by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
   336 
   337   { fix y assume "y \<in> space M"
   338     then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}"
   339       by (auto cong: sub simp: v[symmetric]) }
   340   note eq = this
   341 
   342   have "simple_bochner_integral M f =
   343     (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
   344       if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} else 0) *\<^sub>R y)"
   345     unfolding simple_bochner_integral_def
   346   proof (safe intro!: setsum.cong scaleR_cong_right)
   347     fix y assume y: "y \<in> space M" "f y \<noteq> 0"
   348     have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 
   349         {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
   350       by auto
   351     have eq:"{x \<in> space M. f x = f y} =
   352         (\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i})"
   353       by (auto simp: eq_commute cong: sub rev_conj_cong)
   354     have "finite (g`space M)" by simp
   355     then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
   356       by (rule rev_finite_subset) auto
   357     moreover
   358     { fix x assume "x \<in> space M" "f x = f y"
   359       then have "x \<in> space M" "f x \<noteq> 0"
   360         using y by auto
   361       then have "emeasure M {y \<in> space M. g y = g x} \<le> emeasure M {y \<in> space M. f y \<noteq> 0}"
   362         by (auto intro!: emeasure_mono cong: sub)
   363       then have "emeasure M {xa \<in> space M. g xa = g x} < \<infinity>"
   364         using f by (auto simp: simple_bochner_integrable.simps) }
   365     ultimately
   366     show "measure M {x \<in> space M. f x = f y} =
   367       (\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then measure M {x \<in> space M. g x = z} else 0)"
   368       apply (simp add: setsum.If_cases eq)
   369       apply (subst measure_finite_Union[symmetric])
   370       apply (auto simp: disjoint_family_on_def)
   371       done
   372   qed
   373   also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
   374       if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} *\<^sub>R y else 0))"
   375     by (auto intro!: setsum.cong simp: scaleR_setsum_left)
   376   also have "\<dots> = ?r"
   377     by (subst setsum.commute)
   378        (auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq)
   379   finally show "simple_bochner_integral M f = ?r" .
   380 qed
   381 
   382 lemma simple_bochner_integral_add:
   383   assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
   384   shows "simple_bochner_integral M (\<lambda>x. f x + g x) =
   385     simple_bochner_integral M f + simple_bochner_integral M g"
   386 proof -
   387   from f g have "simple_bochner_integral M (\<lambda>x. f x + g x) =
   388     (\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R (fst y + snd y))"
   389     by (intro simple_bochner_integral_partition)
   390        (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   391   moreover from f g have "simple_bochner_integral M f =
   392     (\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R fst y)"
   393     by (intro simple_bochner_integral_partition)
   394        (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   395   moreover from f g have "simple_bochner_integral M g =
   396     (\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R snd y)"
   397     by (intro simple_bochner_integral_partition)
   398        (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   399   ultimately show ?thesis
   400     by (simp add: setsum.distrib[symmetric] scaleR_add_right)
   401 qed
   402 
   403 lemma (in linear) simple_bochner_integral_linear:
   404   assumes g: "simple_bochner_integrable M g"
   405   shows "simple_bochner_integral M (\<lambda>x. f (g x)) = f (simple_bochner_integral M g)"
   406 proof -
   407   from g have "simple_bochner_integral M (\<lambda>x. f (g x)) =
   408     (\<Sum>y\<in>g ` space M. measure M {x \<in> space M. g x = y} *\<^sub>R f y)"
   409     by (intro simple_bochner_integral_partition)
   410        (auto simp: simple_bochner_integrable_compose2[where p="\<lambda>x y. f x"] zero
   411              elim: simple_bochner_integrable.cases)
   412   also have "\<dots> = f (simple_bochner_integral M g)"
   413     by (simp add: simple_bochner_integral_def setsum scaleR)
   414   finally show ?thesis .
   415 qed
   416 
   417 lemma simple_bochner_integral_minus:
   418   assumes f: "simple_bochner_integrable M f"
   419   shows "simple_bochner_integral M (\<lambda>x. - f x) = - simple_bochner_integral M f"
   420 proof -
   421   interpret linear uminus by unfold_locales auto
   422   from f show ?thesis
   423     by (rule simple_bochner_integral_linear)
   424 qed
   425 
   426 lemma simple_bochner_integral_diff:
   427   assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
   428   shows "simple_bochner_integral M (\<lambda>x. f x - g x) =
   429     simple_bochner_integral M f - simple_bochner_integral M g"
   430   unfolding diff_conv_add_uminus using f g
   431   by (subst simple_bochner_integral_add)
   432      (auto simp: simple_bochner_integral_minus simple_bochner_integrable_compose2[where p="\<lambda>x y. - y"])
   433 
   434 lemma simple_bochner_integral_norm_bound:
   435   assumes f: "simple_bochner_integrable M f"
   436   shows "norm (simple_bochner_integral M f) \<le> simple_bochner_integral M (\<lambda>x. norm (f x))"
   437 proof -
   438   have "norm (simple_bochner_integral M f) \<le> 
   439     (\<Sum>y\<in>f ` space M. norm (measure M {x \<in> space M. f x = y} *\<^sub>R y))"
   440     unfolding simple_bochner_integral_def by (rule norm_setsum)
   441   also have "\<dots> = (\<Sum>y\<in>f ` space M. measure M {x \<in> space M. f x = y} *\<^sub>R norm y)"
   442     by (simp add: measure_nonneg)
   443   also have "\<dots> = simple_bochner_integral M (\<lambda>x. norm (f x))"
   444     using f
   445     by (intro simple_bochner_integral_partition[symmetric])
   446        (auto intro: f simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   447   finally show ?thesis .
   448 qed
   449 
   450 lemma simple_bochner_integral_eq_nn_integral:
   451   assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
   452   shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)"
   453 proof -
   454   { fix x y z have "(x \<noteq> 0 \<Longrightarrow> y = z) \<Longrightarrow> ereal x * y = ereal x * z"
   455       by (cases "x = 0") (auto simp: zero_ereal_def[symmetric]) }
   456   note ereal_cong_mult = this
   457 
   458   have [measurable]: "f \<in> borel_measurable M"
   459     using f(1) by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   460 
   461   { fix y assume y: "y \<in> space M" "f y \<noteq> 0"
   462     have "ereal (measure M {x \<in> space M. f x = f y}) = emeasure M {x \<in> space M. f x = f y}"
   463     proof (rule emeasure_eq_ereal_measure[symmetric])
   464       have "emeasure M {x \<in> space M. f x = f y} \<le> emeasure M {x \<in> space M. f x \<noteq> 0}"
   465         using y by (intro emeasure_mono) auto
   466       with f show "emeasure M {x \<in> space M. f x = f y} \<noteq> \<infinity>"
   467         by (auto simp: simple_bochner_integrable.simps)
   468     qed
   469     moreover have "{x \<in> space M. f x = f y} = (\<lambda>x. ereal (f x)) -` {ereal (f y)} \<inter> space M"
   470       by auto
   471     ultimately have "ereal (measure M {x \<in> space M. f x = f y}) =
   472           emeasure M ((\<lambda>x. ereal (f x)) -` {ereal (f y)} \<inter> space M)" by simp }
   473   with f have "simple_bochner_integral M f = (\<integral>\<^sup>Sx. f x \<partial>M)"
   474     unfolding simple_integral_def
   475     by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ereal (f x)" and v=real])
   476        (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
   477              intro!: setsum.cong ereal_cong_mult
   478              simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] ac_simps
   479              simp del: setsum_ereal times_ereal.simps(1))
   480   also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
   481     using f
   482     by (intro nn_integral_eq_simple_integral[symmetric])
   483        (auto simp: simple_function_compose1 simple_bochner_integrable.simps)
   484   finally show ?thesis .
   485 qed
   486 
   487 lemma simple_bochner_integral_bounded:
   488   fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector, second_countable_topology}"
   489   assumes f[measurable]: "f \<in> borel_measurable M"
   490   assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t"
   491   shows "ereal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) \<le>
   492     (\<integral>\<^sup>+ x. norm (f x - s x) \<partial>M) + (\<integral>\<^sup>+ x. norm (f x - t x) \<partial>M)"
   493     (is "ereal (norm (?s - ?t)) \<le> ?S + ?T")
   494 proof -
   495   have [measurable]: "s \<in> borel_measurable M" "t \<in> borel_measurable M"
   496     using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   497 
   498   have "ereal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))"
   499     using s t by (subst simple_bochner_integral_diff) auto
   500   also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))"
   501     using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t
   502     by (auto intro!: simple_bochner_integral_norm_bound)
   503   also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
   504     using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
   505     by (auto intro!: simple_bochner_integral_eq_nn_integral)
   506   also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s x)) + ereal (norm (f x - t x)) \<partial>M)"
   507     by (auto intro!: nn_integral_mono)
   508        (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
   509               norm_minus_commute norm_triangle_ineq4 order_refl)
   510   also have "\<dots> = ?S + ?T"
   511    by (rule nn_integral_add) auto
   512   finally show ?thesis .
   513 qed
   514 
   515 inductive has_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::{real_normed_vector, second_countable_topology} \<Rightarrow> bool"
   516   for M f x where
   517   "f \<in> borel_measurable M \<Longrightarrow>
   518     (\<And>i. simple_bochner_integrable M (s i)) \<Longrightarrow>
   519     (\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) ----> 0 \<Longrightarrow>
   520     (\<lambda>i. simple_bochner_integral M (s i)) ----> x \<Longrightarrow>
   521     has_bochner_integral M f x"
   522 
   523 lemma has_bochner_integral_cong:
   524   assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
   525   shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
   526   unfolding has_bochner_integral.simps assms(1,3)
   527   using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
   528 
   529 lemma has_bochner_integral_cong_AE:
   530   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
   531     has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
   532   unfolding has_bochner_integral.simps
   533   by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x ----> 0"]
   534             nn_integral_cong_AE)
   535      auto
   536 
   537 lemma borel_measurable_has_bochner_integral:
   538   "has_bochner_integral M f x \<Longrightarrow> f \<in> borel_measurable M"
   539   by (rule has_bochner_integral.cases)
   540 
   541 lemma borel_measurable_has_bochner_integral'[measurable_dest]:
   542   "has_bochner_integral M f x \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   543   using borel_measurable_has_bochner_integral[measurable] by measurable
   544 
   545 lemma has_bochner_integral_simple_bochner_integrable:
   546   "simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)"
   547   by (rule has_bochner_integral.intros[where s="\<lambda>_. f"])
   548      (auto intro: borel_measurable_simple_function 
   549            elim: simple_bochner_integrable.cases
   550            simp: zero_ereal_def[symmetric])
   551 
   552 lemma has_bochner_integral_real_indicator:
   553   assumes [measurable]: "A \<in> sets M" and A: "emeasure M A < \<infinity>"
   554   shows "has_bochner_integral M (indicator A) (measure M A)"
   555 proof -
   556   have sbi: "simple_bochner_integrable M (indicator A::'a \<Rightarrow> real)"
   557   proof
   558     have "{y \<in> space M. (indicator A y::real) \<noteq> 0} = A"
   559       using sets.sets_into_space[OF `A\<in>sets M`] by (auto split: split_indicator)
   560     then show "emeasure M {y \<in> space M. (indicator A y::real) \<noteq> 0} \<noteq> \<infinity>"
   561       using A by auto
   562   qed (rule simple_function_indicator assms)+
   563   moreover have "simple_bochner_integral M (indicator A) = measure M A"
   564     using simple_bochner_integral_eq_nn_integral[OF sbi] A
   565     by (simp add: ereal_indicator emeasure_eq_ereal_measure)
   566   ultimately show ?thesis
   567     by (metis has_bochner_integral_simple_bochner_integrable)
   568 qed
   569 
   570 lemma has_bochner_integral_add[intro]:
   571   "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
   572     has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
   573 proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   574   fix sf sg
   575   assume f_sf: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - sf i x) \<partial>M) ----> 0"
   576   assume g_sg: "(\<lambda>i. \<integral>\<^sup>+ x. norm (g x - sg i x) \<partial>M) ----> 0"
   577 
   578   assume sf: "\<forall>i. simple_bochner_integrable M (sf i)"
   579     and sg: "\<forall>i. simple_bochner_integrable M (sg i)"
   580   then have [measurable]: "\<And>i. sf i \<in> borel_measurable M" "\<And>i. sg i \<in> borel_measurable M"
   581     by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   582   assume [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   583 
   584   show "\<And>i. simple_bochner_integrable M (\<lambda>x. sf i x + sg i x)"
   585     using sf sg by (simp add: simple_bochner_integrable_compose2)
   586 
   587   show "(\<lambda>i. \<integral>\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \<partial>M) ----> 0"
   588     (is "?f ----> 0")
   589   proof (rule tendsto_sandwich)
   590     show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
   591       by (auto simp: nn_integral_nonneg)
   592     show "eventually (\<lambda>i. ?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) \<partial>M) + \<integral>\<^sup>+ x. (norm (g x - sg i x)) \<partial>M) sequentially"
   593       (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
   594     proof (intro always_eventually allI)
   595       fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ereal (norm (g x - sg i x)) \<partial>M)"
   596         by (auto intro!: nn_integral_mono norm_diff_triangle_ineq)
   597       also have "\<dots> = ?g i"
   598         by (intro nn_integral_add) auto
   599       finally show "?f i \<le> ?g i" .
   600     qed
   601     show "?g ----> 0"
   602       using tendsto_add_ereal[OF _ _ f_sf g_sg] by simp
   603   qed
   604 qed (auto simp: simple_bochner_integral_add tendsto_add)
   605 
   606 lemma has_bochner_integral_bounded_linear:
   607   assumes "bounded_linear T"
   608   shows "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M (\<lambda>x. T (f x)) (T x)"
   609 proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   610   interpret T: bounded_linear T by fact
   611   have [measurable]: "T \<in> borel_measurable borel"
   612     by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id)
   613   assume [measurable]: "f \<in> borel_measurable M"
   614   then show "(\<lambda>x. T (f x)) \<in> borel_measurable M"
   615     by auto
   616 
   617   fix s assume f_s: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) ----> 0"
   618   assume s: "\<forall>i. simple_bochner_integrable M (s i)"
   619   then show "\<And>i. simple_bochner_integrable M (\<lambda>x. T (s i x))"
   620     by (auto intro: simple_bochner_integrable_compose2 T.zero)
   621 
   622   have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   623     using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   624 
   625   obtain K where K: "K > 0" "\<And>x i. norm (T (f x) - T (s i x)) \<le> norm (f x - s i x) * K"
   626     using T.pos_bounded by (auto simp: T.diff[symmetric])
   627 
   628   show "(\<lambda>i. \<integral>\<^sup>+ x. norm (T (f x) - T (s i x)) \<partial>M) ----> 0"
   629     (is "?f ----> 0")
   630   proof (rule tendsto_sandwich)
   631     show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
   632       by (auto simp: nn_integral_nonneg)
   633 
   634     show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
   635       (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
   636     proof (intro always_eventually allI)
   637       fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
   638         using K by (intro nn_integral_mono) (auto simp: ac_simps)
   639       also have "\<dots> = ?g i"
   640         using K by (intro nn_integral_cmult) auto
   641       finally show "?f i \<le> ?g i" .
   642     qed
   643     show "?g ----> 0"
   644       using ereal_lim_mult[OF f_s, of "ereal K"] by simp
   645   qed
   646 
   647   assume "(\<lambda>i. simple_bochner_integral M (s i)) ----> x"
   648   with s show "(\<lambda>i. simple_bochner_integral M (\<lambda>x. T (s i x))) ----> T x"
   649     by (auto intro!: T.tendsto simp: T.simple_bochner_integral_linear)
   650 qed
   651 
   652 lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\<lambda>x. 0) 0"
   653   by (auto intro!: has_bochner_integral.intros[where s="\<lambda>_ _. 0"]
   654            simp: zero_ereal_def[symmetric] simple_bochner_integrable.simps
   655                  simple_bochner_integral_def image_constant_conv)
   656 
   657 lemma has_bochner_integral_scaleR_left[intro]:
   658   "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x *\<^sub>R c) (x *\<^sub>R c)"
   659   by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left])
   660 
   661 lemma has_bochner_integral_scaleR_right[intro]:
   662   "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c *\<^sub>R f x) (c *\<^sub>R x)"
   663   by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right])
   664 
   665 lemma has_bochner_integral_mult_left[intro]:
   666   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   667   shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x * c) (x * c)"
   668   by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left])
   669 
   670 lemma has_bochner_integral_mult_right[intro]:
   671   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   672   shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c * f x) (c * x)"
   673   by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right])
   674 
   675 lemmas has_bochner_integral_divide = 
   676   has_bochner_integral_bounded_linear[OF bounded_linear_divide]
   677 
   678 lemma has_bochner_integral_divide_zero[intro]:
   679   fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
   680   shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)"
   681   using has_bochner_integral_divide by (cases "c = 0") auto
   682 
   683 lemma has_bochner_integral_inner_left[intro]:
   684   "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)"
   685   by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left])
   686 
   687 lemma has_bochner_integral_inner_right[intro]:
   688   "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c \<bullet> f x) (c \<bullet> x)"
   689   by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right])
   690 
   691 lemmas has_bochner_integral_minus =
   692   has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
   693 lemmas has_bochner_integral_Re =
   694   has_bochner_integral_bounded_linear[OF bounded_linear_Re]
   695 lemmas has_bochner_integral_Im =
   696   has_bochner_integral_bounded_linear[OF bounded_linear_Im]
   697 lemmas has_bochner_integral_cnj =
   698   has_bochner_integral_bounded_linear[OF bounded_linear_cnj]
   699 lemmas has_bochner_integral_of_real =
   700   has_bochner_integral_bounded_linear[OF bounded_linear_of_real]
   701 lemmas has_bochner_integral_fst =
   702   has_bochner_integral_bounded_linear[OF bounded_linear_fst]
   703 lemmas has_bochner_integral_snd =
   704   has_bochner_integral_bounded_linear[OF bounded_linear_snd]
   705 
   706 lemma has_bochner_integral_indicator:
   707   "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   708     has_bochner_integral M (\<lambda>x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)"
   709   by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator)
   710 
   711 lemma has_bochner_integral_diff:
   712   "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
   713     has_bochner_integral M (\<lambda>x. f x - g x) (x - y)"
   714   unfolding diff_conv_add_uminus
   715   by (intro has_bochner_integral_add has_bochner_integral_minus)
   716 
   717 lemma has_bochner_integral_setsum:
   718   "(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow>
   719     has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
   720   by (induct I rule: infinite_finite_induct) auto
   721 
   722 lemma has_bochner_integral_implies_finite_norm:
   723   "has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   724 proof (elim has_bochner_integral.cases)
   725   fix s v
   726   assume [measurable]: "f \<in> borel_measurable M" and s: "\<And>i. simple_bochner_integrable M (s i)" and
   727     lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
   728   from order_tendstoD[OF lim_0, of "\<infinity>"]
   729   obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) < \<infinity>"
   730     by (metis (mono_tags, lifting) eventually_False_sequentially eventually_elim1
   731               less_ereal.simps(4) zero_ereal_def)
   732 
   733   have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   734     using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   735 
   736   def m \<equiv> "if space M = {} then 0 else Max ((\<lambda>x. norm (s i x))`space M)"
   737   have "finite (s i ` space M)"
   738     using s by (auto simp: simple_function_def simple_bochner_integrable.simps)
   739   then have "finite (norm ` s i ` space M)"
   740     by (rule finite_imageI)
   741   then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m"
   742     by (auto simp: m_def image_comp comp_def Max_ge_iff)
   743   then have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ereal m * indicator {x\<in>space M. s i x \<noteq> 0} x \<partial>M)"
   744     by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
   745   also have "\<dots> < \<infinity>"
   746     using s by (subst nn_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
   747   finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
   748 
   749   have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) + ereal (norm (s i x)) \<partial>M)"
   750     by (auto intro!: nn_integral_mono) (metis add.commute norm_triangle_sub)
   751   also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
   752     by (rule nn_integral_add) auto
   753   also have "\<dots> < \<infinity>"
   754     using s_fin f_s_fin by auto
   755   finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
   756 qed
   757 
   758 lemma has_bochner_integral_norm_bound:
   759   assumes i: "has_bochner_integral M f x"
   760   shows "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   761 using assms proof
   762   fix s assume
   763     x: "(\<lambda>i. simple_bochner_integral M (s i)) ----> x" (is "?s ----> x") and
   764     s[simp]: "\<And>i. simple_bochner_integrable M (s i)" and
   765     lim: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0" and
   766     f[measurable]: "f \<in> borel_measurable M"
   767 
   768   have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   769     using s by (auto simp: simple_bochner_integrable.simps intro: borel_measurable_simple_function)
   770 
   771   show "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   772   proof (rule LIMSEQ_le)
   773     show "(\<lambda>i. ereal (norm (?s i))) ----> norm x"
   774       using x by (intro tendsto_intros lim_ereal[THEN iffD2])
   775     show "\<exists>N. \<forall>n\<ge>N. norm (?s n) \<le> (\<integral>\<^sup>+x. norm (f x - s n x) \<partial>M) + (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   776       (is "\<exists>N. \<forall>n\<ge>N. _ \<le> ?t n")
   777     proof (intro exI allI impI)
   778       fix n
   779       have "ereal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))"
   780         by (auto intro!: simple_bochner_integral_norm_bound)
   781       also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)"
   782         by (intro simple_bochner_integral_eq_nn_integral)
   783            (auto intro: s simple_bochner_integrable_compose2)
   784       also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s n x)) + norm (f x) \<partial>M)"
   785         by (auto intro!: nn_integral_mono)
   786            (metis add.commute norm_minus_commute norm_triangle_sub)
   787       also have "\<dots> = ?t n" 
   788         by (rule nn_integral_add) auto
   789       finally show "norm (?s n) \<le> ?t n" .
   790     qed
   791     have "?t ----> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
   792       using has_bochner_integral_implies_finite_norm[OF i]
   793       by (intro tendsto_add_ereal tendsto_const lim) auto
   794     then show "?t ----> \<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M"
   795       by simp
   796   qed
   797 qed
   798 
   799 lemma has_bochner_integral_eq:
   800   "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M f y \<Longrightarrow> x = y"
   801 proof (elim has_bochner_integral.cases)
   802   assume f[measurable]: "f \<in> borel_measurable M"
   803 
   804   fix s t
   805   assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) ----> 0" (is "?S ----> 0")
   806   assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - t i x) \<partial>M) ----> 0" (is "?T ----> 0")
   807   assume s: "\<And>i. simple_bochner_integrable M (s i)"
   808   assume t: "\<And>i. simple_bochner_integrable M (t i)"
   809 
   810   have [measurable]: "\<And>i. s i \<in> borel_measurable M" "\<And>i. t i \<in> borel_measurable M"
   811     using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   812 
   813   let ?s = "\<lambda>i. simple_bochner_integral M (s i)"
   814   let ?t = "\<lambda>i. simple_bochner_integral M (t i)"
   815   assume "?s ----> x" "?t ----> y"
   816   then have "(\<lambda>i. norm (?s i - ?t i)) ----> norm (x - y)"
   817     by (intro tendsto_intros)
   818   moreover
   819   have "(\<lambda>i. ereal (norm (?s i - ?t i))) ----> ereal 0"
   820   proof (rule tendsto_sandwich)
   821     show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) ----> ereal 0"
   822       by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric])
   823 
   824     show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
   825       by (intro always_eventually allI simple_bochner_integral_bounded s t f)
   826     show "(\<lambda>i. ?S i + ?T i) ----> ereal 0"
   827       using tendsto_add_ereal[OF _ _ `?S ----> 0` `?T ----> 0`]
   828       by (simp add: zero_ereal_def[symmetric])
   829   qed
   830   then have "(\<lambda>i. norm (?s i - ?t i)) ----> 0"
   831     by simp
   832   ultimately have "norm (x - y) = 0"
   833     by (rule LIMSEQ_unique)
   834   then show "x = y" by simp
   835 qed
   836 
   837 lemma has_bochner_integralI_AE:
   838   assumes f: "has_bochner_integral M f x"
   839     and g: "g \<in> borel_measurable M"
   840     and ae: "AE x in M. f x = g x"
   841   shows "has_bochner_integral M g x"
   842   using f
   843 proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   844   fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
   845   also have "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) = (\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M)"
   846     using ae
   847     by (intro ext nn_integral_cong_AE, eventually_elim) simp
   848   finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) ----> 0" .
   849 qed (auto intro: g)
   850 
   851 lemma has_bochner_integral_eq_AE:
   852   assumes f: "has_bochner_integral M f x"
   853     and g: "has_bochner_integral M g y"
   854     and ae: "AE x in M. f x = g x"
   855   shows "x = y"
   856 proof -
   857   from assms have "has_bochner_integral M g x"
   858     by (auto intro: has_bochner_integralI_AE)
   859   from this g show "x = y"
   860     by (rule has_bochner_integral_eq)
   861 qed
   862 
   863 lemma simple_bochner_integrable_restrict_space:
   864   fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   865   assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   866   shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
   867     simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   868   by (simp add: simple_bochner_integrable.simps space_restrict_space
   869     simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
   870     indicator_eq_0_iff conj_ac)
   871 
   872 lemma simple_bochner_integral_restrict_space:
   873   fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   874   assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   875   assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"
   876   shows "simple_bochner_integral (restrict_space M \<Omega>) f =
   877     simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   878 proof -
   879   have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x)`space M)"
   880     using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
   881     by (simp add: simple_bochner_integrable.simps simple_function_def)
   882   then show ?thesis
   883     by (auto simp: space_restrict_space measure_restrict_space[OF \<Omega>(1)] le_infI2
   884                    simple_bochner_integral_def Collect_restrict
   885              split: split_indicator split_indicator_asm
   886              intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure])
   887 qed
   888 
   889 inductive integrable for M f where
   890   "has_bochner_integral M f x \<Longrightarrow> integrable M f"
   891 
   892 definition lebesgue_integral ("integral\<^sup>L") where
   893   "integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
   894 
   895 syntax
   896   "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral>((2 _./ _)/ \<partial>_)" [60,61] 110)
   897 
   898 translations
   899   "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
   900 
   901 lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
   902   by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
   903 
   904 lemma has_bochner_integral_integrable:
   905   "integrable M f \<Longrightarrow> has_bochner_integral M f (integral\<^sup>L M f)"
   906   by (auto simp: has_bochner_integral_integral_eq integrable.simps)
   907 
   908 lemma has_bochner_integral_iff:
   909   "has_bochner_integral M f x \<longleftrightarrow> integrable M f \<and> integral\<^sup>L M f = x"
   910   by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros)
   911 
   912 lemma simple_bochner_integrable_eq_integral:
   913   "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integral M f = integral\<^sup>L M f"
   914   using has_bochner_integral_simple_bochner_integrable[of M f]
   915   by (simp add: has_bochner_integral_integral_eq)
   916 
   917 lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = 0"
   918   unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])
   919 
   920 lemma integral_eq_cases:
   921   "integrable M f \<longleftrightarrow> integrable N g \<Longrightarrow>
   922     (integrable M f \<Longrightarrow> integrable N g \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g) \<Longrightarrow>
   923     integral\<^sup>L M f = integral\<^sup>L N g"
   924   by (metis not_integrable_integral_eq)
   925 
   926 lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
   927   by (auto elim: integrable.cases has_bochner_integral.cases)
   928 
   929 lemma borel_measurable_integrable'[measurable_dest]:
   930   "integrable M f \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   931   using borel_measurable_integrable[measurable] by measurable
   932 
   933 lemma integrable_cong:
   934   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
   935   using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
   936 
   937 lemma integrable_cong_AE:
   938   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   939     integrable M f \<longleftrightarrow> integrable M g"
   940   unfolding integrable.simps
   941   by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)
   942 
   943 lemma integral_cong:
   944   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
   945   using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
   946 
   947 lemma integral_cong_AE:
   948   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   949     integral\<^sup>L M f = integral\<^sup>L M g"
   950   unfolding lebesgue_integral_def
   951   by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)
   952 
   953 lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
   954   by (auto simp: integrable.simps)
   955 
   956 lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
   957   by (metis has_bochner_integral_zero integrable.simps) 
   958 
   959 lemma integrable_setsum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)"
   960   by (metis has_bochner_integral_setsum integrable.simps) 
   961 
   962 lemma integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   963   integrable M (\<lambda>x. indicator A x *\<^sub>R c)"
   964   by (metis has_bochner_integral_indicator integrable.simps) 
   965 
   966 lemma integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   967   integrable M (indicator A :: 'a \<Rightarrow> real)"
   968   by (metis has_bochner_integral_real_indicator integrable.simps)
   969 
   970 lemma integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x - g x)"
   971   by (auto simp: integrable.simps intro: has_bochner_integral_diff)
   972   
   973 lemma integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))"
   974   by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)
   975 
   976 lemma integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)"
   977   unfolding integrable.simps by fastforce
   978 
   979 lemma integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)"
   980   unfolding integrable.simps by fastforce
   981 
   982 lemma integrable_mult_left[simp, intro]:
   983   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   984   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x * c)"
   985   unfolding integrable.simps by fastforce
   986 
   987 lemma integrable_mult_right[simp, intro]:
   988   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   989   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)"
   990   unfolding integrable.simps by fastforce
   991 
   992 lemma integrable_divide_zero[simp, intro]:
   993   fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
   994   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
   995   unfolding integrable.simps by fastforce
   996 
   997 lemma integrable_inner_left[simp, intro]:
   998   "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)"
   999   unfolding integrable.simps by fastforce
  1000 
  1001 lemma integrable_inner_right[simp, intro]:
  1002   "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c \<bullet> f x)"
  1003   unfolding integrable.simps by fastforce
  1004 
  1005 lemmas integrable_minus[simp, intro] =
  1006   integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
  1007 lemmas integrable_divide[simp, intro] =
  1008   integrable_bounded_linear[OF bounded_linear_divide]
  1009 lemmas integrable_Re[simp, intro] =
  1010   integrable_bounded_linear[OF bounded_linear_Re]
  1011 lemmas integrable_Im[simp, intro] =
  1012   integrable_bounded_linear[OF bounded_linear_Im]
  1013 lemmas integrable_cnj[simp, intro] =
  1014   integrable_bounded_linear[OF bounded_linear_cnj]
  1015 lemmas integrable_of_real[simp, intro] =
  1016   integrable_bounded_linear[OF bounded_linear_of_real]
  1017 lemmas integrable_fst[simp, intro] =
  1018   integrable_bounded_linear[OF bounded_linear_fst]
  1019 lemmas integrable_snd[simp, intro] =
  1020   integrable_bounded_linear[OF bounded_linear_snd]
  1021 
  1022 lemma integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0"
  1023   by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)
  1024 
  1025 lemma integral_add[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
  1026     integral\<^sup>L M (\<lambda>x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g"
  1027   by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable)
  1028 
  1029 lemma integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
  1030     integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
  1031   by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
  1032 
  1033 lemma integral_setsum[simp]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
  1034   integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
  1035   by (intro has_bochner_integral_integral_eq has_bochner_integral_setsum has_bochner_integral_integrable)
  1036 
  1037 lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
  1038     integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  1039   by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
  1040 
  1041 lemma integral_bounded_linear':
  1042   assumes T: "bounded_linear T" and T': "bounded_linear T'"
  1043   assumes *: "\<not> (\<forall>x. T x = 0) \<Longrightarrow> (\<forall>x. T' (T x) = x)"
  1044   shows "integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  1045 proof cases
  1046   assume "(\<forall>x. T x = 0)" then show ?thesis
  1047     by simp
  1048 next
  1049   assume **: "\<not> (\<forall>x. T x = 0)"
  1050   show ?thesis
  1051   proof cases
  1052     assume "integrable M f" with T show ?thesis
  1053       by (rule integral_bounded_linear)
  1054   next
  1055     assume not: "\<not> integrable M f"
  1056     moreover have "\<not> integrable M (\<lambda>x. T (f x))"
  1057     proof
  1058       assume "integrable M (\<lambda>x. T (f x))"
  1059       from integrable_bounded_linear[OF T' this] not *[OF **]
  1060       show False
  1061         by auto
  1062     qed
  1063     ultimately show ?thesis
  1064       using T by (simp add: not_integrable_integral_eq linear_simps)
  1065   qed
  1066 qed
  1067 
  1068 lemma integral_scaleR_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x *\<^sub>R c \<partial>M) = integral\<^sup>L M f *\<^sub>R c"
  1069   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
  1070 
  1071 lemma integral_scaleR_right[simp]: "(\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
  1072   by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp
  1073 
  1074 lemma integral_mult_left[simp]:
  1075   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1076   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
  1077   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)
  1078 
  1079 lemma integral_mult_right[simp]:
  1080   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1081   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
  1082   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
  1083 
  1084 lemma integral_mult_left_zero[simp]:
  1085   fixes c :: "_::{real_normed_field,second_countable_topology}"
  1086   shows "(\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
  1087   by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp
  1088 
  1089 lemma integral_mult_right_zero[simp]:
  1090   fixes c :: "_::{real_normed_field,second_countable_topology}"
  1091   shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
  1092   by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp
  1093 
  1094 lemma integral_inner_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x \<bullet> c \<partial>M) = integral\<^sup>L M f \<bullet> c"
  1095   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
  1096 
  1097 lemma integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f"
  1098   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
  1099 
  1100 lemma integral_divide_zero[simp]:
  1101   fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
  1102   shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
  1103   by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
  1104 
  1105 lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f"
  1106   by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp
  1107 
  1108 lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\<lambda>x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
  1109   by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp
  1110 
  1111 lemma integral_cnj[simp]: "integral\<^sup>L M (\<lambda>x. cnj (f x)) = cnj (integral\<^sup>L M f)"
  1112   by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp
  1113 
  1114 lemmas integral_divide[simp] =
  1115   integral_bounded_linear[OF bounded_linear_divide]
  1116 lemmas integral_Re[simp] =
  1117   integral_bounded_linear[OF bounded_linear_Re]
  1118 lemmas integral_Im[simp] =
  1119   integral_bounded_linear[OF bounded_linear_Im]
  1120 lemmas integral_of_real[simp] =
  1121   integral_bounded_linear[OF bounded_linear_of_real]
  1122 lemmas integral_fst[simp] =
  1123   integral_bounded_linear[OF bounded_linear_fst]
  1124 lemmas integral_snd[simp] =
  1125   integral_bounded_linear[OF bounded_linear_snd]
  1126 
  1127 lemma integral_norm_bound_ereal:
  1128   "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
  1129   by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)
  1130 
  1131 lemma integrableI_sequence:
  1132   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1133   assumes f[measurable]: "f \<in> borel_measurable M"
  1134   assumes s: "\<And>i. simple_bochner_integrable M (s i)"
  1135   assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) ----> 0" (is "?S ----> 0")
  1136   shows "integrable M f"
  1137 proof -
  1138   let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
  1139 
  1140   have "\<exists>x. ?s ----> x"
  1141     unfolding convergent_eq_cauchy
  1142   proof (rule metric_CauchyI)
  1143     fix e :: real assume "0 < e"
  1144     then have "0 < ereal (e / 2)" by auto
  1145     from order_tendstoD(2)[OF lim this]
  1146     obtain M where M: "\<And>n. M \<le> n \<Longrightarrow> ?S n < e / 2"
  1147       by (auto simp: eventually_sequentially)
  1148     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (?s m) (?s n) < e"
  1149     proof (intro exI allI impI)
  1150       fix m n assume m: "M \<le> m" and n: "M \<le> n"
  1151       have "?S n \<noteq> \<infinity>"
  1152         using M[OF n] by auto
  1153       have "norm (?s n - ?s m) \<le> ?S n + ?S m"
  1154         by (intro simple_bochner_integral_bounded s f)
  1155       also have "\<dots> < ereal (e / 2) + e / 2"
  1156         using ereal_add_strict_mono[OF less_imp_le[OF M[OF n]] _ `?S n \<noteq> \<infinity>` M[OF m]]
  1157         by (auto simp: nn_integral_nonneg)
  1158       also have "\<dots> = e" by simp
  1159       finally show "dist (?s n) (?s m) < e"
  1160         by (simp add: dist_norm)
  1161     qed
  1162   qed
  1163   then obtain x where "?s ----> x" ..
  1164   show ?thesis
  1165     by (rule, rule) fact+
  1166 qed
  1167 
  1168 lemma nn_integral_dominated_convergence_norm:
  1169   fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
  1170   assumes [measurable]:
  1171        "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
  1172     and bound: "\<And>j. AE x in M. norm (u j x) \<le> w x"
  1173     and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
  1174     and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
  1175   shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> 0"
  1176 proof -
  1177   have "AE x in M. \<forall>j. norm (u j x) \<le> w x"
  1178     unfolding AE_all_countable by rule fact
  1179   with u' have bnd: "AE x in M. \<forall>j. norm (u' x - u j x) \<le> 2 * w x"
  1180   proof (eventually_elim, intro allI)
  1181     fix i x assume "(\<lambda>i. u i x) ----> u' x" "\<forall>j. norm (u j x) \<le> w x" "\<forall>j. norm (u j x) \<le> w x"
  1182     then have "norm (u' x) \<le> w x" "norm (u i x) \<le> w x"
  1183       by (auto intro: LIMSEQ_le_const2 tendsto_norm)
  1184     then have "norm (u' x) + norm (u i x) \<le> 2 * w x"
  1185       by simp
  1186     also have "norm (u' x - u i x) \<le> norm (u' x) + norm (u i x)"
  1187       by (rule norm_triangle_ineq4)
  1188     finally (xtrans) show "norm (u' x - u i x) \<le> 2 * w x" .
  1189   qed
  1190   
  1191   have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> (\<integral>\<^sup>+x. 0 \<partial>M)"
  1192   proof (rule nn_integral_dominated_convergence)  
  1193     show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
  1194       by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto
  1195     show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
  1196       using u' 
  1197     proof eventually_elim
  1198       fix x assume "(\<lambda>i. u i x) ----> u' x"
  1199       from tendsto_diff[OF tendsto_const[of "u' x"] this]
  1200       show "(\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
  1201         by (simp add: zero_ereal_def tendsto_norm_zero_iff)
  1202     qed
  1203   qed (insert bnd, auto)
  1204   then show ?thesis by simp
  1205 qed
  1206 
  1207 lemma integrableI_bounded:
  1208   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1209   assumes f[measurable]: "f \<in> borel_measurable M" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1210   shows "integrable M f"
  1211 proof -
  1212   from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
  1213     s: "\<And>i. simple_function M (s i)" and
  1214     pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x" and
  1215     bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
  1216     by (simp add: norm_conv_dist) metis
  1217   
  1218   show ?thesis
  1219   proof (rule integrableI_sequence)
  1220     { fix i
  1221       have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
  1222         by (intro nn_integral_mono) (simp add: bound)
  1223       also have "\<dots> = 2 * (\<integral>\<^sup>+x. ereal (norm (f x)) \<partial>M)"
  1224         by (rule nn_integral_cmult) auto
  1225       finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
  1226         using fin by auto }
  1227     note fin_s = this
  1228 
  1229     show "\<And>i. simple_bochner_integrable M (s i)"
  1230       by (rule simple_bochner_integrableI_bounded) fact+
  1231 
  1232     show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
  1233     proof (rule nn_integral_dominated_convergence_norm)
  1234       show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
  1235         using bound by auto
  1236       show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
  1237         using s by (auto intro: borel_measurable_simple_function)
  1238       show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>"
  1239         using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto
  1240       show "AE x in M. (\<lambda>i. s i x) ----> f x"
  1241         using pointwise by auto
  1242     qed fact
  1243   qed fact
  1244 qed
  1245 
  1246 lemma integrableI_bounded_set:
  1247   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1248   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M"
  1249   assumes finite: "emeasure M A < \<infinity>"
  1250     and bnd: "AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B"
  1251     and null: "AE x in M. x \<notin> A \<longrightarrow> f x = 0"
  1252   shows "integrable M f"
  1253 proof (rule integrableI_bounded)
  1254   { fix x :: 'b have "norm x \<le> B \<Longrightarrow> 0 \<le> B"
  1255       using norm_ge_zero[of x] by arith }
  1256   with bnd null have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (max 0 B) * indicator A x \<partial>M)"
  1257     by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
  1258   also have "\<dots> < \<infinity>"
  1259     using finite by (subst nn_integral_cmult_indicator) (auto simp: max_def)
  1260   finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
  1261 qed simp
  1262 
  1263 lemma integrableI_bounded_set_indicator:
  1264   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1265   shows "A \<in> sets M \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow>
  1266     emeasure M A < \<infinity> \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B) \<Longrightarrow>
  1267     integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1268   by (rule integrableI_bounded_set[where A=A]) auto
  1269 
  1270 lemma integrableI_nonneg:
  1271   fixes f :: "'a \<Rightarrow> real"
  1272   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
  1273   shows "integrable M f"
  1274 proof -
  1275   have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1276     using assms by (intro nn_integral_cong_AE) auto
  1277   then show ?thesis
  1278     using assms by (intro integrableI_bounded) auto
  1279 qed
  1280 
  1281 lemma integrable_iff_bounded:
  1282   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1283   shows "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1284   using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f]
  1285   unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto
  1286 
  1287 lemma integrable_bound:
  1288   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1289     and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
  1290   shows "integrable M f \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. norm (g x) \<le> norm (f x)) \<Longrightarrow>
  1291     integrable M g"
  1292   unfolding integrable_iff_bounded
  1293 proof safe
  1294   assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1295   assume "AE x in M. norm (g x) \<le> norm (f x)"
  1296   then have "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
  1297     by  (intro nn_integral_mono_AE) auto
  1298   also assume "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
  1299   finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
  1300 qed 
  1301 
  1302 lemma integrable_mult_indicator:
  1303   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1304   shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1305   by (rule integrable_bound[of M f]) (auto split: split_indicator)
  1306 
  1307 lemma integrable_real_mult_indicator:
  1308   fixes f :: "'a \<Rightarrow> real"
  1309   shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
  1310   using integrable_mult_indicator[of A M f] by (simp add: mult_ac)
  1311 
  1312 lemma integrable_abs[simp, intro]:
  1313   fixes f :: "'a \<Rightarrow> real"
  1314   assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
  1315   using assms by (rule integrable_bound) auto
  1316 
  1317 lemma integrable_norm[simp, intro]:
  1318   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1319   assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. norm (f x))"
  1320   using assms by (rule integrable_bound) auto
  1321   
  1322 lemma integrable_norm_cancel:
  1323   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1324   assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
  1325   using assms by (rule integrable_bound) auto
  1326 
  1327 lemma integrable_norm_iff:
  1328   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1329   shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. norm (f x)) \<longleftrightarrow> integrable M f"
  1330   by (auto intro: integrable_norm_cancel)
  1331 
  1332 lemma integrable_abs_cancel:
  1333   fixes f :: "'a \<Rightarrow> real"
  1334   assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
  1335   using assms by (rule integrable_bound) auto
  1336 
  1337 lemma integrable_abs_iff:
  1338   fixes f :: "'a \<Rightarrow> real"
  1339   shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
  1340   by (auto intro: integrable_abs_cancel)
  1341 
  1342 lemma integrable_max[simp, intro]:
  1343   fixes f :: "'a \<Rightarrow> real"
  1344   assumes fg[measurable]: "integrable M f" "integrable M g"
  1345   shows "integrable M (\<lambda>x. max (f x) (g x))"
  1346   using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
  1347   by (rule integrable_bound) auto
  1348 
  1349 lemma integrable_min[simp, intro]:
  1350   fixes f :: "'a \<Rightarrow> real"
  1351   assumes fg[measurable]: "integrable M f" "integrable M g"
  1352   shows "integrable M (\<lambda>x. min (f x) (g x))"
  1353   using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
  1354   by (rule integrable_bound) auto
  1355 
  1356 lemma integral_minus_iff[simp]:
  1357   "integrable M (\<lambda>x. - f x ::'a::{banach, second_countable_topology}) \<longleftrightarrow> integrable M f"
  1358   unfolding integrable_iff_bounded
  1359   by (auto intro: borel_measurable_uminus[of "\<lambda>x. - f x" M, simplified])
  1360 
  1361 lemma integrable_indicator_iff:
  1362   "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
  1363   by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
  1364            cong: conj_cong)
  1365 
  1366 lemma integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \<inter> space M)"
  1367 proof cases
  1368   assume *: "A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
  1369   have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M))"
  1370     by (intro integral_cong) (auto split: split_indicator)
  1371   also have "\<dots> = measure M (A \<inter> space M)"
  1372     using * by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator) auto
  1373   finally show ?thesis .
  1374 next
  1375   assume *: "\<not> (A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>)"
  1376   have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M) :: _ \<Rightarrow> real)"
  1377     by (intro integral_cong) (auto split: split_indicator)
  1378   also have "\<dots> = 0"
  1379     using * by (subst not_integrable_integral_eq) (auto simp: integrable_indicator_iff)
  1380   also have "\<dots> = measure M (A \<inter> space M)"
  1381     using * by (auto simp: measure_def emeasure_notin_sets)
  1382   finally show ?thesis .
  1383 qed
  1384 
  1385 lemma integrable_discrete_difference:
  1386   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1387   assumes X: "countable X"
  1388   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
  1389   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1390   assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1391   shows "integrable M f \<longleftrightarrow> integrable M g"
  1392   unfolding integrable_iff_bounded
  1393 proof (rule conj_cong)
  1394   { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
  1395       by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
  1396   moreover
  1397   { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
  1398       by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
  1399   ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
  1400 next
  1401   have "AE x in M. x \<notin> X"
  1402     by (rule AE_discrete_difference) fact+
  1403   then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
  1404     by (intro nn_integral_cong_AE) (auto simp: eq)
  1405   then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
  1406     by simp
  1407 qed
  1408 
  1409 lemma integral_discrete_difference:
  1410   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1411   assumes X: "countable X"
  1412   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
  1413   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1414   assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1415   shows "integral\<^sup>L M f = integral\<^sup>L M g"
  1416 proof (rule integral_eq_cases)
  1417   show eq: "integrable M f \<longleftrightarrow> integrable M g"
  1418     by (rule integrable_discrete_difference[where X=X]) fact+
  1419 
  1420   assume f: "integrable M f"
  1421   show "integral\<^sup>L M f = integral\<^sup>L M g"
  1422   proof (rule integral_cong_AE)
  1423     show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1424       using f eq by (auto intro: borel_measurable_integrable)
  1425 
  1426     have "AE x in M. x \<notin> X"
  1427       by (rule AE_discrete_difference) fact+
  1428     with AE_space show "AE x in M. f x = g x"
  1429       by eventually_elim fact
  1430   qed
  1431 qed
  1432 
  1433 lemma has_bochner_integral_discrete_difference:
  1434   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1435   assumes X: "countable X"
  1436   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
  1437   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1438   assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1439   shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
  1440   using integrable_discrete_difference[of X M f g, OF assms]
  1441   using integral_discrete_difference[of X M f g, OF assms]
  1442   by (metis has_bochner_integral_iff)
  1443 
  1444 lemma
  1445   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
  1446   assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
  1447   assumes lim: "AE x in M. (\<lambda>i. s i x) ----> f x"
  1448   assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
  1449   shows integrable_dominated_convergence: "integrable M f"
  1450     and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
  1451     and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
  1452 proof -
  1453   have "AE x in M. 0 \<le> w x"
  1454     using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
  1455   then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
  1456     by (intro nn_integral_cong_AE) auto
  1457   with `integrable M w` have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
  1458     unfolding integrable_iff_bounded by auto
  1459 
  1460   show int_s: "\<And>i. integrable M (s i)"
  1461     unfolding integrable_iff_bounded
  1462   proof
  1463     fix i 
  1464     have "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
  1465       using bound by (intro nn_integral_mono_AE) auto
  1466     with w show "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) < \<infinity>" by auto
  1467   qed fact
  1468 
  1469   have all_bound: "AE x in M. \<forall>i. norm (s i x) \<le> w x"
  1470     using bound unfolding AE_all_countable by auto
  1471 
  1472   show int_f: "integrable M f"
  1473     unfolding integrable_iff_bounded
  1474   proof
  1475     have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
  1476       using all_bound lim
  1477     proof (intro nn_integral_mono_AE, eventually_elim)
  1478       fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) ----> f x"
  1479       then show "ereal (norm (f x)) \<le> ereal (w x)"
  1480         by (intro LIMSEQ_le_const2[where X="\<lambda>i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto
  1481     qed
  1482     with w show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" by auto
  1483   qed fact
  1484 
  1485   have "(\<lambda>n. ereal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) ----> ereal 0" (is "?d ----> ereal 0")
  1486   proof (rule tendsto_sandwich)
  1487     show "eventually (\<lambda>n. ereal 0 \<le> ?d n) sequentially" "(\<lambda>_. ereal 0) ----> ereal 0" by auto
  1488     show "eventually (\<lambda>n. ?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)) sequentially"
  1489     proof (intro always_eventually allI)
  1490       fix n
  1491       have "?d n = norm (integral\<^sup>L M (\<lambda>x. s n x - f x))"
  1492         using int_f int_s by simp
  1493       also have "\<dots> \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)"
  1494         by (intro int_f int_s integrable_diff integral_norm_bound_ereal)
  1495       finally show "?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)" .
  1496     qed
  1497     show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) ----> ereal 0"
  1498       unfolding zero_ereal_def[symmetric]
  1499       apply (subst norm_minus_commute)
  1500     proof (rule nn_integral_dominated_convergence_norm[where w=w])
  1501       show "\<And>n. s n \<in> borel_measurable M"
  1502         using int_s unfolding integrable_iff_bounded by auto
  1503     qed fact+
  1504   qed
  1505   then have "(\<lambda>n. integral\<^sup>L M (s n) - integral\<^sup>L M f) ----> 0"
  1506     unfolding lim_ereal tendsto_norm_zero_iff .
  1507   from tendsto_add[OF this tendsto_const[of "integral\<^sup>L M f"]]
  1508   show "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"  by simp
  1509 qed
  1510 
  1511 lemma integrable_mult_left_iff:
  1512   fixes f :: "'a \<Rightarrow> real"
  1513   shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
  1514   using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
  1515   by (cases "c = 0") auto
  1516 
  1517 lemma nn_integral_eq_integral:
  1518   assumes f: "integrable M f"
  1519   assumes nonneg: "AE x in M. 0 \<le> f x" 
  1520   shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
  1521 proof -
  1522   { fix f :: "'a \<Rightarrow> real" assume f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "integrable M f"
  1523     then have "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
  1524     proof (induct rule: borel_measurable_induct_real)
  1525       case (set A) then show ?case
  1526         by (simp add: integrable_indicator_iff ereal_indicator emeasure_eq_ereal_measure)
  1527     next
  1528       case (mult f c) then show ?case
  1529         unfolding times_ereal.simps(1)[symmetric]
  1530         by (subst nn_integral_cmult)
  1531            (auto simp add: integrable_mult_left_iff zero_ereal_def[symmetric])
  1532     next
  1533       case (add g f)
  1534       then have "integrable M f" "integrable M g"
  1535         by (auto intro!: integrable_bound[OF add(8)])
  1536       with add show ?case
  1537         unfolding plus_ereal.simps(1)[symmetric]
  1538         by (subst nn_integral_add) auto
  1539     next
  1540       case (seq s)
  1541       { fix i x assume "x \<in> space M" with seq(4) have "s i x \<le> f x"
  1542           by (intro LIMSEQ_le_const[OF seq(5)] exI[of _ i]) (auto simp: incseq_def le_fun_def) }
  1543       note s_le_f = this
  1544 
  1545       show ?case
  1546       proof (rule LIMSEQ_unique)
  1547         show "(\<lambda>i. ereal (integral\<^sup>L M (s i))) ----> ereal (integral\<^sup>L M f)"
  1548           unfolding lim_ereal
  1549         proof (rule integral_dominated_convergence[where w=f])
  1550           show "integrable M f" by fact
  1551           from s_le_f seq show "\<And>i. AE x in M. norm (s i x) \<le> f x"
  1552             by auto
  1553         qed (insert seq, auto)
  1554         have int_s: "\<And>i. integrable M (s i)"
  1555           using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto
  1556         have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) ----> \<integral>\<^sup>+ x. f x \<partial>M"
  1557           using seq s_le_f f
  1558           by (intro nn_integral_dominated_convergence[where w=f])
  1559              (auto simp: integrable_iff_bounded)
  1560         also have "(\<lambda>i. \<integral>\<^sup>+x. s i x \<partial>M) = (\<lambda>i. \<integral>x. s i x \<partial>M)"
  1561           using seq int_s by simp
  1562         finally show "(\<lambda>i. \<integral>x. s i x \<partial>M) ----> \<integral>\<^sup>+x. f x \<partial>M"
  1563           by simp
  1564       qed
  1565     qed }
  1566   from this[of "\<lambda>x. max 0 (f x)"] assms have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = integral\<^sup>L M (\<lambda>x. max 0 (f x))"
  1567     by simp
  1568   also have "\<dots> = integral\<^sup>L M f"
  1569     using assms by (auto intro!: integral_cong_AE)
  1570   also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
  1571     using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
  1572   finally show ?thesis .
  1573 qed
  1574 
  1575 lemma
  1576   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1577   assumes integrable[measurable]: "\<And>i. integrable M (f i)"
  1578   and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
  1579   and sums: "summable (\<lambda>i. (\<integral>x. norm (f i x) \<partial>M))"
  1580   shows integrable_suminf: "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
  1581     and sums_integral: "(\<lambda>i. integral\<^sup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is "?f sums ?x")
  1582     and integral_suminf: "(\<integral>x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>L M (f i))"
  1583     and summable_integral: "summable (\<lambda>i. integral\<^sup>L M (f i))"
  1584 proof -
  1585   have 1: "integrable M (\<lambda>x. \<Sum>i. norm (f i x))"
  1586   proof (rule integrableI_bounded)
  1587     have "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) = (\<integral>\<^sup>+ x. (\<Sum>i. ereal (norm (f i x))) \<partial>M)"
  1588       apply (intro nn_integral_cong_AE) 
  1589       using summable
  1590       apply eventually_elim
  1591       apply (simp add: suminf_ereal' suminf_nonneg)
  1592       done
  1593     also have "\<dots> = (\<Sum>i. \<integral>\<^sup>+ x. norm (f i x) \<partial>M)"
  1594       by (intro nn_integral_suminf) auto
  1595     also have "\<dots> = (\<Sum>i. ereal (\<integral>x. norm (f i x) \<partial>M))"
  1596       by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
  1597     finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) < \<infinity>"
  1598       by (simp add: suminf_ereal' sums)
  1599   qed simp
  1600 
  1601   have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
  1602     using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
  1603 
  1604   have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
  1605     using summable
  1606   proof eventually_elim
  1607     fix j x assume [simp]: "summable (\<lambda>i. norm (f i x))"
  1608     have "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i<j. norm (f i x))" by (rule norm_setsum)
  1609     also have "\<dots> \<le> (\<Sum>i. norm (f i x))"
  1610       using setsum_le_suminf[of "\<lambda>i. norm (f i x)"] unfolding sums_iff by auto
  1611     finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
  1612   qed
  1613 
  1614   note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
  1615   note int = integral_dominated_convergence[OF _ _ 1 2 3]
  1616 
  1617   show "integrable M ?S"
  1618     by (rule ibl) measurable
  1619 
  1620   show "?f sums ?x" unfolding sums_def
  1621     using int by (simp add: integrable)
  1622   then show "?x = suminf ?f" "summable ?f"
  1623     unfolding sums_iff by auto
  1624 qed
  1625 
  1626 lemma integral_norm_bound:
  1627   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1628   shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
  1629   using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
  1630   using integral_norm_bound_ereal[of M f] by simp
  1631   
  1632 lemma integrableI_nn_integral_finite:
  1633   assumes [measurable]: "f \<in> borel_measurable M"
  1634     and nonneg: "AE x in M. 0 \<le> f x"
  1635     and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
  1636   shows "integrable M f"
  1637 proof (rule integrableI_bounded)
  1638   have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
  1639     using nonneg by (intro nn_integral_cong_AE) auto
  1640   with finite show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
  1641     by auto
  1642 qed simp
  1643 
  1644 lemma integral_eq_nn_integral:
  1645   assumes [measurable]: "f \<in> borel_measurable M"
  1646   assumes nonneg: "AE x in M. 0 \<le> f x"
  1647   shows "integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
  1648 proof cases
  1649   assume *: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = \<infinity>"
  1650   also have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
  1651     using nonneg by (intro nn_integral_cong_AE) auto
  1652   finally have "\<not> integrable M f"
  1653     by (auto simp: integrable_iff_bounded)
  1654   then show ?thesis
  1655     by (simp add: * not_integrable_integral_eq)
  1656 next
  1657   assume "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
  1658   then have "integrable M f"
  1659     by (cases "\<integral>\<^sup>+ x. ereal (f x) \<partial>M") (auto intro!: integrableI_nn_integral_finite assms)
  1660   from nn_integral_eq_integral[OF this nonneg] show ?thesis
  1661     by simp
  1662 qed
  1663   
  1664 lemma has_bochner_integral_nn_integral:
  1665   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
  1666   assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
  1667   shows "has_bochner_integral M f x"
  1668   unfolding has_bochner_integral_iff
  1669   using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
  1670 
  1671 lemma integrableI_simple_bochner_integrable:
  1672   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1673   shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
  1674   by (intro integrableI_sequence[where s="\<lambda>_. f"] borel_measurable_simple_function)
  1675      (auto simp: zero_ereal_def[symmetric] simple_bochner_integrable.simps)
  1676 
  1677 lemma integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
  1678   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1679   assumes "integrable M f"
  1680   assumes base: "\<And>A c. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R c)"
  1681   assumes add: "\<And>f g. integrable M f \<Longrightarrow> P f \<Longrightarrow> integrable M g \<Longrightarrow> P g \<Longrightarrow> P (\<lambda>x. f x + g x)"
  1682   assumes lim: "\<And>f s. (\<And>i. integrable M (s i)) \<Longrightarrow> (\<And>i. P (s i)) \<Longrightarrow>
  1683    (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x) \<Longrightarrow>
  1684    (\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)) \<Longrightarrow> integrable M f \<Longrightarrow> P f"
  1685   shows "P f"
  1686 proof -
  1687   from `integrable M f` have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1688     unfolding integrable_iff_bounded by auto
  1689   from borel_measurable_implies_sequence_metric[OF f(1)]
  1690   obtain s where s: "\<And>i. simple_function M (s i)" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x"
  1691     "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
  1692     unfolding norm_conv_dist by metis
  1693 
  1694   { fix f A 
  1695     have [simp]: "P (\<lambda>x. 0)"
  1696       using base[of "{}" undefined] by simp
  1697     have "(\<And>i::'b. i \<in> A \<Longrightarrow> integrable M (f i::'a \<Rightarrow> 'b)) \<Longrightarrow>
  1698     (\<And>i. i \<in> A \<Longrightarrow> P (f i)) \<Longrightarrow> P (\<lambda>x. \<Sum>i\<in>A. f i x)"
  1699     by (induct A rule: infinite_finite_induct) (auto intro!: add) }
  1700   note setsum = this
  1701 
  1702   def s' \<equiv> "\<lambda>i z. indicator (space M) z *\<^sub>R s i z"
  1703   then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x"
  1704     by simp
  1705 
  1706   have sf[measurable]: "\<And>i. simple_function M (s' i)"
  1707     unfolding s'_def using s(1)
  1708     by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto
  1709 
  1710   { fix i 
  1711     have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
  1712         (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})"
  1713       by (auto simp add: s'_def split: split_indicator)
  1714     then have "\<And>z. s' i = (\<lambda>z. \<Sum>y\<in>s' i`space M - {0}. indicator {x\<in>space M. s' i x = y} z *\<^sub>R y)"
  1715       using sf by (auto simp: fun_eq_iff simple_function_def s'_def) }
  1716   note s'_eq = this
  1717 
  1718   show "P f"
  1719   proof (rule lim)
  1720     fix i
  1721 
  1722     have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
  1723       using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
  1724     also have "\<dots> < \<infinity>"
  1725       using f by (subst nn_integral_cmult) auto
  1726     finally have sbi: "simple_bochner_integrable M (s' i)"
  1727       using sf by (intro simple_bochner_integrableI_bounded) auto
  1728     then show "integrable M (s' i)"
  1729       by (rule integrableI_simple_bochner_integrable)
  1730 
  1731     { fix x assume"x \<in> space M" "s' i x \<noteq> 0"
  1732       then have "emeasure M {y \<in> space M. s' i y = s' i x} \<le> emeasure M {y \<in> space M. s' i y \<noteq> 0}"
  1733         by (intro emeasure_mono) auto
  1734       also have "\<dots> < \<infinity>"
  1735         using sbi by (auto elim: simple_bochner_integrable.cases)
  1736       finally have "emeasure M {y \<in> space M. s' i y = s' i x} \<noteq> \<infinity>" by simp }
  1737     then show "P (s' i)"
  1738       by (subst s'_eq) (auto intro!: setsum base)
  1739 
  1740     fix x assume "x \<in> space M" with s show "(\<lambda>i. s' i x) ----> f x"
  1741       by (simp add: s'_eq_s)
  1742     show "norm (s' i x) \<le> 2 * norm (f x)"
  1743       using `x \<in> space M` s by (simp add: s'_eq_s)
  1744   qed fact
  1745 qed
  1746 
  1747 lemma integral_nonneg_AE:
  1748   fixes f :: "'a \<Rightarrow> real"
  1749   assumes [measurable]: "AE x in M. 0 \<le> f x"
  1750   shows "0 \<le> integral\<^sup>L M f"
  1751 proof cases
  1752   assume [measurable]: "integrable M f"
  1753   then have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
  1754     by (subst integral_eq_nn_integral) (auto intro: real_of_ereal_pos nn_integral_nonneg assms)
  1755   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
  1756     using assms by (intro integral_cong_AE assms integrable_max) auto
  1757   finally show ?thesis
  1758     by simp
  1759 qed (simp add: not_integrable_integral_eq)
  1760 
  1761 lemma integral_eq_zero_AE:
  1762   "(AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
  1763   using integral_cong_AE[of f M "\<lambda>_. 0"]
  1764   by (cases "integrable M f") (simp_all add: not_integrable_integral_eq)
  1765 
  1766 lemma integral_nonneg_eq_0_iff_AE:
  1767   fixes f :: "_ \<Rightarrow> real"
  1768   assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \<le> f x"
  1769   shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
  1770 proof
  1771   assume "integral\<^sup>L M f = 0"
  1772   then have "integral\<^sup>N M f = 0"
  1773     using nn_integral_eq_integral[OF f nonneg] by simp
  1774   then have "AE x in M. ereal (f x) \<le> 0"
  1775     by (simp add: nn_integral_0_iff_AE)
  1776   with nonneg show "AE x in M. f x = 0"
  1777     by auto
  1778 qed (auto simp add: integral_eq_zero_AE)
  1779 
  1780 lemma integral_mono_AE:
  1781   fixes f :: "'a \<Rightarrow> real"
  1782   assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
  1783   shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1784 proof -
  1785   have "0 \<le> integral\<^sup>L M (\<lambda>x. g x - f x)"
  1786     using assms by (intro integral_nonneg_AE integrable_diff assms) auto
  1787   also have "\<dots> = integral\<^sup>L M g - integral\<^sup>L M f"
  1788     by (intro integral_diff assms)
  1789   finally show ?thesis by simp
  1790 qed
  1791 
  1792 lemma integral_mono:
  1793   fixes f :: "'a \<Rightarrow> real"
  1794   shows "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x) \<Longrightarrow> 
  1795     integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1796   by (intro integral_mono_AE) auto
  1797 
  1798 lemma (in finite_measure) integrable_measure: 
  1799   assumes I: "disjoint_family_on X I" "countable I"
  1800   shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
  1801 proof -
  1802   have "(\<integral>\<^sup>+i. measure M (X i) \<partial>count_space I) = (\<integral>\<^sup>+i. measure M (if X i \<in> sets M then X i else {}) \<partial>count_space I)"
  1803     by (auto intro!: nn_integral_cong measure_notin_sets)
  1804   also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
  1805     using I unfolding emeasure_eq_measure[symmetric]
  1806     by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
  1807   finally show ?thesis
  1808     by (auto intro!: integrableI_bounded simp: measure_nonneg)
  1809 qed
  1810 
  1811 lemma integrableI_real_bounded:
  1812   assumes f: "f \<in> borel_measurable M" and ae: "AE x in M. 0 \<le> f x" and fin: "integral\<^sup>N M f < \<infinity>"
  1813   shows "integrable M f"
  1814 proof (rule integrableI_bounded)
  1815   have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ereal (f x) \<partial>M"
  1816     using ae by (auto intro: nn_integral_cong_AE)
  1817   also note fin
  1818   finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
  1819 qed fact
  1820 
  1821 lemma integral_real_bounded:
  1822   assumes "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
  1823   shows "integral\<^sup>L M f \<le> r"
  1824 proof cases
  1825   assume "integrable M f" from nn_integral_eq_integral[OF this] assms show ?thesis
  1826     by simp
  1827 next
  1828   assume "\<not> integrable M f"
  1829   moreover have "0 \<le> ereal r"
  1830     using nn_integral_nonneg assms(2) by (rule order_trans)
  1831   ultimately show ?thesis
  1832     by (simp add: not_integrable_integral_eq)
  1833 qed
  1834 
  1835 subsection {* Restricted measure spaces *}
  1836 
  1837 lemma integrable_restrict_space:
  1838   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1839   assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  1840   shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  1841   unfolding integrable_iff_bounded
  1842     borel_measurable_restrict_space_iff[OF \<Omega>]
  1843     nn_integral_restrict_space[OF \<Omega>]
  1844   by (simp add: ac_simps ereal_indicator times_ereal.simps(1)[symmetric] del: times_ereal.simps)
  1845 
  1846 lemma integral_restrict_space:
  1847   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1848   assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  1849   shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  1850 proof (rule integral_eq_cases)
  1851   assume "integrable (restrict_space M \<Omega>) f"
  1852   then show ?thesis
  1853   proof induct
  1854     case (base A c) then show ?case
  1855       by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
  1856                     emeasure_restrict_space Int_absorb1 measure_restrict_space)
  1857   next
  1858     case (add g f) then show ?case
  1859       by (simp add: scaleR_add_right integrable_restrict_space)
  1860   next
  1861     case (lim f s)
  1862     show ?case
  1863     proof (rule LIMSEQ_unique)
  1864       show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> integral\<^sup>L (restrict_space M \<Omega>) f"
  1865         using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
  1866       
  1867       show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
  1868         unfolding lim
  1869         using lim
  1870         by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
  1871            (auto simp add: space_restrict_space integrable_restrict_space
  1872                  simp del: norm_scaleR
  1873                  split: split_indicator)
  1874     qed
  1875   qed
  1876 qed (simp add: integrable_restrict_space)
  1877 
  1878 subsection {* Measure spaces with an associated density *}
  1879 
  1880 lemma integrable_density:
  1881   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1882   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1883     and nn: "AE x in M. 0 \<le> g x"
  1884   shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
  1885   unfolding integrable_iff_bounded using nn
  1886   apply (simp add: nn_integral_density )
  1887   apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
  1888   apply auto
  1889   done
  1890 
  1891 lemma integral_density:
  1892   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1893   assumes f: "f \<in> borel_measurable M"
  1894     and g[measurable]: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
  1895   shows "integral\<^sup>L (density M g) f = integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
  1896 proof (rule integral_eq_cases)
  1897   assume "integrable (density M g) f"
  1898   then show ?thesis
  1899   proof induct
  1900     case (base A c)
  1901     then have [measurable]: "A \<in> sets M" by auto
  1902   
  1903     have int: "integrable M (\<lambda>x. g x * indicator A x)"
  1904       using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
  1905     then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ereal (g x * indicator A x) \<partial>M)"
  1906       using g by (subst nn_integral_eq_integral) auto
  1907     also have "\<dots> = (\<integral>\<^sup>+ x. ereal (g x) * indicator A x \<partial>M)"
  1908       by (intro nn_integral_cong) (auto split: split_indicator)
  1909     also have "\<dots> = emeasure (density M g) A"
  1910       by (rule emeasure_density[symmetric]) auto
  1911     also have "\<dots> = ereal (measure (density M g) A)"
  1912       using base by (auto intro: emeasure_eq_ereal_measure)
  1913     also have "\<dots> = integral\<^sup>L (density M g) (indicator A)"
  1914       using base by simp
  1915     finally show ?case
  1916       using base by (simp add: int)
  1917   next
  1918     case (add f h)
  1919     then have [measurable]: "f \<in> borel_measurable M" "h \<in> borel_measurable M"
  1920       by (auto dest!: borel_measurable_integrable)
  1921     from add g show ?case
  1922       by (simp add: scaleR_add_right integrable_density)
  1923   next
  1924     case (lim f s)
  1925     have [measurable]: "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M"
  1926       using lim(1,5)[THEN borel_measurable_integrable] by auto
  1927   
  1928     show ?case
  1929     proof (rule LIMSEQ_unique)
  1930       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
  1931       proof (rule integral_dominated_convergence)
  1932         show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
  1933           by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
  1934         show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x"
  1935           using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M])
  1936         show "\<And>i. AE x in M. norm (g x *\<^sub>R s i x) \<le> 2 * norm (g x *\<^sub>R f x)"
  1937           using lim(4) g by (auto intro!: AE_I2[of M] mult_left_mono simp: field_simps)
  1938       qed auto
  1939       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
  1940         unfolding lim(2)[symmetric]
  1941         by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  1942            (insert lim(3-5), auto)
  1943     qed
  1944   qed
  1945 qed (simp add: f g integrable_density)
  1946 
  1947 lemma
  1948   fixes g :: "'a \<Rightarrow> real"
  1949   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "g \<in> borel_measurable M"
  1950   shows integral_real_density: "integral\<^sup>L (density M f) g = (\<integral> x. f x * g x \<partial>M)"
  1951     and integrable_real_density: "integrable (density M f) g \<longleftrightarrow> integrable M (\<lambda>x. f x * g x)"
  1952   using assms integral_density[of g M f] integrable_density[of g M f] by auto
  1953 
  1954 lemma has_bochner_integral_density:
  1955   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1956   shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. 0 \<le> g x) \<Longrightarrow>
  1957     has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
  1958   by (simp add: has_bochner_integral_iff integrable_density integral_density)
  1959 
  1960 subsection {* Distributions *}
  1961 
  1962 lemma integrable_distr_eq:
  1963   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1964   assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
  1965   shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
  1966   unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
  1967 
  1968 lemma integrable_distr:
  1969   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1970   shows "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
  1971   by (subst integrable_distr_eq[symmetric, where g=T])
  1972      (auto dest: borel_measurable_integrable)
  1973 
  1974 lemma integral_distr:
  1975   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1976   assumes g[measurable]: "g \<in> measurable M N" and f: "f \<in> borel_measurable N"
  1977   shows "integral\<^sup>L (distr M N g) f = integral\<^sup>L M (\<lambda>x. f (g x))"
  1978 proof (rule integral_eq_cases)
  1979   assume "integrable (distr M N g) f"
  1980   then show ?thesis
  1981   proof induct
  1982     case (base A c)
  1983     then have [measurable]: "A \<in> sets N" by auto
  1984     from base have int: "integrable (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c)"
  1985       by (intro integrable_indicator)
  1986   
  1987     have "integral\<^sup>L (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c) = measure (distr M N g) A *\<^sub>R c"
  1988       using base by auto
  1989     also have "\<dots> = measure M (g -` A \<inter> space M) *\<^sub>R c"
  1990       by (subst measure_distr) auto
  1991     also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator (g -` A \<inter> space M) a *\<^sub>R c)"
  1992       using base by (auto simp: emeasure_distr)
  1993     also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator A (g a) *\<^sub>R c)"
  1994       using int base by (intro integral_cong_AE) (auto simp: emeasure_distr split: split_indicator)
  1995     finally show ?case .
  1996   next
  1997     case (add f h)
  1998     then have [measurable]: "f \<in> borel_measurable N" "h \<in> borel_measurable N"
  1999       by (auto dest!: borel_measurable_integrable)
  2000     from add g show ?case
  2001       by (simp add: scaleR_add_right integrable_distr_eq)
  2002   next
  2003     case (lim f s)
  2004     have [measurable]: "f \<in> borel_measurable N" "\<And>i. s i \<in> borel_measurable N"
  2005       using lim(1,5)[THEN borel_measurable_integrable] by auto
  2006   
  2007     show ?case
  2008     proof (rule LIMSEQ_unique)
  2009       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
  2010       proof (rule integral_dominated_convergence)
  2011         show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
  2012           using lim by (auto simp: integrable_distr_eq) 
  2013         show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
  2014           using lim(3) g[THEN measurable_space] by auto
  2015         show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
  2016           using lim(4) g[THEN measurable_space] by auto
  2017       qed auto
  2018       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
  2019         unfolding lim(2)[symmetric]
  2020         by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  2021            (insert lim(3-5), auto)
  2022     qed
  2023   qed
  2024 qed (simp add: f g integrable_distr_eq)
  2025 
  2026 lemma has_bochner_integral_distr:
  2027   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2028   shows "f \<in> borel_measurable N \<Longrightarrow> g \<in> measurable M N \<Longrightarrow>
  2029     has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
  2030   by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
  2031 
  2032 subsection {* Lebesgue integration on @{const count_space} *}
  2033 
  2034 lemma integrable_count_space:
  2035   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  2036   shows "finite X \<Longrightarrow> integrable (count_space X) f"
  2037   by (auto simp: nn_integral_count_space integrable_iff_bounded)
  2038 
  2039 lemma measure_count_space[simp]:
  2040   "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
  2041   unfolding measure_def by (subst emeasure_count_space ) auto
  2042 
  2043 lemma lebesgue_integral_count_space_finite_support:
  2044   assumes f: "finite {a\<in>A. f a \<noteq> 0}"
  2045   shows "(\<integral>x. f x \<partial>count_space A) = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. f a)"
  2046 proof -
  2047   have eq: "\<And>x. x \<in> A \<Longrightarrow> (\<Sum>a | x = a \<and> a \<in> A \<and> f a \<noteq> 0. f a) = (\<Sum>x\<in>{x}. f x)"
  2048     by (intro setsum.mono_neutral_cong_left) auto
  2049     
  2050   have "(\<integral>x. f x \<partial>count_space A) = (\<integral>x. (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. indicator {a} x *\<^sub>R f a) \<partial>count_space A)"
  2051     by (intro integral_cong refl) (simp add: f eq)
  2052   also have "\<dots> = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. measure (count_space A) {a} *\<^sub>R f a)"
  2053     by (subst integral_setsum) (auto intro!: setsum.cong)
  2054   finally show ?thesis
  2055     by auto
  2056 qed
  2057 
  2058 lemma lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
  2059   by (subst lebesgue_integral_count_space_finite_support)
  2060      (auto intro!: setsum.mono_neutral_cong_left)
  2061 
  2062 lemma integrable_count_space_nat_iff:
  2063   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2064   shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
  2065   by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat summable_ereal suminf_ereal_finite)
  2066 
  2067 lemma sums_integral_count_space_nat:
  2068   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2069   assumes *: "integrable (count_space UNIV) f"
  2070   shows "f sums (integral\<^sup>L (count_space UNIV) f)"
  2071 proof -
  2072   let ?f = "\<lambda>n i. indicator {n} i *\<^sub>R f i"
  2073   have f': "\<And>n i. ?f n i = indicator {n} i *\<^sub>R f n"
  2074     by (auto simp: fun_eq_iff split: split_indicator)
  2075 
  2076   have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) sums \<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV"
  2077   proof (rule sums_integral)
  2078     show "\<And>i. integrable (count_space UNIV) (?f i)"
  2079       using * by (intro integrable_mult_indicator) auto
  2080     show "AE n in count_space UNIV. summable (\<lambda>i. norm (?f i n))"
  2081       using summable_finite[of "{n}" "\<lambda>i. norm (?f i n)" for n] by simp
  2082     show "summable (\<lambda>i. \<integral> n. norm (?f i n) \<partial>count_space UNIV)"
  2083       using * by (subst f') (simp add: integrable_count_space_nat_iff)
  2084   qed
  2085   also have "(\<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV) = (\<integral>n. f n \<partial>count_space UNIV)"
  2086     using suminf_finite[of "{n}" "\<lambda>i. ?f i n" for n] by (auto intro!: integral_cong)
  2087   also have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) = f"
  2088     by (subst f') simp
  2089   finally show ?thesis .
  2090 qed
  2091 
  2092 lemma integral_count_space_nat:
  2093   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2094   shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
  2095   using sums_integral_count_space_nat by (rule sums_unique)
  2096 
  2097 subsection {* Point measure *}
  2098 
  2099 lemma lebesgue_integral_point_measure_finite:
  2100   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2101   shows "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow>
  2102     integral\<^sup>L (point_measure A f) g = (\<Sum>a\<in>A. f a *\<^sub>R g a)"
  2103   by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def)
  2104 
  2105 lemma integrable_point_measure_finite:
  2106   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and f :: "'a \<Rightarrow> real"
  2107   shows "finite A \<Longrightarrow> integrable (point_measure A f) g"
  2108   unfolding point_measure_def
  2109   apply (subst density_ereal_max_0)
  2110   apply (subst integrable_density)
  2111   apply (auto simp: AE_count_space integrable_count_space)
  2112   done
  2113 
  2114 subsection {* Lebesgue integration on @{const null_measure} *}
  2115 
  2116 lemma has_bochner_integral_null_measure_iff[iff]:
  2117   "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
  2118   by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
  2119            intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
  2120 
  2121 lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
  2122   by (auto simp add: integrable.simps)
  2123 
  2124 lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
  2125   by (cases "integrable (null_measure M) f")
  2126      (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
  2127 
  2128 subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
  2129 
  2130 lemma real_lebesgue_integral_def:
  2131   assumes f[measurable]: "integrable M f"
  2132   shows "integral\<^sup>L M f = real (\<integral>\<^sup>+x. f x \<partial>M) - real (\<integral>\<^sup>+x. - f x \<partial>M)"
  2133 proof -
  2134   have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
  2135     by (auto intro!: arg_cong[where f="integral\<^sup>L M"])
  2136   also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
  2137     by (intro integral_diff integrable_max integrable_minus integrable_zero f)
  2138   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
  2139     by (subst integral_eq_nn_integral[symmetric]) auto
  2140   also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
  2141     by (subst integral_eq_nn_integral[symmetric]) auto
  2142   also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
  2143     by (auto simp: max_def)
  2144   also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
  2145     by (auto simp: max_def)
  2146   finally show ?thesis
  2147     unfolding nn_integral_max_0 .
  2148 qed
  2149 
  2150 lemma real_integrable_def:
  2151   "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
  2152     (\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
  2153   unfolding integrable_iff_bounded
  2154 proof (safe del: notI)
  2155   assume *: "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
  2156   have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
  2157     by (intro nn_integral_mono) auto
  2158   also note *
  2159   finally show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
  2160     by simp
  2161   have "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
  2162     by (intro nn_integral_mono) auto
  2163   also note *
  2164   finally show "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
  2165     by simp
  2166 next
  2167   assume [measurable]: "f \<in> borel_measurable M"
  2168   assume fin: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
  2169   have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) + max 0 (ereal (- f x)) \<partial>M)"
  2170     by (intro nn_integral_cong) (auto simp: max_def)
  2171   also have"\<dots> = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (ereal (- f x)) \<partial>M)"
  2172     by (intro nn_integral_add) auto
  2173   also have "\<dots> < \<infinity>"
  2174     using fin by (auto simp: nn_integral_max_0)
  2175   finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
  2176 qed
  2177 
  2178 lemma integrableD[dest]:
  2179   assumes "integrable M f"
  2180   shows "f \<in> borel_measurable M" "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
  2181   using assms unfolding real_integrable_def by auto
  2182 
  2183 lemma integrableE:
  2184   assumes "integrable M f"
  2185   obtains r q where
  2186     "(\<integral>\<^sup>+x. ereal (f x)\<partial>M) = ereal r"
  2187     "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M) = ereal q"
  2188     "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
  2189   using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
  2190   using nn_integral_nonneg[of M "\<lambda>x. ereal (f x)"]
  2191   using nn_integral_nonneg[of M "\<lambda>x. ereal (-f x)"]
  2192   by (cases rule: ereal2_cases[of "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ereal (f x)\<partial>M)"]) auto
  2193 
  2194 lemma integral_monotone_convergence_nonneg:
  2195   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  2196   assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  2197     and pos: "\<And>i. AE x in M. 0 \<le> f i x"
  2198     and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
  2199     and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) ----> x"
  2200     and u: "u \<in> borel_measurable M"
  2201   shows "integrable M u"
  2202   and "integral\<^sup>L M u = x"
  2203 proof -
  2204   have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ereal (f n x) \<partial>M))"
  2205   proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
  2206     fix i
  2207     from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
  2208       by eventually_elim (auto simp: mono_def)
  2209     show "(\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
  2210       using i by auto
  2211   next
  2212     show "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ereal (f i x)) \<partial>M"
  2213       apply (rule nn_integral_cong_AE)
  2214       using lim mono
  2215       by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2])
  2216   qed
  2217   also have "\<dots> = ereal x"
  2218     using mono i unfolding nn_integral_eq_integral[OF i pos]
  2219     by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim)
  2220   finally have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = ereal x" .
  2221   moreover have "(\<integral>\<^sup>+ x. ereal (- u x) \<partial>M) = 0"
  2222   proof (subst nn_integral_0_iff_AE)
  2223     show "(\<lambda>x. ereal (- u x)) \<in> borel_measurable M"
  2224       using u by auto
  2225     from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
  2226     proof eventually_elim
  2227       fix x assume "mono (\<lambda>n. f n x)" "0 \<le> f 0 x" "(\<lambda>i. f i x) ----> u x"
  2228       then show "ereal (- u x) \<le> 0"
  2229         using incseq_le[of "\<lambda>n. f n x" "u x" 0] by (simp add: mono_def incseq_def)
  2230     qed
  2231   qed
  2232   ultimately show "integrable M u" "integral\<^sup>L M u = x"
  2233     by (auto simp: real_integrable_def real_lebesgue_integral_def u)
  2234 qed
  2235 
  2236 lemma
  2237   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  2238   assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  2239   and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
  2240   and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) ----> x"
  2241   and u: "u \<in> borel_measurable M"
  2242   shows integrable_monotone_convergence: "integrable M u"
  2243     and integral_monotone_convergence: "integral\<^sup>L M u = x"
  2244     and has_bochner_integral_monotone_convergence: "has_bochner_integral M u x"
  2245 proof -
  2246   have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
  2247     using f by auto
  2248   have 2: "AE x in M. mono (\<lambda>n. f n x - f 0 x)"
  2249     using mono by (auto simp: mono_def le_fun_def)
  2250   have 3: "\<And>n. AE x in M. 0 \<le> f n x - f 0 x"
  2251     using mono by (auto simp: field_simps mono_def le_fun_def)
  2252   have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
  2253     using lim by (auto intro!: tendsto_diff)
  2254   have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^sup>L M (f 0)"
  2255     using f ilim by (auto intro!: tendsto_diff)
  2256   have 6: "(\<lambda>x. u x - f 0 x) \<in> borel_measurable M"
  2257     using f[of 0] u by auto
  2258   note diff = integral_monotone_convergence_nonneg[OF 1 2 3 4 5 6]
  2259   have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
  2260     using diff(1) f by (rule integrable_add)
  2261   with diff(2) f show "integrable M u" "integral\<^sup>L M u = x"
  2262     by auto
  2263   then show "has_bochner_integral M u x"
  2264     by (metis has_bochner_integral_integrable)
  2265 qed
  2266 
  2267 lemma integral_norm_eq_0_iff:
  2268   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2269   assumes f[measurable]: "integrable M f"
  2270   shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
  2271 proof -
  2272   have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>x. norm (f x) \<partial>M)"
  2273     using f by (intro nn_integral_eq_integral integrable_norm) auto
  2274   then have "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) = 0"
  2275     by simp
  2276   also have "\<dots> \<longleftrightarrow> emeasure M {x\<in>space M. ereal (norm (f x)) \<noteq> 0} = 0"
  2277     by (intro nn_integral_0_iff) auto
  2278   finally show ?thesis
  2279     by simp
  2280 qed
  2281 
  2282 lemma integral_0_iff:
  2283   fixes f :: "'a \<Rightarrow> real"
  2284   shows "integrable M f \<Longrightarrow> (\<integral>x. abs (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
  2285   using integral_norm_eq_0_iff[of M f] by simp
  2286 
  2287 lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
  2288   using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong)
  2289 
  2290 lemma lebesgue_integral_const[simp]: 
  2291   fixes a :: "'a :: {banach, second_countable_topology}"
  2292   shows "(\<integral>x. a \<partial>M) = measure M (space M) *\<^sub>R a"
  2293 proof -
  2294   { assume "emeasure M (space M) = \<infinity>" "a \<noteq> 0"
  2295     then have ?thesis
  2296       by (simp add: not_integrable_integral_eq measure_def integrable_iff_bounded) }
  2297   moreover
  2298   { assume "a = 0" then have ?thesis by simp }
  2299   moreover
  2300   { assume "emeasure M (space M) \<noteq> \<infinity>"
  2301     interpret finite_measure M
  2302       proof qed fact
  2303     have "(\<integral>x. a \<partial>M) = (\<integral>x. indicator (space M) x *\<^sub>R a \<partial>M)"
  2304       by (intro integral_cong) auto
  2305     also have "\<dots> = measure M (space M) *\<^sub>R a"
  2306       by simp
  2307     finally have ?thesis . }
  2308   ultimately show ?thesis by blast
  2309 qed
  2310 
  2311 lemma (in finite_measure) integrable_const_bound:
  2312   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  2313   shows "AE x in M. norm (f x) \<le> B \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> integrable M f"
  2314   apply (rule integrable_bound[OF integrable_const[of B], of f])
  2315   apply assumption
  2316   apply (cases "0 \<le> B")
  2317   apply auto
  2318   done
  2319 
  2320 lemma integral_indicator_finite_real:
  2321   fixes f :: "'a \<Rightarrow> real"
  2322   assumes [simp]: "finite A"
  2323   assumes [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"
  2324   assumes finite: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} < \<infinity>"
  2325   shows "(\<integral>x. f x * indicator A x \<partial>M) = (\<Sum>a\<in>A. f a * measure M {a})"
  2326 proof -
  2327   have "(\<integral>x. f x * indicator A x \<partial>M) = (\<integral>x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
  2328   proof (intro integral_cong refl)
  2329     fix x show "f x * indicator A x = (\<Sum>a\<in>A. f a * indicator {a} x)"
  2330       by (auto split: split_indicator simp: eq_commute[of x] cong: conj_cong)
  2331   qed
  2332   also have "\<dots> = (\<Sum>a\<in>A. f a * measure M {a})"
  2333     using finite by (subst integral_setsum) (auto simp add: integrable_mult_left_iff)
  2334   finally show ?thesis .
  2335 qed
  2336 
  2337 lemma (in finite_measure) ereal_integral_real:
  2338   assumes [measurable]: "f \<in> borel_measurable M" 
  2339   assumes ae: "AE x in M. 0 \<le> f x" "AE x in M. f x \<le> ereal B"
  2340   shows "ereal (\<integral>x. real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  2341 proof (subst nn_integral_eq_integral[symmetric])
  2342   show "integrable M (\<lambda>x. real (f x))"
  2343     using ae by (intro integrable_const_bound[where B=B]) (auto simp: real_le_ereal_iff)
  2344   show "AE x in M. 0 \<le> real (f x)"
  2345     using ae by (auto simp: real_of_ereal_pos)
  2346   show "(\<integral>\<^sup>+ x. ereal (real (f x)) \<partial>M) = integral\<^sup>N M f"
  2347     using ae by (intro nn_integral_cong_AE) (auto simp: ereal_real)
  2348 qed
  2349 
  2350 lemma (in finite_measure) integral_less_AE:
  2351   fixes X Y :: "'a \<Rightarrow> real"
  2352   assumes int: "integrable M X" "integrable M Y"
  2353   assumes A: "(emeasure M) A \<noteq> 0" "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> X x \<noteq> Y x"
  2354   assumes gt: "AE x in M. X x \<le> Y x"
  2355   shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  2356 proof -
  2357   have "integral\<^sup>L M X \<le> integral\<^sup>L M Y"
  2358     using gt int by (intro integral_mono_AE) auto
  2359   moreover
  2360   have "integral\<^sup>L M X \<noteq> integral\<^sup>L M Y"
  2361   proof
  2362     assume eq: "integral\<^sup>L M X = integral\<^sup>L M Y"
  2363     have "integral\<^sup>L M (\<lambda>x. \<bar>Y x - X x\<bar>) = integral\<^sup>L M (\<lambda>x. Y x - X x)"
  2364       using gt int by (intro integral_cong_AE) auto
  2365     also have "\<dots> = 0"
  2366       using eq int by simp
  2367     finally have "(emeasure M) {x \<in> space M. Y x - X x \<noteq> 0} = 0"
  2368       using int by (simp add: integral_0_iff)
  2369     moreover
  2370     have "(\<integral>\<^sup>+x. indicator A x \<partial>M) \<le> (\<integral>\<^sup>+x. indicator {x \<in> space M. Y x - X x \<noteq> 0} x \<partial>M)"
  2371       using A by (intro nn_integral_mono_AE) auto
  2372     then have "(emeasure M) A \<le> (emeasure M) {x \<in> space M. Y x - X x \<noteq> 0}"
  2373       using int A by (simp add: integrable_def)
  2374     ultimately have "emeasure M A = 0"
  2375       using emeasure_nonneg[of M A] by simp
  2376     with `(emeasure M) A \<noteq> 0` show False by auto
  2377   qed
  2378   ultimately show ?thesis by auto
  2379 qed
  2380 
  2381 lemma (in finite_measure) integral_less_AE_space:
  2382   fixes X Y :: "'a \<Rightarrow> real"
  2383   assumes int: "integrable M X" "integrable M Y"
  2384   assumes gt: "AE x in M. X x < Y x" "emeasure M (space M) \<noteq> 0"
  2385   shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  2386   using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
  2387 
  2388 lemma tendsto_integral_at_top:
  2389   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
  2390   assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
  2391   shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
  2392 proof (rule tendsto_at_topI_sequentially)
  2393   fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
  2394   show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) ----> integral\<^sup>L M f"
  2395   proof (rule integral_dominated_convergence)
  2396     show "integrable M (\<lambda>x. norm (f x))"
  2397       by (rule integrable_norm) fact
  2398     show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
  2399     proof
  2400       fix x
  2401       from `filterlim X at_top sequentially` 
  2402       have "eventually (\<lambda>n. x \<le> X n) sequentially"
  2403         unfolding filterlim_at_top_ge[where c=x] by auto
  2404       then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
  2405         by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
  2406     qed
  2407     fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
  2408       by (auto split: split_indicator)
  2409   qed auto
  2410 qed
  2411 
  2412 lemma
  2413   fixes f :: "real \<Rightarrow> real"
  2414   assumes M: "sets M = sets borel"
  2415   assumes nonneg: "AE x in M. 0 \<le> f x"
  2416   assumes borel: "f \<in> borel_measurable borel"
  2417   assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
  2418   assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> x) at_top"
  2419   shows has_bochner_integral_monotone_convergence_at_top: "has_bochner_integral M f x"
  2420     and integrable_monotone_convergence_at_top: "integrable M f"
  2421     and integral_monotone_convergence_at_top:"integral\<^sup>L M f = x"
  2422 proof -
  2423   from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
  2424     by (auto split: split_indicator intro!: monoI)
  2425   { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
  2426       by (rule eventually_sequentiallyI[of "natceiling x"])
  2427          (auto split: split_indicator simp: natceiling_le_eq) }
  2428   from filterlim_cong[OF refl refl this]
  2429   have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
  2430     by simp
  2431   have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
  2432     using conv filterlim_real_sequentially by (rule filterlim_compose)
  2433   have M_measure[simp]: "borel_measurable M = borel_measurable borel"
  2434     using M by (simp add: sets_eq_imp_space_eq measurable_def)
  2435   have "f \<in> borel_measurable M"
  2436     using borel by simp
  2437   show "has_bochner_integral M f x"
  2438     by (rule has_bochner_integral_monotone_convergence) fact+
  2439   then show "integrable M f" "integral\<^sup>L M f = x"
  2440     by (auto simp: _has_bochner_integral_iff)
  2441 qed
  2442 
  2443 subsection {* Product measure *}
  2444 
  2445 lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
  2446   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  2447   assumes [measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  2448   shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
  2449 proof -
  2450   have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
  2451     unfolding integrable_iff_bounded by simp
  2452   show ?thesis
  2453     by (simp cong: measurable_cong)
  2454 qed
  2455 
  2456 lemma (in sigma_finite_measure) measurable_measure[measurable (raw)]:
  2457   "(\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M) \<Longrightarrow>
  2458     {x \<in> space (N \<Otimes>\<^sub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^sub>M M) \<Longrightarrow>
  2459     (\<lambda>x. measure M (A x)) \<in> borel_measurable N"
  2460   unfolding measure_def by (intro measurable_emeasure borel_measurable_real_of_ereal)
  2461 
  2462 lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
  2463 
  2464 lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
  2465   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  2466   assumes f[measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  2467   shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
  2468 proof -
  2469   from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
  2470   then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
  2471     "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) ----> f x y"
  2472     "\<And>i x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> norm (s i (x, y)) \<le> 2 * norm (f x y)"
  2473     by (auto simp: space_pair_measure norm_conv_dist)
  2474 
  2475   have [measurable]: "\<And>i. s i \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  2476     by (rule borel_measurable_simple_function) fact
  2477 
  2478   have "\<And>i. s i \<in> measurable (N \<Otimes>\<^sub>M M) (count_space UNIV)"
  2479     by (rule measurable_simple_function) fact
  2480 
  2481   def f' \<equiv> "\<lambda>i x. if integrable M (f x) then simple_bochner_integral M (\<lambda>y. s i (x, y)) else 0"
  2482 
  2483   { fix i x assume "x \<in> space N"
  2484     then have "simple_bochner_integral M (\<lambda>y. s i (x, y)) =
  2485       (\<Sum>z\<in>s i ` (space N \<times> space M). measure M {y \<in> space M. s i (x, y) = z} *\<^sub>R z)"
  2486       using s(1)[THEN simple_functionD(1)]
  2487       unfolding simple_bochner_integral_def
  2488       by (intro setsum.mono_neutral_cong_left)
  2489          (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
  2490   note eq = this
  2491 
  2492   show ?thesis
  2493   proof (rule borel_measurable_LIMSEQ_metric)
  2494     fix i show "f' i \<in> borel_measurable N"
  2495       unfolding f'_def by (simp_all add: eq cong: measurable_cong if_cong)
  2496   next
  2497     fix x assume x: "x \<in> space N"
  2498     { assume int_f: "integrable M (f x)"
  2499       have int_2f: "integrable M (\<lambda>y. 2 * norm (f x y))"
  2500         by (intro integrable_norm integrable_mult_right int_f)
  2501       have "(\<lambda>i. integral\<^sup>L M (\<lambda>y. s i (x, y))) ----> integral\<^sup>L M (f x)"
  2502       proof (rule integral_dominated_convergence)
  2503         from int_f show "f x \<in> borel_measurable M" by auto
  2504         show "\<And>i. (\<lambda>y. s i (x, y)) \<in> borel_measurable M"
  2505           using x by simp
  2506         show "AE xa in M. (\<lambda>i. s i (x, xa)) ----> f x xa"
  2507           using x s(2) by auto
  2508         show "\<And>i. AE xa in M. norm (s i (x, xa)) \<le> 2 * norm (f x xa)"
  2509           using x s(3) by auto
  2510       qed fact
  2511       moreover
  2512       { fix i
  2513         have "simple_bochner_integrable M (\<lambda>y. s i (x, y))"
  2514         proof (rule simple_bochner_integrableI_bounded)
  2515           have "(\<lambda>y. s i (x, y)) ` space M \<subseteq> s i ` (space N \<times> space M)"
  2516             using x by auto
  2517           then show "simple_function M (\<lambda>y. s i (x, y))"
  2518             using simple_functionD(1)[OF s(1), of i] x
  2519             by (intro simple_function_borel_measurable)
  2520                (auto simp: space_pair_measure dest: finite_subset)
  2521           have "(\<integral>\<^sup>+ y. ereal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
  2522             using x s by (intro nn_integral_mono) auto
  2523           also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
  2524             using int_2f by (simp add: integrable_iff_bounded)
  2525           finally show "(\<integral>\<^sup>+ xa. ereal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
  2526         qed
  2527         then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"
  2528           by (rule simple_bochner_integrable_eq_integral[symmetric]) }
  2529       ultimately have "(\<lambda>i. simple_bochner_integral M (\<lambda>y. s i (x, y))) ----> integral\<^sup>L M (f x)"
  2530         by simp }
  2531     then 
  2532     show "(\<lambda>i. f' i x) ----> integral\<^sup>L M (f x)"
  2533       unfolding f'_def
  2534       by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
  2535   qed
  2536 qed
  2537 
  2538 lemma (in pair_sigma_finite) integrable_product_swap:
  2539   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2540   assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
  2541   shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
  2542 proof -
  2543   interpret Q: pair_sigma_finite M2 M1 by default
  2544   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  2545   show ?thesis unfolding *
  2546     by (rule integrable_distr[OF measurable_pair_swap'])
  2547        (simp add: distr_pair_swap[symmetric] assms)
  2548 qed
  2549 
  2550 lemma (in pair_sigma_finite) integrable_product_swap_iff:
  2551   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2552   shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
  2553 proof -
  2554   interpret Q: pair_sigma_finite M2 M1 by default
  2555   from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
  2556   show ?thesis by auto
  2557 qed
  2558 
  2559 lemma (in pair_sigma_finite) integral_product_swap:
  2560   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2561   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  2562   shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  2563 proof -
  2564   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  2565   show ?thesis unfolding *
  2566     by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
  2567 qed
  2568 
  2569 lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
  2570   assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
  2571   shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
  2572 proof -
  2573   from M2.emeasure_pair_measure_alt[OF A] finite
  2574   have "(\<integral>\<^sup>+ x. emeasure M2 (Pair x -` A) \<partial>M1) \<noteq> \<infinity>"
  2575     by simp
  2576   then have "AE x in M1. emeasure M2 (Pair x -` A) \<noteq> \<infinity>"
  2577     by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
  2578   moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> Pair x -` A = {y\<in>space M2. (x, y) \<in> A}"
  2579     using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
  2580   ultimately show ?thesis by auto
  2581 qed
  2582 
  2583 lemma (in pair_sigma_finite) AE_integrable_fst':
  2584   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2585   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  2586   shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  2587 proof -
  2588   have "(\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1) = (\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2))"
  2589     by (rule M2.nn_integral_fst) simp
  2590   also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) \<noteq> \<infinity>"
  2591     using f unfolding integrable_iff_bounded by simp
  2592   finally have "AE x in M1. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
  2593     by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
  2594        (auto simp: measurable_split_conv)
  2595   with AE_space show ?thesis
  2596     by eventually_elim
  2597        (auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]])
  2598 qed
  2599 
  2600 lemma (in pair_sigma_finite) integrable_fst':
  2601   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2602   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  2603   shows "integrable M1 (\<lambda>x. \<integral>y. f (x, y) \<partial>M2)"
  2604   unfolding integrable_iff_bounded
  2605 proof
  2606   show "(\<lambda>x. \<integral> y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
  2607     by (rule M2.borel_measurable_lebesgue_integral) simp
  2608   have "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) \<le> (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
  2609     using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ereal)
  2610   also have "(\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1) = (\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2))"
  2611     by (rule M2.nn_integral_fst) simp
  2612   also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>"
  2613     using f unfolding integrable_iff_bounded by simp
  2614   finally show "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
  2615 qed
  2616 
  2617 lemma (in pair_sigma_finite) integral_fst':
  2618   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2619   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  2620   shows "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  2621 using f proof induct
  2622   case (base A c)
  2623   have A[measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" by fact
  2624 
  2625   have eq: "\<And>x y. x \<in> space M1 \<Longrightarrow> indicator A (x, y) = indicator {y\<in>space M2. (x, y) \<in> A} y"
  2626     using sets.sets_into_space[OF A] by (auto split: split_indicator simp: space_pair_measure)
  2627 
  2628   have int_A: "integrable (M1 \<Otimes>\<^sub>M M2) (indicator A :: _ \<Rightarrow> real)"
  2629     using base by (rule integrable_real_indicator)
  2630 
  2631   have "(\<integral> x. \<integral> y. indicator A (x, y) *\<^sub>R c \<partial>M2 \<partial>M1) = (\<integral>x. measure M2 {y\<in>space M2. (x, y) \<in> A} *\<^sub>R c \<partial>M1)"
  2632   proof (intro integral_cong_AE, simp, simp)
  2633     from AE_integrable_fst'[OF int_A] AE_space
  2634     show "AE x in M1. (\<integral>y. indicator A (x, y) *\<^sub>R c \<partial>M2) = measure M2 {y\<in>space M2. (x, y) \<in> A} *\<^sub>R c"
  2635       by eventually_elim (simp add: eq integrable_indicator_iff)
  2636   qed
  2637   also have "\<dots> = measure (M1 \<Otimes>\<^sub>M M2) A *\<^sub>R c"
  2638   proof (subst integral_scaleR_left)
  2639     have "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) =
  2640       (\<integral>\<^sup>+x. emeasure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1)"
  2641       using emeasure_pair_measure_finite[OF base]
  2642       by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
  2643     also have "\<dots> = emeasure (M1 \<Otimes>\<^sub>M M2) A"
  2644       using sets.sets_into_space[OF A]
  2645       by (subst M2.emeasure_pair_measure_alt)
  2646          (auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
  2647     finally have *: "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) = emeasure (M1 \<Otimes>\<^sub>M M2) A" .
  2648 
  2649     from base * show "integrable M1 (\<lambda>x. measure M2 {y \<in> space M2. (x, y) \<in> A})"
  2650       by (simp add: measure_nonneg integrable_iff_bounded)
  2651     then have "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) = 
  2652       (\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1)"
  2653       by (rule nn_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
  2654     also note *
  2655     finally show "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) *\<^sub>R c = measure (M1 \<Otimes>\<^sub>M M2) A *\<^sub>R c"
  2656       using base by (simp add: emeasure_eq_ereal_measure)
  2657   qed
  2658   also have "\<dots> = (\<integral> a. indicator A a *\<^sub>R c \<partial>(M1 \<Otimes>\<^sub>M M2))"
  2659     using base by simp
  2660   finally show ?case .
  2661 next
  2662   case (add f g)
  2663   then have [measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" "g \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  2664     by auto
  2665   have "(\<integral> x. \<integral> y. f (x, y) + g (x, y) \<partial>M2 \<partial>M1) = 
  2666     (\<integral> x. (\<integral> y. f (x, y) \<partial>M2) + (\<integral> y. g (x, y) \<partial>M2) \<partial>M1)"
  2667     apply (rule integral_cong_AE)
  2668     apply simp_all
  2669     using AE_integrable_fst'[OF add(1)] AE_integrable_fst'[OF add(3)]
  2670     apply eventually_elim
  2671     apply simp
  2672     done 
  2673   also have "\<dots> = (\<integral> x. f x \<partial>(M1 \<Otimes>\<^sub>M M2)) + (\<integral> x. g x \<partial>(M1 \<Otimes>\<^sub>M M2))"
  2674     using integrable_fst'[OF add(1)] integrable_fst'[OF add(3)] add(2,4) by simp
  2675   finally show ?case
  2676     using add by simp
  2677 next
  2678   case (lim f s)
  2679   then have [measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" "\<And>i. s i \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  2680     by auto
  2681   
  2682   show ?case
  2683   proof (rule LIMSEQ_unique)
  2684     show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) ----> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  2685     proof (rule integral_dominated_convergence)
  2686       show "integrable (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. 2 * norm (f x))"
  2687         using lim(5) by auto
  2688     qed (insert lim, auto)
  2689     have "(\<lambda>i. \<integral> x. \<integral> y. s i (x, y) \<partial>M2 \<partial>M1) ----> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
  2690     proof (rule integral_dominated_convergence)
  2691       have "AE x in M1. \<forall>i. integrable M2 (\<lambda>y. s i (x, y))"
  2692         unfolding AE_all_countable using AE_integrable_fst'[OF lim(1)] ..
  2693       with AE_space AE_integrable_fst'[OF lim(5)]
  2694       show "AE x in M1. (\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) ----> \<integral> y. f (x, y) \<partial>M2"
  2695       proof eventually_elim
  2696         fix x assume x: "x \<in> space M1" and
  2697           s: "\<forall>i. integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
  2698         show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) ----> \<integral> y. f (x, y) \<partial>M2"
  2699         proof (rule integral_dominated_convergence)
  2700           show "integrable M2 (\<lambda>y. 2 * norm (f (x, y)))"
  2701              using f by auto
  2702           show "AE xa in M2. (\<lambda>i. s i (x, xa)) ----> f (x, xa)"
  2703             using x lim(3) by (auto simp: space_pair_measure)
  2704           show "\<And>i. AE xa in M2. norm (s i (x, xa)) \<le> 2 * norm (f (x, xa))"
  2705             using x lim(4) by (auto simp: space_pair_measure)
  2706         qed (insert x, measurable)
  2707       qed
  2708       show "integrable M1 (\<lambda>x. (\<integral> y. 2 * norm (f (x, y)) \<partial>M2))"
  2709         by (intro integrable_mult_right integrable_norm integrable_fst' lim)
  2710       fix i show "AE x in M1. norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
  2711         using AE_space AE_integrable_fst'[OF lim(1), of i] AE_integrable_fst'[OF lim(5)]
  2712       proof eventually_elim 
  2713         fix x assume x: "x \<in> space M1"
  2714           and s: "integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
  2715         from s have "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral>\<^sup>+y. norm (s i (x, y)) \<partial>M2)"
  2716           by (rule integral_norm_bound_ereal)
  2717         also have "\<dots> \<le> (\<integral>\<^sup>+y. 2 * norm (f (x, y)) \<partial>M2)"
  2718           using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
  2719         also have "\<dots> = (\<integral>y. 2 * norm (f (x, y)) \<partial>M2)"
  2720           using f by (intro nn_integral_eq_integral) auto
  2721         finally show "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
  2722           by simp
  2723       qed
  2724     qed simp_all
  2725     then show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) ----> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
  2726       using lim by simp
  2727   qed
  2728 qed
  2729 
  2730 lemma (in pair_sigma_finite)
  2731   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  2732   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
  2733   shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
  2734     and integrable_fst: "integrable M1 (\<lambda>x. \<integral>y. f x y \<partial>M2)" (is "?INT")
  2735     and integral_fst: "(\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). f x y)" (is "?EQ")
  2736   using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto
  2737 
  2738 lemma (in pair_sigma_finite)
  2739   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  2740   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
  2741   shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
  2742     and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
  2743     and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (split f)" (is "?EQ")
  2744 proof -
  2745   interpret Q: pair_sigma_finite M2 M1 by default
  2746   have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
  2747     using f unfolding integrable_product_swap_iff[symmetric] by simp
  2748   show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
  2749   show ?INT using Q.integrable_fst'[OF Q_int] by simp
  2750   show ?EQ using Q.integral_fst'[OF Q_int]
  2751     using integral_product_swap[of "split f"] by simp
  2752 qed
  2753 
  2754 lemma (in pair_sigma_finite) Fubini_integral:
  2755   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
  2756   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
  2757   shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
  2758   unfolding integral_snd[OF assms] integral_fst[OF assms] ..
  2759 
  2760 lemma (in product_sigma_finite) product_integral_singleton:
  2761   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2762   shows "f \<in> borel_measurable (M i) \<Longrightarrow> (\<integral>x. f (x i) \<partial>Pi\<^sub>M {i} M) = integral\<^sup>L (M i) f"
  2763   apply (subst distr_singleton[symmetric])
  2764   apply (subst integral_distr)
  2765   apply simp_all
  2766   done
  2767 
  2768 lemma (in product_sigma_finite) product_integral_fold:
  2769   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2770   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  2771   and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
  2772   shows "integral\<^sup>L (Pi\<^sub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^sub>M J M) \<partial>Pi\<^sub>M I M)"
  2773 proof -
  2774   interpret I: finite_product_sigma_finite M I by default fact
  2775   interpret J: finite_product_sigma_finite M J by default fact
  2776   have "finite (I \<union> J)" using fin by auto
  2777   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
  2778   interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
  2779   let ?M = "merge I J"
  2780   let ?f = "\<lambda>x. f (?M x)"
  2781   from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
  2782     by auto
  2783   have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
  2784     using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
  2785   have f_int: "integrable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) ?f"
  2786     by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
  2787   show ?thesis
  2788     apply (subst distr_merge[symmetric, OF IJ fin])
  2789     apply (subst integral_distr[OF measurable_merge f_borel])
  2790     apply (subst P.integral_fst'[symmetric, OF f_int])
  2791     apply simp
  2792     done
  2793 qed
  2794 
  2795 lemma (in product_sigma_finite) product_integral_insert:
  2796   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2797   assumes I: "finite I" "i \<notin> I"
  2798     and f: "integrable (Pi\<^sub>M (insert i I) M) f"
  2799   shows "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = (\<integral>x. (\<integral>y. f (x(i:=y)) \<partial>M i) \<partial>Pi\<^sub>M I M)"
  2800 proof -
  2801   have "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = integral\<^sup>L (Pi\<^sub>M (I \<union> {i}) M) f"
  2802     by simp
  2803   also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I {i} (x,y)) \<partial>Pi\<^sub>M {i} M) \<partial>Pi\<^sub>M I M)"
  2804     using f I by (intro product_integral_fold) auto
  2805   also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^sub>M I M)"
  2806   proof (rule integral_cong[OF refl], subst product_integral_singleton[symmetric])
  2807     fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
  2808     have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
  2809       using f by auto
  2810     show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
  2811       using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
  2812       unfolding comp_def .
  2813     from x I show "(\<integral> y. f (merge I {i} (x,y)) \<partial>Pi\<^sub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^sub>M {i} M)"
  2814       by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
  2815   qed
  2816   finally show ?thesis .
  2817 qed
  2818 
  2819 lemma (in product_sigma_finite) product_integrable_setprod:
  2820   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  2821   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  2822   shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
  2823 proof (unfold integrable_iff_bounded, intro conjI)
  2824   interpret finite_product_sigma_finite M I by default fact
  2825 
  2826   show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
  2827     using assms by simp
  2828   have "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) = 
  2829       (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ereal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
  2830     by (simp add: setprod_norm setprod_ereal)
  2831   also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ereal (norm (f i x)) \<partial>M i)"
  2832     using assms by (intro product_nn_integral_setprod) auto
  2833   also have "\<dots> < \<infinity>"
  2834     using integrable by (simp add: setprod_PInf nn_integral_nonneg integrable_iff_bounded)
  2835   finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
  2836 qed
  2837 
  2838 lemma (in product_sigma_finite) product_integral_setprod:
  2839   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  2840   assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  2841   shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>L (M i) (f i))"
  2842 using assms proof induct
  2843   case empty
  2844   interpret finite_measure "Pi\<^sub>M {} M"
  2845     by rule (simp add: space_PiM)
  2846   show ?case by (simp add: space_PiM measure_def)
  2847 next
  2848   case (insert i I)
  2849   then have iI: "finite (insert i I)" by auto
  2850   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
  2851     integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
  2852     by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
  2853   interpret I: finite_product_sigma_finite M I by default fact
  2854   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
  2855     using `i \<notin> I` by (auto intro!: setprod.cong)
  2856   show ?case
  2857     unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
  2858     by (simp add: * insert prod subset_insertI)
  2859 qed
  2860 
  2861 lemma integrable_subalgebra:
  2862   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2863   assumes borel: "f \<in> borel_measurable N"
  2864   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  2865   shows "integrable N f \<longleftrightarrow> integrable M f" (is ?P)
  2866 proof -
  2867   have "f \<in> borel_measurable M"
  2868     using assms by (auto simp: measurable_def)
  2869   with assms show ?thesis
  2870     using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
  2871 qed
  2872 
  2873 lemma integral_subalgebra:
  2874   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2875   assumes borel: "f \<in> borel_measurable N"
  2876   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  2877   shows "integral\<^sup>L N f = integral\<^sup>L M f"
  2878 proof cases
  2879   assume "integrable N f"
  2880   then show ?thesis
  2881   proof induct
  2882     case base with assms show ?case by (auto simp: subset_eq measure_def)
  2883   next
  2884     case (add f g)
  2885     then have "(\<integral> a. f a + g a \<partial>N) = integral\<^sup>L M f + integral\<^sup>L M g"
  2886       by simp
  2887     also have "\<dots> = (\<integral> a. f a + g a \<partial>M)"
  2888       using add integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of g] by simp
  2889     finally show ?case .
  2890   next
  2891     case (lim f s)
  2892     then have M: "\<And>i. integrable M (s i)" "integrable M f"
  2893       using integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of "s i" for i] by simp_all
  2894     show ?case
  2895     proof (intro LIMSEQ_unique)
  2896       show "(\<lambda>i. integral\<^sup>L N (s i)) ----> integral\<^sup>L N f"
  2897         apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  2898         using lim
  2899         apply auto
  2900         done
  2901       show "(\<lambda>i. integral\<^sup>L N (s i)) ----> integral\<^sup>L M f"
  2902         unfolding lim
  2903         apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  2904         using lim M N(2)
  2905         apply auto
  2906         done
  2907     qed
  2908   qed
  2909 qed (simp add: not_integrable_integral_eq integrable_subalgebra[OF assms])
  2910 
  2911 hide_const simple_bochner_integral
  2912 hide_const simple_bochner_integrable
  2913 
  2914 end
  2915