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