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