src/HOL/Analysis/Bochner_Integration.thy
author wenzelm
Tue Jan 17 13:59:10 2017 +0100 (2017-01-17)
changeset 64911 f0e07600de47
parent 64287 d85d88722745
child 65680 378a2f11bec9
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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 sum_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 sum_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!: sum.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)
   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)
   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 sum_nonneg split: split_indicator split_indicator_asm
   224                  simp del: sum_mult_indicator simp: sum_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!: sum.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: sum.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!: sum.cong simp: scaleR_sum_left)
   370   also have "\<dots> = ?r"
   371     by (subst sum.commute)
   372        (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_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: sum.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 sum 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_sum)
   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: sum_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!: sum.cong ennreal_cong_mult
   477              simp: sum_ennreal[symmetric] ac_simps ennreal_mult
   478              simp del: sum_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_sum:
   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_left_commute)
   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!: sum.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 integrable_cong_AE_imp:
   955   "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
   956   using integrable_cong_AE[of f M g] by (auto simp: eq_commute)
   957 
   958 lemma integral_cong:
   959   "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"
   960   by (simp cong: has_bochner_integral_cong cong del: if_weak_cong add: lebesgue_integral_def)
   961 
   962 lemma integral_cong_AE:
   963   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   964     integral\<^sup>L M f = integral\<^sup>L M g"
   965   unfolding lebesgue_integral_def
   966   by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)
   967 
   968 lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
   969   by (auto simp: integrable.simps)
   970 
   971 lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
   972   by (metis has_bochner_integral_zero integrable.simps)
   973 
   974 lemma integrable_sum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)"
   975   by (metis has_bochner_integral_sum integrable.simps)
   976 
   977 lemma integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   978   integrable M (\<lambda>x. indicator A x *\<^sub>R c)"
   979   by (metis has_bochner_integral_indicator integrable.simps)
   980 
   981 lemma integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   982   integrable M (indicator A :: 'a \<Rightarrow> real)"
   983   by (metis has_bochner_integral_real_indicator integrable.simps)
   984 
   985 lemma integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x - g x)"
   986   by (auto simp: integrable.simps intro: has_bochner_integral_diff)
   987 
   988 lemma integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))"
   989   by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)
   990 
   991 lemma integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)"
   992   unfolding integrable.simps by fastforce
   993 
   994 lemma integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)"
   995   unfolding integrable.simps by fastforce
   996 
   997 lemma integrable_mult_left[simp, intro]:
   998   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   999   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x * c)"
  1000   unfolding integrable.simps by fastforce
  1001 
  1002 lemma integrable_mult_right[simp, intro]:
  1003   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1004   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)"
  1005   unfolding integrable.simps by fastforce
  1006 
  1007 lemma integrable_divide_zero[simp, intro]:
  1008   fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  1009   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
  1010   unfolding integrable.simps by fastforce
  1011 
  1012 lemma integrable_inner_left[simp, intro]:
  1013   "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)"
  1014   unfolding integrable.simps by fastforce
  1015 
  1016 lemma integrable_inner_right[simp, intro]:
  1017   "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c \<bullet> f x)"
  1018   unfolding integrable.simps by fastforce
  1019 
  1020 lemmas integrable_minus[simp, intro] =
  1021   integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
  1022 lemmas integrable_divide[simp, intro] =
  1023   integrable_bounded_linear[OF bounded_linear_divide]
  1024 lemmas integrable_Re[simp, intro] =
  1025   integrable_bounded_linear[OF bounded_linear_Re]
  1026 lemmas integrable_Im[simp, intro] =
  1027   integrable_bounded_linear[OF bounded_linear_Im]
  1028 lemmas integrable_cnj[simp, intro] =
  1029   integrable_bounded_linear[OF bounded_linear_cnj]
  1030 lemmas integrable_of_real[simp, intro] =
  1031   integrable_bounded_linear[OF bounded_linear_of_real]
  1032 lemmas integrable_fst[simp, intro] =
  1033   integrable_bounded_linear[OF bounded_linear_fst]
  1034 lemmas integrable_snd[simp, intro] =
  1035   integrable_bounded_linear[OF bounded_linear_snd]
  1036 
  1037 lemma integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0"
  1038   by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)
  1039 
  1040 lemma integral_add[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_add has_bochner_integral_integrable)
  1043 
  1044 lemma integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
  1045     integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
  1046   by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
  1047 
  1048 lemma integral_sum: "(\<And>i. i \<in> I \<Longrightarrow> 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   by (intro has_bochner_integral_integral_eq has_bochner_integral_sum has_bochner_integral_integrable)
  1051 
  1052 lemma integral_sum'[simp]: "(\<And>i. i \<in> I =simp=> integrable M (f i)) \<Longrightarrow>
  1053   integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
  1054   unfolding simp_implies_def by (rule integral_sum)
  1055 
  1056 lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
  1057     integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  1058   by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
  1059 
  1060 lemma integral_bounded_linear':
  1061   assumes T: "bounded_linear T" and T': "bounded_linear T'"
  1062   assumes *: "\<not> (\<forall>x. T x = 0) \<Longrightarrow> (\<forall>x. T' (T x) = x)"
  1063   shows "integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  1064 proof cases
  1065   assume "(\<forall>x. T x = 0)" then show ?thesis
  1066     by simp
  1067 next
  1068   assume **: "\<not> (\<forall>x. T x = 0)"
  1069   show ?thesis
  1070   proof cases
  1071     assume "integrable M f" with T show ?thesis
  1072       by (rule integral_bounded_linear)
  1073   next
  1074     assume not: "\<not> integrable M f"
  1075     moreover have "\<not> integrable M (\<lambda>x. T (f x))"
  1076     proof
  1077       assume "integrable M (\<lambda>x. T (f x))"
  1078       from integrable_bounded_linear[OF T' this] not *[OF **]
  1079       show False
  1080         by auto
  1081     qed
  1082     ultimately show ?thesis
  1083       using T by (simp add: not_integrable_integral_eq linear_simps)
  1084   qed
  1085 qed
  1086 
  1087 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"
  1088   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
  1089 
  1090 lemma integral_scaleR_right[simp]: "(\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
  1091   by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp
  1092 
  1093 lemma integral_mult_left[simp]:
  1094   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1095   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
  1096   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)
  1097 
  1098 lemma integral_mult_right[simp]:
  1099   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1100   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
  1101   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
  1102 
  1103 lemma integral_mult_left_zero[simp]:
  1104   fixes c :: "_::{real_normed_field,second_countable_topology}"
  1105   shows "(\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
  1106   by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp
  1107 
  1108 lemma integral_mult_right_zero[simp]:
  1109   fixes c :: "_::{real_normed_field,second_countable_topology}"
  1110   shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
  1111   by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp
  1112 
  1113 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"
  1114   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
  1115 
  1116 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"
  1117   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
  1118 
  1119 lemma integral_divide_zero[simp]:
  1120   fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  1121   shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
  1122   by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
  1123 
  1124 lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f"
  1125   by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp
  1126 
  1127 lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\<lambda>x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
  1128   by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp
  1129 
  1130 lemma integral_cnj[simp]: "integral\<^sup>L M (\<lambda>x. cnj (f x)) = cnj (integral\<^sup>L M f)"
  1131   by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp
  1132 
  1133 lemmas integral_divide[simp] =
  1134   integral_bounded_linear[OF bounded_linear_divide]
  1135 lemmas integral_Re[simp] =
  1136   integral_bounded_linear[OF bounded_linear_Re]
  1137 lemmas integral_Im[simp] =
  1138   integral_bounded_linear[OF bounded_linear_Im]
  1139 lemmas integral_of_real[simp] =
  1140   integral_bounded_linear[OF bounded_linear_of_real]
  1141 lemmas integral_fst[simp] =
  1142   integral_bounded_linear[OF bounded_linear_fst]
  1143 lemmas integral_snd[simp] =
  1144   integral_bounded_linear[OF bounded_linear_snd]
  1145 
  1146 lemma integral_norm_bound_ennreal:
  1147   "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
  1148   by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)
  1149 
  1150 lemma integrableI_sequence:
  1151   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1152   assumes f[measurable]: "f \<in> borel_measurable M"
  1153   assumes s: "\<And>i. simple_bochner_integrable M (s i)"
  1154   assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?S \<longlonglongrightarrow> 0")
  1155   shows "integrable M f"
  1156 proof -
  1157   let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
  1158 
  1159   have "\<exists>x. ?s \<longlonglongrightarrow> x"
  1160     unfolding convergent_eq_Cauchy
  1161   proof (rule metric_CauchyI)
  1162     fix e :: real assume "0 < e"
  1163     then have "0 < ennreal (e / 2)" by auto
  1164     from order_tendstoD(2)[OF lim this]
  1165     obtain M where M: "\<And>n. M \<le> n \<Longrightarrow> ?S n < e / 2"
  1166       by (auto simp: eventually_sequentially)
  1167     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (?s m) (?s n) < e"
  1168     proof (intro exI allI impI)
  1169       fix m n assume m: "M \<le> m" and n: "M \<le> n"
  1170       have "?S n \<noteq> \<infinity>"
  1171         using M[OF n] by auto
  1172       have "norm (?s n - ?s m) \<le> ?S n + ?S m"
  1173         by (intro simple_bochner_integral_bounded s f)
  1174       also have "\<dots> < ennreal (e / 2) + e / 2"
  1175         by (intro add_strict_mono M n m)
  1176       also have "\<dots> = e" using \<open>0<e\<close> by (simp del: ennreal_plus add: ennreal_plus[symmetric])
  1177       finally show "dist (?s n) (?s m) < e"
  1178         using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
  1179     qed
  1180   qed
  1181   then obtain x where "?s \<longlonglongrightarrow> x" ..
  1182   show ?thesis
  1183     by (rule, rule) fact+
  1184 qed
  1185 
  1186 lemma nn_integral_dominated_convergence_norm:
  1187   fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
  1188   assumes [measurable]:
  1189        "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
  1190     and bound: "\<And>j. AE x in M. norm (u j x) \<le> w x"
  1191     and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
  1192     and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
  1193   shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> 0"
  1194 proof -
  1195   have "AE x in M. \<forall>j. norm (u j x) \<le> w x"
  1196     unfolding AE_all_countable by rule fact
  1197   with u' have bnd: "AE x in M. \<forall>j. norm (u' x - u j x) \<le> 2 * w x"
  1198   proof (eventually_elim, intro allI)
  1199     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"
  1200     then have "norm (u' x) \<le> w x" "norm (u i x) \<le> w x"
  1201       by (auto intro: LIMSEQ_le_const2 tendsto_norm)
  1202     then have "norm (u' x) + norm (u i x) \<le> 2 * w x"
  1203       by simp
  1204     also have "norm (u' x - u i x) \<le> norm (u' x) + norm (u i x)"
  1205       by (rule norm_triangle_ineq4)
  1206     finally (xtrans) show "norm (u' x - u i x) \<le> 2 * w x" .
  1207   qed
  1208   have w_nonneg: "AE x in M. 0 \<le> w x"
  1209     using bound[of 0] by (auto intro: order_trans[OF norm_ge_zero])
  1210 
  1211   have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. 0 \<partial>M)"
  1212   proof (rule nn_integral_dominated_convergence)
  1213     show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
  1214       by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) (insert w_nonneg, auto simp: ennreal_mult )
  1215     show "AE x in M. (\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
  1216       using u'
  1217     proof eventually_elim
  1218       fix x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
  1219       from tendsto_diff[OF tendsto_const[of "u' x"] this]
  1220       show "(\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
  1221         by (simp add: tendsto_norm_zero_iff ennreal_0[symmetric] del: ennreal_0)
  1222     qed
  1223   qed (insert bnd w_nonneg, auto)
  1224   then show ?thesis by simp
  1225 qed
  1226 
  1227 lemma integrableI_bounded:
  1228   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1229   assumes f[measurable]: "f \<in> borel_measurable M" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1230   shows "integrable M f"
  1231 proof -
  1232   from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
  1233     s: "\<And>i. simple_function M (s i)" and
  1234     pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" and
  1235     bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
  1236     by simp metis
  1237 
  1238   show ?thesis
  1239   proof (rule integrableI_sequence)
  1240     { fix i
  1241       have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ennreal (2 * norm (f x)) \<partial>M)"
  1242         by (intro nn_integral_mono) (simp add: bound)
  1243       also have "\<dots> = 2 * (\<integral>\<^sup>+x. ennreal (norm (f x)) \<partial>M)"
  1244         by (simp add: ennreal_mult nn_integral_cmult)
  1245       also have "\<dots> < top"
  1246         using fin by (simp add: ennreal_mult_less_top)
  1247       finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
  1248         by simp }
  1249     note fin_s = this
  1250 
  1251     show "\<And>i. simple_bochner_integrable M (s i)"
  1252       by (rule simple_bochner_integrableI_bounded) fact+
  1253 
  1254     show "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
  1255     proof (rule nn_integral_dominated_convergence_norm)
  1256       show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
  1257         using bound by auto
  1258       show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
  1259         using s by (auto intro: borel_measurable_simple_function)
  1260       show "(\<integral>\<^sup>+ x. ennreal (2 * norm (f x)) \<partial>M) < \<infinity>"
  1261         using fin by (simp add: nn_integral_cmult ennreal_mult ennreal_mult_less_top)
  1262       show "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
  1263         using pointwise by auto
  1264     qed fact
  1265   qed fact
  1266 qed
  1267 
  1268 lemma integrableI_bounded_set:
  1269   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1270   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M"
  1271   assumes finite: "emeasure M A < \<infinity>"
  1272     and bnd: "AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B"
  1273     and null: "AE x in M. x \<notin> A \<longrightarrow> f x = 0"
  1274   shows "integrable M f"
  1275 proof (rule integrableI_bounded)
  1276   { fix x :: 'b have "norm x \<le> B \<Longrightarrow> 0 \<le> B"
  1277       using norm_ge_zero[of x] by arith }
  1278   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)"
  1279     by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
  1280   also have "\<dots> < \<infinity>"
  1281     using finite by (subst nn_integral_cmult_indicator) (auto simp: ennreal_mult_less_top)
  1282   finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
  1283 qed simp
  1284 
  1285 lemma integrableI_bounded_set_indicator:
  1286   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1287   shows "A \<in> sets M \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow>
  1288     emeasure M A < \<infinity> \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B) \<Longrightarrow>
  1289     integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1290   by (rule integrableI_bounded_set[where A=A]) auto
  1291 
  1292 lemma integrableI_nonneg:
  1293   fixes f :: "'a \<Rightarrow> real"
  1294   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
  1295   shows "integrable M f"
  1296 proof -
  1297   have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1298     using assms by (intro nn_integral_cong_AE) auto
  1299   then show ?thesis
  1300     using assms by (intro integrableI_bounded) auto
  1301 qed
  1302 
  1303 lemma integrable_iff_bounded:
  1304   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1305   shows "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1306   using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f]
  1307   unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto
  1308 
  1309 lemma integrable_bound:
  1310   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1311     and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
  1312   shows "integrable M f \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. norm (g x) \<le> norm (f x)) \<Longrightarrow>
  1313     integrable M g"
  1314   unfolding integrable_iff_bounded
  1315 proof safe
  1316   assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1317   assume "AE x in M. norm (g x) \<le> norm (f x)"
  1318   then have "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1319     by  (intro nn_integral_mono_AE) auto
  1320   also assume "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  1321   finally show "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) < \<infinity>" .
  1322 qed
  1323 
  1324 lemma integrable_mult_indicator:
  1325   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1326   shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1327   by (rule integrable_bound[of M f]) (auto split: split_indicator)
  1328 
  1329 lemma integrable_real_mult_indicator:
  1330   fixes f :: "'a \<Rightarrow> real"
  1331   shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
  1332   using integrable_mult_indicator[of A M f] by (simp add: mult_ac)
  1333 
  1334 lemma integrable_abs[simp, intro]:
  1335   fixes f :: "'a \<Rightarrow> real"
  1336   assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
  1337   using assms by (rule integrable_bound) auto
  1338 
  1339 lemma integrable_norm[simp, intro]:
  1340   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1341   assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. norm (f x))"
  1342   using assms by (rule integrable_bound) auto
  1343 
  1344 lemma integrable_norm_cancel:
  1345   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1346   assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
  1347   using assms by (rule integrable_bound) auto
  1348 
  1349 lemma integrable_norm_iff:
  1350   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1351   shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. norm (f x)) \<longleftrightarrow> integrable M f"
  1352   by (auto intro: integrable_norm_cancel)
  1353 
  1354 lemma integrable_abs_cancel:
  1355   fixes f :: "'a \<Rightarrow> real"
  1356   assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
  1357   using assms by (rule integrable_bound) auto
  1358 
  1359 lemma integrable_abs_iff:
  1360   fixes f :: "'a \<Rightarrow> real"
  1361   shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
  1362   by (auto intro: integrable_abs_cancel)
  1363 
  1364 lemma integrable_max[simp, intro]:
  1365   fixes f :: "'a \<Rightarrow> real"
  1366   assumes fg[measurable]: "integrable M f" "integrable M g"
  1367   shows "integrable M (\<lambda>x. max (f x) (g x))"
  1368   using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
  1369   by (rule integrable_bound) auto
  1370 
  1371 lemma integrable_min[simp, intro]:
  1372   fixes f :: "'a \<Rightarrow> real"
  1373   assumes fg[measurable]: "integrable M f" "integrable M g"
  1374   shows "integrable M (\<lambda>x. min (f x) (g x))"
  1375   using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
  1376   by (rule integrable_bound) auto
  1377 
  1378 lemma integral_minus_iff[simp]:
  1379   "integrable M (\<lambda>x. - f x ::'a::{banach, second_countable_topology}) \<longleftrightarrow> integrable M f"
  1380   unfolding integrable_iff_bounded
  1381   by (auto intro: borel_measurable_uminus[of "\<lambda>x. - f x" M, simplified])
  1382 
  1383 lemma integrable_indicator_iff:
  1384   "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
  1385   by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator nn_integral_indicator'
  1386            cong: conj_cong)
  1387 
  1388 lemma integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \<inter> space M)"
  1389 proof cases
  1390   assume *: "A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
  1391   have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M))"
  1392     by (intro integral_cong) (auto split: split_indicator)
  1393   also have "\<dots> = measure M (A \<inter> space M)"
  1394     using * by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator) auto
  1395   finally show ?thesis .
  1396 next
  1397   assume *: "\<not> (A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>)"
  1398   have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M) :: _ \<Rightarrow> real)"
  1399     by (intro integral_cong) (auto split: split_indicator)
  1400   also have "\<dots> = 0"
  1401     using * by (subst not_integrable_integral_eq) (auto simp: integrable_indicator_iff)
  1402   also have "\<dots> = measure M (A \<inter> space M)"
  1403     using * by (auto simp: measure_def emeasure_notin_sets not_less top_unique)
  1404   finally show ?thesis .
  1405 qed
  1406 
  1407 lemma integrable_discrete_difference:
  1408   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1409   assumes X: "countable X"
  1410   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
  1411   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1412   assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1413   shows "integrable M f \<longleftrightarrow> integrable M g"
  1414   unfolding integrable_iff_bounded
  1415 proof (rule conj_cong)
  1416   { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
  1417       by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
  1418   moreover
  1419   { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
  1420       by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
  1421   ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
  1422 next
  1423   have "AE x in M. x \<notin> X"
  1424     by (rule AE_discrete_difference) fact+
  1425   then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
  1426     by (intro nn_integral_cong_AE) (auto simp: eq)
  1427   then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
  1428     by simp
  1429 qed
  1430 
  1431 lemma integral_discrete_difference:
  1432   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1433   assumes X: "countable X"
  1434   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
  1435   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1436   assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1437   shows "integral\<^sup>L M f = integral\<^sup>L M g"
  1438 proof (rule integral_eq_cases)
  1439   show eq: "integrable M f \<longleftrightarrow> integrable M g"
  1440     by (rule integrable_discrete_difference[where X=X]) fact+
  1441 
  1442   assume f: "integrable M f"
  1443   show "integral\<^sup>L M f = integral\<^sup>L M g"
  1444   proof (rule integral_cong_AE)
  1445     show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1446       using f eq by (auto intro: borel_measurable_integrable)
  1447 
  1448     have "AE x in M. x \<notin> X"
  1449       by (rule AE_discrete_difference) fact+
  1450     with AE_space show "AE x in M. f x = g x"
  1451       by eventually_elim fact
  1452   qed
  1453 qed
  1454 
  1455 lemma has_bochner_integral_discrete_difference:
  1456   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1457   assumes X: "countable X"
  1458   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
  1459   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1460   assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1461   shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
  1462   using integrable_discrete_difference[of X M f g, OF assms]
  1463   using integral_discrete_difference[of X M f g, OF assms]
  1464   by (metis has_bochner_integral_iff)
  1465 
  1466 lemma
  1467   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
  1468   assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
  1469   assumes lim: "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
  1470   assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
  1471   shows integrable_dominated_convergence: "integrable M f"
  1472     and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
  1473     and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
  1474 proof -
  1475   have w_nonneg: "AE x in M. 0 \<le> w x"
  1476     using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
  1477   then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
  1478     by (intro nn_integral_cong_AE) auto
  1479   with \<open>integrable M w\<close> have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
  1480     unfolding integrable_iff_bounded by auto
  1481 
  1482   show int_s: "\<And>i. integrable M (s i)"
  1483     unfolding integrable_iff_bounded
  1484   proof
  1485     fix i
  1486     have "(\<integral>\<^sup>+ x. ennreal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
  1487       using bound[of i] w_nonneg by (intro nn_integral_mono_AE) auto
  1488     with w show "(\<integral>\<^sup>+ x. ennreal (norm (s i x)) \<partial>M) < \<infinity>" by auto
  1489   qed fact
  1490 
  1491   have all_bound: "AE x in M. \<forall>i. norm (s i x) \<le> w x"
  1492     using bound unfolding AE_all_countable by auto
  1493 
  1494   show int_f: "integrable M f"
  1495     unfolding integrable_iff_bounded
  1496   proof
  1497     have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
  1498       using all_bound lim w_nonneg
  1499     proof (intro nn_integral_mono_AE, eventually_elim)
  1500       fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) \<longlonglongrightarrow> f x" "0 \<le> w x"
  1501       then show "ennreal (norm (f x)) \<le> ennreal (w x)"
  1502         by (intro LIMSEQ_le_const2[where X="\<lambda>i. ennreal (norm (s i x))"]) (auto intro: tendsto_intros)
  1503     qed
  1504     with w show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by auto
  1505   qed fact
  1506 
  1507   have "(\<lambda>n. ennreal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) \<longlonglongrightarrow> ennreal 0" (is "?d \<longlonglongrightarrow> ennreal 0")
  1508   proof (rule tendsto_sandwich)
  1509     show "eventually (\<lambda>n. ennreal 0 \<le> ?d n) sequentially" "(\<lambda>_. ennreal 0) \<longlonglongrightarrow> ennreal 0" by auto
  1510     show "eventually (\<lambda>n. ?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)) sequentially"
  1511     proof (intro always_eventually allI)
  1512       fix n
  1513       have "?d n = norm (integral\<^sup>L M (\<lambda>x. s n x - f x))"
  1514         using int_f int_s by simp
  1515       also have "\<dots> \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)"
  1516         by (intro int_f int_s integrable_diff integral_norm_bound_ennreal)
  1517       finally show "?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)" .
  1518     qed
  1519     show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) \<longlonglongrightarrow> ennreal 0"
  1520       unfolding ennreal_0
  1521       apply (subst norm_minus_commute)
  1522     proof (rule nn_integral_dominated_convergence_norm[where w=w])
  1523       show "\<And>n. s n \<in> borel_measurable M"
  1524         using int_s unfolding integrable_iff_bounded by auto
  1525     qed fact+
  1526   qed
  1527   then have "(\<lambda>n. integral\<^sup>L M (s n) - integral\<^sup>L M f) \<longlonglongrightarrow> 0"
  1528     by (simp add: tendsto_norm_zero_iff del: ennreal_0)
  1529   from tendsto_add[OF this tendsto_const[of "integral\<^sup>L M f"]]
  1530   show "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"  by simp
  1531 qed
  1532 
  1533 context
  1534   fixes s :: "real \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
  1535     and f :: "'a \<Rightarrow> 'b" and M
  1536   assumes "f \<in> borel_measurable M" "\<And>t. s t \<in> borel_measurable M" "integrable M w"
  1537   assumes lim: "AE x in M. ((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
  1538   assumes bound: "\<forall>\<^sub>F i in at_top. AE x in M. norm (s i x) \<le> w x"
  1539 begin
  1540 
  1541 lemma integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) \<longlongrightarrow> integral\<^sup>L M f) at_top"
  1542 proof (rule tendsto_at_topI_sequentially)
  1543   fix X :: "nat \<Rightarrow> real" assume X: "filterlim X at_top sequentially"
  1544   from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
  1545   obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s (X n) x) \<le> w x"
  1546     by (auto simp: eventually_sequentially)
  1547 
  1548   show "(\<lambda>n. integral\<^sup>L M (s (X n))) \<longlonglongrightarrow> integral\<^sup>L M f"
  1549   proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
  1550     show "AE x in M. norm (s (X (n + N)) x) \<le> w x" for n
  1551       by (rule w) auto
  1552     show "AE x in M. (\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
  1553       using lim
  1554     proof eventually_elim
  1555       fix x assume "((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
  1556       then show "(\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
  1557         by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
  1558     qed
  1559   qed fact+
  1560 qed
  1561 
  1562 lemma integrable_dominated_convergence_at_top: "integrable M f"
  1563 proof -
  1564   from bound obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s n x) \<le> w x"
  1565     by (auto simp: eventually_at_top_linorder)
  1566   show ?thesis
  1567   proof (rule integrable_dominated_convergence)
  1568     show "AE x in M. norm (s (N + i) x) \<le> w x" for i :: nat
  1569       by (intro w) auto
  1570     show "AE x in M. (\<lambda>i. s (N + real i) x) \<longlonglongrightarrow> f x"
  1571       using lim
  1572     proof eventually_elim
  1573       fix x assume "((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
  1574       then show "(\<lambda>n. s (N + n) x) \<longlonglongrightarrow> f x"
  1575         by (rule filterlim_compose)
  1576            (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially)
  1577     qed
  1578   qed fact+
  1579 qed
  1580 
  1581 end
  1582 
  1583 lemma integrable_mult_left_iff:
  1584   fixes f :: "'a \<Rightarrow> real"
  1585   shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
  1586   using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
  1587   by (cases "c = 0") auto
  1588 
  1589 lemma integrableI_nn_integral_finite:
  1590   assumes [measurable]: "f \<in> borel_measurable M"
  1591     and nonneg: "AE x in M. 0 \<le> f x"
  1592     and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
  1593   shows "integrable M f"
  1594 proof (rule integrableI_bounded)
  1595   have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M)"
  1596     using nonneg by (intro nn_integral_cong_AE) auto
  1597   with finite show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  1598     by auto
  1599 qed simp
  1600 
  1601 lemma integral_nonneg_AE:
  1602   fixes f :: "'a \<Rightarrow> real"
  1603   assumes nonneg: "AE x in M. 0 \<le> f x"
  1604   shows "0 \<le> integral\<^sup>L M f"
  1605 proof cases
  1606   assume f: "integrable M f"
  1607   then have [measurable]: "f \<in> M \<rightarrow>\<^sub>M borel"
  1608     by auto
  1609   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))"
  1610     using f by auto
  1611   from this have "0 \<le> integral\<^sup>L M (\<lambda>x. max 0 (f x))"
  1612   proof (induction rule: borel_measurable_induct_real)
  1613     case (add f g)
  1614     then have "integrable M f" "integrable M g"
  1615       by (auto intro!: integrable_bound[OF add.prems])
  1616     with add show ?case
  1617       by (simp add: nn_integral_add)
  1618   next
  1619     case (seq U)
  1620     show ?case
  1621     proof (rule LIMSEQ_le_const)
  1622       have U_le: "x \<in> space M \<Longrightarrow> U i x \<le> max 0 (f x)" for x i
  1623         using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
  1624       with seq nonneg show "(\<lambda>i. integral\<^sup>L M (U i)) \<longlonglongrightarrow> LINT x|M. max 0 (f x)"
  1625         by (intro integral_dominated_convergence) auto
  1626       have "integrable M (U i)" for i
  1627         using seq.prems by (rule integrable_bound) (insert U_le seq, auto)
  1628       with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
  1629         by auto
  1630     qed
  1631   qed (auto simp: integrable_mult_left_iff)
  1632   also have "\<dots> = integral\<^sup>L M f"
  1633     using nonneg by (auto intro!: integral_cong_AE)
  1634   finally show ?thesis .
  1635 qed (simp add: not_integrable_integral_eq)
  1636 
  1637 lemma integral_nonneg[simp]:
  1638   fixes f :: "'a \<Rightarrow> real"
  1639   shows "(\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> integral\<^sup>L M f"
  1640   by (intro integral_nonneg_AE) auto
  1641 
  1642 lemma nn_integral_eq_integral:
  1643   assumes f: "integrable M f"
  1644   assumes nonneg: "AE x in M. 0 \<le> f x"
  1645   shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
  1646 proof -
  1647   { fix f :: "'a \<Rightarrow> real" assume f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "integrable M f"
  1648     then have "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
  1649     proof (induct rule: borel_measurable_induct_real)
  1650       case (set A) then show ?case
  1651         by (simp add: integrable_indicator_iff ennreal_indicator emeasure_eq_ennreal_measure)
  1652     next
  1653       case (mult f c) then show ?case
  1654         by (auto simp add: integrable_mult_left_iff nn_integral_cmult ennreal_mult integral_nonneg_AE)
  1655     next
  1656       case (add g f)
  1657       then have "integrable M f" "integrable M g"
  1658         by (auto intro!: integrable_bound[OF add.prems])
  1659       with add show ?case
  1660         by (simp add: nn_integral_add integral_nonneg_AE)
  1661     next
  1662       case (seq U)
  1663       show ?case
  1664       proof (rule LIMSEQ_unique)
  1665         have U_le_f: "x \<in> space M \<Longrightarrow> U i x \<le> f x" for x i
  1666           using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
  1667         have int_U: "\<And>i. integrable M (U i)"
  1668           using seq f U_le_f by (intro integrable_bound[OF f(3)]) auto
  1669         from U_le_f seq have "(\<lambda>i. integral\<^sup>L M (U i)) \<longlonglongrightarrow> integral\<^sup>L M f"
  1670           by (intro integral_dominated_convergence) auto
  1671         then show "(\<lambda>i. ennreal (integral\<^sup>L M (U i))) \<longlonglongrightarrow> ennreal (integral\<^sup>L M f)"
  1672           using seq f int_U by (simp add: f integral_nonneg_AE)
  1673         have "(\<lambda>i. \<integral>\<^sup>+ x. U i x \<partial>M) \<longlonglongrightarrow> \<integral>\<^sup>+ x. f x \<partial>M"
  1674           using seq U_le_f f
  1675           by (intro nn_integral_dominated_convergence[where w=f]) (auto simp: integrable_iff_bounded)
  1676         then show "(\<lambda>i. \<integral>x. U i x \<partial>M) \<longlonglongrightarrow> \<integral>\<^sup>+x. f x \<partial>M"
  1677           using seq int_U by simp
  1678       qed
  1679     qed }
  1680   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))"
  1681     by simp
  1682   also have "\<dots> = integral\<^sup>L M f"
  1683     using assms by (auto intro!: integral_cong_AE simp: integral_nonneg_AE)
  1684   also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
  1685     using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
  1686   finally show ?thesis .
  1687 qed
  1688 
  1689 lemma nn_integral_eq_integrable:
  1690   assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" "AE x in M. 0 \<le> f x" and "0 \<le> x"
  1691   shows "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x \<longleftrightarrow> (integrable M f \<and> integral\<^sup>L M f = x)"
  1692 proof (safe intro!: nn_integral_eq_integral assms)
  1693   assume *: "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
  1694   with integrableI_nn_integral_finite[OF f this] nn_integral_eq_integral[of M f, OF _ f(2)]
  1695   show "integrable M f" "integral\<^sup>L M f = x"
  1696     by (simp_all add: * assms integral_nonneg_AE)
  1697 qed
  1698 
  1699 lemma
  1700   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1701   assumes integrable[measurable]: "\<And>i. integrable M (f i)"
  1702   and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
  1703   and sums: "summable (\<lambda>i. (\<integral>x. norm (f i x) \<partial>M))"
  1704   shows integrable_suminf: "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
  1705     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")
  1706     and integral_suminf: "(\<integral>x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>L M (f i))"
  1707     and summable_integral: "summable (\<lambda>i. integral\<^sup>L M (f i))"
  1708 proof -
  1709   have 1: "integrable M (\<lambda>x. \<Sum>i. norm (f i x))"
  1710   proof (rule integrableI_bounded)
  1711     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)"
  1712       apply (intro nn_integral_cong_AE)
  1713       using summable
  1714       apply eventually_elim
  1715       apply (simp add: suminf_nonneg ennreal_suminf_neq_top)
  1716       done
  1717     also have "\<dots> = (\<Sum>i. \<integral>\<^sup>+ x. norm (f i x) \<partial>M)"
  1718       by (intro nn_integral_suminf) auto
  1719     also have "\<dots> = (\<Sum>i. ennreal (\<integral>x. norm (f i x) \<partial>M))"
  1720       by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
  1721     finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Sum>i. norm (f i x))) \<partial>M) < \<infinity>"
  1722       by (simp add: sums ennreal_suminf_neq_top less_top[symmetric] integral_nonneg_AE)
  1723   qed simp
  1724 
  1725   have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> (\<Sum>i. f i x)"
  1726     using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
  1727 
  1728   have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
  1729     using summable
  1730   proof eventually_elim
  1731     fix j x assume [simp]: "summable (\<lambda>i. norm (f i x))"
  1732     have "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i<j. norm (f i x))" by (rule norm_sum)
  1733     also have "\<dots> \<le> (\<Sum>i. norm (f i x))"
  1734       using sum_le_suminf[of "\<lambda>i. norm (f i x)"] unfolding sums_iff by auto
  1735     finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
  1736   qed
  1737 
  1738   note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
  1739   note int = integral_dominated_convergence[OF _ _ 1 2 3]
  1740 
  1741   show "integrable M ?S"
  1742     by (rule ibl) measurable
  1743 
  1744   show "?f sums ?x" unfolding sums_def
  1745     using int by (simp add: integrable)
  1746   then show "?x = suminf ?f" "summable ?f"
  1747     unfolding sums_iff by auto
  1748 qed
  1749 
  1750 lemma integral_norm_bound [simp]:
  1751   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1752   shows "norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
  1753 proof (cases "integrable M f")
  1754   case True then show ?thesis
  1755     using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"] integral_norm_bound_ennreal[of M f]
  1756     by (simp add: integral_nonneg_AE)
  1757 next
  1758   case False
  1759   then have "norm (integral\<^sup>L M f) = 0" by (simp add: not_integrable_integral_eq)
  1760   moreover have "(\<integral>x. norm (f x) \<partial>M) \<ge> 0" by auto
  1761   ultimately show ?thesis by simp
  1762 qed
  1763 
  1764 lemma integral_abs_bound [simp]:
  1765   fixes f :: "'a \<Rightarrow> real" shows "abs (\<integral>x. f x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
  1766 using integral_norm_bound[of M f] by auto
  1767 
  1768 lemma integral_eq_nn_integral:
  1769   assumes [measurable]: "f \<in> borel_measurable M"
  1770   assumes nonneg: "AE x in M. 0 \<le> f x"
  1771   shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M)"
  1772 proof cases
  1773   assume *: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) = \<infinity>"
  1774   also have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1775     using nonneg by (intro nn_integral_cong_AE) auto
  1776   finally have "\<not> integrable M f"
  1777     by (auto simp: integrable_iff_bounded)
  1778   then show ?thesis
  1779     by (simp add: * not_integrable_integral_eq)
  1780 next
  1781   assume "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>"
  1782   then have "integrable M f"
  1783     by (cases "\<integral>\<^sup>+ x. ennreal (f x) \<partial>M" rule: ennreal_cases)
  1784        (auto intro!: integrableI_nn_integral_finite assms)
  1785   from nn_integral_eq_integral[OF this] nonneg show ?thesis
  1786     by (simp add: integral_nonneg_AE)
  1787 qed
  1788 
  1789 lemma enn2real_nn_integral_eq_integral:
  1790   assumes eq: "AE x in M. f x = ennreal (g x)" and nn: "AE x in M. 0 \<le> g x"
  1791     and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < top"
  1792     and [measurable]: "g \<in> M \<rightarrow>\<^sub>M borel"
  1793   shows "enn2real (\<integral>\<^sup>+x. f x \<partial>M) = (\<integral>x. g x \<partial>M)"
  1794 proof -
  1795   have "ennreal (enn2real (\<integral>\<^sup>+x. f x \<partial>M)) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1796     using fin by (intro ennreal_enn2real) auto
  1797   also have "\<dots> = (\<integral>\<^sup>+x. g x \<partial>M)"
  1798     using eq by (rule nn_integral_cong_AE)
  1799   also have "\<dots> = (\<integral>x. g x \<partial>M)"
  1800   proof (rule nn_integral_eq_integral)
  1801     show "integrable M g"
  1802     proof (rule integrableI_bounded)
  1803       have "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
  1804         using eq nn by (auto intro!: nn_integral_cong_AE elim!: eventually_elim2)
  1805       also note fin
  1806       finally show "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) < \<infinity>"
  1807         by simp
  1808     qed simp
  1809   qed fact
  1810   finally show ?thesis
  1811     using nn by (simp add: integral_nonneg_AE)
  1812 qed
  1813 
  1814 lemma has_bochner_integral_nn_integral:
  1815   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "0 \<le> x"
  1816   assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
  1817   shows "has_bochner_integral M f x"
  1818   unfolding has_bochner_integral_iff
  1819   using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
  1820 
  1821 lemma integrableI_simple_bochner_integrable:
  1822   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1823   shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
  1824   by (intro integrableI_sequence[where s="\<lambda>_. f"] borel_measurable_simple_function)
  1825      (auto simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps)
  1826 
  1827 lemma integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
  1828   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1829   assumes "integrable M f"
  1830   assumes base: "\<And>A c. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R c)"
  1831   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)"
  1832   assumes lim: "\<And>f s. (\<And>i. integrable M (s i)) \<Longrightarrow> (\<And>i. P (s i)) \<Longrightarrow>
  1833    (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x) \<Longrightarrow>
  1834    (\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)) \<Longrightarrow> integrable M f \<Longrightarrow> P f"
  1835   shows "P f"
  1836 proof -
  1837   from \<open>integrable M f\<close> have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1838     unfolding integrable_iff_bounded by auto
  1839   from borel_measurable_implies_sequence_metric[OF f(1)]
  1840   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"
  1841     "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
  1842     unfolding norm_conv_dist by metis
  1843 
  1844   { fix f A
  1845     have [simp]: "P (\<lambda>x. 0)"
  1846       using base[of "{}" undefined] by simp
  1847     have "(\<And>i::'b. i \<in> A \<Longrightarrow> integrable M (f i::'a \<Rightarrow> 'b)) \<Longrightarrow>
  1848     (\<And>i. i \<in> A \<Longrightarrow> P (f i)) \<Longrightarrow> P (\<lambda>x. \<Sum>i\<in>A. f i x)"
  1849     by (induct A rule: infinite_finite_induct) (auto intro!: add) }
  1850   note sum = this
  1851 
  1852   define s' where [abs_def]: "s' i z = indicator (space M) z *\<^sub>R s i z" for i z
  1853   then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x"
  1854     by simp
  1855 
  1856   have sf[measurable]: "\<And>i. simple_function M (s' i)"
  1857     unfolding s'_def using s(1)
  1858     by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto
  1859 
  1860   { fix i
  1861     have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
  1862         (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})"
  1863       by (auto simp add: s'_def split: split_indicator)
  1864     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)"
  1865       using sf by (auto simp: fun_eq_iff simple_function_def s'_def) }
  1866   note s'_eq = this
  1867 
  1868   show "P f"
  1869   proof (rule lim)
  1870     fix i
  1871 
  1872     have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ennreal (2 * norm (f x)) \<partial>M)"
  1873       using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
  1874     also have "\<dots> < \<infinity>"
  1875       using f by (simp add: nn_integral_cmult ennreal_mult_less_top ennreal_mult)
  1876     finally have sbi: "simple_bochner_integrable M (s' i)"
  1877       using sf by (intro simple_bochner_integrableI_bounded) auto
  1878     then show "integrable M (s' i)"
  1879       by (rule integrableI_simple_bochner_integrable)
  1880 
  1881     { fix x assume"x \<in> space M" "s' i x \<noteq> 0"
  1882       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}"
  1883         by (intro emeasure_mono) auto
  1884       also have "\<dots> < \<infinity>"
  1885         using sbi by (auto elim: simple_bochner_integrable.cases simp: less_top)
  1886       finally have "emeasure M {y \<in> space M. s' i y = s' i x} \<noteq> \<infinity>" by simp }
  1887     then show "P (s' i)"
  1888       by (subst s'_eq) (auto intro!: sum base simp: less_top)
  1889 
  1890     fix x assume "x \<in> space M" with s show "(\<lambda>i. s' i x) \<longlonglongrightarrow> f x"
  1891       by (simp add: s'_eq_s)
  1892     show "norm (s' i x) \<le> 2 * norm (f x)"
  1893       using \<open>x \<in> space M\<close> s by (simp add: s'_eq_s)
  1894   qed fact
  1895 qed
  1896 
  1897 lemma integral_eq_zero_AE:
  1898   "(AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
  1899   using integral_cong_AE[of f M "\<lambda>_. 0"]
  1900   by (cases "integrable M f") (simp_all add: not_integrable_integral_eq)
  1901 
  1902 lemma integral_nonneg_eq_0_iff_AE:
  1903   fixes f :: "_ \<Rightarrow> real"
  1904   assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \<le> f x"
  1905   shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
  1906 proof
  1907   assume "integral\<^sup>L M f = 0"
  1908   then have "integral\<^sup>N M f = 0"
  1909     using nn_integral_eq_integral[OF f nonneg] by simp
  1910   then have "AE x in M. ennreal (f x) \<le> 0"
  1911     by (simp add: nn_integral_0_iff_AE)
  1912   with nonneg show "AE x in M. f x = 0"
  1913     by auto
  1914 qed (auto simp add: integral_eq_zero_AE)
  1915 
  1916 lemma integral_mono_AE:
  1917   fixes f :: "'a \<Rightarrow> real"
  1918   assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
  1919   shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1920 proof -
  1921   have "0 \<le> integral\<^sup>L M (\<lambda>x. g x - f x)"
  1922     using assms by (intro integral_nonneg_AE integrable_diff assms) auto
  1923   also have "\<dots> = integral\<^sup>L M g - integral\<^sup>L M f"
  1924     by (intro integral_diff assms)
  1925   finally show ?thesis by simp
  1926 qed
  1927 
  1928 lemma integral_mono:
  1929   fixes f :: "'a \<Rightarrow> real"
  1930   shows "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x) \<Longrightarrow>
  1931     integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1932   by (intro integral_mono_AE) auto
  1933 
  1934 text \<open>The next two statements are useful to bound Lebesgue integrals, as they avoid one
  1935 integrability assumption. The price to pay is that the upper function has to be nonnegative,
  1936 but this is often true and easy to check in computations.\<close>
  1937 
  1938 lemma integral_mono_AE':
  1939   fixes f::"_ \<Rightarrow> real"
  1940   assumes "integrable M f" "AE x in M. g x \<le> f x" "AE x in M. 0 \<le> f x"
  1941   shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
  1942 proof (cases "integrable M g")
  1943   case True
  1944   show ?thesis by (rule integral_mono_AE, auto simp add: assms True)
  1945 next
  1946   case False
  1947   then have "(\<integral>x. g x \<partial>M) = 0" by (simp add: not_integrable_integral_eq)
  1948   also have "... \<le> (\<integral>x. f x \<partial>M)" by (simp add: integral_nonneg_AE[OF assms(3)])
  1949   finally show ?thesis by simp
  1950 qed
  1951 
  1952 lemma integral_mono':
  1953   fixes f::"_ \<Rightarrow> real"
  1954   assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
  1955   shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
  1956 by (rule integral_mono_AE', insert assms, auto)
  1957 
  1958 lemma (in finite_measure) integrable_measure:
  1959   assumes I: "disjoint_family_on X I" "countable I"
  1960   shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
  1961 proof -
  1962   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)"
  1963     by (auto intro!: nn_integral_cong measure_notin_sets)
  1964   also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
  1965     using I unfolding emeasure_eq_measure[symmetric]
  1966     by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
  1967   finally show ?thesis
  1968     by (auto intro!: integrableI_bounded)
  1969 qed
  1970 
  1971 lemma integrableI_real_bounded:
  1972   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>"
  1973   shows "integrable M f"
  1974 proof (rule integrableI_bounded)
  1975   have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ennreal (f x) \<partial>M"
  1976     using ae by (auto intro: nn_integral_cong_AE)
  1977   also note fin
  1978   finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
  1979 qed fact
  1980 
  1981 lemma nn_integral_nonneg_infinite:
  1982   fixes f::"'a \<Rightarrow> real"
  1983   assumes "f \<in> borel_measurable M" "\<not> integrable M f" "AE x in M. f x \<ge> 0"
  1984   shows "(\<integral>\<^sup>+x. f x \<partial>M) = \<infinity>"
  1985 using assms integrableI_real_bounded less_top by auto
  1986 
  1987 lemma integral_real_bounded:
  1988   assumes "0 \<le> r" "integral\<^sup>N M f \<le> ennreal r"
  1989   shows "integral\<^sup>L M f \<le> r"
  1990 proof cases
  1991   assume [simp]: "integrable M f"
  1992 
  1993   have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>N M (\<lambda>x. max 0 (f x))"
  1994     by (intro nn_integral_eq_integral[symmetric]) auto
  1995   also have "\<dots> = integral\<^sup>N M f"
  1996     by (intro nn_integral_cong) (simp add: max_def ennreal_neg)
  1997   also have "\<dots> \<le> r"
  1998     by fact
  1999   finally have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) \<le> r"
  2000     using \<open>0 \<le> r\<close> by simp
  2001 
  2002   moreover have "integral\<^sup>L M f \<le> integral\<^sup>L M (\<lambda>x. max 0 (f x))"
  2003     by (rule integral_mono_AE) auto
  2004   ultimately show ?thesis
  2005     by simp
  2006 next
  2007   assume "\<not> integrable M f" then show ?thesis
  2008     using \<open>0 \<le> r\<close> by (simp add: not_integrable_integral_eq)
  2009 qed
  2010 
  2011 lemma integrable_Min:
  2012   fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
  2013   assumes "finite I" "I \<noteq> {}"
  2014           "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
  2015   shows "integrable M (\<lambda>x. Min {f i x|i. i \<in> I})"
  2016 using assms apply (induct rule: finite_ne_induct) apply simp+
  2017 proof -
  2018   fix j F assume H: "finite F" "F \<noteq> {}" "integrable M (\<lambda>x. Min {f i x |i. i \<in> F})"
  2019                     "(\<And>i. i = j \<or> i \<in> F \<Longrightarrow> integrable M (f i))"
  2020   have "{f i x |i. i = j \<or> i \<in> F} = insert (f j x) {f i x |i. i \<in> F}" for x by blast
  2021   then have "Min {f i x |i. i = j \<or> i \<in> F} = min (f j x) (Min {f i x |i. i \<in> F})" for x
  2022     using H(1) H(2) Min_insert by simp
  2023   moreover have "integrable M (\<lambda>x. min (f j x) (Min {f i x |i. i \<in> F}))"
  2024     by (rule integrable_min, auto simp add: H)
  2025   ultimately show "integrable M (\<lambda>x. Min {f i x |i. i = j \<or> i \<in> F})" by simp
  2026 qed
  2027 
  2028 lemma integrable_Max:
  2029   fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
  2030   assumes "finite I" "I \<noteq> {}"
  2031           "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
  2032   shows "integrable M (\<lambda>x. Max {f i x|i. i \<in> I})"
  2033 using assms apply (induct rule: finite_ne_induct) apply simp+
  2034 proof -
  2035   fix j F assume H: "finite F" "F \<noteq> {}" "integrable M (\<lambda>x. Max {f i x |i. i \<in> F})"
  2036                     "(\<And>i. i = j \<or> i \<in> F \<Longrightarrow> integrable M (f i))"
  2037   have "{f i x |i. i = j \<or> i \<in> F} = insert (f j x) {f i x |i. i \<in> F}" for x by blast
  2038   then have "Max {f i x |i. i = j \<or> i \<in> F} = max (f j x) (Max {f i x |i. i \<in> F})" for x
  2039     using H(1) H(2) Max_insert by simp
  2040   moreover have "integrable M (\<lambda>x. max (f j x) (Max {f i x |i. i \<in> F}))"
  2041     by (rule integrable_max, auto simp add: H)
  2042   ultimately show "integrable M (\<lambda>x. Max {f i x |i. i = j \<or> i \<in> F})" by simp
  2043 qed
  2044 
  2045 lemma integral_Markov_inequality:
  2046   assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)"
  2047   shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
  2048 proof -
  2049   have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
  2050     by (rule nn_integral_mono_AE, auto simp add: \<open>c>0\<close> less_eq_real_def)
  2051   also have "... = (\<integral>x. u x \<partial>M)"
  2052     by (rule nn_integral_eq_integral, auto simp add: assms)
  2053   finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
  2054     by simp
  2055 
  2056   have "{x \<in> space M. u x \<ge> c} = {x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M)"
  2057     using \<open>c>0\<close> by (auto simp: ennreal_mult'[symmetric])
  2058   then have "emeasure M {x \<in> space M. u x \<ge> c} = emeasure M ({x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M))"
  2059     by simp
  2060   also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
  2061     by (rule nn_integral_Markov_inequality) (auto simp add: assms)
  2062   also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
  2063     apply (rule mult_left_mono) using * \<open>c>0\<close> by auto
  2064   finally show ?thesis
  2065     using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
  2066 qed
  2067 
  2068 lemma integral_ineq_eq_0_then_AE:
  2069   fixes f::"_ \<Rightarrow> real"
  2070   assumes "AE x in M. f x \<le> g x" "integrable M f" "integrable M g"
  2071           "(\<integral>x. f x \<partial>M) = (\<integral>x. g x \<partial>M)"
  2072   shows "AE x in M. f x = g x"
  2073 proof -
  2074   define h where "h = (\<lambda>x. g x - f x)"
  2075   have "AE x in M. h x = 0"
  2076     apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
  2077     unfolding h_def using assms by auto
  2078   then show ?thesis unfolding h_def by auto
  2079 qed
  2080 
  2081 lemma not_AE_zero_int_E:
  2082   fixes f::"'a \<Rightarrow> real"
  2083   assumes "AE x in M. f x \<ge> 0" "(\<integral>x. f x \<partial>M) > 0"
  2084       and [measurable]: "f \<in> borel_measurable M"
  2085   shows "\<exists>A e. A \<in> sets M \<and> e>0 \<and> emeasure M A > 0 \<and> (\<forall>x \<in> A. f x \<ge> e)"
  2086 proof (rule not_AE_zero_E, auto simp add: assms)
  2087   assume *: "AE x in M. f x = 0"
  2088   have "(\<integral>x. f x \<partial>M) = (\<integral>x. 0 \<partial>M)" by (rule integral_cong_AE, auto simp add: *)
  2089   then have "(\<integral>x. f x \<partial>M) = 0" by simp
  2090   then show False using assms(2) by simp
  2091 qed
  2092 
  2093 lemma tendsto_L1_int:
  2094   fixes u :: "_ \<Rightarrow> _ \<Rightarrow> 'b::{banach, second_countable_topology}"
  2095   assumes [measurable]: "\<And>n. integrable M (u n)" "integrable M f"
  2096           and "((\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)) \<longlongrightarrow> 0) F"
  2097   shows "((\<lambda>n. (\<integral>x. u n x \<partial>M)) \<longlongrightarrow> (\<integral>x. f x \<partial>M)) F"
  2098 proof -
  2099   have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> (0::ennreal)) F"
  2100   proof (rule tendsto_sandwich[of "\<lambda>_. 0", where ?h = "\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)"], auto simp add: assms)
  2101     {
  2102       fix n
  2103       have "(\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M) = (\<integral>x. u n x - f x \<partial>M)"
  2104         apply (rule Bochner_Integration.integral_diff[symmetric]) using assms by auto
  2105       then have "norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M)) = norm (\<integral>x. u n x - f x \<partial>M)"
  2106         by auto
  2107       also have "... \<le> (\<integral>x. norm(u n x - f x) \<partial>M)"
  2108         by (rule integral_norm_bound)
  2109       finally have "ennreal(norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<le> (\<integral>x. norm(u n x - f x) \<partial>M)"
  2110         by simp
  2111       also have "... = (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)"
  2112         apply (rule nn_integral_eq_integral[symmetric]) using assms by auto
  2113       finally have "norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M)) \<le> (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)" by simp
  2114     }
  2115     then show "eventually (\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M)) \<le> (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)) F"
  2116       by auto
  2117   qed
  2118   then have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F"
  2119     by (simp add: ennreal_0[symmetric] del: ennreal_0)
  2120   then have "((\<lambda>n. ((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F" using tendsto_norm_zero_iff by blast
  2121   then show ?thesis using Lim_null by auto
  2122 qed
  2123 
  2124 text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then
  2125 it admits a subsequence that converges almost everywhere.\<close>
  2126 
  2127 lemma tendsto_L1_AE_subseq:
  2128   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2129   assumes [measurable]: "\<And>n. integrable M (u n)"
  2130       and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
  2131   shows "\<exists>r. subseq r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
  2132 proof -
  2133   {
  2134     fix k
  2135     have "eventually (\<lambda>n. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k) sequentially"
  2136       using order_tendstoD(2)[OF assms(2)] by auto
  2137     with eventually_elim2[OF eventually_gt_at_top[of k] this]
  2138     have "\<exists>n>k. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k"
  2139       by (metis eventually_False_sequentially)
  2140   }
  2141   then have "\<exists>r. \<forall>n. True \<and> (r (Suc n) > r n \<and> (\<integral>x. norm(u (r (Suc n)) x) \<partial>M) < (1/2)^(r n))"
  2142     by (intro dependent_nat_choice, auto)
  2143   then obtain r0 where r0: "subseq r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
  2144     by (auto simp: subseq_Suc_iff)
  2145   define r where "r = (\<lambda>n. r0(n+1))"
  2146   have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
  2147   have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
  2148   proof -
  2149     have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
  2150     have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
  2151     then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
  2152     then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
  2153     moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
  2154       by (rule nn_integral_eq_integral, auto simp add: integrable_norm[OF assms(1)[of "r n"]])
  2155     ultimately show ?thesis by (auto intro: ennreal_lessI)
  2156   qed
  2157 
  2158   have "AE x in M. limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
  2159   proof (rule AE_upper_bound_inf_ennreal)
  2160     fix e::real assume "e > 0"
  2161     define A where "A = (\<lambda>n. {x \<in> space M. norm(u (r n) x) \<ge> e})"
  2162     have A_meas [measurable]: "\<And>n. A n \<in> sets M" unfolding A_def by auto
  2163     have A_bound: "emeasure M (A n) < (1/e) * ennreal((1/2)^n)" for n
  2164     proof -
  2165       have *: "indicator (A n) x \<le> (1/e) * ennreal(norm(u (r n) x))" for x
  2166         apply (cases "x \<in> A n") unfolding A_def using \<open>0 < e\<close> by (auto simp: ennreal_mult[symmetric])
  2167       have "emeasure M (A n) = (\<integral>\<^sup>+x. indicator (A n) x \<partial>M)" by auto
  2168       also have "... \<le> (\<integral>\<^sup>+x. (1/e) * ennreal(norm(u (r n) x)) \<partial>M)"
  2169         apply (rule nn_integral_mono) using * by auto
  2170       also have "... = (1/e) * (\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M)"
  2171         apply (rule nn_integral_cmult) using \<open>e > 0\<close> by auto
  2172       also have "... < (1/e) * ennreal((1/2)^n)"
  2173         using I[of n] \<open>e > 0\<close> by (intro ennreal_mult_strict_left_mono) auto
  2174       finally show ?thesis by simp
  2175     qed
  2176     have A_fin: "emeasure M (A n) < \<infinity>" for n
  2177       using \<open>e > 0\<close> A_bound[of n]
  2178       by (auto simp add: ennreal_mult less_top[symmetric])
  2179 
  2180     have A_sum: "summable (\<lambda>n. measure M (A n))"
  2181     proof (rule summable_comparison_test'[of "\<lambda>n. (1/e) * (1/2)^n" 0])
  2182       have "summable (\<lambda>n. (1/(2::real))^n)" by (simp add: summable_geometric)
  2183       then show "summable (\<lambda>n. (1/e) * (1/2)^n)" using summable_mult by blast
  2184       fix n::nat assume "n \<ge> 0"
  2185       have "norm(measure M (A n)) = measure M (A n)" by simp
  2186       also have "... = enn2real(emeasure M (A n))" unfolding measure_def by simp
  2187       also have "... < enn2real((1/e) * (1/2)^n)"
  2188         using A_bound[of n] \<open>emeasure M (A n) < \<infinity>\<close> \<open>0 < e\<close>
  2189         by (auto simp: emeasure_eq_ennreal_measure ennreal_mult[symmetric] ennreal_less_iff)
  2190       also have "... = (1/e) * (1/2)^n"
  2191         using \<open>0<e\<close> by auto
  2192       finally show "norm(measure M (A n)) \<le> (1/e) * (1/2)^n" by simp
  2193     qed
  2194 
  2195     have "AE x in M. eventually (\<lambda>n. x \<in> space M - A n) sequentially"
  2196       by (rule borel_cantelli_AE1[OF A_meas A_fin A_sum])
  2197     moreover
  2198     {
  2199       fix x assume "eventually (\<lambda>n. x \<in> space M - A n) sequentially"
  2200       moreover have "norm(u (r n) x) \<le> ennreal e" if "x \<in> space M - A n" for n
  2201         using that unfolding A_def by (auto intro: ennreal_leI)
  2202       ultimately have "eventually (\<lambda>n. norm(u (r n) x) \<le> ennreal e) sequentially"
  2203         by (simp add: eventually_mono)
  2204       then have "limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> e"
  2205         by (simp add: Limsup_bounded)
  2206     }
  2207     ultimately show "AE x in M. limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0 + ennreal e" by auto
  2208   qed
  2209   moreover
  2210   {
  2211     fix x assume "limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
  2212     moreover then have "liminf (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
  2213       by (rule order_trans[rotated]) (auto intro: Liminf_le_Limsup)
  2214     ultimately have "(\<lambda>n. ennreal (norm(u (r n) x))) \<longlonglongrightarrow> 0"
  2215       using tendsto_Limsup[of sequentially "\<lambda>n. ennreal (norm(u (r n) x))"] by auto
  2216     then have "(\<lambda>n. norm(u (r n) x)) \<longlonglongrightarrow> 0"
  2217       by (simp add: ennreal_0[symmetric] del: ennreal_0)
  2218     then have "(\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0"
  2219       by (simp add: tendsto_norm_zero_iff)
  2220   }
  2221   ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
  2222   then show ?thesis using \<open>subseq r\<close> by auto
  2223 qed
  2224 
  2225 subsection \<open>Restricted measure spaces\<close>
  2226 
  2227 lemma integrable_restrict_space:
  2228   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2229   assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  2230   shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  2231   unfolding integrable_iff_bounded
  2232     borel_measurable_restrict_space_iff[OF \<Omega>]
  2233     nn_integral_restrict_space[OF \<Omega>]
  2234   by (simp add: ac_simps ennreal_indicator ennreal_mult)
  2235 
  2236 lemma integral_restrict_space:
  2237   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2238   assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  2239   shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  2240 proof (rule integral_eq_cases)
  2241   assume "integrable (restrict_space M \<Omega>) f"
  2242   then show ?thesis
  2243   proof induct
  2244     case (base A c) then show ?case
  2245       by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
  2246                     emeasure_restrict_space Int_absorb1 measure_restrict_space)
  2247   next
  2248     case (add g f) then show ?case
  2249       by (simp add: scaleR_add_right integrable_restrict_space)
  2250   next
  2251     case (lim f s)
  2252     show ?case
  2253     proof (rule LIMSEQ_unique)
  2254       show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) \<longlonglongrightarrow> integral\<^sup>L (restrict_space M \<Omega>) f"
  2255         using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
  2256 
  2257       show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) \<longlonglongrightarrow> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
  2258         unfolding lim
  2259         using lim
  2260         by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
  2261            (auto simp add: space_restrict_space integrable_restrict_space simp del: norm_scaleR
  2262                  split: split_indicator)
  2263     qed
  2264   qed
  2265 qed (simp add: integrable_restrict_space)
  2266 
  2267 lemma integral_empty:
  2268   assumes "space M = {}"
  2269   shows "integral\<^sup>L M f = 0"
  2270 proof -
  2271   have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
  2272     by(rule integral_cong)(simp_all add: assms)
  2273   thus ?thesis by simp
  2274 qed
  2275 
  2276 subsection \<open>Measure spaces with an associated density\<close>
  2277 
  2278 lemma integrable_density:
  2279   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  2280   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  2281     and nn: "AE x in M. 0 \<le> g x"
  2282   shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
  2283   unfolding integrable_iff_bounded using nn
  2284   apply (simp add: nn_integral_density less_top[symmetric])
  2285   apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
  2286   apply (auto simp: ennreal_mult)
  2287   done
  2288 
  2289 lemma integral_density:
  2290   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  2291   assumes f: "f \<in> borel_measurable M"
  2292     and g[measurable]: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
  2293   shows "integral\<^sup>L (density M g) f = integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
  2294 proof (rule integral_eq_cases)
  2295   assume "integrable (density M g) f"
  2296   then show ?thesis
  2297   proof induct
  2298     case (base A c)
  2299     then have [measurable]: "A \<in> sets M" by auto
  2300 
  2301     have int: "integrable M (\<lambda>x. g x * indicator A x)"
  2302       using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
  2303     then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ennreal (g x * indicator A x) \<partial>M)"
  2304       using g by (subst nn_integral_eq_integral) auto
  2305     also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (g x) * indicator A x \<partial>M)"
  2306       by (intro nn_integral_cong) (auto split: split_indicator)
  2307     also have "\<dots> = emeasure (density M g) A"
  2308       by (rule emeasure_density[symmetric]) auto
  2309     also have "\<dots> = ennreal (measure (density M g) A)"
  2310       using base by (auto intro: emeasure_eq_ennreal_measure)
  2311     also have "\<dots> = integral\<^sup>L (density M g) (indicator A)"
  2312       using base by simp
  2313     finally show ?case
  2314       using base g
  2315       apply (simp add: int integral_nonneg_AE)
  2316       apply (subst (asm) ennreal_inj)
  2317       apply (auto intro!: integral_nonneg_AE)
  2318       done
  2319   next
  2320     case (add f h)
  2321     then have [measurable]: "f \<in> borel_measurable M" "h \<in> borel_measurable M"
  2322       by (auto dest!: borel_measurable_integrable)
  2323     from add g show ?case
  2324       by (simp add: scaleR_add_right integrable_density)
  2325   next
  2326     case (lim f s)
  2327     have [measurable]: "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M"
  2328       using lim(1,5)[THEN borel_measurable_integrable] by auto
  2329 
  2330     show ?case
  2331     proof (rule LIMSEQ_unique)
  2332       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)"
  2333       proof (rule integral_dominated_convergence)
  2334         show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
  2335           by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
  2336         show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) \<longlonglongrightarrow> g x *\<^sub>R f x"
  2337           using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M])
  2338         show "\<And>i. AE x in M. norm (g x *\<^sub>R s i x) \<le> 2 * norm (g x *\<^sub>R f x)"
  2339           using lim(4) g by (auto intro!: AE_I2[of M] mult_left_mono simp: field_simps)
  2340       qed auto
  2341       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) \<longlonglongrightarrow> integral\<^sup>L (density M g) f"
  2342         unfolding lim(2)[symmetric]
  2343         by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  2344            (insert lim(3-5), auto)
  2345     qed
  2346   qed
  2347 qed (simp add: f g integrable_density)
  2348 
  2349 lemma
  2350   fixes g :: "'a \<Rightarrow> real"
  2351   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "g \<in> borel_measurable M"
  2352   shows integral_real_density: "integral\<^sup>L (density M f) g = (\<integral> x. f x * g x \<partial>M)"
  2353     and integrable_real_density: "integrable (density M f) g \<longleftrightarrow> integrable M (\<lambda>x. f x * g x)"
  2354   using assms integral_density[of g M f] integrable_density[of g M f] by auto
  2355 
  2356 lemma has_bochner_integral_density:
  2357   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  2358   shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. 0 \<le> g x) \<Longrightarrow>
  2359     has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
  2360   by (simp add: has_bochner_integral_iff integrable_density integral_density)
  2361 
  2362 subsection \<open>Distributions\<close>
  2363 
  2364 lemma integrable_distr_eq:
  2365   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2366   assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
  2367   shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
  2368   unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
  2369 
  2370 lemma integrable_distr:
  2371   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2372   shows "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
  2373   by (subst integrable_distr_eq[symmetric, where g=T])
  2374      (auto dest: borel_measurable_integrable)
  2375 
  2376 lemma integral_distr:
  2377   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2378   assumes g[measurable]: "g \<in> measurable M N" and f: "f \<in> borel_measurable N"
  2379   shows "integral\<^sup>L (distr M N g) f = integral\<^sup>L M (\<lambda>x. f (g x))"
  2380 proof (rule integral_eq_cases)
  2381   assume "integrable (distr M N g) f"
  2382   then show ?thesis
  2383   proof induct
  2384     case (base A c)
  2385     then have [measurable]: "A \<in> sets N" by auto
  2386     from base have int: "integrable (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c)"
  2387       by (intro integrable_indicator)
  2388 
  2389     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"
  2390       using base by auto
  2391     also have "\<dots> = measure M (g -` A \<inter> space M) *\<^sub>R c"
  2392       by (subst measure_distr) auto
  2393     also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator (g -` A \<inter> space M) a *\<^sub>R c)"
  2394       using base by (auto simp: emeasure_distr)
  2395     also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator A (g a) *\<^sub>R c)"
  2396       using int base by (intro integral_cong_AE) (auto simp: emeasure_distr split: split_indicator)
  2397     finally show ?case .
  2398   next
  2399     case (add f h)
  2400     then have [measurable]: "f \<in> borel_measurable N" "h \<in> borel_measurable N"
  2401       by (auto dest!: borel_measurable_integrable)
  2402     from add g show ?case
  2403       by (simp add: scaleR_add_right integrable_distr_eq)
  2404   next
  2405     case (lim f s)
  2406     have [measurable]: "f \<in> borel_measurable N" "\<And>i. s i \<in> borel_measurable N"
  2407       using lim(1,5)[THEN borel_measurable_integrable] by auto
  2408 
  2409     show ?case
  2410     proof (rule LIMSEQ_unique)
  2411       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) \<longlonglongrightarrow> integral\<^sup>L M (\<lambda>x. f (g x))"
  2412       proof (rule integral_dominated_convergence)
  2413         show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
  2414           using lim by (auto simp: integrable_distr_eq)
  2415         show "AE x in M. (\<lambda>i. s i (g x)) \<longlonglongrightarrow> f (g x)"
  2416           using lim(3) g[THEN measurable_space] by auto
  2417         show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
  2418           using lim(4) g[THEN measurable_space] by auto
  2419       qed auto
  2420       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) \<longlonglongrightarrow> integral\<^sup>L (distr M N g) f"
  2421         unfolding lim(2)[symmetric]
  2422         by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  2423            (insert lim(3-5), auto)
  2424     qed
  2425   qed
  2426 qed (simp add: f g integrable_distr_eq)
  2427 
  2428 lemma has_bochner_integral_distr:
  2429   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2430   shows "f \<in> borel_measurable N \<Longrightarrow> g \<in> measurable M N \<Longrightarrow>
  2431     has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
  2432   by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
  2433 
  2434 subsection \<open>Lebesgue integration on @{const count_space}\<close>
  2435 
  2436 lemma integrable_count_space:
  2437   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  2438   shows "finite X \<Longrightarrow> integrable (count_space X) f"
  2439   by (auto simp: nn_integral_count_space integrable_iff_bounded)
  2440 
  2441 lemma measure_count_space[simp]:
  2442   "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
  2443   unfolding measure_def by (subst emeasure_count_space ) auto
  2444 
  2445 lemma lebesgue_integral_count_space_finite_support:
  2446   assumes f: "finite {a\<in>A. f a \<noteq> 0}"
  2447   shows "(\<integral>x. f x \<partial>count_space A) = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. f a)"
  2448 proof -
  2449   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)"
  2450     by (intro sum.mono_neutral_cong_left) auto
  2451 
  2452   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)"
  2453     by (intro integral_cong refl) (simp add: f eq)
  2454   also have "\<dots> = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. measure (count_space A) {a} *\<^sub>R f a)"
  2455     by (subst integral_sum) (auto intro!: sum.cong)
  2456   finally show ?thesis
  2457     by auto
  2458 qed
  2459 
  2460 lemma lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
  2461   by (subst lebesgue_integral_count_space_finite_support)
  2462      (auto intro!: sum.mono_neutral_cong_left)
  2463 
  2464 lemma integrable_count_space_nat_iff:
  2465   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2466   shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
  2467   by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat ennreal_suminf_neq_top
  2468            intro:  summable_suminf_not_top)
  2469 
  2470 lemma sums_integral_count_space_nat:
  2471   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2472   assumes *: "integrable (count_space UNIV) f"
  2473   shows "f sums (integral\<^sup>L (count_space UNIV) f)"
  2474 proof -
  2475   let ?f = "\<lambda>n i. indicator {n} i *\<^sub>R f i"
  2476   have f': "\<And>n i. ?f n i = indicator {n} i *\<^sub>R f n"
  2477     by (auto simp: fun_eq_iff split: split_indicator)
  2478 
  2479   have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) sums \<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV"
  2480   proof (rule sums_integral)
  2481     show "\<And>i. integrable (count_space UNIV) (?f i)"
  2482       using * by (intro integrable_mult_indicator) auto
  2483     show "AE n in count_space UNIV. summable (\<lambda>i. norm (?f i n))"
  2484       using summable_finite[of "{n}" "\<lambda>i. norm (?f i n)" for n] by simp
  2485     show "summable (\<lambda>i. \<integral> n. norm (?f i n) \<partial>count_space UNIV)"
  2486       using * by (subst f') (simp add: integrable_count_space_nat_iff)
  2487   qed
  2488   also have "(\<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV) = (\<integral>n. f n \<partial>count_space UNIV)"
  2489     using suminf_finite[of "{n}" "\<lambda>i. ?f i n" for n] by (auto intro!: integral_cong)
  2490   also have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) = f"
  2491     by (subst f') simp
  2492   finally show ?thesis .
  2493 qed
  2494 
  2495 lemma integral_count_space_nat:
  2496   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2497   shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
  2498   using sums_integral_count_space_nat by (rule sums_unique)
  2499 
  2500 lemma integrable_bij_count_space:
  2501   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2502   assumes g: "bij_betw g A B"
  2503   shows "integrable (count_space A) (\<lambda>x. f (g x)) \<longleftrightarrow> integrable (count_space B) f"
  2504   unfolding integrable_iff_bounded by (subst nn_integral_bij_count_space[OF g]) auto
  2505 
  2506 lemma integral_bij_count_space:
  2507   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2508   assumes g: "bij_betw g A B"
  2509   shows "integral\<^sup>L (count_space A) (\<lambda>x. f (g x)) = integral\<^sup>L (count_space B) f"
  2510   using g[THEN bij_betw_imp_funcset]
  2511   apply (subst distr_bij_count_space[OF g, symmetric])
  2512   apply (intro integral_distr[symmetric])
  2513   apply auto
  2514   done
  2515 
  2516 lemma has_bochner_integral_count_space_nat:
  2517   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  2518   shows "has_bochner_integral (count_space UNIV) f x \<Longrightarrow> f sums x"
  2519   unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat)
  2520 
  2521 subsection \<open>Point measure\<close>
  2522 
  2523 lemma lebesgue_integral_point_measure_finite:
  2524   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2525   shows "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow>
  2526     integral\<^sup>L (point_measure A f) g = (\<Sum>a\<in>A. f a *\<^sub>R g a)"
  2527   by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def)
  2528 
  2529 lemma integrable_point_measure_finite:
  2530   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and f :: "'a \<Rightarrow> real"
  2531   shows "finite A \<Longrightarrow> integrable (point_measure A f) g"
  2532   unfolding point_measure_def
  2533   apply (subst density_cong[where f'="\<lambda>x. ennreal (max 0 (f x))"])
  2534   apply (auto split: split_max simp: ennreal_neg)
  2535   apply (subst integrable_density)
  2536   apply (auto simp: AE_count_space integrable_count_space)
  2537   done
  2538 
  2539 subsection \<open>Lebesgue integration on @{const null_measure}\<close>
  2540 
  2541 lemma has_bochner_integral_null_measure_iff[iff]:
  2542   "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
  2543   by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
  2544            intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
  2545 
  2546 lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
  2547   by (auto simp add: integrable.simps)
  2548 
  2549 lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
  2550   by (cases "integrable (null_measure M) f")
  2551      (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
  2552 
  2553 subsection \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
  2554 
  2555 lemma real_lebesgue_integral_def:
  2556   assumes f[measurable]: "integrable M f"
  2557   shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+x. f x \<partial>M) - enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
  2558 proof -
  2559   have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
  2560     by (auto intro!: arg_cong[where f="integral\<^sup>L M"])
  2561   also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
  2562     by (intro integral_diff integrable_max integrable_minus integrable_zero f)
  2563   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = enn2real (\<integral>\<^sup>+x. ennreal (f x) \<partial>M)"
  2564     by (subst integral_eq_nn_integral) (auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: max_def ennreal_neg)
  2565   also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
  2566     by (subst integral_eq_nn_integral) (auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: max_def ennreal_neg)
  2567   finally show ?thesis .
  2568 qed
  2569 
  2570 lemma real_integrable_def:
  2571   "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
  2572     (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  2573   unfolding integrable_iff_bounded
  2574 proof (safe del: notI)
  2575   assume *: "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  2576   have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  2577     by (intro nn_integral_mono) auto
  2578   also note *
  2579   finally show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>"
  2580     by simp
  2581   have "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  2582     by (intro nn_integral_mono) auto
  2583   also note *
  2584   finally show "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  2585     by simp
  2586 next
  2587   assume [measurable]: "f \<in> borel_measurable M"
  2588   assume fin: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  2589   have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (f x) + ennreal (- f x) \<partial>M)"
  2590     by (intro nn_integral_cong) (auto simp: abs_real_def ennreal_neg)
  2591   also have"\<dots> = (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) + (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M)"
  2592     by (intro nn_integral_add) auto
  2593   also have "\<dots> < \<infinity>"
  2594     using fin by (auto simp: less_top)
  2595   finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
  2596 qed
  2597 
  2598 lemma integrableD[dest]:
  2599   assumes "integrable M f"
  2600   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>"
  2601   using assms unfolding real_integrable_def by auto
  2602 
  2603 lemma integrableE:
  2604   assumes "integrable M f"
  2605   obtains r q where "0 \<le> r" "0 \<le> q"
  2606     "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M) = ennreal r"
  2607     "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M) = ennreal q"
  2608     "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
  2609   using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
  2610   by (cases rule: ennreal2_cases[of "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M)"]) auto
  2611 
  2612 lemma integral_monotone_convergence_nonneg:
  2613   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  2614   assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  2615     and pos: "\<And>i. AE x in M. 0 \<le> f i x"
  2616     and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
  2617     and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) \<longlonglongrightarrow> x"
  2618     and u: "u \<in> borel_measurable M"
  2619   shows "integrable M u"
  2620   and "integral\<^sup>L M u = x"
  2621 proof -
  2622   have nn: "AE x in M. \<forall>i. 0 \<le> f i x"
  2623     using pos unfolding AE_all_countable by auto
  2624   with lim have u_nn: "AE x in M. 0 \<le> u x"
  2625     by eventually_elim (auto intro: LIMSEQ_le_const)
  2626   have [simp]: "0 \<le> x"
  2627     by (intro LIMSEQ_le_const[OF ilim] allI exI impI integral_nonneg_AE pos)
  2628   have "(\<integral>\<^sup>+ x. ennreal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ennreal (f n x) \<partial>M))"
  2629   proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
  2630     fix i
  2631     from mono nn show "AE x in M. ennreal (f i x) \<le> ennreal (f (Suc i) x)"
  2632       by eventually_elim (auto simp: mono_def)
  2633     show "(\<lambda>x. ennreal (f i x)) \<in> borel_measurable M"
  2634       using i by auto
  2635   next
  2636     show "(\<integral>\<^sup>+ x. ennreal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ennreal (f i x)) \<partial>M"
  2637       apply (rule nn_integral_cong_AE)
  2638       using lim mono nn u_nn
  2639       apply eventually_elim
  2640       apply (simp add: LIMSEQ_unique[OF _ LIMSEQ_SUP] incseq_def)
  2641       done
  2642   qed
  2643   also have "\<dots> = ennreal x"
  2644     using mono i nn unfolding nn_integral_eq_integral[OF i pos]
  2645     by (subst LIMSEQ_unique[OF LIMSEQ_SUP]) (auto simp: mono_def integral_nonneg_AE pos intro!: integral_mono_AE ilim)
  2646   finally have "(\<integral>\<^sup>+ x. ennreal (u x) \<partial>M) = ennreal x" .
  2647   moreover have "(\<integral>\<^sup>+ x. ennreal (- u x) \<partial>M) = 0"
  2648     using u u_nn by (subst nn_integral_0_iff_AE) (auto simp add: ennreal_neg)
  2649   ultimately show "integrable M u" "integral\<^sup>L M u = x"
  2650     by (auto simp: real_integrable_def real_lebesgue_integral_def u)
  2651 qed
  2652 
  2653 lemma
  2654   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  2655   assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  2656   and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
  2657   and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) \<longlonglongrightarrow> x"
  2658   and u: "u \<in> borel_measurable M"
  2659   shows integrable_monotone_convergence: "integrable M u"
  2660     and integral_monotone_convergence: "integral\<^sup>L M u = x"
  2661     and has_bochner_integral_monotone_convergence: "has_bochner_integral M u x"
  2662 proof -
  2663   have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
  2664     using f by auto
  2665   have 2: "AE x in M. mono (\<lambda>n. f n x - f 0 x)"
  2666     using mono by (auto simp: mono_def le_fun_def)
  2667   have 3: "\<And>n. AE x in M. 0 \<le> f n x - f 0 x"
  2668     using mono by (auto simp: field_simps mono_def le_fun_def)
  2669   have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) \<longlonglongrightarrow> u x - f 0 x"
  2670     using lim by (auto intro!: tendsto_diff)
  2671   have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) \<longlonglongrightarrow> x - integral\<^sup>L M (f 0)"
  2672     using f ilim by (auto intro!: tendsto_diff)
  2673   have 6: "(\<lambda>x. u x - f 0 x) \<in> borel_measurable M"
  2674     using f[of 0] u by auto
  2675   note diff = integral_monotone_convergence_nonneg[OF 1 2 3 4 5 6]
  2676   have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
  2677     using diff(1) f by (rule integrable_add)
  2678   with diff(2) f show "integrable M u" "integral\<^sup>L M u = x"
  2679     by auto
  2680   then show "has_bochner_integral M u x"
  2681     by (metis has_bochner_integral_integrable)
  2682 qed
  2683 
  2684 lemma integral_norm_eq_0_iff:
  2685   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2686   assumes f[measurable]: "integrable M f"
  2687   shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
  2688 proof -
  2689   have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>x. norm (f x) \<partial>M)"
  2690     using f by (intro nn_integral_eq_integral integrable_norm) auto
  2691   then have "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) = 0"
  2692     by simp
  2693   also have "\<dots> \<longleftrightarrow> emeasure M {x\<in>space M. ennreal (norm (f x)) \<noteq> 0} = 0"
  2694     by (intro nn_integral_0_iff) auto
  2695   finally show ?thesis
  2696     by simp
  2697 qed
  2698 
  2699 lemma integral_0_iff:
  2700   fixes f :: "'a \<Rightarrow> real"
  2701   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"
  2702   using integral_norm_eq_0_iff[of M f] by simp
  2703 
  2704 lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
  2705   using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong add: less_top[symmetric])
  2706 
  2707 lemma lebesgue_integral_const[simp]:
  2708   fixes a :: "'a :: {banach, second_countable_topology}"
  2709   shows "(\<integral>x. a \<partial>M) = measure M (space M) *\<^sub>R a"
  2710 proof -
  2711   { assume "emeasure M (space M) = \<infinity>" "a \<noteq> 0"
  2712     then have ?thesis
  2713       by (auto simp add: not_integrable_integral_eq ennreal_mult_less_top measure_def integrable_iff_bounded) }
  2714   moreover
  2715   { assume "a = 0" then have ?thesis by simp }
  2716   moreover
  2717   { assume "emeasure M (space M) \<noteq> \<infinity>"
  2718     interpret finite_measure M
  2719       proof qed fact
  2720     have "(\<integral>x. a \<partial>M) = (\<integral>x. indicator (space M) x *\<^sub>R a \<partial>M)"
  2721       by (intro integral_cong) auto
  2722     also have "\<dots> = measure M (space M) *\<^sub>R a"
  2723       by (simp add: less_top[symmetric])
  2724     finally have ?thesis . }
  2725   ultimately show ?thesis by blast
  2726 qed
  2727 
  2728 lemma (in finite_measure) integrable_const_bound:
  2729   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  2730   shows "AE x in M. norm (f x) \<le> B \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> integrable M f"
  2731   apply (rule integrable_bound[OF integrable_const[of B], of f])
  2732   apply assumption
  2733   apply (cases "0 \<le> B")
  2734   apply auto
  2735   done
  2736 
  2737 lemma (in finite_measure) integral_bounded_eq_bound_then_AE:
  2738   assumes "AE x in M. f x \<le> (c::real)"
  2739     "integrable M f" "(\<integral>x. f x \<partial>M) = c * measure M (space M)"
  2740   shows "AE x in M. f x = c"
  2741   apply (rule integral_ineq_eq_0_then_AE) using assms by auto
  2742 
  2743 lemma integral_indicator_finite_real:
  2744   fixes f :: "'a \<Rightarrow> real"
  2745   assumes [simp]: "finite A"
  2746   assumes [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"
  2747   assumes finite: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} < \<infinity>"
  2748   shows "(\<integral>x. f x * indicator A x \<partial>M) = (\<Sum>a\<in>A. f a * measure M {a})"
  2749 proof -
  2750   have "(\<integral>x. f x * indicator A x \<partial>M) = (\<integral>x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
  2751   proof (intro integral_cong refl)
  2752     fix x show "f x * indicator A x = (\<Sum>a\<in>A. f a * indicator {a} x)"
  2753       by (auto split: split_indicator simp: eq_commute[of x] cong: conj_cong)
  2754   qed
  2755   also have "\<dots> = (\<Sum>a\<in>A. f a * measure M {a})"
  2756     using finite by (subst integral_sum) (auto simp add: integrable_mult_left_iff)
  2757   finally show ?thesis .
  2758 qed
  2759 
  2760 lemma (in finite_measure) ennreal_integral_real:
  2761   assumes [measurable]: "f \<in> borel_measurable M"
  2762   assumes ae: "AE x in M. f x \<le> ennreal B" "0 \<le> B"
  2763   shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  2764 proof (subst nn_integral_eq_integral[symmetric])
  2765   show "integrable M (\<lambda>x. enn2real (f x))"
  2766     using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI)
  2767   show "(\<integral>\<^sup>+ x. ennreal (enn2real (f x)) \<partial>M) = integral\<^sup>N M f"
  2768     using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
  2769 qed auto
  2770 
  2771 lemma (in finite_measure) integral_less_AE:
  2772   fixes X Y :: "'a \<Rightarrow> real"
  2773   assumes int: "integrable M X" "integrable M Y"
  2774   assumes A: "(emeasure M) A \<noteq> 0" "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> X x \<noteq> Y x"
  2775   assumes gt: "AE x in M. X x \<le> Y x"
  2776   shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  2777 proof -
  2778   have "integral\<^sup>L M X \<le> integral\<^sup>L M Y"
  2779     using gt int by (intro integral_mono_AE) auto
  2780   moreover
  2781   have "integral\<^sup>L M X \<noteq> integral\<^sup>L M Y"
  2782   proof
  2783     assume eq: "integral\<^sup>L M X = integral\<^sup>L M Y"
  2784     have "integral\<^sup>L M (\<lambda>x. \<bar>Y x - X x\<bar>) = integral\<^sup>L M (\<lambda>x. Y x - X x)"
  2785       using gt int by (intro integral_cong_AE) auto
  2786     also have "\<dots> = 0"
  2787       using eq int by simp
  2788     finally have "(emeasure M) {x \<in> space M. Y x - X x \<noteq> 0} = 0"
  2789       using int by (simp add: integral_0_iff)
  2790     moreover
  2791     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)"
  2792       using A by (intro nn_integral_mono_AE) auto
  2793     then have "(emeasure M) A \<le> (emeasure M) {x \<in> space M. Y x - X x \<noteq> 0}"
  2794       using int A by (simp add: integrable_def)
  2795     ultimately have "emeasure M A = 0"
  2796       by simp
  2797     with \<open>(emeasure M) A \<noteq> 0\<close> show False by auto
  2798   qed
  2799   ultimately show ?thesis by auto
  2800 qed
  2801 
  2802 lemma (in finite_measure) integral_less_AE_space:
  2803   fixes X Y :: "'a \<Rightarrow> real"
  2804   assumes int: "integrable M X" "integrable M Y"
  2805   assumes gt: "AE x in M. X x < Y x" "emeasure M (space M) \<noteq> 0"
  2806   shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  2807   using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
  2808 
  2809 lemma tendsto_integral_at_top:
  2810   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
  2811   assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
  2812   shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) \<longlongrightarrow> \<integral> x. f x \<partial>M) at_top"
  2813 proof (rule tendsto_at_topI_sequentially)
  2814   fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
  2815   show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) \<longlonglongrightarrow> integral\<^sup>L M f"
  2816   proof (rule integral_dominated_convergence)
  2817     show "integrable M (\<lambda>x. norm (f x))"
  2818       by (rule integrable_norm) fact
  2819     show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
  2820     proof
  2821       fix x
  2822       from \<open>filterlim X at_top sequentially\<close>
  2823       have "eventually (\<lambda>n. x \<le> X n) sequentially"
  2824         unfolding filterlim_at_top_ge[where c=x] by auto
  2825       then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
  2826         by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
  2827     qed
  2828     fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
  2829       by (auto split: split_indicator)
  2830   qed auto
  2831 qed
  2832 
  2833 lemma
  2834   fixes f :: "real \<Rightarrow> real"
  2835   assumes M: "sets M = sets borel"
  2836   assumes nonneg: "AE x in M. 0 \<le> f x"
  2837   assumes borel: "f \<in> borel_measurable borel"
  2838   assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
  2839   assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) \<longlongrightarrow> x) at_top"
  2840   shows has_bochner_integral_monotone_convergence_at_top: "has_bochner_integral M f x"
  2841     and integrable_monotone_convergence_at_top: "integrable M f"
  2842     and integral_monotone_convergence_at_top:"integral\<^sup>L M f = x"
  2843 proof -
  2844   from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
  2845     by (auto split: split_indicator intro!: monoI)
  2846   { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
  2847       by (rule eventually_sequentiallyI[of "nat \<lceil>x\<rceil>"])
  2848          (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
  2849   from filterlim_cong[OF refl refl this]
  2850   have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) \<longlonglongrightarrow> f x"
  2851     by simp
  2852   have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) \<longlonglongrightarrow> x"
  2853     using conv filterlim_real_sequentially by (rule filterlim_compose)
  2854   have M_measure[simp]: "borel_measurable M = borel_measurable borel"
  2855     using M by (simp add: sets_eq_imp_space_eq measurable_def)
  2856   have "f \<in> borel_measurable M"
  2857     using borel by simp
  2858   show "has_bochner_integral M f x"
  2859     by (rule has_bochner_integral_monotone_convergence) fact+
  2860   then show "integrable M f" "integral\<^sup>L M f = x"
  2861     by (auto simp: _has_bochner_integral_iff)
  2862 qed
  2863 
  2864 subsection \<open>Product measure\<close>
  2865 
  2866 lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
  2867   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  2868   assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  2869   shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
  2870 proof -
  2871   have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
  2872     unfolding integrable_iff_bounded by simp
  2873   show ?thesis
  2874     by (simp cong: measurable_cong)
  2875 qed
  2876 
  2877 lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
  2878 
  2879 lemma (in sigma_finite_measure) measurable_measure[measurable (raw)]:
  2880   "(\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M) \<Longrightarrow>
  2881     {x \<in> space (N \<Otimes>\<^sub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^sub>M M) \<Longrightarrow>
  2882     (\<lambda>x. measure M (A x)) \<in> borel_measurable N"
  2883   unfolding measure_def by (intro measurable_emeasure borel_measurable_enn2real) auto
  2884 
  2885 lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
  2886   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  2887   assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  2888   shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
  2889 proof -
  2890   from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
  2891   then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
  2892     "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
  2893     "\<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)"
  2894     by (auto simp: space_pair_measure)
  2895 
  2896   have [measurable]: "\<And>i. s i \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  2897     by (rule borel_measurable_simple_function) fact
  2898 
  2899   have "\<And>i. s i \<in> measurable (N \<Otimes>\<^sub>M M) (count_space UNIV)"
  2900     by (rule measurable_simple_function) fact
  2901 
  2902   define f' where [abs_def]: "f' i x =
  2903     (if integrable M (f x) then simple_bochner_integral M (\<lambda>y. s i (x, y)) else 0)" for i x
  2904 
  2905   { fix i x assume "x \<in> space N"
  2906     then have "simple_bochner_integral M (\<lambda>y. s i (x, y)) =
  2907       (\<Sum>z\<in>s i ` (space N \<times> space M). measure M {y \<in> space M. s i (x, y) = z} *\<^sub>R z)"
  2908       using s(1)[THEN simple_functionD(1)]
  2909       unfolding simple_bochner_integral_def
  2910       by (intro sum.mono_neutral_cong_left)
  2911          (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
  2912   note eq = this
  2913 
  2914   show ?thesis
  2915   proof (rule borel_measurable_LIMSEQ_metric)
  2916     fix i show "f' i \<in> borel_measurable N"
  2917       unfolding f'_def by (simp_all add: eq cong: measurable_cong if_cong)
  2918   next
  2919     fix x assume x: "x \<in> space N"
  2920     { assume int_f: "integrable M (f x)"
  2921       have int_2f: "integrable M (\<lambda>y. 2 * norm (f x y))"
  2922         by (intro integrable_norm integrable_mult_right int_f)
  2923       have "(\<lambda>i. integral\<^sup>L M (\<lambda>y. s i (x, y))) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
  2924       proof (rule integral_dominated_convergence)
  2925         from int_f show "f x \<in> borel_measurable M" by auto
  2926         show "\<And>i. (\<lambda>y. s i (x, y)) \<in> borel_measurable M"
  2927           using x by simp
  2928         show "AE xa in M. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f x xa"
  2929           using x s(2) by auto
  2930         show "\<And>i. AE xa in M. norm (s i (x, xa)) \<le> 2 * norm (f x xa)"
  2931           using x s(3) by auto
  2932       qed fact
  2933       moreover
  2934       { fix i
  2935         have "simple_bochner_integrable M (\<lambda>y. s i (x, y))"
  2936         proof (rule simple_bochner_integrableI_bounded)
  2937           have "(\<lambda>y. s i (x, y)) ` space M \<subseteq> s i ` (space N \<times> space M)"
  2938             using x by auto
  2939           then show "simple_function M (\<lambda>y. s i (x, y))"
  2940             using simple_functionD(1)[OF s(1), of i] x
  2941             by (intro simple_function_borel_measurable)
  2942                (auto simp: space_pair_measure dest: finite_subset)
  2943           have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
  2944             using x s by (intro nn_integral_mono) auto
  2945           also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
  2946             using int_2f by (simp add: integrable_iff_bounded)
  2947           finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
  2948         qed
  2949         then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"
  2950           by (rule simple_bochner_integrable_eq_integral[symmetric]) }
  2951       ultimately have "(\<lambda>i. simple_bochner_integral M (\<lambda>y. s i (x, y))) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
  2952         by simp }
  2953     then
  2954     show "(\<lambda>i. f' i x) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
  2955       unfolding f'_def
  2956       by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
  2957   qed
  2958 qed
  2959 
  2960 lemma (in pair_sigma_finite) integrable_product_swap:
  2961   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2962   assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
  2963   shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
  2964 proof -
  2965   interpret Q: pair_sigma_finite M2 M1 ..
  2966   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  2967   show ?thesis unfolding *
  2968     by (rule integrable_distr[OF measurable_pair_swap'])
  2969        (simp add: distr_pair_swap[symmetric] assms)
  2970 qed
  2971 
  2972 lemma (in pair_sigma_finite) integrable_product_swap_iff:
  2973   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2974   shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
  2975 proof -
  2976   interpret Q: pair_sigma_finite M2 M1 ..
  2977   from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
  2978   show ?thesis by auto
  2979 qed
  2980 
  2981 lemma (in pair_sigma_finite) integral_product_swap:
  2982   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2983   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  2984   shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  2985 proof -
  2986   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  2987   show ?thesis unfolding *
  2988     by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
  2989 qed
  2990 
  2991 lemma (in pair_sigma_finite) Fubini_integrable:
  2992   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  2993   assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  2994     and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
  2995     and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  2996   shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
  2997 proof (rule integrableI_bounded)
  2998   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)"
  2999     by (simp add: M2.nn_integral_fst [symmetric])
  3000   also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
  3001     apply (intro nn_integral_cong_AE)
  3002     using integ2
  3003   proof eventually_elim
  3004     fix x assume "integrable M2 (\<lambda>y. f (x, y))"
  3005     then have f: "integrable M2 (\<lambda>y. norm (f (x, y)))"
  3006       by simp
  3007     then have "(\<integral>\<^sup>+y. ennreal (norm (f (x, y))) \<partial>M2) = ennreal (LINT y|M2. norm (f (x, y)))"
  3008       by (rule nn_integral_eq_integral) simp
  3009     also have "\<dots> = ennreal \<bar>LINT y|M2. norm (f (x, y))\<bar>"
  3010       using f by simp
  3011     finally show "(\<integral>\<^sup>+y. ennreal (norm (f (x, y))) \<partial>M2) = ennreal \<bar>LINT y|M2. norm (f (x, y))\<bar>" .
  3012   qed
  3013   also have "\<dots> < \<infinity>"
  3014     using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
  3015   finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
  3016 qed fact
  3017 
  3018 lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
  3019   assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
  3020   shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
  3021 proof -
  3022   from M2.emeasure_pair_measure_alt[OF A] finite
  3023   have "(\<integral>\<^sup>+ x. emeasure M2 (Pair x -` A) \<partial>M1) \<noteq> \<infinity>"
  3024     by simp
  3025   then have "AE x in M1. emeasure M2 (Pair x -` A) \<noteq> \<infinity>"
  3026     by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
  3027   moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> Pair x -` A = {y\<in>space M2. (x, y) \<in> A}"
  3028     using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
  3029   ultimately show ?thesis by (auto simp: less_top)
  3030 qed
  3031 
  3032 lemma (in pair_sigma_finite) AE_integrable_fst':
  3033   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  3034   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  3035   shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  3036 proof -
  3037   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))"
  3038     by (rule M2.nn_integral_fst) simp
  3039   also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) \<noteq> \<infinity>"
  3040     using f unfolding integrable_iff_bounded by simp
  3041   finally have "AE x in M1. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
  3042     by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
  3043        (auto simp: measurable_split_conv)
  3044   with AE_space show ?thesis
  3045     by eventually_elim
  3046        (auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top)
  3047 qed
  3048 
  3049 lemma (in pair_sigma_finite) integrable_fst':
  3050   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  3051   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  3052   shows "integrable M1 (\<lambda>x. \<integral>y. f (x, y) \<partial>M2)"
  3053   unfolding integrable_iff_bounded
  3054 proof
  3055   show "(\<lambda>x. \<integral> y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
  3056     by (rule M2.borel_measurable_lebesgue_integral) simp
  3057   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)"
  3058     using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ennreal)
  3059   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))"
  3060     by (rule M2.nn_integral_fst) simp
  3061   also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>"
  3062     using f unfolding integrable_iff_bounded by simp
  3063   finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
  3064 qed
  3065 
  3066 lemma (in pair_sigma_finite) integral_fst':
  3067   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  3068   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  3069   shows "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  3070 using f proof induct
  3071   case (base A c)
  3072   have A[measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" by fact
  3073 
  3074   have eq: "\<And>x y. x \<in> space M1 \<Longrightarrow> indicator A (x, y) = indicator {y\<in>space M2. (x, y) \<in> A} y"
  3075     using sets.sets_into_space[OF A] by (auto split: split_indicator simp: space_pair_measure)
  3076 
  3077   have int_A: "integrable (M1 \<Otimes>\<^sub>M M2) (indicator A :: _ \<Rightarrow> real)"
  3078     using base by (rule integrable_real_indicator)
  3079 
  3080   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)"
  3081   proof (intro integral_cong_AE, simp, simp)
  3082     from AE_integrable_fst'[OF int_A] AE_space
  3083     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"
  3084       by eventually_elim (simp add: eq integrable_indicator_iff)
  3085   qed
  3086   also have "\<dots> = measure (M1 \<Otimes>\<^sub>M M2) A *\<^sub>R c"
  3087   proof (subst integral_scaleR_left)
  3088     have "(\<integral>\<^sup>+x. ennreal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) =
  3089       (\<integral>\<^sup>+x. emeasure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1)"
  3090       using emeasure_pair_measure_finite[OF base]
  3091       by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ennreal_measure)
  3092     also have "\<dots> = emeasure (M1 \<Otimes>\<^sub>M M2) A"
  3093       using sets.sets_into_space[OF A]
  3094       by (subst M2.emeasure_pair_measure_alt)
  3095          (auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
  3096     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" .
  3097 
  3098     from base * show "integrable M1 (\<lambda>x. measure M2 {y \<in> space M2. (x, y) \<in> A})"
  3099       by (simp add: integrable_iff_bounded)
  3100     then have "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) =
  3101       (\<integral>\<^sup>+x. ennreal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1)"
  3102       by (rule nn_integral_eq_integral[symmetric]) simp
  3103     also note *
  3104     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"
  3105       using base by (simp add: emeasure_eq_ennreal_measure)
  3106   qed
  3107   also have "\<dots> = (\<integral> a. indicator A a *\<^sub>R c \<partial>(M1 \<Otimes>\<^sub>M M2))"
  3108     using base by simp
  3109   finally show ?case .
  3110 next
  3111   case (add f g)
  3112   then have [measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" "g \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  3113     by auto
  3114   have "(\<integral> x. \<integral> y. f (x, y) + g (x, y) \<partial>M2 \<partial>M1) =
  3115     (\<integral> x. (\<integral> y. f (x, y) \<partial>M2) + (\<integral> y. g (x, y) \<partial>M2) \<partial>M1)"
  3116     apply (rule integral_cong_AE)
  3117     apply simp_all
  3118     using AE_integrable_fst'[OF add(1)] AE_integrable_fst'[OF add(3)]
  3119     apply eventually_elim
  3120     apply simp
  3121     done
  3122   also have "\<dots> = (\<integral> x. f x \<partial>(M1 \<Otimes>\<^sub>M M2)) + (\<integral> x. g x \<partial>(M1 \<Otimes>\<^sub>M M2))"
  3123     using integrable_fst'[OF add(1)] integrable_fst'[OF add(3)] add(2,4) by simp
  3124   finally show ?case
  3125     using add by simp
  3126 next
  3127   case (lim f s)
  3128   then have [measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" "\<And>i. s i \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  3129     by auto
  3130 
  3131   show ?case
  3132   proof (rule LIMSEQ_unique)
  3133     show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) \<longlonglongrightarrow> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  3134     proof (rule integral_dominated_convergence)
  3135       show "integrable (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. 2 * norm (f x))"
  3136         using lim(5) by auto
  3137     qed (insert lim, auto)
  3138     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"
  3139     proof (rule integral_dominated_convergence)
  3140       have "AE x in M1. \<forall>i. integrable M2 (\<lambda>y. s i (x, y))"
  3141         unfolding AE_all_countable using AE_integrable_fst'[OF lim(1)] ..
  3142       with AE_space AE_integrable_fst'[OF lim(5)]
  3143       show "AE x in M1. (\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) \<longlonglongrightarrow> \<integral> y. f (x, y) \<partial>M2"
  3144       proof eventually_elim
  3145         fix x assume x: "x \<in> space M1" and
  3146           s: "\<forall>i. integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
  3147         show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) \<longlonglongrightarrow> \<integral> y. f (x, y) \<partial>M2"
  3148         proof (rule integral_dominated_convergence)
  3149           show "integrable M2 (\<lambda>y. 2 * norm (f (x, y)))"
  3150              using f by auto
  3151           show "AE xa in M2. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f (x, xa)"
  3152             using x lim(3) by (auto simp: space_pair_measure)
  3153           show "\<And>i. AE xa in M2. norm (s i (x, xa)) \<le> 2 * norm (f (x, xa))"
  3154             using x lim(4) by (auto simp: space_pair_measure)
  3155         qed (insert x, measurable)
  3156       qed
  3157       show "integrable M1 (\<lambda>x. (\<integral> y. 2 * norm (f (x, y)) \<partial>M2))"
  3158         by (intro integrable_mult_right integrable_norm integrable_fst' lim)
  3159       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)"
  3160         using AE_space AE_integrable_fst'[OF lim(1), of i] AE_integrable_fst'[OF lim(5)]
  3161       proof eventually_elim
  3162         fix x assume x: "x \<in> space M1"
  3163           and s: "integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
  3164         from s have "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral>\<^sup>+y. norm (s i (x, y)) \<partial>M2)"
  3165           by (rule integral_norm_bound_ennreal)
  3166         also have "\<dots> \<le> (\<integral>\<^sup>+y. 2 * norm (f (x, y)) \<partial>M2)"
  3167           using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
  3168         also have "\<dots> = (\<integral>y. 2 * norm (f (x, y)) \<partial>M2)"
  3169           using f by (intro nn_integral_eq_integral) auto
  3170         finally show "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
  3171           by simp
  3172       qed
  3173     qed simp_all
  3174     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"
  3175       using lim by simp
  3176   qed
  3177 qed
  3178 
  3179 lemma (in pair_sigma_finite)
  3180   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  3181   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  3182   shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
  3183     and integrable_fst: "integrable M1 (\<lambda>x. \<integral>y. f x y \<partial>M2)" (is "?INT")
  3184     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")
  3185   using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto
  3186 
  3187 lemma (in pair_sigma_finite)
  3188   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  3189   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  3190   shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
  3191     and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
  3192     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")
  3193 proof -
  3194   interpret Q: pair_sigma_finite M2 M1 ..
  3195   have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
  3196     using f unfolding integrable_product_swap_iff[symmetric] by simp
  3197   show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
  3198   show ?INT using Q.integrable_fst'[OF Q_int] by simp
  3199   show ?EQ using Q.integral_fst'[OF Q_int]
  3200     using integral_product_swap[of "case_prod f"] by simp
  3201 qed
  3202 
  3203 lemma (in pair_sigma_finite) Fubini_integral:
  3204   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
  3205   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  3206   shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
  3207   unfolding integral_snd[OF assms] integral_fst[OF assms] ..
  3208 
  3209 lemma (in product_sigma_finite) product_integral_singleton:
  3210   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  3211   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"
  3212   apply (subst distr_singleton[symmetric])
  3213   apply (subst integral_distr)
  3214   apply simp_all
  3215   done
  3216 
  3217 lemma (in product_sigma_finite) product_integral_fold:
  3218   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  3219   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  3220   and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
  3221   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)"
  3222 proof -
  3223   interpret I: finite_product_sigma_finite M I by standard fact
  3224   interpret J: finite_product_sigma_finite M J by standard fact
  3225   have "finite (I \<union> J)" using fin by auto
  3226   interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
  3227   interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
  3228   let ?M = "merge I J"
  3229   let ?f = "\<lambda>x. f (?M x)"
  3230   from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
  3231     by auto
  3232   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)"
  3233     using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
  3234   have f_int: "integrable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) ?f"
  3235     by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
  3236   show ?thesis
  3237     apply (subst distr_merge[symmetric, OF IJ fin])
  3238     apply (subst integral_distr[OF measurable_merge f_borel])
  3239     apply (subst P.integral_fst'[symmetric, OF f_int])
  3240     apply simp
  3241     done
  3242 qed
  3243 
  3244 lemma (in product_sigma_finite) product_integral_insert:
  3245   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  3246   assumes I: "finite I" "i \<notin> I"
  3247     and f: "integrable (Pi\<^sub>M (insert i I) M) f"
  3248   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)"
  3249 proof -
  3250   have "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = integral\<^sup>L (Pi\<^sub>M (I \<union> {i}) M) f"
  3251     by simp
  3252   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)"
  3253     using f I by (intro product_integral_fold) auto
  3254   also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^sub>M I M)"
  3255   proof (rule integral_cong[OF refl], subst product_integral_singleton[symmetric])
  3256     fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
  3257     have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
  3258       using f by auto
  3259     show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
  3260       using measurable_comp[OF measurable_component_update f_borel, OF x \<open>i \<notin> I\<close>]
  3261       unfolding comp_def .
  3262     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)"
  3263       by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
  3264   qed
  3265   finally show ?thesis .
  3266 qed
  3267 
  3268 lemma (in product_sigma_finite) product_integrable_prod:
  3269   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  3270   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  3271   shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
  3272 proof (unfold integrable_iff_bounded, intro conjI)
  3273   interpret finite_product_sigma_finite M I by standard fact
  3274 
  3275   show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
  3276     using assms by simp
  3277   have "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) =
  3278       (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ennreal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
  3279     by (simp add: prod_norm prod_ennreal)
  3280   also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ennreal (norm (f i x)) \<partial>M i)"
  3281     using assms by (intro product_nn_integral_prod) auto
  3282   also have "\<dots> < \<infinity>"
  3283     using integrable by (simp add: less_top[symmetric] ennreal_prod_eq_top integrable_iff_bounded)
  3284   finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
  3285 qed
  3286 
  3287 lemma (in product_sigma_finite) product_integral_prod:
  3288   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  3289   assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  3290   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))"
  3291 using assms proof induct
  3292   case empty
  3293   interpret finite_measure "Pi\<^sub>M {} M"
  3294     by rule (simp add: space_PiM)
  3295   show ?case by (simp add: space_PiM measure_def)
  3296 next
  3297   case (insert i I)
  3298   then have iI: "finite (insert i I)" by auto
  3299   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
  3300     integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
  3301     by (intro product_integrable_prod insert(4)) (auto intro: finite_subset)
  3302   interpret I: finite_product_sigma_finite M I by standard fact
  3303   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))"
  3304     using \<open>i \<notin> I\<close> by (auto intro!: prod.cong)
  3305   show ?case
  3306     unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
  3307     by (simp add: * insert prod subset_insertI)
  3308 qed
  3309 
  3310 lemma integrable_subalgebra:
  3311   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  3312   assumes borel: "f \<in> borel_measurable N"
  3313   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  3314   shows "integrable N f \<longleftrightarrow> integrable M f" (is ?P)
  3315 proof -
  3316   have "f \<in> borel_measurable M"
  3317     using assms by (auto simp: measurable_def)
  3318   with assms show ?thesis
  3319     using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
  3320 qed
  3321 
  3322 lemma integral_subalgebra:
  3323   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  3324   assumes borel: "f \<in> borel_measurable N"
  3325   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  3326   shows "integral\<^sup>L N f = integral\<^sup>L M f"
  3327 proof cases
  3328   assume "integrable N f"
  3329   then show ?thesis
  3330   proof induct
  3331     case base with assms show ?case by (auto simp: subset_eq measure_def)
  3332   next
  3333     case (add f g)
  3334     then have "(\<integral> a. f a + g a \<partial>N) = integral\<^sup>L M f + integral\<^sup>L M g"
  3335       by simp
  3336     also have "\<dots> = (\<integral> a. f a + g a \<partial>M)"
  3337       using add integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of g] by simp
  3338     finally show ?case .
  3339   next
  3340     case (lim f s)
  3341     then have M: "\<And>i. integrable M (s i)" "integrable M f"
  3342       using integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of "s i" for i] by simp_all
  3343     show ?case
  3344     proof (intro LIMSEQ_unique)
  3345       show "(\<lambda>i. integral\<^sup>L N (s i)) \<longlonglongrightarrow> integral\<^sup>L N f"
  3346         apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  3347         using lim
  3348         apply auto
  3349         done
  3350       show "(\<lambda>i. integral\<^sup>L N (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
  3351         unfolding lim
  3352         apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  3353         using lim M N(2)
  3354         apply auto
  3355         done
  3356     qed
  3357   qed
  3358 qed (simp add: not_integrable_integral_eq integrable_subalgebra[OF assms])
  3359 
  3360 hide_const (open) simple_bochner_integral
  3361 hide_const (open) simple_bochner_integrable
  3362 
  3363 end