src/HOL/Multivariate_Analysis/Bochner_Integration.thy
changeset 63627 6ddb43c6b711
parent 63626 44ce6b524ff3
child 63631 2edc8da89edc
child 63633 2accfb71e33b
     1.1 --- a/src/HOL/Multivariate_Analysis/Bochner_Integration.thy	Fri Aug 05 18:34:57 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,3066 +0,0 @@
     1.4 -(*  Title:      HOL/Probability/Bochner_Integration.thy
     1.5 -    Author:     Johannes Hölzl, TU München
     1.6 -*)
     1.7 -
     1.8 -section \<open>Bochner Integration for Vector-Valued Functions\<close>
     1.9 -
    1.10 -theory Bochner_Integration
    1.11 -  imports Finite_Product_Measure
    1.12 -begin
    1.13 -
    1.14 -text \<open>
    1.15 -
    1.16 -In the following development of the Bochner integral we use second countable topologies instead
    1.17 -of separable spaces. A second countable topology is also separable.
    1.18 -
    1.19 -\<close>
    1.20 -
    1.21 -lemma borel_measurable_implies_sequence_metric:
    1.22 -  fixes f :: "'a \<Rightarrow> 'b :: {metric_space, second_countable_topology}"
    1.23 -  assumes [measurable]: "f \<in> borel_measurable M"
    1.24 -  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>
    1.25 -    (\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)"
    1.26 -proof -
    1.27 -  obtain D :: "'b set" where "countable D" and D: "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
    1.28 -    by (erule countable_dense_setE)
    1.29 -
    1.30 -  define e where "e = from_nat_into D"
    1.31 -  { fix n x
    1.32 -    obtain d where "d \<in> D" and d: "d \<in> ball x (1 / Suc n)"
    1.33 -      using D[of "ball x (1 / Suc n)"] by auto
    1.34 -    from \<open>d \<in> D\<close> D[of UNIV] \<open>countable D\<close> obtain i where "d = e i"
    1.35 -      unfolding e_def by (auto dest: from_nat_into_surj)
    1.36 -    with d have "\<exists>i. dist x (e i) < 1 / Suc n"
    1.37 -      by auto }
    1.38 -  note e = this
    1.39 -
    1.40 -  define A where [abs_def]: "A m n =
    1.41 -    {x\<in>space M. dist (f x) (e n) < 1 / (Suc m) \<and> 1 / (Suc m) \<le> dist (f x) z}" for m n
    1.42 -  define B where [abs_def]: "B m = disjointed (A m)" for m
    1.43 -
    1.44 -  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
    1.45 -  define F where [abs_def]: "F N x =
    1.46 -    (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)
    1.47 -     then e (LEAST n. x \<in> B (m N x) n) else z)" for N x
    1.48 -
    1.49 -  have B_imp_A[intro, simp]: "\<And>x m n. x \<in> B m n \<Longrightarrow> x \<in> A m n"
    1.50 -    using disjointed_subset[of "A m" for m] unfolding B_def by auto
    1.51 -
    1.52 -  { fix m
    1.53 -    have "\<And>n. A m n \<in> sets M"
    1.54 -      by (auto simp: A_def)
    1.55 -    then have "\<And>n. B m n \<in> sets M"
    1.56 -      using sets.range_disjointed_sets[of "A m" M] by (auto simp: B_def) }
    1.57 -  note this[measurable]
    1.58 -
    1.59 -  { fix N i x assume "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)"
    1.60 -    then have "m N x \<in> {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}"
    1.61 -      unfolding m_def by (intro Max_in) auto
    1.62 -    then have "m N x \<le> N" "\<exists>n\<le>N. x \<in> B (m N x) n"
    1.63 -      by auto }
    1.64 -  note m = this
    1.65 -
    1.66 -  { fix j N i x assume "j \<le> N" "i \<le> N" "x \<in> B j i"
    1.67 -    then have "j \<le> m N x"
    1.68 -      unfolding m_def by (intro Max_ge) auto }
    1.69 -  note m_upper = this
    1.70 -
    1.71 -  show ?thesis
    1.72 -    unfolding simple_function_def
    1.73 -  proof (safe intro!: exI[of _ F])
    1.74 -    have [measurable]: "\<And>i. F i \<in> borel_measurable M"
    1.75 -      unfolding F_def m_def by measurable
    1.76 -    show "\<And>x i. F i -` {x} \<inter> space M \<in> sets M"
    1.77 -      by measurable
    1.78 -
    1.79 -    { fix i
    1.80 -      { fix n x assume "x \<in> B (m i x) n"
    1.81 -        then have "(LEAST n. x \<in> B (m i x) n) \<le> n"
    1.82 -          by (intro Least_le)
    1.83 -        also assume "n \<le> i"
    1.84 -        finally have "(LEAST n. x \<in> B (m i x) n) \<le> i" . }
    1.85 -      then have "F i ` space M \<subseteq> {z} \<union> e ` {.. i}"
    1.86 -        by (auto simp: F_def)
    1.87 -      then show "finite (F i ` space M)"
    1.88 -        by (rule finite_subset) auto }
    1.89 -
    1.90 -    { fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n"
    1.91 -      then have 1: "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)" by auto
    1.92 -      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
    1.93 -      moreover
    1.94 -      define L where "L = (LEAST n. x \<in> B (m N x) n)"
    1.95 -      have "dist (f x) (e L) < 1 / Suc (m N x)"
    1.96 -      proof -
    1.97 -        have "x \<in> B (m N x) L"
    1.98 -          using n(3) unfolding L_def by (rule LeastI)
    1.99 -        then have "x \<in> A (m N x) L"
   1.100 -          by auto
   1.101 -        then show ?thesis
   1.102 -          unfolding A_def by simp
   1.103 -      qed
   1.104 -      ultimately have "dist (f x) (F N x) < 1 / Suc (m N x)"
   1.105 -        by (auto simp add: F_def L_def) }
   1.106 -    note * = this
   1.107 -
   1.108 -    fix x assume "x \<in> space M"
   1.109 -    show "(\<lambda>i. F i x) \<longlonglongrightarrow> f x"
   1.110 -    proof cases
   1.111 -      assume "f x = z"
   1.112 -      then have "\<And>i n. x \<notin> A i n"
   1.113 -        unfolding A_def by auto
   1.114 -      then have "\<And>i. F i x = z"
   1.115 -        by (auto simp: F_def)
   1.116 -      then show ?thesis
   1.117 -        using \<open>f x = z\<close> by auto
   1.118 -    next
   1.119 -      assume "f x \<noteq> z"
   1.120 -
   1.121 -      show ?thesis
   1.122 -      proof (rule tendstoI)
   1.123 -        fix e :: real assume "0 < e"
   1.124 -        with \<open>f x \<noteq> z\<close> obtain n where "1 / Suc n < e" "1 / Suc n < dist (f x) z"
   1.125 -          by (metis dist_nz order_less_trans neq_iff nat_approx_posE)
   1.126 -        with \<open>x\<in>space M\<close> \<open>f x \<noteq> z\<close> have "x \<in> (\<Union>i. B n i)"
   1.127 -          unfolding A_def B_def UN_disjointed_eq using e by auto
   1.128 -        then obtain i where i: "x \<in> B n i" by auto
   1.129 -
   1.130 -        show "eventually (\<lambda>i. dist (F i x) (f x) < e) sequentially"
   1.131 -          using eventually_ge_at_top[of "max n i"]
   1.132 -        proof eventually_elim
   1.133 -          fix j assume j: "max n i \<le> j"
   1.134 -          with i have "dist (f x) (F j x) < 1 / Suc (m j x)"
   1.135 -            by (intro *[OF _ _ i]) auto
   1.136 -          also have "\<dots> \<le> 1 / Suc n"
   1.137 -            using j m_upper[OF _ _ i]
   1.138 -            by (auto simp: field_simps)
   1.139 -          also note \<open>1 / Suc n < e\<close>
   1.140 -          finally show "dist (F j x) (f x) < e"
   1.141 -            by (simp add: less_imp_le dist_commute)
   1.142 -        qed
   1.143 -      qed
   1.144 -    qed
   1.145 -    fix i
   1.146 -    { fix n m assume "x \<in> A n m"
   1.147 -      then have "dist (e m) (f x) + dist (f x) z \<le> 2 * dist (f x) z"
   1.148 -        unfolding A_def by (auto simp: dist_commute)
   1.149 -      also have "dist (e m) z \<le> dist (e m) (f x) + dist (f x) z"
   1.150 -        by (rule dist_triangle)
   1.151 -      finally (xtrans) have "dist (e m) z \<le> 2 * dist (f x) z" . }
   1.152 -    then show "dist (F i x) z \<le> 2 * dist (f x) z"
   1.153 -      unfolding F_def
   1.154 -      apply auto
   1.155 -      apply (rule LeastI2)
   1.156 -      apply auto
   1.157 -      done
   1.158 -  qed
   1.159 -qed
   1.160 -
   1.161 -lemma
   1.162 -  fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
   1.163 -  shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator (B x) (g x)) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
   1.164 -  and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator (B x) (g x) * f x) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
   1.165 -  unfolding indicator_def
   1.166 -  using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm)
   1.167 -
   1.168 -lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
   1.169 -  fixes P :: "('a \<Rightarrow> real) \<Rightarrow> bool"
   1.170 -  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
   1.171 -  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
   1.172 -  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)"
   1.173 -  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)"
   1.174 -  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"
   1.175 -  shows "P u"
   1.176 -proof -
   1.177 -  have "(\<lambda>x. ennreal (u x)) \<in> borel_measurable M" using u by auto
   1.178 -  from borel_measurable_implies_simple_function_sequence'[OF this]
   1.179 -  obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and
   1.180 -    sup: "\<And>x. (SUP i. U i x) = ennreal (u x)"
   1.181 -    by blast
   1.182 -
   1.183 -  define U' where [abs_def]: "U' i x = indicator (space M) x * enn2real (U i x)" for i x
   1.184 -  then have U'_sf[measurable]: "\<And>i. simple_function M (U' i)"
   1.185 -    using U by (auto intro!: simple_function_compose1[where g=enn2real])
   1.186 -
   1.187 -  show "P u"
   1.188 -  proof (rule seq)
   1.189 -    show U': "U' i \<in> borel_measurable M" "\<And>x. 0 \<le> U' i x" for i
   1.190 -      using U by (auto
   1.191 -          intro: borel_measurable_simple_function
   1.192 -          intro!: borel_measurable_enn2real borel_measurable_times
   1.193 -          simp: U'_def zero_le_mult_iff enn2real_nonneg)
   1.194 -    show "incseq U'"
   1.195 -      using U(2,3)
   1.196 -      by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)
   1.197 -
   1.198 -    fix x assume x: "x \<in> space M"
   1.199 -    have "(\<lambda>i. U i x) \<longlonglongrightarrow> (SUP i. U i x)"
   1.200 -      using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def)
   1.201 -    moreover have "(\<lambda>i. U i x) = (\<lambda>i. ennreal (U' i x))"
   1.202 -      using x U(3) by (auto simp: fun_eq_iff U'_def image_iff eq_commute)
   1.203 -    moreover have "(SUP i. U i x) = ennreal (u x)"
   1.204 -      using sup u(2) by (simp add: max_def)
   1.205 -    ultimately show "(\<lambda>i. U' i x) \<longlonglongrightarrow> u x"
   1.206 -      using u U' by simp
   1.207 -  next
   1.208 -    fix i
   1.209 -    have "U' i ` space M \<subseteq> enn2real ` (U i ` space M)" "finite (U i ` space M)"
   1.210 -      unfolding U'_def using U(1) by (auto dest: simple_functionD)
   1.211 -    then have fin: "finite (U' i ` space M)"
   1.212 -      by (metis finite_subset finite_imageI)
   1.213 -    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 {})"
   1.214 -      by auto
   1.215 -    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"
   1.216 -      by (simp add: U'_def fun_eq_iff)
   1.217 -    have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
   1.218 -      by (auto simp: U'_def enn2real_nonneg)
   1.219 -    with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
   1.220 -    proof induct
   1.221 -      case empty from set[of "{}"] show ?case
   1.222 -        by (simp add: indicator_def[abs_def])
   1.223 -    next
   1.224 -      case (insert x F)
   1.225 -      then show ?case
   1.226 -        by (auto intro!: add mult set setsum_nonneg split: split_indicator split_indicator_asm
   1.227 -                 simp del: setsum_mult_indicator simp: setsum_nonneg_eq_0_iff)
   1.228 -    qed
   1.229 -    with U' show "P (U' i)" by simp
   1.230 -  qed
   1.231 -qed
   1.232 -
   1.233 -lemma scaleR_cong_right:
   1.234 -  fixes x :: "'a :: real_vector"
   1.235 -  shows "(x \<noteq> 0 \<Longrightarrow> r = p) \<Longrightarrow> r *\<^sub>R x = p *\<^sub>R x"
   1.236 -  by (cases "x = 0") auto
   1.237 -
   1.238 -inductive simple_bochner_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" for M f where
   1.239 -  "simple_function M f \<Longrightarrow> emeasure M {y\<in>space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
   1.240 -    simple_bochner_integrable M f"
   1.241 -
   1.242 -lemma simple_bochner_integrable_compose2:
   1.243 -  assumes p_0: "p 0 0 = 0"
   1.244 -  shows "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integrable M g \<Longrightarrow>
   1.245 -    simple_bochner_integrable M (\<lambda>x. p (f x) (g x))"
   1.246 -proof (safe intro!: simple_bochner_integrable.intros elim!: simple_bochner_integrable.cases del: notI)
   1.247 -  assume sf: "simple_function M f" "simple_function M g"
   1.248 -  then show "simple_function M (\<lambda>x. p (f x) (g x))"
   1.249 -    by (rule simple_function_compose2)
   1.250 -
   1.251 -  from sf have [measurable]:
   1.252 -      "f \<in> measurable M (count_space UNIV)"
   1.253 -      "g \<in> measurable M (count_space UNIV)"
   1.254 -    by (auto intro: measurable_simple_function)
   1.255 -
   1.256 -  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>"
   1.257 -
   1.258 -  have "emeasure M {x\<in>space M. p (f x) (g x) \<noteq> 0} \<le>
   1.259 -      emeasure M ({x\<in>space M. f x \<noteq> 0} \<union> {x\<in>space M. g x \<noteq> 0})"
   1.260 -    by (intro emeasure_mono) (auto simp: p_0)
   1.261 -  also have "\<dots> \<le> emeasure M {x\<in>space M. f x \<noteq> 0} + emeasure M {x\<in>space M. g x \<noteq> 0}"
   1.262 -    by (intro emeasure_subadditive) auto
   1.263 -  finally show "emeasure M {y \<in> space M. p (f y) (g y) \<noteq> 0} \<noteq> \<infinity>"
   1.264 -    using fin by (auto simp: top_unique)
   1.265 -qed
   1.266 -
   1.267 -lemma simple_function_finite_support:
   1.268 -  assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" and nn: "\<And>x. 0 \<le> f x"
   1.269 -  shows "emeasure M {x\<in>space M. f x \<noteq> 0} \<noteq> \<infinity>"
   1.270 -proof cases
   1.271 -  from f have meas[measurable]: "f \<in> borel_measurable M"
   1.272 -    by (rule borel_measurable_simple_function)
   1.273 -
   1.274 -  assume non_empty: "\<exists>x\<in>space M. f x \<noteq> 0"
   1.275 -
   1.276 -  define m where "m = Min (f`space M - {0})"
   1.277 -  have "m \<in> f`space M - {0}"
   1.278 -    unfolding m_def using f non_empty by (intro Min_in) (auto simp: simple_function_def)
   1.279 -  then have m: "0 < m"
   1.280 -    using nn by (auto simp: less_le)
   1.281 -
   1.282 -  from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} =
   1.283 -    (\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
   1.284 -    using f by (intro nn_integral_cmult_indicator[symmetric]) auto
   1.285 -  also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
   1.286 -    using AE_space
   1.287 -  proof (intro nn_integral_mono_AE, eventually_elim)
   1.288 -    fix x assume "x \<in> space M"
   1.289 -    with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x"
   1.290 -      using f by (auto split: split_indicator simp: simple_function_def m_def)
   1.291 -  qed
   1.292 -  also note \<open>\<dots> < \<infinity>\<close>
   1.293 -  finally show ?thesis
   1.294 -    using m by (auto simp: ennreal_mult_less_top)
   1.295 -next
   1.296 -  assume "\<not> (\<exists>x\<in>space M. f x \<noteq> 0)"
   1.297 -  with nn have *: "{x\<in>space M. f x \<noteq> 0} = {}"
   1.298 -    by auto
   1.299 -  show ?thesis unfolding * by simp
   1.300 -qed
   1.301 -
   1.302 -lemma simple_bochner_integrableI_bounded:
   1.303 -  assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   1.304 -  shows "simple_bochner_integrable M f"
   1.305 -proof
   1.306 -  have "emeasure M {y \<in> space M. ennreal (norm (f y)) \<noteq> 0} \<noteq> \<infinity>"
   1.307 -  proof (rule simple_function_finite_support)
   1.308 -    show "simple_function M (\<lambda>x. ennreal (norm (f x)))"
   1.309 -      using f by (rule simple_function_compose1)
   1.310 -    show "(\<integral>\<^sup>+ y. ennreal (norm (f y)) \<partial>M) < \<infinity>" by fact
   1.311 -  qed simp
   1.312 -  then show "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" by simp
   1.313 -qed fact
   1.314 -
   1.315 -definition simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where
   1.316 -  "simple_bochner_integral M f = (\<Sum>y\<in>f`space M. measure M {x\<in>space M. f x = y} *\<^sub>R y)"
   1.317 -
   1.318 -lemma simple_bochner_integral_partition:
   1.319 -  assumes f: "simple_bochner_integrable M f" and g: "simple_function M g"
   1.320 -  assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y"
   1.321 -  assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)"
   1.322 -  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)"
   1.323 -    (is "_ = ?r")
   1.324 -proof -
   1.325 -  from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
   1.326 -    by (auto simp: simple_function_def elim: simple_bochner_integrable.cases)
   1.327 -
   1.328 -  from f have [measurable]: "f \<in> measurable M (count_space UNIV)"
   1.329 -    by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
   1.330 -
   1.331 -  from g have [measurable]: "g \<in> measurable M (count_space UNIV)"
   1.332 -    by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
   1.333 -
   1.334 -  { fix y assume "y \<in> space M"
   1.335 -    then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}"
   1.336 -      by (auto cong: sub simp: v[symmetric]) }
   1.337 -  note eq = this
   1.338 -
   1.339 -  have "simple_bochner_integral M f =
   1.340 -    (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M.
   1.341 -      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)"
   1.342 -    unfolding simple_bochner_integral_def
   1.343 -  proof (safe intro!: setsum.cong scaleR_cong_right)
   1.344 -    fix y assume y: "y \<in> space M" "f y \<noteq> 0"
   1.345 -    have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} =
   1.346 -        {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
   1.347 -      by auto
   1.348 -    have eq:"{x \<in> space M. f x = f y} =
   1.349 -        (\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i})"
   1.350 -      by (auto simp: eq_commute cong: sub rev_conj_cong)
   1.351 -    have "finite (g`space M)" by simp
   1.352 -    then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
   1.353 -      by (rule rev_finite_subset) auto
   1.354 -    moreover
   1.355 -    { fix x assume "x \<in> space M" "f x = f y"
   1.356 -      then have "x \<in> space M" "f x \<noteq> 0"
   1.357 -        using y by auto
   1.358 -      then have "emeasure M {y \<in> space M. g y = g x} \<le> emeasure M {y \<in> space M. f y \<noteq> 0}"
   1.359 -        by (auto intro!: emeasure_mono cong: sub)
   1.360 -      then have "emeasure M {xa \<in> space M. g xa = g x} < \<infinity>"
   1.361 -        using f by (auto simp: simple_bochner_integrable.simps less_top) }
   1.362 -    ultimately
   1.363 -    show "measure M {x \<in> space M. f x = f y} =
   1.364 -      (\<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)"
   1.365 -      apply (simp add: setsum.If_cases eq)
   1.366 -      apply (subst measure_finite_Union[symmetric])
   1.367 -      apply (auto simp: disjoint_family_on_def less_top)
   1.368 -      done
   1.369 -  qed
   1.370 -  also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M.
   1.371 -      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))"
   1.372 -    by (auto intro!: setsum.cong simp: scaleR_setsum_left)
   1.373 -  also have "\<dots> = ?r"
   1.374 -    by (subst setsum.commute)
   1.375 -       (auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq)
   1.376 -  finally show "simple_bochner_integral M f = ?r" .
   1.377 -qed
   1.378 -
   1.379 -lemma simple_bochner_integral_add:
   1.380 -  assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
   1.381 -  shows "simple_bochner_integral M (\<lambda>x. f x + g x) =
   1.382 -    simple_bochner_integral M f + simple_bochner_integral M g"
   1.383 -proof -
   1.384 -  from f g have "simple_bochner_integral M (\<lambda>x. f x + g x) =
   1.385 -    (\<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))"
   1.386 -    by (intro simple_bochner_integral_partition)
   1.387 -       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   1.388 -  moreover from f g have "simple_bochner_integral M f =
   1.389 -    (\<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)"
   1.390 -    by (intro simple_bochner_integral_partition)
   1.391 -       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   1.392 -  moreover from f g have "simple_bochner_integral M g =
   1.393 -    (\<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)"
   1.394 -    by (intro simple_bochner_integral_partition)
   1.395 -       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   1.396 -  ultimately show ?thesis
   1.397 -    by (simp add: setsum.distrib[symmetric] scaleR_add_right)
   1.398 -qed
   1.399 -
   1.400 -lemma (in linear) simple_bochner_integral_linear:
   1.401 -  assumes g: "simple_bochner_integrable M g"
   1.402 -  shows "simple_bochner_integral M (\<lambda>x. f (g x)) = f (simple_bochner_integral M g)"
   1.403 -proof -
   1.404 -  from g have "simple_bochner_integral M (\<lambda>x. f (g x)) =
   1.405 -    (\<Sum>y\<in>g ` space M. measure M {x \<in> space M. g x = y} *\<^sub>R f y)"
   1.406 -    by (intro simple_bochner_integral_partition)
   1.407 -       (auto simp: simple_bochner_integrable_compose2[where p="\<lambda>x y. f x"] zero
   1.408 -             elim: simple_bochner_integrable.cases)
   1.409 -  also have "\<dots> = f (simple_bochner_integral M g)"
   1.410 -    by (simp add: simple_bochner_integral_def setsum scaleR)
   1.411 -  finally show ?thesis .
   1.412 -qed
   1.413 -
   1.414 -lemma simple_bochner_integral_minus:
   1.415 -  assumes f: "simple_bochner_integrable M f"
   1.416 -  shows "simple_bochner_integral M (\<lambda>x. - f x) = - simple_bochner_integral M f"
   1.417 -proof -
   1.418 -  interpret linear uminus by unfold_locales auto
   1.419 -  from f show ?thesis
   1.420 -    by (rule simple_bochner_integral_linear)
   1.421 -qed
   1.422 -
   1.423 -lemma simple_bochner_integral_diff:
   1.424 -  assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
   1.425 -  shows "simple_bochner_integral M (\<lambda>x. f x - g x) =
   1.426 -    simple_bochner_integral M f - simple_bochner_integral M g"
   1.427 -  unfolding diff_conv_add_uminus using f g
   1.428 -  by (subst simple_bochner_integral_add)
   1.429 -     (auto simp: simple_bochner_integral_minus simple_bochner_integrable_compose2[where p="\<lambda>x y. - y"])
   1.430 -
   1.431 -lemma simple_bochner_integral_norm_bound:
   1.432 -  assumes f: "simple_bochner_integrable M f"
   1.433 -  shows "norm (simple_bochner_integral M f) \<le> simple_bochner_integral M (\<lambda>x. norm (f x))"
   1.434 -proof -
   1.435 -  have "norm (simple_bochner_integral M f) \<le>
   1.436 -    (\<Sum>y\<in>f ` space M. norm (measure M {x \<in> space M. f x = y} *\<^sub>R y))"
   1.437 -    unfolding simple_bochner_integral_def by (rule norm_setsum)
   1.438 -  also have "\<dots> = (\<Sum>y\<in>f ` space M. measure M {x \<in> space M. f x = y} *\<^sub>R norm y)"
   1.439 -    by simp
   1.440 -  also have "\<dots> = simple_bochner_integral M (\<lambda>x. norm (f x))"
   1.441 -    using f
   1.442 -    by (intro simple_bochner_integral_partition[symmetric])
   1.443 -       (auto intro: f simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
   1.444 -  finally show ?thesis .
   1.445 -qed
   1.446 -
   1.447 -lemma simple_bochner_integral_nonneg[simp]:
   1.448 -  fixes f :: "'a \<Rightarrow> real"
   1.449 -  shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> 0 \<le> simple_bochner_integral M f"
   1.450 -  by (simp add: setsum_nonneg simple_bochner_integral_def)
   1.451 -
   1.452 -lemma simple_bochner_integral_eq_nn_integral:
   1.453 -  assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
   1.454 -  shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)"
   1.455 -proof -
   1.456 -  { fix x y z have "(x \<noteq> 0 \<Longrightarrow> y = z) \<Longrightarrow> ennreal x * y = ennreal x * z"
   1.457 -      by (cases "x = 0") (auto simp: zero_ennreal_def[symmetric]) }
   1.458 -  note ennreal_cong_mult = this
   1.459 -
   1.460 -  have [measurable]: "f \<in> borel_measurable M"
   1.461 -    using f(1) by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.462 -
   1.463 -  { fix y assume y: "y \<in> space M" "f y \<noteq> 0"
   1.464 -    have "ennreal (measure M {x \<in> space M. f x = f y}) = emeasure M {x \<in> space M. f x = f y}"
   1.465 -    proof (rule emeasure_eq_ennreal_measure[symmetric])
   1.466 -      have "emeasure M {x \<in> space M. f x = f y} \<le> emeasure M {x \<in> space M. f x \<noteq> 0}"
   1.467 -        using y by (intro emeasure_mono) auto
   1.468 -      with f show "emeasure M {x \<in> space M. f x = f y} \<noteq> top"
   1.469 -        by (auto simp: simple_bochner_integrable.simps top_unique)
   1.470 -    qed
   1.471 -    moreover have "{x \<in> space M. f x = f y} = (\<lambda>x. ennreal (f x)) -` {ennreal (f y)} \<inter> space M"
   1.472 -      using f by auto
   1.473 -    ultimately have "ennreal (measure M {x \<in> space M. f x = f y}) =
   1.474 -          emeasure M ((\<lambda>x. ennreal (f x)) -` {ennreal (f y)} \<inter> space M)" by simp }
   1.475 -  with f have "simple_bochner_integral M f = (\<integral>\<^sup>Sx. f x \<partial>M)"
   1.476 -    unfolding simple_integral_def
   1.477 -    by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ennreal (f x)" and v=enn2real])
   1.478 -       (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
   1.479 -             intro!: setsum.cong ennreal_cong_mult
   1.480 -             simp: setsum_ennreal[symmetric] ac_simps ennreal_mult
   1.481 -             simp del: setsum_ennreal)
   1.482 -  also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
   1.483 -    using f
   1.484 -    by (intro nn_integral_eq_simple_integral[symmetric])
   1.485 -       (auto simp: simple_function_compose1 simple_bochner_integrable.simps)
   1.486 -  finally show ?thesis .
   1.487 -qed
   1.488 -
   1.489 -lemma simple_bochner_integral_bounded:
   1.490 -  fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector, second_countable_topology}"
   1.491 -  assumes f[measurable]: "f \<in> borel_measurable M"
   1.492 -  assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t"
   1.493 -  shows "ennreal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) \<le>
   1.494 -    (\<integral>\<^sup>+ x. norm (f x - s x) \<partial>M) + (\<integral>\<^sup>+ x. norm (f x - t x) \<partial>M)"
   1.495 -    (is "ennreal (norm (?s - ?t)) \<le> ?S + ?T")
   1.496 -proof -
   1.497 -  have [measurable]: "s \<in> borel_measurable M" "t \<in> borel_measurable M"
   1.498 -    using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.499 -
   1.500 -  have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))"
   1.501 -    using s t by (subst simple_bochner_integral_diff) auto
   1.502 -  also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))"
   1.503 -    using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t
   1.504 -    by (auto intro!: simple_bochner_integral_norm_bound)
   1.505 -  also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
   1.506 -    using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
   1.507 -    by (auto intro!: simple_bochner_integral_eq_nn_integral)
   1.508 -  also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)"
   1.509 -    by (auto intro!: nn_integral_mono simp: ennreal_plus[symmetric] simp del: ennreal_plus)
   1.510 -       (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
   1.511 -              norm_minus_commute norm_triangle_ineq4 order_refl)
   1.512 -  also have "\<dots> = ?S + ?T"
   1.513 -   by (rule nn_integral_add) auto
   1.514 -  finally show ?thesis .
   1.515 -qed
   1.516 -
   1.517 -inductive has_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::{real_normed_vector, second_countable_topology} \<Rightarrow> bool"
   1.518 -  for M f x where
   1.519 -  "f \<in> borel_measurable M \<Longrightarrow>
   1.520 -    (\<And>i. simple_bochner_integrable M (s i)) \<Longrightarrow>
   1.521 -    (\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0 \<Longrightarrow>
   1.522 -    (\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x \<Longrightarrow>
   1.523 -    has_bochner_integral M f x"
   1.524 -
   1.525 -lemma has_bochner_integral_cong:
   1.526 -  assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
   1.527 -  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
   1.528 -  unfolding has_bochner_integral.simps assms(1,3)
   1.529 -  using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
   1.530 -
   1.531 -lemma has_bochner_integral_cong_AE:
   1.532 -  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
   1.533 -    has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
   1.534 -  unfolding has_bochner_integral.simps
   1.535 -  by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x \<longlonglongrightarrow> 0"]
   1.536 -            nn_integral_cong_AE)
   1.537 -     auto
   1.538 -
   1.539 -lemma borel_measurable_has_bochner_integral:
   1.540 -  "has_bochner_integral M f x \<Longrightarrow> f \<in> borel_measurable M"
   1.541 -  by (rule has_bochner_integral.cases)
   1.542 -
   1.543 -lemma borel_measurable_has_bochner_integral'[measurable_dest]:
   1.544 -  "has_bochner_integral M f x \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   1.545 -  using borel_measurable_has_bochner_integral[measurable] by measurable
   1.546 -
   1.547 -lemma has_bochner_integral_simple_bochner_integrable:
   1.548 -  "simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)"
   1.549 -  by (rule has_bochner_integral.intros[where s="\<lambda>_. f"])
   1.550 -     (auto intro: borel_measurable_simple_function
   1.551 -           elim: simple_bochner_integrable.cases
   1.552 -           simp: zero_ennreal_def[symmetric])
   1.553 -
   1.554 -lemma has_bochner_integral_real_indicator:
   1.555 -  assumes [measurable]: "A \<in> sets M" and A: "emeasure M A < \<infinity>"
   1.556 -  shows "has_bochner_integral M (indicator A) (measure M A)"
   1.557 -proof -
   1.558 -  have sbi: "simple_bochner_integrable M (indicator A::'a \<Rightarrow> real)"
   1.559 -  proof
   1.560 -    have "{y \<in> space M. (indicator A y::real) \<noteq> 0} = A"
   1.561 -      using sets.sets_into_space[OF \<open>A\<in>sets M\<close>] by (auto split: split_indicator)
   1.562 -    then show "emeasure M {y \<in> space M. (indicator A y::real) \<noteq> 0} \<noteq> \<infinity>"
   1.563 -      using A by auto
   1.564 -  qed (rule simple_function_indicator assms)+
   1.565 -  moreover have "simple_bochner_integral M (indicator A) = measure M A"
   1.566 -    using simple_bochner_integral_eq_nn_integral[OF sbi] A
   1.567 -    by (simp add: ennreal_indicator emeasure_eq_ennreal_measure)
   1.568 -  ultimately show ?thesis
   1.569 -    by (metis has_bochner_integral_simple_bochner_integrable)
   1.570 -qed
   1.571 -
   1.572 -lemma has_bochner_integral_add[intro]:
   1.573 -  "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
   1.574 -    has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
   1.575 -proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   1.576 -  fix sf sg
   1.577 -  assume f_sf: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - sf i x) \<partial>M) \<longlonglongrightarrow> 0"
   1.578 -  assume g_sg: "(\<lambda>i. \<integral>\<^sup>+ x. norm (g x - sg i x) \<partial>M) \<longlonglongrightarrow> 0"
   1.579 -
   1.580 -  assume sf: "\<forall>i. simple_bochner_integrable M (sf i)"
   1.581 -    and sg: "\<forall>i. simple_bochner_integrable M (sg i)"
   1.582 -  then have [measurable]: "\<And>i. sf i \<in> borel_measurable M" "\<And>i. sg i \<in> borel_measurable M"
   1.583 -    by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.584 -  assume [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.585 -
   1.586 -  show "\<And>i. simple_bochner_integrable M (\<lambda>x. sf i x + sg i x)"
   1.587 -    using sf sg by (simp add: simple_bochner_integrable_compose2)
   1.588 -
   1.589 -  show "(\<lambda>i. \<integral>\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \<partial>M) \<longlonglongrightarrow> 0"
   1.590 -    (is "?f \<longlonglongrightarrow> 0")
   1.591 -  proof (rule tendsto_sandwich)
   1.592 -    show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) \<longlonglongrightarrow> 0"
   1.593 -      by auto
   1.594 -    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"
   1.595 -      (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
   1.596 -    proof (intro always_eventually allI)
   1.597 -      fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) \<partial>M)"
   1.598 -        by (auto intro!: nn_integral_mono norm_diff_triangle_ineq
   1.599 -                 simp del: ennreal_plus simp add: ennreal_plus[symmetric])
   1.600 -      also have "\<dots> = ?g i"
   1.601 -        by (intro nn_integral_add) auto
   1.602 -      finally show "?f i \<le> ?g i" .
   1.603 -    qed
   1.604 -    show "?g \<longlonglongrightarrow> 0"
   1.605 -      using tendsto_add[OF f_sf g_sg] by simp
   1.606 -  qed
   1.607 -qed (auto simp: simple_bochner_integral_add tendsto_add)
   1.608 -
   1.609 -lemma has_bochner_integral_bounded_linear:
   1.610 -  assumes "bounded_linear T"
   1.611 -  shows "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M (\<lambda>x. T (f x)) (T x)"
   1.612 -proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   1.613 -  interpret T: bounded_linear T by fact
   1.614 -  have [measurable]: "T \<in> borel_measurable borel"
   1.615 -    by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id)
   1.616 -  assume [measurable]: "f \<in> borel_measurable M"
   1.617 -  then show "(\<lambda>x. T (f x)) \<in> borel_measurable M"
   1.618 -    by auto
   1.619 -
   1.620 -  fix s assume f_s: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0"
   1.621 -  assume s: "\<forall>i. simple_bochner_integrable M (s i)"
   1.622 -  then show "\<And>i. simple_bochner_integrable M (\<lambda>x. T (s i x))"
   1.623 -    by (auto intro: simple_bochner_integrable_compose2 T.zero)
   1.624 -
   1.625 -  have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   1.626 -    using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.627 -
   1.628 -  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"
   1.629 -    using T.pos_bounded by (auto simp: T.diff[symmetric])
   1.630 -
   1.631 -  show "(\<lambda>i. \<integral>\<^sup>+ x. norm (T (f x) - T (s i x)) \<partial>M) \<longlonglongrightarrow> 0"
   1.632 -    (is "?f \<longlonglongrightarrow> 0")
   1.633 -  proof (rule tendsto_sandwich)
   1.634 -    show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) \<longlonglongrightarrow> 0"
   1.635 -      by auto
   1.636 -
   1.637 -    show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
   1.638 -      (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
   1.639 -    proof (intro always_eventually allI)
   1.640 -      fix i have "?f i \<le> (\<integral>\<^sup>+ x. ennreal K * norm (f x - s i x) \<partial>M)"
   1.641 -        using K by (intro nn_integral_mono) (auto simp: ac_simps ennreal_mult[symmetric])
   1.642 -      also have "\<dots> = ?g i"
   1.643 -        using K by (intro nn_integral_cmult) auto
   1.644 -      finally show "?f i \<le> ?g i" .
   1.645 -    qed
   1.646 -    show "?g \<longlonglongrightarrow> 0"
   1.647 -      using ennreal_tendsto_cmult[OF _ f_s] by simp
   1.648 -  qed
   1.649 -
   1.650 -  assume "(\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x"
   1.651 -  with s show "(\<lambda>i. simple_bochner_integral M (\<lambda>x. T (s i x))) \<longlonglongrightarrow> T x"
   1.652 -    by (auto intro!: T.tendsto simp: T.simple_bochner_integral_linear)
   1.653 -qed
   1.654 -
   1.655 -lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\<lambda>x. 0) 0"
   1.656 -  by (auto intro!: has_bochner_integral.intros[where s="\<lambda>_ _. 0"]
   1.657 -           simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps
   1.658 -                 simple_bochner_integral_def image_constant_conv)
   1.659 -
   1.660 -lemma has_bochner_integral_scaleR_left[intro]:
   1.661 -  "(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)"
   1.662 -  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left])
   1.663 -
   1.664 -lemma has_bochner_integral_scaleR_right[intro]:
   1.665 -  "(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)"
   1.666 -  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right])
   1.667 -
   1.668 -lemma has_bochner_integral_mult_left[intro]:
   1.669 -  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.670 -  shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x * c) (x * c)"
   1.671 -  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left])
   1.672 -
   1.673 -lemma has_bochner_integral_mult_right[intro]:
   1.674 -  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.675 -  shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c * f x) (c * x)"
   1.676 -  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right])
   1.677 -
   1.678 -lemmas has_bochner_integral_divide =
   1.679 -  has_bochner_integral_bounded_linear[OF bounded_linear_divide]
   1.680 -
   1.681 -lemma has_bochner_integral_divide_zero[intro]:
   1.682 -  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
   1.683 -  shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)"
   1.684 -  using has_bochner_integral_divide by (cases "c = 0") auto
   1.685 -
   1.686 -lemma has_bochner_integral_inner_left[intro]:
   1.687 -  "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)"
   1.688 -  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left])
   1.689 -
   1.690 -lemma has_bochner_integral_inner_right[intro]:
   1.691 -  "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c \<bullet> f x) (c \<bullet> x)"
   1.692 -  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right])
   1.693 -
   1.694 -lemmas has_bochner_integral_minus =
   1.695 -  has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
   1.696 -lemmas has_bochner_integral_Re =
   1.697 -  has_bochner_integral_bounded_linear[OF bounded_linear_Re]
   1.698 -lemmas has_bochner_integral_Im =
   1.699 -  has_bochner_integral_bounded_linear[OF bounded_linear_Im]
   1.700 -lemmas has_bochner_integral_cnj =
   1.701 -  has_bochner_integral_bounded_linear[OF bounded_linear_cnj]
   1.702 -lemmas has_bochner_integral_of_real =
   1.703 -  has_bochner_integral_bounded_linear[OF bounded_linear_of_real]
   1.704 -lemmas has_bochner_integral_fst =
   1.705 -  has_bochner_integral_bounded_linear[OF bounded_linear_fst]
   1.706 -lemmas has_bochner_integral_snd =
   1.707 -  has_bochner_integral_bounded_linear[OF bounded_linear_snd]
   1.708 -
   1.709 -lemma has_bochner_integral_indicator:
   1.710 -  "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.711 -    has_bochner_integral M (\<lambda>x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)"
   1.712 -  by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator)
   1.713 -
   1.714 -lemma has_bochner_integral_diff:
   1.715 -  "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
   1.716 -    has_bochner_integral M (\<lambda>x. f x - g x) (x - y)"
   1.717 -  unfolding diff_conv_add_uminus
   1.718 -  by (intro has_bochner_integral_add has_bochner_integral_minus)
   1.719 -
   1.720 -lemma has_bochner_integral_setsum:
   1.721 -  "(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow>
   1.722 -    has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
   1.723 -  by (induct I rule: infinite_finite_induct) auto
   1.724 -
   1.725 -lemma has_bochner_integral_implies_finite_norm:
   1.726 -  "has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   1.727 -proof (elim has_bochner_integral.cases)
   1.728 -  fix s v
   1.729 -  assume [measurable]: "f \<in> borel_measurable M" and s: "\<And>i. simple_bochner_integrable M (s i)" and
   1.730 -    lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
   1.731 -  from order_tendstoD[OF lim_0, of "\<infinity>"]
   1.732 -  obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) < \<infinity>"
   1.733 -    by (auto simp: eventually_sequentially)
   1.734 -
   1.735 -  have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   1.736 -    using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.737 -
   1.738 -  define m where "m = (if space M = {} then 0 else Max ((\<lambda>x. norm (s i x))`space M))"
   1.739 -  have "finite (s i ` space M)"
   1.740 -    using s by (auto simp: simple_function_def simple_bochner_integrable.simps)
   1.741 -  then have "finite (norm ` s i ` space M)"
   1.742 -    by (rule finite_imageI)
   1.743 -  then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m"
   1.744 -    by (auto simp: m_def image_comp comp_def Max_ge_iff)
   1.745 -  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)"
   1.746 -    by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
   1.747 -  also have "\<dots> < \<infinity>"
   1.748 -    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)
   1.749 -  finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
   1.750 -
   1.751 -  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)"
   1.752 -    by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
   1.753 -       (metis add.commute norm_triangle_sub)
   1.754 -  also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
   1.755 -    by (rule nn_integral_add) auto
   1.756 -  also have "\<dots> < \<infinity>"
   1.757 -    using s_fin f_s_fin by auto
   1.758 -  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
   1.759 -qed
   1.760 -
   1.761 -lemma has_bochner_integral_norm_bound:
   1.762 -  assumes i: "has_bochner_integral M f x"
   1.763 -  shows "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   1.764 -using assms proof
   1.765 -  fix s assume
   1.766 -    x: "(\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x" (is "?s \<longlonglongrightarrow> x") and
   1.767 -    s[simp]: "\<And>i. simple_bochner_integrable M (s i)" and
   1.768 -    lim: "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0" and
   1.769 -    f[measurable]: "f \<in> borel_measurable M"
   1.770 -
   1.771 -  have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   1.772 -    using s by (auto simp: simple_bochner_integrable.simps intro: borel_measurable_simple_function)
   1.773 -
   1.774 -  show "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   1.775 -  proof (rule LIMSEQ_le)
   1.776 -    show "(\<lambda>i. ennreal (norm (?s i))) \<longlonglongrightarrow> norm x"
   1.777 -      using x by (auto simp: tendsto_ennreal_iff intro: tendsto_intros)
   1.778 -    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)"
   1.779 -      (is "\<exists>N. \<forall>n\<ge>N. _ \<le> ?t n")
   1.780 -    proof (intro exI allI impI)
   1.781 -      fix n
   1.782 -      have "ennreal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))"
   1.783 -        by (auto intro!: simple_bochner_integral_norm_bound)
   1.784 -      also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)"
   1.785 -        by (intro simple_bochner_integral_eq_nn_integral)
   1.786 -           (auto intro: s simple_bochner_integrable_compose2)
   1.787 -      also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s n x)) + norm (f x) \<partial>M)"
   1.788 -        by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
   1.789 -           (metis add.commute norm_minus_commute norm_triangle_sub)
   1.790 -      also have "\<dots> = ?t n"
   1.791 -        by (rule nn_integral_add) auto
   1.792 -      finally show "norm (?s n) \<le> ?t n" .
   1.793 -    qed
   1.794 -    have "?t \<longlonglongrightarrow> 0 + (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
   1.795 -      using has_bochner_integral_implies_finite_norm[OF i]
   1.796 -      by (intro tendsto_add tendsto_const lim)
   1.797 -    then show "?t \<longlonglongrightarrow> \<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M"
   1.798 -      by simp
   1.799 -  qed
   1.800 -qed
   1.801 -
   1.802 -lemma has_bochner_integral_eq:
   1.803 -  "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M f y \<Longrightarrow> x = y"
   1.804 -proof (elim has_bochner_integral.cases)
   1.805 -  assume f[measurable]: "f \<in> borel_measurable M"
   1.806 -
   1.807 -  fix s t
   1.808 -  assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?S \<longlonglongrightarrow> 0")
   1.809 -  assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - t i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?T \<longlonglongrightarrow> 0")
   1.810 -  assume s: "\<And>i. simple_bochner_integrable M (s i)"
   1.811 -  assume t: "\<And>i. simple_bochner_integrable M (t i)"
   1.812 -
   1.813 -  have [measurable]: "\<And>i. s i \<in> borel_measurable M" "\<And>i. t i \<in> borel_measurable M"
   1.814 -    using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.815 -
   1.816 -  let ?s = "\<lambda>i. simple_bochner_integral M (s i)"
   1.817 -  let ?t = "\<lambda>i. simple_bochner_integral M (t i)"
   1.818 -  assume "?s \<longlonglongrightarrow> x" "?t \<longlonglongrightarrow> y"
   1.819 -  then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> norm (x - y)"
   1.820 -    by (intro tendsto_intros)
   1.821 -  moreover
   1.822 -  have "(\<lambda>i. ennreal (norm (?s i - ?t i))) \<longlonglongrightarrow> ennreal 0"
   1.823 -  proof (rule tendsto_sandwich)
   1.824 -    show "eventually (\<lambda>i. 0 \<le> ennreal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) \<longlonglongrightarrow> ennreal 0"
   1.825 -      by auto
   1.826 -
   1.827 -    show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
   1.828 -      by (intro always_eventually allI simple_bochner_integral_bounded s t f)
   1.829 -    show "(\<lambda>i. ?S i + ?T i) \<longlonglongrightarrow> ennreal 0"
   1.830 -      using tendsto_add[OF \<open>?S \<longlonglongrightarrow> 0\<close> \<open>?T \<longlonglongrightarrow> 0\<close>] by simp
   1.831 -  qed
   1.832 -  then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> 0"
   1.833 -    by (simp add: ennreal_0[symmetric] del: ennreal_0)
   1.834 -  ultimately have "norm (x - y) = 0"
   1.835 -    by (rule LIMSEQ_unique)
   1.836 -  then show "x = y" by simp
   1.837 -qed
   1.838 -
   1.839 -lemma has_bochner_integralI_AE:
   1.840 -  assumes f: "has_bochner_integral M f x"
   1.841 -    and g: "g \<in> borel_measurable M"
   1.842 -    and ae: "AE x in M. f x = g x"
   1.843 -  shows "has_bochner_integral M g x"
   1.844 -  using f
   1.845 -proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   1.846 -  fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
   1.847 -  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)"
   1.848 -    using ae
   1.849 -    by (intro ext nn_integral_cong_AE, eventually_elim) simp
   1.850 -  finally show "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (g x - s i x)) \<partial>M) \<longlonglongrightarrow> 0" .
   1.851 -qed (auto intro: g)
   1.852 -
   1.853 -lemma has_bochner_integral_eq_AE:
   1.854 -  assumes f: "has_bochner_integral M f x"
   1.855 -    and g: "has_bochner_integral M g y"
   1.856 -    and ae: "AE x in M. f x = g x"
   1.857 -  shows "x = y"
   1.858 -proof -
   1.859 -  from assms have "has_bochner_integral M g x"
   1.860 -    by (auto intro: has_bochner_integralI_AE)
   1.861 -  from this g show "x = y"
   1.862 -    by (rule has_bochner_integral_eq)
   1.863 -qed
   1.864 -
   1.865 -lemma simple_bochner_integrable_restrict_space:
   1.866 -  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   1.867 -  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   1.868 -  shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
   1.869 -    simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   1.870 -  by (simp add: simple_bochner_integrable.simps space_restrict_space
   1.871 -    simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
   1.872 -    indicator_eq_0_iff conj_ac)
   1.873 -
   1.874 -lemma simple_bochner_integral_restrict_space:
   1.875 -  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   1.876 -  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   1.877 -  assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"
   1.878 -  shows "simple_bochner_integral (restrict_space M \<Omega>) f =
   1.879 -    simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   1.880 -proof -
   1.881 -  have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x)`space M)"
   1.882 -    using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
   1.883 -    by (simp add: simple_bochner_integrable.simps simple_function_def)
   1.884 -  then show ?thesis
   1.885 -    by (auto simp: space_restrict_space measure_restrict_space[OF \<Omega>(1)] le_infI2
   1.886 -                   simple_bochner_integral_def Collect_restrict
   1.887 -             split: split_indicator split_indicator_asm
   1.888 -             intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure])
   1.889 -qed
   1.890 -
   1.891 -context
   1.892 -  notes [[inductive_internals]]
   1.893 -begin
   1.894 -
   1.895 -inductive integrable for M f where
   1.896 -  "has_bochner_integral M f x \<Longrightarrow> integrable M f"
   1.897 -
   1.898 -end
   1.899 -
   1.900 -definition lebesgue_integral ("integral\<^sup>L") where
   1.901 -  "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)"
   1.902 -
   1.903 -syntax
   1.904 -  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral>((2 _./ _)/ \<partial>_)" [60,61] 110)
   1.905 -
   1.906 -translations
   1.907 -  "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
   1.908 -
   1.909 -syntax
   1.910 -  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
   1.911 -
   1.912 -translations
   1.913 -  "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
   1.914 -
   1.915 -lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
   1.916 -  by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
   1.917 -
   1.918 -lemma has_bochner_integral_integrable:
   1.919 -  "integrable M f \<Longrightarrow> has_bochner_integral M f (integral\<^sup>L M f)"
   1.920 -  by (auto simp: has_bochner_integral_integral_eq integrable.simps)
   1.921 -
   1.922 -lemma has_bochner_integral_iff:
   1.923 -  "has_bochner_integral M f x \<longleftrightarrow> integrable M f \<and> integral\<^sup>L M f = x"
   1.924 -  by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros)
   1.925 -
   1.926 -lemma simple_bochner_integrable_eq_integral:
   1.927 -  "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integral M f = integral\<^sup>L M f"
   1.928 -  using has_bochner_integral_simple_bochner_integrable[of M f]
   1.929 -  by (simp add: has_bochner_integral_integral_eq)
   1.930 -
   1.931 -lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = 0"
   1.932 -  unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])
   1.933 -
   1.934 -lemma integral_eq_cases:
   1.935 -  "integrable M f \<longleftrightarrow> integrable N g \<Longrightarrow>
   1.936 -    (integrable M f \<Longrightarrow> integrable N g \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g) \<Longrightarrow>
   1.937 -    integral\<^sup>L M f = integral\<^sup>L N g"
   1.938 -  by (metis not_integrable_integral_eq)
   1.939 -
   1.940 -lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
   1.941 -  by (auto elim: integrable.cases has_bochner_integral.cases)
   1.942 -
   1.943 -lemma borel_measurable_integrable'[measurable_dest]:
   1.944 -  "integrable M f \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   1.945 -  using borel_measurable_integrable[measurable] by measurable
   1.946 -
   1.947 -lemma integrable_cong:
   1.948 -  "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
   1.949 -  by (simp cong: has_bochner_integral_cong add: integrable.simps)
   1.950 -
   1.951 -lemma integrable_cong_AE:
   1.952 -  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   1.953 -    integrable M f \<longleftrightarrow> integrable M g"
   1.954 -  unfolding integrable.simps
   1.955 -  by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)
   1.956 -
   1.957 -lemma integral_cong:
   1.958 -  "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"
   1.959 -  by (simp cong: has_bochner_integral_cong cong del: if_weak_cong add: lebesgue_integral_def)
   1.960 -
   1.961 -lemma integral_cong_AE:
   1.962 -  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   1.963 -    integral\<^sup>L M f = integral\<^sup>L M g"
   1.964 -  unfolding lebesgue_integral_def
   1.965 -  by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)
   1.966 -
   1.967 -lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
   1.968 -  by (auto simp: integrable.simps)
   1.969 -
   1.970 -lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
   1.971 -  by (metis has_bochner_integral_zero integrable.simps)
   1.972 -
   1.973 -lemma integrable_setsum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)"
   1.974 -  by (metis has_bochner_integral_setsum integrable.simps)
   1.975 -
   1.976 -lemma integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.977 -  integrable M (\<lambda>x. indicator A x *\<^sub>R c)"
   1.978 -  by (metis has_bochner_integral_indicator integrable.simps)
   1.979 -
   1.980 -lemma integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.981 -  integrable M (indicator A :: 'a \<Rightarrow> real)"
   1.982 -  by (metis has_bochner_integral_real_indicator integrable.simps)
   1.983 -
   1.984 -lemma integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x - g x)"
   1.985 -  by (auto simp: integrable.simps intro: has_bochner_integral_diff)
   1.986 -
   1.987 -lemma integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))"
   1.988 -  by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)
   1.989 -
   1.990 -lemma integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)"
   1.991 -  unfolding integrable.simps by fastforce
   1.992 -
   1.993 -lemma integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)"
   1.994 -  unfolding integrable.simps by fastforce
   1.995 -
   1.996 -lemma integrable_mult_left[simp, intro]:
   1.997 -  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.998 -  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x * c)"
   1.999 -  unfolding integrable.simps by fastforce
  1.1000 -
  1.1001 -lemma integrable_mult_right[simp, intro]:
  1.1002 -  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1.1003 -  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)"
  1.1004 -  unfolding integrable.simps by fastforce
  1.1005 -
  1.1006 -lemma integrable_divide_zero[simp, intro]:
  1.1007 -  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  1.1008 -  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
  1.1009 -  unfolding integrable.simps by fastforce
  1.1010 -
  1.1011 -lemma integrable_inner_left[simp, intro]:
  1.1012 -  "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)"
  1.1013 -  unfolding integrable.simps by fastforce
  1.1014 -
  1.1015 -lemma integrable_inner_right[simp, intro]:
  1.1016 -  "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c \<bullet> f x)"
  1.1017 -  unfolding integrable.simps by fastforce
  1.1018 -
  1.1019 -lemmas integrable_minus[simp, intro] =
  1.1020 -  integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
  1.1021 -lemmas integrable_divide[simp, intro] =
  1.1022 -  integrable_bounded_linear[OF bounded_linear_divide]
  1.1023 -lemmas integrable_Re[simp, intro] =
  1.1024 -  integrable_bounded_linear[OF bounded_linear_Re]
  1.1025 -lemmas integrable_Im[simp, intro] =
  1.1026 -  integrable_bounded_linear[OF bounded_linear_Im]
  1.1027 -lemmas integrable_cnj[simp, intro] =
  1.1028 -  integrable_bounded_linear[OF bounded_linear_cnj]
  1.1029 -lemmas integrable_of_real[simp, intro] =
  1.1030 -  integrable_bounded_linear[OF bounded_linear_of_real]
  1.1031 -lemmas integrable_fst[simp, intro] =
  1.1032 -  integrable_bounded_linear[OF bounded_linear_fst]
  1.1033 -lemmas integrable_snd[simp, intro] =
  1.1034 -  integrable_bounded_linear[OF bounded_linear_snd]
  1.1035 -
  1.1036 -lemma integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0"
  1.1037 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)
  1.1038 -
  1.1039 -lemma integral_add[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
  1.1040 -    integral\<^sup>L M (\<lambda>x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g"
  1.1041 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable)
  1.1042 -
  1.1043 -lemma integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
  1.1044 -    integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
  1.1045 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
  1.1046 -
  1.1047 -lemma integral_setsum: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
  1.1048 -  integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
  1.1049 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_setsum has_bochner_integral_integrable)
  1.1050 -
  1.1051 -lemma integral_setsum'[simp]: "(\<And>i. i \<in> I =simp=> integrable M (f i)) \<Longrightarrow>
  1.1052 -  integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
  1.1053 -  unfolding simp_implies_def by (rule integral_setsum)
  1.1054 -
  1.1055 -lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
  1.1056 -    integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  1.1057 -  by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
  1.1058 -
  1.1059 -lemma integral_bounded_linear':
  1.1060 -  assumes T: "bounded_linear T" and T': "bounded_linear T'"
  1.1061 -  assumes *: "\<not> (\<forall>x. T x = 0) \<Longrightarrow> (\<forall>x. T' (T x) = x)"
  1.1062 -  shows "integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  1.1063 -proof cases
  1.1064 -  assume "(\<forall>x. T x = 0)" then show ?thesis
  1.1065 -    by simp
  1.1066 -next
  1.1067 -  assume **: "\<not> (\<forall>x. T x = 0)"
  1.1068 -  show ?thesis
  1.1069 -  proof cases
  1.1070 -    assume "integrable M f" with T show ?thesis
  1.1071 -      by (rule integral_bounded_linear)
  1.1072 -  next
  1.1073 -    assume not: "\<not> integrable M f"
  1.1074 -    moreover have "\<not> integrable M (\<lambda>x. T (f x))"
  1.1075 -    proof
  1.1076 -      assume "integrable M (\<lambda>x. T (f x))"
  1.1077 -      from integrable_bounded_linear[OF T' this] not *[OF **]
  1.1078 -      show False
  1.1079 -        by auto
  1.1080 -    qed
  1.1081 -    ultimately show ?thesis
  1.1082 -      using T by (simp add: not_integrable_integral_eq linear_simps)
  1.1083 -  qed
  1.1084 -qed
  1.1085 -
  1.1086 -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"
  1.1087 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
  1.1088 -
  1.1089 -lemma integral_scaleR_right[simp]: "(\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
  1.1090 -  by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp
  1.1091 -
  1.1092 -lemma integral_mult_left[simp]:
  1.1093 -  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1.1094 -  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
  1.1095 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)
  1.1096 -
  1.1097 -lemma integral_mult_right[simp]:
  1.1098 -  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  1.1099 -  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
  1.1100 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
  1.1101 -
  1.1102 -lemma integral_mult_left_zero[simp]:
  1.1103 -  fixes c :: "_::{real_normed_field,second_countable_topology}"
  1.1104 -  shows "(\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
  1.1105 -  by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp
  1.1106 -
  1.1107 -lemma integral_mult_right_zero[simp]:
  1.1108 -  fixes c :: "_::{real_normed_field,second_countable_topology}"
  1.1109 -  shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
  1.1110 -  by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp
  1.1111 -
  1.1112 -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"
  1.1113 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
  1.1114 -
  1.1115 -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"
  1.1116 -  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
  1.1117 -
  1.1118 -lemma integral_divide_zero[simp]:
  1.1119 -  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  1.1120 -  shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
  1.1121 -  by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
  1.1122 -
  1.1123 -lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f"
  1.1124 -  by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp
  1.1125 -
  1.1126 -lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\<lambda>x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
  1.1127 -  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp
  1.1128 -
  1.1129 -lemma integral_cnj[simp]: "integral\<^sup>L M (\<lambda>x. cnj (f x)) = cnj (integral\<^sup>L M f)"
  1.1130 -  by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp
  1.1131 -
  1.1132 -lemmas integral_divide[simp] =
  1.1133 -  integral_bounded_linear[OF bounded_linear_divide]
  1.1134 -lemmas integral_Re[simp] =
  1.1135 -  integral_bounded_linear[OF bounded_linear_Re]
  1.1136 -lemmas integral_Im[simp] =
  1.1137 -  integral_bounded_linear[OF bounded_linear_Im]
  1.1138 -lemmas integral_of_real[simp] =
  1.1139 -  integral_bounded_linear[OF bounded_linear_of_real]
  1.1140 -lemmas integral_fst[simp] =
  1.1141 -  integral_bounded_linear[OF bounded_linear_fst]
  1.1142 -lemmas integral_snd[simp] =
  1.1143 -  integral_bounded_linear[OF bounded_linear_snd]
  1.1144 -
  1.1145 -lemma integral_norm_bound_ennreal:
  1.1146 -  "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
  1.1147 -  by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)
  1.1148 -
  1.1149 -lemma integrableI_sequence:
  1.1150 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1151 -  assumes f[measurable]: "f \<in> borel_measurable M"
  1.1152 -  assumes s: "\<And>i. simple_bochner_integrable M (s i)"
  1.1153 -  assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?S \<longlonglongrightarrow> 0")
  1.1154 -  shows "integrable M f"
  1.1155 -proof -
  1.1156 -  let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
  1.1157 -
  1.1158 -  have "\<exists>x. ?s \<longlonglongrightarrow> x"
  1.1159 -    unfolding convergent_eq_cauchy
  1.1160 -  proof (rule metric_CauchyI)
  1.1161 -    fix e :: real assume "0 < e"
  1.1162 -    then have "0 < ennreal (e / 2)" by auto
  1.1163 -    from order_tendstoD(2)[OF lim this]
  1.1164 -    obtain M where M: "\<And>n. M \<le> n \<Longrightarrow> ?S n < e / 2"
  1.1165 -      by (auto simp: eventually_sequentially)
  1.1166 -    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (?s m) (?s n) < e"
  1.1167 -    proof (intro exI allI impI)
  1.1168 -      fix m n assume m: "M \<le> m" and n: "M \<le> n"
  1.1169 -      have "?S n \<noteq> \<infinity>"
  1.1170 -        using M[OF n] by auto
  1.1171 -      have "norm (?s n - ?s m) \<le> ?S n + ?S m"
  1.1172 -        by (intro simple_bochner_integral_bounded s f)
  1.1173 -      also have "\<dots> < ennreal (e / 2) + e / 2"
  1.1174 -        by (intro add_strict_mono M n m)
  1.1175 -      also have "\<dots> = e" using \<open>0<e\<close> by (simp del: ennreal_plus add: ennreal_plus[symmetric])
  1.1176 -      finally show "dist (?s n) (?s m) < e"
  1.1177 -        using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
  1.1178 -    qed
  1.1179 -  qed
  1.1180 -  then obtain x where "?s \<longlonglongrightarrow> x" ..
  1.1181 -  show ?thesis
  1.1182 -    by (rule, rule) fact+
  1.1183 -qed
  1.1184 -
  1.1185 -lemma nn_integral_dominated_convergence_norm:
  1.1186 -  fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
  1.1187 -  assumes [measurable]:
  1.1188 -       "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
  1.1189 -    and bound: "\<And>j. AE x in M. norm (u j x) \<le> w x"
  1.1190 -    and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
  1.1191 -    and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
  1.1192 -  shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> 0"
  1.1193 -proof -
  1.1194 -  have "AE x in M. \<forall>j. norm (u j x) \<le> w x"
  1.1195 -    unfolding AE_all_countable by rule fact
  1.1196 -  with u' have bnd: "AE x in M. \<forall>j. norm (u' x - u j x) \<le> 2 * w x"
  1.1197 -  proof (eventually_elim, intro allI)
  1.1198 -    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"
  1.1199 -    then have "norm (u' x) \<le> w x" "norm (u i x) \<le> w x"
  1.1200 -      by (auto intro: LIMSEQ_le_const2 tendsto_norm)
  1.1201 -    then have "norm (u' x) + norm (u i x) \<le> 2 * w x"
  1.1202 -      by simp
  1.1203 -    also have "norm (u' x - u i x) \<le> norm (u' x) + norm (u i x)"
  1.1204 -      by (rule norm_triangle_ineq4)
  1.1205 -    finally (xtrans) show "norm (u' x - u i x) \<le> 2 * w x" .
  1.1206 -  qed
  1.1207 -  have w_nonneg: "AE x in M. 0 \<le> w x"
  1.1208 -    using bound[of 0] by (auto intro: order_trans[OF norm_ge_zero])
  1.1209 -
  1.1210 -  have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. 0 \<partial>M)"
  1.1211 -  proof (rule nn_integral_dominated_convergence)
  1.1212 -    show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
  1.1213 -      by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) (insert w_nonneg, auto simp: ennreal_mult )
  1.1214 -    show "AE x in M. (\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
  1.1215 -      using u'
  1.1216 -    proof eventually_elim
  1.1217 -      fix x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
  1.1218 -      from tendsto_diff[OF tendsto_const[of "u' x"] this]
  1.1219 -      show "(\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
  1.1220 -        by (simp add: tendsto_norm_zero_iff ennreal_0[symmetric] del: ennreal_0)
  1.1221 -    qed
  1.1222 -  qed (insert bnd w_nonneg, auto)
  1.1223 -  then show ?thesis by simp
  1.1224 -qed
  1.1225 -
  1.1226 -lemma integrableI_bounded:
  1.1227 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1228 -  assumes f[measurable]: "f \<in> borel_measurable M" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1.1229 -  shows "integrable M f"
  1.1230 -proof -
  1.1231 -  from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
  1.1232 -    s: "\<And>i. simple_function M (s i)" and
  1.1233 -    pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" and
  1.1234 -    bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
  1.1235 -    by simp metis
  1.1236 -
  1.1237 -  show ?thesis
  1.1238 -  proof (rule integrableI_sequence)
  1.1239 -    { fix i
  1.1240 -      have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ennreal (2 * norm (f x)) \<partial>M)"
  1.1241 -        by (intro nn_integral_mono) (simp add: bound)
  1.1242 -      also have "\<dots> = 2 * (\<integral>\<^sup>+x. ennreal (norm (f x)) \<partial>M)"
  1.1243 -        by (simp add: ennreal_mult nn_integral_cmult)
  1.1244 -      also have "\<dots> < top"
  1.1245 -        using fin by (simp add: ennreal_mult_less_top)
  1.1246 -      finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
  1.1247 -        by simp }
  1.1248 -    note fin_s = this
  1.1249 -
  1.1250 -    show "\<And>i. simple_bochner_integrable M (s i)"
  1.1251 -      by (rule simple_bochner_integrableI_bounded) fact+
  1.1252 -
  1.1253 -    show "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
  1.1254 -    proof (rule nn_integral_dominated_convergence_norm)
  1.1255 -      show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
  1.1256 -        using bound by auto
  1.1257 -      show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
  1.1258 -        using s by (auto intro: borel_measurable_simple_function)
  1.1259 -      show "(\<integral>\<^sup>+ x. ennreal (2 * norm (f x)) \<partial>M) < \<infinity>"
  1.1260 -        using fin by (simp add: nn_integral_cmult ennreal_mult ennreal_mult_less_top)
  1.1261 -      show "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
  1.1262 -        using pointwise by auto
  1.1263 -    qed fact
  1.1264 -  qed fact
  1.1265 -qed
  1.1266 -
  1.1267 -lemma integrableI_bounded_set:
  1.1268 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1269 -  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M"
  1.1270 -  assumes finite: "emeasure M A < \<infinity>"
  1.1271 -    and bnd: "AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B"
  1.1272 -    and null: "AE x in M. x \<notin> A \<longrightarrow> f x = 0"
  1.1273 -  shows "integrable M f"
  1.1274 -proof (rule integrableI_bounded)
  1.1275 -  { fix x :: 'b have "norm x \<le> B \<Longrightarrow> 0 \<le> B"
  1.1276 -      using norm_ge_zero[of x] by arith }
  1.1277 -  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)"
  1.1278 -    by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
  1.1279 -  also have "\<dots> < \<infinity>"
  1.1280 -    using finite by (subst nn_integral_cmult_indicator) (auto simp: ennreal_mult_less_top)
  1.1281 -  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
  1.1282 -qed simp
  1.1283 -
  1.1284 -lemma integrableI_bounded_set_indicator:
  1.1285 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1286 -  shows "A \<in> sets M \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow>
  1.1287 -    emeasure M A < \<infinity> \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B) \<Longrightarrow>
  1.1288 -    integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1.1289 -  by (rule integrableI_bounded_set[where A=A]) auto
  1.1290 -
  1.1291 -lemma integrableI_nonneg:
  1.1292 -  fixes f :: "'a \<Rightarrow> real"
  1.1293 -  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
  1.1294 -  shows "integrable M f"
  1.1295 -proof -
  1.1296 -  have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1.1297 -    using assms by (intro nn_integral_cong_AE) auto
  1.1298 -  then show ?thesis
  1.1299 -    using assms by (intro integrableI_bounded) auto
  1.1300 -qed
  1.1301 -
  1.1302 -lemma integrable_iff_bounded:
  1.1303 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1304 -  shows "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1.1305 -  using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f]
  1.1306 -  unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto
  1.1307 -
  1.1308 -lemma integrable_bound:
  1.1309 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1310 -    and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
  1.1311 -  shows "integrable M f \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. norm (g x) \<le> norm (f x)) \<Longrightarrow>
  1.1312 -    integrable M g"
  1.1313 -  unfolding integrable_iff_bounded
  1.1314 -proof safe
  1.1315 -  assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1.1316 -  assume "AE x in M. norm (g x) \<le> norm (f x)"
  1.1317 -  then have "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1.1318 -    by  (intro nn_integral_mono_AE) auto
  1.1319 -  also assume "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  1.1320 -  finally show "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) < \<infinity>" .
  1.1321 -qed
  1.1322 -
  1.1323 -lemma integrable_mult_indicator:
  1.1324 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1325 -  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1.1326 -  by (rule integrable_bound[of M f]) (auto split: split_indicator)
  1.1327 -
  1.1328 -lemma integrable_real_mult_indicator:
  1.1329 -  fixes f :: "'a \<Rightarrow> real"
  1.1330 -  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
  1.1331 -  using integrable_mult_indicator[of A M f] by (simp add: mult_ac)
  1.1332 -
  1.1333 -lemma integrable_abs[simp, intro]:
  1.1334 -  fixes f :: "'a \<Rightarrow> real"
  1.1335 -  assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
  1.1336 -  using assms by (rule integrable_bound) auto
  1.1337 -
  1.1338 -lemma integrable_norm[simp, intro]:
  1.1339 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1340 -  assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. norm (f x))"
  1.1341 -  using assms by (rule integrable_bound) auto
  1.1342 -
  1.1343 -lemma integrable_norm_cancel:
  1.1344 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1345 -  assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
  1.1346 -  using assms by (rule integrable_bound) auto
  1.1347 -
  1.1348 -lemma integrable_norm_iff:
  1.1349 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1350 -  shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. norm (f x)) \<longleftrightarrow> integrable M f"
  1.1351 -  by (auto intro: integrable_norm_cancel)
  1.1352 -
  1.1353 -lemma integrable_abs_cancel:
  1.1354 -  fixes f :: "'a \<Rightarrow> real"
  1.1355 -  assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
  1.1356 -  using assms by (rule integrable_bound) auto
  1.1357 -
  1.1358 -lemma integrable_abs_iff:
  1.1359 -  fixes f :: "'a \<Rightarrow> real"
  1.1360 -  shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
  1.1361 -  by (auto intro: integrable_abs_cancel)
  1.1362 -
  1.1363 -lemma integrable_max[simp, intro]:
  1.1364 -  fixes f :: "'a \<Rightarrow> real"
  1.1365 -  assumes fg[measurable]: "integrable M f" "integrable M g"
  1.1366 -  shows "integrable M (\<lambda>x. max (f x) (g x))"
  1.1367 -  using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
  1.1368 -  by (rule integrable_bound) auto
  1.1369 -
  1.1370 -lemma integrable_min[simp, intro]:
  1.1371 -  fixes f :: "'a \<Rightarrow> real"
  1.1372 -  assumes fg[measurable]: "integrable M f" "integrable M g"
  1.1373 -  shows "integrable M (\<lambda>x. min (f x) (g x))"
  1.1374 -  using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
  1.1375 -  by (rule integrable_bound) auto
  1.1376 -
  1.1377 -lemma integral_minus_iff[simp]:
  1.1378 -  "integrable M (\<lambda>x. - f x ::'a::{banach, second_countable_topology}) \<longleftrightarrow> integrable M f"
  1.1379 -  unfolding integrable_iff_bounded
  1.1380 -  by (auto intro: borel_measurable_uminus[of "\<lambda>x. - f x" M, simplified])
  1.1381 -
  1.1382 -lemma integrable_indicator_iff:
  1.1383 -  "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
  1.1384 -  by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator nn_integral_indicator'
  1.1385 -           cong: conj_cong)
  1.1386 -
  1.1387 -lemma integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \<inter> space M)"
  1.1388 -proof cases
  1.1389 -  assume *: "A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
  1.1390 -  have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M))"
  1.1391 -    by (intro integral_cong) (auto split: split_indicator)
  1.1392 -  also have "\<dots> = measure M (A \<inter> space M)"
  1.1393 -    using * by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator) auto
  1.1394 -  finally show ?thesis .
  1.1395 -next
  1.1396 -  assume *: "\<not> (A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>)"
  1.1397 -  have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M) :: _ \<Rightarrow> real)"
  1.1398 -    by (intro integral_cong) (auto split: split_indicator)
  1.1399 -  also have "\<dots> = 0"
  1.1400 -    using * by (subst not_integrable_integral_eq) (auto simp: integrable_indicator_iff)
  1.1401 -  also have "\<dots> = measure M (A \<inter> space M)"
  1.1402 -    using * by (auto simp: measure_def emeasure_notin_sets not_less top_unique)
  1.1403 -  finally show ?thesis .
  1.1404 -qed
  1.1405 -
  1.1406 -lemma integrable_discrete_difference:
  1.1407 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1408 -  assumes X: "countable X"
  1.1409 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
  1.1410 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1.1411 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1.1412 -  shows "integrable M f \<longleftrightarrow> integrable M g"
  1.1413 -  unfolding integrable_iff_bounded
  1.1414 -proof (rule conj_cong)
  1.1415 -  { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
  1.1416 -      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
  1.1417 -  moreover
  1.1418 -  { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
  1.1419 -      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
  1.1420 -  ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
  1.1421 -next
  1.1422 -  have "AE x in M. x \<notin> X"
  1.1423 -    by (rule AE_discrete_difference) fact+
  1.1424 -  then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
  1.1425 -    by (intro nn_integral_cong_AE) (auto simp: eq)
  1.1426 -  then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
  1.1427 -    by simp
  1.1428 -qed
  1.1429 -
  1.1430 -lemma integral_discrete_difference:
  1.1431 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1432 -  assumes X: "countable X"
  1.1433 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
  1.1434 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1.1435 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1.1436 -  shows "integral\<^sup>L M f = integral\<^sup>L M g"
  1.1437 -proof (rule integral_eq_cases)
  1.1438 -  show eq: "integrable M f \<longleftrightarrow> integrable M g"
  1.1439 -    by (rule integrable_discrete_difference[where X=X]) fact+
  1.1440 -
  1.1441 -  assume f: "integrable M f"
  1.1442 -  show "integral\<^sup>L M f = integral\<^sup>L M g"
  1.1443 -  proof (rule integral_cong_AE)
  1.1444 -    show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1.1445 -      using f eq by (auto intro: borel_measurable_integrable)
  1.1446 -
  1.1447 -    have "AE x in M. x \<notin> X"
  1.1448 -      by (rule AE_discrete_difference) fact+
  1.1449 -    with AE_space show "AE x in M. f x = g x"
  1.1450 -      by eventually_elim fact
  1.1451 -  qed
  1.1452 -qed
  1.1453 -
  1.1454 -lemma has_bochner_integral_discrete_difference:
  1.1455 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1456 -  assumes X: "countable X"
  1.1457 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
  1.1458 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1.1459 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
  1.1460 -  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
  1.1461 -  using integrable_discrete_difference[of X M f g, OF assms]
  1.1462 -  using integral_discrete_difference[of X M f g, OF assms]
  1.1463 -  by (metis has_bochner_integral_iff)
  1.1464 -
  1.1465 -lemma
  1.1466 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
  1.1467 -  assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
  1.1468 -  assumes lim: "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
  1.1469 -  assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
  1.1470 -  shows integrable_dominated_convergence: "integrable M f"
  1.1471 -    and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
  1.1472 -    and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
  1.1473 -proof -
  1.1474 -  have w_nonneg: "AE x in M. 0 \<le> w x"
  1.1475 -    using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
  1.1476 -  then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
  1.1477 -    by (intro nn_integral_cong_AE) auto
  1.1478 -  with \<open>integrable M w\<close> have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
  1.1479 -    unfolding integrable_iff_bounded by auto
  1.1480 -
  1.1481 -  show int_s: "\<And>i. integrable M (s i)"
  1.1482 -    unfolding integrable_iff_bounded
  1.1483 -  proof
  1.1484 -    fix i
  1.1485 -    have "(\<integral>\<^sup>+ x. ennreal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
  1.1486 -      using bound[of i] w_nonneg by (intro nn_integral_mono_AE) auto
  1.1487 -    with w show "(\<integral>\<^sup>+ x. ennreal (norm (s i x)) \<partial>M) < \<infinity>" by auto
  1.1488 -  qed fact
  1.1489 -
  1.1490 -  have all_bound: "AE x in M. \<forall>i. norm (s i x) \<le> w x"
  1.1491 -    using bound unfolding AE_all_countable by auto
  1.1492 -
  1.1493 -  show int_f: "integrable M f"
  1.1494 -    unfolding integrable_iff_bounded
  1.1495 -  proof
  1.1496 -    have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
  1.1497 -      using all_bound lim w_nonneg
  1.1498 -    proof (intro nn_integral_mono_AE, eventually_elim)
  1.1499 -      fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) \<longlonglongrightarrow> f x" "0 \<le> w x"
  1.1500 -      then show "ennreal (norm (f x)) \<le> ennreal (w x)"
  1.1501 -        by (intro LIMSEQ_le_const2[where X="\<lambda>i. ennreal (norm (s i x))"]) (auto intro: tendsto_intros)
  1.1502 -    qed
  1.1503 -    with w show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by auto
  1.1504 -  qed fact
  1.1505 -
  1.1506 -  have "(\<lambda>n. ennreal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) \<longlonglongrightarrow> ennreal 0" (is "?d \<longlonglongrightarrow> ennreal 0")
  1.1507 -  proof (rule tendsto_sandwich)
  1.1508 -    show "eventually (\<lambda>n. ennreal 0 \<le> ?d n) sequentially" "(\<lambda>_. ennreal 0) \<longlonglongrightarrow> ennreal 0" by auto
  1.1509 -    show "eventually (\<lambda>n. ?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)) sequentially"
  1.1510 -    proof (intro always_eventually allI)
  1.1511 -      fix n
  1.1512 -      have "?d n = norm (integral\<^sup>L M (\<lambda>x. s n x - f x))"
  1.1513 -        using int_f int_s by simp
  1.1514 -      also have "\<dots> \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)"
  1.1515 -        by (intro int_f int_s integrable_diff integral_norm_bound_ennreal)
  1.1516 -      finally show "?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)" .
  1.1517 -    qed
  1.1518 -    show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) \<longlonglongrightarrow> ennreal 0"
  1.1519 -      unfolding ennreal_0
  1.1520 -      apply (subst norm_minus_commute)
  1.1521 -    proof (rule nn_integral_dominated_convergence_norm[where w=w])
  1.1522 -      show "\<And>n. s n \<in> borel_measurable M"
  1.1523 -        using int_s unfolding integrable_iff_bounded by auto
  1.1524 -    qed fact+
  1.1525 -  qed
  1.1526 -  then have "(\<lambda>n. integral\<^sup>L M (s n) - integral\<^sup>L M f) \<longlonglongrightarrow> 0"
  1.1527 -    by (simp add: tendsto_norm_zero_iff del: ennreal_0)
  1.1528 -  from tendsto_add[OF this tendsto_const[of "integral\<^sup>L M f"]]
  1.1529 -  show "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"  by simp
  1.1530 -qed
  1.1531 -
  1.1532 -context
  1.1533 -  fixes s :: "real \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
  1.1534 -    and f :: "'a \<Rightarrow> 'b" and M
  1.1535 -  assumes "f \<in> borel_measurable M" "\<And>t. s t \<in> borel_measurable M" "integrable M w"
  1.1536 -  assumes lim: "AE x in M. ((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
  1.1537 -  assumes bound: "\<forall>\<^sub>F i in at_top. AE x in M. norm (s i x) \<le> w x"
  1.1538 -begin
  1.1539 -
  1.1540 -lemma integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) \<longlongrightarrow> integral\<^sup>L M f) at_top"
  1.1541 -proof (rule tendsto_at_topI_sequentially)
  1.1542 -  fix X :: "nat \<Rightarrow> real" assume X: "filterlim X at_top sequentially"
  1.1543 -  from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
  1.1544 -  obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s (X n) x) \<le> w x"
  1.1545 -    by (auto simp: eventually_sequentially)
  1.1546 -
  1.1547 -  show "(\<lambda>n. integral\<^sup>L M (s (X n))) \<longlonglongrightarrow> integral\<^sup>L M f"
  1.1548 -  proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
  1.1549 -    show "AE x in M. norm (s (X (n + N)) x) \<le> w x" for n
  1.1550 -      by (rule w) auto
  1.1551 -    show "AE x in M. (\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
  1.1552 -      using lim
  1.1553 -    proof eventually_elim
  1.1554 -      fix x assume "((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
  1.1555 -      then show "(\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
  1.1556 -        by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
  1.1557 -    qed
  1.1558 -  qed fact+
  1.1559 -qed
  1.1560 -
  1.1561 -lemma integrable_dominated_convergence_at_top: "integrable M f"
  1.1562 -proof -
  1.1563 -  from bound obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s n x) \<le> w x"
  1.1564 -    by (auto simp: eventually_at_top_linorder)
  1.1565 -  show ?thesis
  1.1566 -  proof (rule integrable_dominated_convergence)
  1.1567 -    show "AE x in M. norm (s (N + i) x) \<le> w x" for i :: nat
  1.1568 -      by (intro w) auto
  1.1569 -    show "AE x in M. (\<lambda>i. s (N + real i) x) \<longlonglongrightarrow> f x"
  1.1570 -      using lim
  1.1571 -    proof eventually_elim
  1.1572 -      fix x assume "((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
  1.1573 -      then show "(\<lambda>n. s (N + n) x) \<longlonglongrightarrow> f x"
  1.1574 -        by (rule filterlim_compose)
  1.1575 -           (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially)
  1.1576 -    qed
  1.1577 -  qed fact+
  1.1578 -qed
  1.1579 -
  1.1580 -end
  1.1581 -
  1.1582 -lemma integrable_mult_left_iff:
  1.1583 -  fixes f :: "'a \<Rightarrow> real"
  1.1584 -  shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
  1.1585 -  using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
  1.1586 -  by (cases "c = 0") auto
  1.1587 -
  1.1588 -lemma integrableI_nn_integral_finite:
  1.1589 -  assumes [measurable]: "f \<in> borel_measurable M"
  1.1590 -    and nonneg: "AE x in M. 0 \<le> f x"
  1.1591 -    and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
  1.1592 -  shows "integrable M f"
  1.1593 -proof (rule integrableI_bounded)
  1.1594 -  have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M)"
  1.1595 -    using nonneg by (intro nn_integral_cong_AE) auto
  1.1596 -  with finite show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  1.1597 -    by auto
  1.1598 -qed simp
  1.1599 -
  1.1600 -lemma integral_nonneg_AE:
  1.1601 -  fixes f :: "'a \<Rightarrow> real"
  1.1602 -  assumes nonneg: "AE x in M. 0 \<le> f x"
  1.1603 -  shows "0 \<le> integral\<^sup>L M f"
  1.1604 -proof cases
  1.1605 -  assume f: "integrable M f"
  1.1606 -  then have [measurable]: "f \<in> M \<rightarrow>\<^sub>M borel"
  1.1607 -    by auto
  1.1608 -  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))"
  1.1609 -    using f by auto
  1.1610 -  from this have "0 \<le> integral\<^sup>L M (\<lambda>x. max 0 (f x))"
  1.1611 -  proof (induction rule: borel_measurable_induct_real)
  1.1612 -    case (add f g)
  1.1613 -    then have "integrable M f" "integrable M g"
  1.1614 -      by (auto intro!: integrable_bound[OF add.prems])
  1.1615 -    with add show ?case
  1.1616 -      by (simp add: nn_integral_add)
  1.1617 -  next
  1.1618 -    case (seq U)
  1.1619 -    show ?case
  1.1620 -    proof (rule LIMSEQ_le_const)
  1.1621 -      have U_le: "x \<in> space M \<Longrightarrow> U i x \<le> max 0 (f x)" for x i
  1.1622 -        using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
  1.1623 -      with seq nonneg show "(\<lambda>i. integral\<^sup>L M (U i)) \<longlonglongrightarrow> LINT x|M. max 0 (f x)"
  1.1624 -        by (intro integral_dominated_convergence) auto
  1.1625 -      have "integrable M (U i)" for i
  1.1626 -        using seq.prems by (rule integrable_bound) (insert U_le seq, auto)
  1.1627 -      with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
  1.1628 -        by auto
  1.1629 -    qed
  1.1630 -  qed (auto simp: measure_nonneg integrable_mult_left_iff)
  1.1631 -  also have "\<dots> = integral\<^sup>L M f"
  1.1632 -    using nonneg by (auto intro!: integral_cong_AE)
  1.1633 -  finally show ?thesis .
  1.1634 -qed (simp add: not_integrable_integral_eq)
  1.1635 -
  1.1636 -lemma integral_nonneg[simp]:
  1.1637 -  fixes f :: "'a \<Rightarrow> real"
  1.1638 -  shows "(\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> integral\<^sup>L M f"
  1.1639 -  by (intro integral_nonneg_AE) auto
  1.1640 -
  1.1641 -lemma nn_integral_eq_integral:
  1.1642 -  assumes f: "integrable M f"
  1.1643 -  assumes nonneg: "AE x in M. 0 \<le> f x"
  1.1644 -  shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
  1.1645 -proof -
  1.1646 -  { fix f :: "'a \<Rightarrow> real" assume f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "integrable M f"
  1.1647 -    then have "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
  1.1648 -    proof (induct rule: borel_measurable_induct_real)
  1.1649 -      case (set A) then show ?case
  1.1650 -        by (simp add: integrable_indicator_iff ennreal_indicator emeasure_eq_ennreal_measure)
  1.1651 -    next
  1.1652 -      case (mult f c) then show ?case
  1.1653 -        by (auto simp add: integrable_mult_left_iff nn_integral_cmult ennreal_mult integral_nonneg_AE)
  1.1654 -    next
  1.1655 -      case (add g f)
  1.1656 -      then have "integrable M f" "integrable M g"
  1.1657 -        by (auto intro!: integrable_bound[OF add.prems])
  1.1658 -      with add show ?case
  1.1659 -        by (simp add: nn_integral_add integral_nonneg_AE)
  1.1660 -    next
  1.1661 -      case (seq U)
  1.1662 -      show ?case
  1.1663 -      proof (rule LIMSEQ_unique)
  1.1664 -        have U_le_f: "x \<in> space M \<Longrightarrow> U i x \<le> f x" for x i
  1.1665 -          using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
  1.1666 -        have int_U: "\<And>i. integrable M (U i)"
  1.1667 -          using seq f U_le_f by (intro integrable_bound[OF f(3)]) auto
  1.1668 -        from U_le_f seq have "(\<lambda>i. integral\<^sup>L M (U i)) \<longlonglongrightarrow> integral\<^sup>L M f"
  1.1669 -          by (intro integral_dominated_convergence) auto
  1.1670 -        then show "(\<lambda>i. ennreal (integral\<^sup>L M (U i))) \<longlonglongrightarrow> ennreal (integral\<^sup>L M f)"
  1.1671 -          using seq f int_U by (simp add: f integral_nonneg_AE)
  1.1672 -        have "(\<lambda>i. \<integral>\<^sup>+ x. U i x \<partial>M) \<longlonglongrightarrow> \<integral>\<^sup>+ x. f x \<partial>M"
  1.1673 -          using seq U_le_f f
  1.1674 -          by (intro nn_integral_dominated_convergence[where w=f]) (auto simp: integrable_iff_bounded)
  1.1675 -        then show "(\<lambda>i. \<integral>x. U i x \<partial>M) \<longlonglongrightarrow> \<integral>\<^sup>+x. f x \<partial>M"
  1.1676 -          using seq int_U by simp
  1.1677 -      qed
  1.1678 -    qed }
  1.1679 -  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))"
  1.1680 -    by simp
  1.1681 -  also have "\<dots> = integral\<^sup>L M f"
  1.1682 -    using assms by (auto intro!: integral_cong_AE simp: integral_nonneg_AE)
  1.1683 -  also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
  1.1684 -    using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
  1.1685 -  finally show ?thesis .
  1.1686 -qed
  1.1687 -
  1.1688 -lemma
  1.1689 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1.1690 -  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
  1.1691 -  and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
  1.1692 -  and sums: "summable (\<lambda>i. (\<integral>x. norm (f i x) \<partial>M))"
  1.1693 -  shows integrable_suminf: "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
  1.1694 -    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")
  1.1695 -    and integral_suminf: "(\<integral>x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>L M (f i))"
  1.1696 -    and summable_integral: "summable (\<lambda>i. integral\<^sup>L M (f i))"
  1.1697 -proof -
  1.1698 -  have 1: "integrable M (\<lambda>x. \<Sum>i. norm (f i x))"
  1.1699 -  proof (rule integrableI_bounded)
  1.1700 -    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)"
  1.1701 -      apply (intro nn_integral_cong_AE)
  1.1702 -      using summable
  1.1703 -      apply eventually_elim
  1.1704 -      apply (simp add: suminf_nonneg ennreal_suminf_neq_top)
  1.1705 -      done
  1.1706 -    also have "\<dots> = (\<Sum>i. \<integral>\<^sup>+ x. norm (f i x) \<partial>M)"
  1.1707 -      by (intro nn_integral_suminf) auto
  1.1708 -    also have "\<dots> = (\<Sum>i. ennreal (\<integral>x. norm (f i x) \<partial>M))"
  1.1709 -      by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
  1.1710 -    finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Sum>i. norm (f i x))) \<partial>M) < \<infinity>"
  1.1711 -      by (simp add: sums ennreal_suminf_neq_top less_top[symmetric] integral_nonneg_AE)
  1.1712 -  qed simp
  1.1713 -
  1.1714 -  have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> (\<Sum>i. f i x)"
  1.1715 -    using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
  1.1716 -
  1.1717 -  have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
  1.1718 -    using summable
  1.1719 -  proof eventually_elim
  1.1720 -    fix j x assume [simp]: "summable (\<lambda>i. norm (f i x))"
  1.1721 -    have "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i<j. norm (f i x))" by (rule norm_setsum)
  1.1722 -    also have "\<dots> \<le> (\<Sum>i. norm (f i x))"
  1.1723 -      using setsum_le_suminf[of "\<lambda>i. norm (f i x)"] unfolding sums_iff by auto
  1.1724 -    finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
  1.1725 -  qed
  1.1726 -
  1.1727 -  note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
  1.1728 -  note int = integral_dominated_convergence[OF _ _ 1 2 3]
  1.1729 -
  1.1730 -  show "integrable M ?S"
  1.1731 -    by (rule ibl) measurable
  1.1732 -
  1.1733 -  show "?f sums ?x" unfolding sums_def
  1.1734 -    using int by (simp add: integrable)
  1.1735 -  then show "?x = suminf ?f" "summable ?f"
  1.1736 -    unfolding sums_iff by auto
  1.1737 -qed
  1.1738 -
  1.1739 -lemma integral_norm_bound:
  1.1740 -  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1.1741 -  shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
  1.1742 -  using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
  1.1743 -  using integral_norm_bound_ennreal[of M f] by (simp add: integral_nonneg_AE)
  1.1744 -
  1.1745 -lemma integral_eq_nn_integral:
  1.1746 -  assumes [measurable]: "f \<in> borel_measurable M"
  1.1747 -  assumes nonneg: "AE x in M. 0 \<le> f x"
  1.1748 -  shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M)"
  1.1749 -proof cases
  1.1750 -  assume *: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) = \<infinity>"
  1.1751 -  also have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1.1752 -    using nonneg by (intro nn_integral_cong_AE) auto
  1.1753 -  finally have "\<not> integrable M f"
  1.1754 -    by (auto simp: integrable_iff_bounded)
  1.1755 -  then show ?thesis
  1.1756 -    by (simp add: * not_integrable_integral_eq)
  1.1757 -next
  1.1758 -  assume "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>"
  1.1759 -  then have "integrable M f"
  1.1760 -    by (cases "\<integral>\<^sup>+ x. ennreal (f x) \<partial>M" rule: ennreal_cases)
  1.1761 -       (auto intro!: integrableI_nn_integral_finite assms)
  1.1762 -  from nn_integral_eq_integral[OF this] nonneg show ?thesis
  1.1763 -    by (simp add: integral_nonneg_AE)
  1.1764 -qed
  1.1765 -
  1.1766 -lemma enn2real_nn_integral_eq_integral:
  1.1767 -  assumes eq: "AE x in M. f x = ennreal (g x)" and nn: "AE x in M. 0 \<le> g x"
  1.1768 -    and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < top"
  1.1769 -    and [measurable]: "g \<in> M \<rightarrow>\<^sub>M borel"
  1.1770 -  shows "enn2real (\<integral>\<^sup>+x. f x \<partial>M) = (\<integral>x. g x \<partial>M)"
  1.1771 -proof -
  1.1772 -  have "ennreal (enn2real (\<integral>\<^sup>+x. f x \<partial>M)) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1.1773 -    using fin by (intro ennreal_enn2real) auto
  1.1774 -  also have "\<dots> = (\<integral>\<^sup>+x. g x \<partial>M)"
  1.1775 -    using eq by (rule nn_integral_cong_AE)
  1.1776 -  also have "\<dots> = (\<integral>x. g x \<partial>M)"
  1.1777 -  proof (rule nn_integral_eq_integral)
  1.1778 -    show "integrable M g"
  1.1779 -    proof (rule integrableI_bounded)
  1.1780 -      have "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
  1.1781 -        using eq nn by (auto intro!: nn_integral_cong_AE elim!: eventually_elim2)
  1.1782 -      also note fin
  1.1783 -      finally show "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) < \<infinity>"
  1.1784 -        by simp
  1.1785 -    qed simp
  1.1786 -  qed fact
  1.1787 -  finally show ?thesis
  1.1788 -    using nn by (simp add: integral_nonneg_AE)
  1.1789 -qed
  1.1790 -
  1.1791 -lemma has_bochner_integral_nn_integral:
  1.1792 -  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "0 \<le> x"
  1.1793 -  assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
  1.1794 -  shows "has_bochner_integral M f x"
  1.1795 -  unfolding has_bochner_integral_iff
  1.1796 -  using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
  1.1797 -
  1.1798 -lemma integrableI_simple_bochner_integrable:
  1.1799 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1800 -  shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
  1.1801 -  by (intro integrableI_sequence[where s="\<lambda>_. f"] borel_measurable_simple_function)
  1.1802 -     (auto simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps)
  1.1803 -
  1.1804 -lemma integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
  1.1805 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1806 -  assumes "integrable M f"
  1.1807 -  assumes base: "\<And>A c. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R c)"
  1.1808 -  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)"
  1.1809 -  assumes lim: "\<And>f s. (\<And>i. integrable M (s i)) \<Longrightarrow> (\<And>i. P (s i)) \<Longrightarrow>
  1.1810 -   (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x) \<Longrightarrow>
  1.1811 -   (\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)) \<Longrightarrow> integrable M f \<Longrightarrow> P f"
  1.1812 -  shows "P f"
  1.1813 -proof -
  1.1814 -  from \<open>integrable M f\<close> have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1.1815 -    unfolding integrable_iff_bounded by auto
  1.1816 -  from borel_measurable_implies_sequence_metric[OF f(1)]
  1.1817 -  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"
  1.1818 -    "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
  1.1819 -    unfolding norm_conv_dist by metis
  1.1820 -
  1.1821 -  { fix f A
  1.1822 -    have [simp]: "P (\<lambda>x. 0)"
  1.1823 -      using base[of "{}" undefined] by simp
  1.1824 -    have "(\<And>i::'b. i \<in> A \<Longrightarrow> integrable M (f i::'a \<Rightarrow> 'b)) \<Longrightarrow>
  1.1825 -    (\<And>i. i \<in> A \<Longrightarrow> P (f i)) \<Longrightarrow> P (\<lambda>x. \<Sum>i\<in>A. f i x)"
  1.1826 -    by (induct A rule: infinite_finite_induct) (auto intro!: add) }
  1.1827 -  note setsum = this
  1.1828 -
  1.1829 -  define s' where [abs_def]: "s' i z = indicator (space M) z *\<^sub>R s i z" for i z
  1.1830 -  then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x"
  1.1831 -    by simp
  1.1832 -
  1.1833 -  have sf[measurable]: "\<And>i. simple_function M (s' i)"
  1.1834 -    unfolding s'_def using s(1)
  1.1835 -    by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto
  1.1836 -
  1.1837 -  { fix i
  1.1838 -    have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
  1.1839 -        (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})"
  1.1840 -      by (auto simp add: s'_def split: split_indicator)
  1.1841 -    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)"
  1.1842 -      using sf by (auto simp: fun_eq_iff simple_function_def s'_def) }
  1.1843 -  note s'_eq = this
  1.1844 -
  1.1845 -  show "P f"
  1.1846 -  proof (rule lim)
  1.1847 -    fix i
  1.1848 -
  1.1849 -    have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ennreal (2 * norm (f x)) \<partial>M)"
  1.1850 -      using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
  1.1851 -    also have "\<dots> < \<infinity>"
  1.1852 -      using f by (simp add: nn_integral_cmult ennreal_mult_less_top ennreal_mult)
  1.1853 -    finally have sbi: "simple_bochner_integrable M (s' i)"
  1.1854 -      using sf by (intro simple_bochner_integrableI_bounded) auto
  1.1855 -    then show "integrable M (s' i)"
  1.1856 -      by (rule integrableI_simple_bochner_integrable)
  1.1857 -
  1.1858 -    { fix x assume"x \<in> space M" "s' i x \<noteq> 0"
  1.1859 -      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}"
  1.1860 -        by (intro emeasure_mono) auto
  1.1861 -      also have "\<dots> < \<infinity>"
  1.1862 -        using sbi by (auto elim: simple_bochner_integrable.cases simp: less_top)
  1.1863 -      finally have "emeasure M {y \<in> space M. s' i y = s' i x} \<noteq> \<infinity>" by simp }
  1.1864 -    then show "P (s' i)"
  1.1865 -      by (subst s'_eq) (auto intro!: setsum base simp: less_top)
  1.1866 -
  1.1867 -    fix x assume "x \<in> space M" with s show "(\<lambda>i. s' i x) \<longlonglongrightarrow> f x"
  1.1868 -      by (simp add: s'_eq_s)
  1.1869 -    show "norm (s' i x) \<le> 2 * norm (f x)"
  1.1870 -      using \<open>x \<in> space M\<close> s by (simp add: s'_eq_s)
  1.1871 -  qed fact
  1.1872 -qed
  1.1873 -
  1.1874 -lemma integral_eq_zero_AE:
  1.1875 -  "(AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
  1.1876 -  using integral_cong_AE[of f M "\<lambda>_. 0"]
  1.1877 -  by (cases "integrable M f") (simp_all add: not_integrable_integral_eq)
  1.1878 -
  1.1879 -lemma integral_nonneg_eq_0_iff_AE:
  1.1880 -  fixes f :: "_ \<Rightarrow> real"
  1.1881 -  assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \<le> f x"
  1.1882 -  shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
  1.1883 -proof
  1.1884 -  assume "integral\<^sup>L M f = 0"
  1.1885 -  then have "integral\<^sup>N M f = 0"
  1.1886 -    using nn_integral_eq_integral[OF f nonneg] by simp
  1.1887 -  then have "AE x in M. ennreal (f x) \<le> 0"
  1.1888 -    by (simp add: nn_integral_0_iff_AE)
  1.1889 -  with nonneg show "AE x in M. f x = 0"
  1.1890 -    by auto
  1.1891 -qed (auto simp add: integral_eq_zero_AE)
  1.1892 -
  1.1893 -lemma integral_mono_AE:
  1.1894 -  fixes f :: "'a \<Rightarrow> real"
  1.1895 -  assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
  1.1896 -  shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1.1897 -proof -
  1.1898 -  have "0 \<le> integral\<^sup>L M (\<lambda>x. g x - f x)"
  1.1899 -    using assms by (intro integral_nonneg_AE integrable_diff assms) auto
  1.1900 -  also have "\<dots> = integral\<^sup>L M g - integral\<^sup>L M f"
  1.1901 -    by (intro integral_diff assms)
  1.1902 -  finally show ?thesis by simp
  1.1903 -qed
  1.1904 -
  1.1905 -lemma integral_mono:
  1.1906 -  fixes f :: "'a \<Rightarrow> real"
  1.1907 -  shows "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x) \<Longrightarrow>
  1.1908 -    integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1.1909 -  by (intro integral_mono_AE) auto
  1.1910 -
  1.1911 -lemma (in finite_measure) integrable_measure:
  1.1912 -  assumes I: "disjoint_family_on X I" "countable I"
  1.1913 -  shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
  1.1914 -proof -
  1.1915 -  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)"
  1.1916 -    by (auto intro!: nn_integral_cong measure_notin_sets)
  1.1917 -  also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
  1.1918 -    using I unfolding emeasure_eq_measure[symmetric]
  1.1919 -    by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
  1.1920 -  finally show ?thesis
  1.1921 -    by (auto intro!: integrableI_bounded)
  1.1922 -qed
  1.1923 -
  1.1924 -lemma integrableI_real_bounded:
  1.1925 -  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>"
  1.1926 -  shows "integrable M f"
  1.1927 -proof (rule integrableI_bounded)
  1.1928 -  have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ennreal (f x) \<partial>M"
  1.1929 -    using ae by (auto intro: nn_integral_cong_AE)
  1.1930 -  also note fin
  1.1931 -  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
  1.1932 -qed fact
  1.1933 -
  1.1934 -lemma integral_real_bounded:
  1.1935 -  assumes "0 \<le> r" "integral\<^sup>N M f \<le> ennreal r"
  1.1936 -  shows "integral\<^sup>L M f \<le> r"
  1.1937 -proof cases
  1.1938 -  assume [simp]: "integrable M f"
  1.1939 -
  1.1940 -  have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>N M (\<lambda>x. max 0 (f x))"
  1.1941 -    by (intro nn_integral_eq_integral[symmetric]) auto
  1.1942 -  also have "\<dots> = integral\<^sup>N M f"
  1.1943 -    by (intro nn_integral_cong) (simp add: max_def ennreal_neg)
  1.1944 -  also have "\<dots> \<le> r"
  1.1945 -    by fact
  1.1946 -  finally have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) \<le> r"
  1.1947 -    using \<open>0 \<le> r\<close> by simp
  1.1948 -
  1.1949 -  moreover have "integral\<^sup>L M f \<le> integral\<^sup>L M (\<lambda>x. max 0 (f x))"
  1.1950 -    by (rule integral_mono_AE) auto
  1.1951 -  ultimately show ?thesis
  1.1952 -    by simp
  1.1953 -next
  1.1954 -  assume "\<not> integrable M f" then show ?thesis
  1.1955 -    using \<open>0 \<le> r\<close> by (simp add: not_integrable_integral_eq)
  1.1956 -qed
  1.1957 -
  1.1958 -subsection \<open>Restricted measure spaces\<close>
  1.1959 -
  1.1960 -lemma integrable_restrict_space:
  1.1961 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1962 -  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  1.1963 -  shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  1.1964 -  unfolding integrable_iff_bounded
  1.1965 -    borel_measurable_restrict_space_iff[OF \<Omega>]
  1.1966 -    nn_integral_restrict_space[OF \<Omega>]
  1.1967 -  by (simp add: ac_simps ennreal_indicator ennreal_mult)
  1.1968 -
  1.1969 -lemma integral_restrict_space:
  1.1970 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1971 -  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  1.1972 -  shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  1.1973 -proof (rule integral_eq_cases)
  1.1974 -  assume "integrable (restrict_space M \<Omega>) f"
  1.1975 -  then show ?thesis
  1.1976 -  proof induct
  1.1977 -    case (base A c) then show ?case
  1.1978 -      by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
  1.1979 -                    emeasure_restrict_space Int_absorb1 measure_restrict_space)
  1.1980 -  next
  1.1981 -    case (add g f) then show ?case
  1.1982 -      by (simp add: scaleR_add_right integrable_restrict_space)
  1.1983 -  next
  1.1984 -    case (lim f s)
  1.1985 -    show ?case
  1.1986 -    proof (rule LIMSEQ_unique)
  1.1987 -      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) \<longlonglongrightarrow> integral\<^sup>L (restrict_space M \<Omega>) f"
  1.1988 -        using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
  1.1989 -
  1.1990 -      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) \<longlonglongrightarrow> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
  1.1991 -        unfolding lim
  1.1992 -        using lim
  1.1993 -        by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
  1.1994 -           (auto simp add: space_restrict_space integrable_restrict_space simp del: norm_scaleR
  1.1995 -                 split: split_indicator)
  1.1996 -    qed
  1.1997 -  qed
  1.1998 -qed (simp add: integrable_restrict_space)
  1.1999 -
  1.2000 -lemma integral_empty:
  1.2001 -  assumes "space M = {}"
  1.2002 -  shows "integral\<^sup>L M f = 0"
  1.2003 -proof -
  1.2004 -  have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
  1.2005 -    by(rule integral_cong)(simp_all add: assms)
  1.2006 -  thus ?thesis by simp
  1.2007 -qed
  1.2008 -
  1.2009 -subsection \<open>Measure spaces with an associated density\<close>
  1.2010 -
  1.2011 -lemma integrable_density:
  1.2012 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1.2013 -  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1.2014 -    and nn: "AE x in M. 0 \<le> g x"
  1.2015 -  shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
  1.2016 -  unfolding integrable_iff_bounded using nn
  1.2017 -  apply (simp add: nn_integral_density less_top[symmetric])
  1.2018 -  apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
  1.2019 -  apply (auto simp: ennreal_mult)
  1.2020 -  done
  1.2021 -
  1.2022 -lemma integral_density:
  1.2023 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1.2024 -  assumes f: "f \<in> borel_measurable M"
  1.2025 -    and g[measurable]: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
  1.2026 -  shows "integral\<^sup>L (density M g) f = integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
  1.2027 -proof (rule integral_eq_cases)
  1.2028 -  assume "integrable (density M g) f"
  1.2029 -  then show ?thesis
  1.2030 -  proof induct
  1.2031 -    case (base A c)
  1.2032 -    then have [measurable]: "A \<in> sets M" by auto
  1.2033 -
  1.2034 -    have int: "integrable M (\<lambda>x. g x * indicator A x)"
  1.2035 -      using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
  1.2036 -    then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ennreal (g x * indicator A x) \<partial>M)"
  1.2037 -      using g by (subst nn_integral_eq_integral) auto
  1.2038 -    also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (g x) * indicator A x \<partial>M)"
  1.2039 -      by (intro nn_integral_cong) (auto split: split_indicator)
  1.2040 -    also have "\<dots> = emeasure (density M g) A"
  1.2041 -      by (rule emeasure_density[symmetric]) auto
  1.2042 -    also have "\<dots> = ennreal (measure (density M g) A)"
  1.2043 -      using base by (auto intro: emeasure_eq_ennreal_measure)
  1.2044 -    also have "\<dots> = integral\<^sup>L (density M g) (indicator A)"
  1.2045 -      using base by simp
  1.2046 -    finally show ?case
  1.2047 -      using base g
  1.2048 -      apply (simp add: int integral_nonneg_AE)
  1.2049 -      apply (subst (asm) ennreal_inj)
  1.2050 -      apply (auto intro!: integral_nonneg_AE)
  1.2051 -      done
  1.2052 -  next
  1.2053 -    case (add f h)
  1.2054 -    then have [measurable]: "f \<in> borel_measurable M" "h \<in> borel_measurable M"
  1.2055 -      by (auto dest!: borel_measurable_integrable)
  1.2056 -    from add g show ?case
  1.2057 -      by (simp add: scaleR_add_right integrable_density)
  1.2058 -  next
  1.2059 -    case (lim f s)
  1.2060 -    have [measurable]: "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M"
  1.2061 -      using lim(1,5)[THEN borel_measurable_integrable] by auto
  1.2062 -
  1.2063 -    show ?case
  1.2064 -    proof (rule LIMSEQ_unique)
  1.2065 -      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)"
  1.2066 -      proof (rule integral_dominated_convergence)
  1.2067 -        show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
  1.2068 -          by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
  1.2069 -        show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) \<longlonglongrightarrow> g x *\<^sub>R f x"
  1.2070 -          using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M])
  1.2071 -        show "\<And>i. AE x in M. norm (g x *\<^sub>R s i x) \<le> 2 * norm (g x *\<^sub>R f x)"
  1.2072 -          using lim(4) g by (auto intro!: AE_I2[of M] mult_left_mono simp: field_simps)
  1.2073 -      qed auto
  1.2074 -      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) \<longlonglongrightarrow> integral\<^sup>L (density M g) f"
  1.2075 -        unfolding lim(2)[symmetric]
  1.2076 -        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  1.2077 -           (insert lim(3-5), auto)
  1.2078 -    qed
  1.2079 -  qed
  1.2080 -qed (simp add: f g integrable_density)
  1.2081 -
  1.2082 -lemma
  1.2083 -  fixes g :: "'a \<Rightarrow> real"
  1.2084 -  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "g \<in> borel_measurable M"
  1.2085 -  shows integral_real_density: "integral\<^sup>L (density M f) g = (\<integral> x. f x * g x \<partial>M)"
  1.2086 -    and integrable_real_density: "integrable (density M f) g \<longleftrightarrow> integrable M (\<lambda>x. f x * g x)"
  1.2087 -  using assms integral_density[of g M f] integrable_density[of g M f] by auto
  1.2088 -
  1.2089 -lemma has_bochner_integral_density:
  1.2090 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1.2091 -  shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. 0 \<le> g x) \<Longrightarrow>
  1.2092 -    has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
  1.2093 -  by (simp add: has_bochner_integral_iff integrable_density integral_density)
  1.2094 -
  1.2095 -subsection \<open>Distributions\<close>
  1.2096 -
  1.2097 -lemma integrable_distr_eq:
  1.2098 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.2099 -  assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
  1.2100 -  shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
  1.2101 -  unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
  1.2102 -
  1.2103 -lemma integrable_distr:
  1.2104 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.2105 -  shows "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
  1.2106 -  by (subst integrable_distr_eq[symmetric, where g=T])
  1.2107 -     (auto dest: borel_measurable_integrable)
  1.2108 -
  1.2109 -lemma integral_distr:
  1.2110 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.2111 -  assumes g[measurable]: "g \<in> measurable M N" and f: "f \<in> borel_measurable N"
  1.2112 -  shows "integral\<^sup>L (distr M N g) f = integral\<^sup>L M (\<lambda>x. f (g x))"
  1.2113 -proof (rule integral_eq_cases)
  1.2114 -  assume "integrable (distr M N g) f"
  1.2115 -  then show ?thesis
  1.2116 -  proof induct
  1.2117 -    case (base A c)
  1.2118 -    then have [measurable]: "A \<in> sets N" by auto
  1.2119 -    from base have int: "integrable (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c)"
  1.2120 -      by (intro integrable_indicator)
  1.2121 -
  1.2122 -    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"
  1.2123 -      using base by auto
  1.2124 -    also have "\<dots> = measure M (g -` A \<inter> space M) *\<^sub>R c"
  1.2125 -      by (subst measure_distr) auto
  1.2126 -    also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator (g -` A \<inter> space M) a *\<^sub>R c)"
  1.2127 -      using base by (auto simp: emeasure_distr)
  1.2128 -    also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator A (g a) *\<^sub>R c)"
  1.2129 -      using int base by (intro integral_cong_AE) (auto simp: emeasure_distr split: split_indicator)
  1.2130 -    finally show ?case .
  1.2131 -  next
  1.2132 -    case (add f h)
  1.2133 -    then have [measurable]: "f \<in> borel_measurable N" "h \<in> borel_measurable N"
  1.2134 -      by (auto dest!: borel_measurable_integrable)
  1.2135 -    from add g show ?case
  1.2136 -      by (simp add: scaleR_add_right integrable_distr_eq)
  1.2137 -  next
  1.2138 -    case (lim f s)
  1.2139 -    have [measurable]: "f \<in> borel_measurable N" "\<And>i. s i \<in> borel_measurable N"
  1.2140 -      using lim(1,5)[THEN borel_measurable_integrable] by auto
  1.2141 -
  1.2142 -    show ?case
  1.2143 -    proof (rule LIMSEQ_unique)
  1.2144 -      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) \<longlonglongrightarrow> integral\<^sup>L M (\<lambda>x. f (g x))"
  1.2145 -      proof (rule integral_dominated_convergence)
  1.2146 -        show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
  1.2147 -          using lim by (auto simp: integrable_distr_eq)
  1.2148 -        show "AE x in M. (\<lambda>i. s i (g x)) \<longlonglongrightarrow> f (g x)"
  1.2149 -          using lim(3) g[THEN measurable_space] by auto
  1.2150 -        show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
  1.2151 -          using lim(4) g[THEN measurable_space] by auto
  1.2152 -      qed auto
  1.2153 -      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) \<longlonglongrightarrow> integral\<^sup>L (distr M N g) f"
  1.2154 -        unfolding lim(2)[symmetric]
  1.2155 -        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  1.2156 -           (insert lim(3-5), auto)
  1.2157 -    qed
  1.2158 -  qed
  1.2159 -qed (simp add: f g integrable_distr_eq)
  1.2160 -
  1.2161 -lemma has_bochner_integral_distr:
  1.2162 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.2163 -  shows "f \<in> borel_measurable N \<Longrightarrow> g \<in> measurable M N \<Longrightarrow>
  1.2164 -    has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
  1.2165 -  by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
  1.2166 -
  1.2167 -subsection \<open>Lebesgue integration on @{const count_space}\<close>
  1.2168 -
  1.2169 -lemma integrable_count_space:
  1.2170 -  fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  1.2171 -  shows "finite X \<Longrightarrow> integrable (count_space X) f"
  1.2172 -  by (auto simp: nn_integral_count_space integrable_iff_bounded)
  1.2173 -
  1.2174 -lemma measure_count_space[simp]:
  1.2175 -  "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
  1.2176 -  unfolding measure_def by (subst emeasure_count_space ) auto
  1.2177 -
  1.2178 -lemma lebesgue_integral_count_space_finite_support:
  1.2179 -  assumes f: "finite {a\<in>A. f a \<noteq> 0}"
  1.2180 -  shows "(\<integral>x. f x \<partial>count_space A) = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. f a)"
  1.2181 -proof -
  1.2182 -  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)"
  1.2183 -    by (intro setsum.mono_neutral_cong_left) auto
  1.2184 -
  1.2185 -  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)"
  1.2186 -    by (intro integral_cong refl) (simp add: f eq)
  1.2187 -  also have "\<dots> = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. measure (count_space A) {a} *\<^sub>R f a)"
  1.2188 -    by (subst integral_setsum) (auto intro!: setsum.cong)
  1.2189 -  finally show ?thesis
  1.2190 -    by auto
  1.2191 -qed
  1.2192 -
  1.2193 -lemma lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
  1.2194 -  by (subst lebesgue_integral_count_space_finite_support)
  1.2195 -     (auto intro!: setsum.mono_neutral_cong_left)
  1.2196 -
  1.2197 -lemma integrable_count_space_nat_iff:
  1.2198 -  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.2199 -  shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
  1.2200 -  by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat ennreal_suminf_neq_top
  1.2201 -           intro:  summable_suminf_not_top)
  1.2202 -
  1.2203 -lemma sums_integral_count_space_nat:
  1.2204 -  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.2205 -  assumes *: "integrable (count_space UNIV) f"
  1.2206 -  shows "f sums (integral\<^sup>L (count_space UNIV) f)"
  1.2207 -proof -
  1.2208 -  let ?f = "\<lambda>n i. indicator {n} i *\<^sub>R f i"
  1.2209 -  have f': "\<And>n i. ?f n i = indicator {n} i *\<^sub>R f n"
  1.2210 -    by (auto simp: fun_eq_iff split: split_indicator)
  1.2211 -
  1.2212 -  have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) sums \<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV"
  1.2213 -  proof (rule sums_integral)
  1.2214 -    show "\<And>i. integrable (count_space UNIV) (?f i)"
  1.2215 -      using * by (intro integrable_mult_indicator) auto
  1.2216 -    show "AE n in count_space UNIV. summable (\<lambda>i. norm (?f i n))"
  1.2217 -      using summable_finite[of "{n}" "\<lambda>i. norm (?f i n)" for n] by simp
  1.2218 -    show "summable (\<lambda>i. \<integral> n. norm (?f i n) \<partial>count_space UNIV)"
  1.2219 -      using * by (subst f') (simp add: integrable_count_space_nat_iff)
  1.2220 -  qed
  1.2221 -  also have "(\<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV) = (\<integral>n. f n \<partial>count_space UNIV)"
  1.2222 -    using suminf_finite[of "{n}" "\<lambda>i. ?f i n" for n] by (auto intro!: integral_cong)
  1.2223 -  also have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) = f"
  1.2224 -    by (subst f') simp
  1.2225 -  finally show ?thesis .
  1.2226 -qed
  1.2227 -
  1.2228 -lemma integral_count_space_nat:
  1.2229 -  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.2230 -  shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
  1.2231 -  using sums_integral_count_space_nat by (rule sums_unique)
  1.2232 -
  1.2233 -subsection \<open>Point measure\<close>
  1.2234 -
  1.2235 -lemma lebesgue_integral_point_measure_finite:
  1.2236 -  fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.2237 -  shows "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow>
  1.2238 -    integral\<^sup>L (point_measure A f) g = (\<Sum>a\<in>A. f a *\<^sub>R g a)"
  1.2239 -  by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def)
  1.2240 -
  1.2241 -lemma integrable_point_measure_finite:
  1.2242 -  fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and f :: "'a \<Rightarrow> real"
  1.2243 -  shows "finite A \<Longrightarrow> integrable (point_measure A f) g"
  1.2244 -  unfolding point_measure_def
  1.2245 -  apply (subst density_cong[where f'="\<lambda>x. ennreal (max 0 (f x))"])
  1.2246 -  apply (auto split: split_max simp: ennreal_neg)
  1.2247 -  apply (subst integrable_density)
  1.2248 -  apply (auto simp: AE_count_space integrable_count_space)
  1.2249 -  done
  1.2250 -
  1.2251 -subsection \<open>Lebesgue integration on @{const null_measure}\<close>
  1.2252 -
  1.2253 -lemma has_bochner_integral_null_measure_iff[iff]:
  1.2254 -  "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
  1.2255 -  by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
  1.2256 -           intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
  1.2257 -
  1.2258 -lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
  1.2259 -  by (auto simp add: integrable.simps)
  1.2260 -
  1.2261 -lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
  1.2262 -  by (cases "integrable (null_measure M) f")
  1.2263 -     (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
  1.2264 -
  1.2265 -subsection \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
  1.2266 -
  1.2267 -lemma real_lebesgue_integral_def:
  1.2268 -  assumes f[measurable]: "integrable M f"
  1.2269 -  shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+x. f x \<partial>M) - enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
  1.2270 -proof -
  1.2271 -  have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
  1.2272 -    by (auto intro!: arg_cong[where f="integral\<^sup>L M"])
  1.2273 -  also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
  1.2274 -    by (intro integral_diff integrable_max integrable_minus integrable_zero f)
  1.2275 -  also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = enn2real (\<integral>\<^sup>+x. ennreal (f x) \<partial>M)"
  1.2276 -    by (subst integral_eq_nn_integral) (auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: max_def ennreal_neg)
  1.2277 -  also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
  1.2278 -    by (subst integral_eq_nn_integral) (auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: max_def ennreal_neg)
  1.2279 -  finally show ?thesis .
  1.2280 -qed
  1.2281 -
  1.2282 -lemma real_integrable_def:
  1.2283 -  "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
  1.2284 -    (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1.2285 -  unfolding integrable_iff_bounded
  1.2286 -proof (safe del: notI)
  1.2287 -  assume *: "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  1.2288 -  have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1.2289 -    by (intro nn_integral_mono) auto
  1.2290 -  also note *
  1.2291 -  finally show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>"
  1.2292 -    by simp
  1.2293 -  have "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1.2294 -    by (intro nn_integral_mono) auto
  1.2295 -  also note *
  1.2296 -  finally show "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1.2297 -    by simp
  1.2298 -next
  1.2299 -  assume [measurable]: "f \<in> borel_measurable M"
  1.2300 -  assume fin: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1.2301 -  have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (f x) + ennreal (- f x) \<partial>M)"
  1.2302 -    by (intro nn_integral_cong) (auto simp: abs_real_def ennreal_neg)
  1.2303 -  also have"\<dots> = (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) + (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M)"
  1.2304 -    by (intro nn_integral_add) auto
  1.2305 -  also have "\<dots> < \<infinity>"
  1.2306 -    using fin by (auto simp: less_top)
  1.2307 -  finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
  1.2308 -qed
  1.2309 -
  1.2310 -lemma integrableD[dest]:
  1.2311 -  assumes "integrable M f"
  1.2312 -  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>"
  1.2313 -  using assms unfolding real_integrable_def by auto
  1.2314 -
  1.2315 -lemma integrableE:
  1.2316 -  assumes "integrable M f"
  1.2317 -  obtains r q where
  1.2318 -    "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M) = ennreal r"
  1.2319 -    "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M) = ennreal q"
  1.2320 -    "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
  1.2321 -  using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
  1.2322 -  by (cases rule: ennreal2_cases[of "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M)"]) auto
  1.2323 -
  1.2324 -lemma integral_monotone_convergence_nonneg:
  1.2325 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  1.2326 -  assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  1.2327 -    and pos: "\<And>i. AE x in M. 0 \<le> f i x"
  1.2328 -    and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
  1.2329 -    and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) \<longlonglongrightarrow> x"
  1.2330 -    and u: "u \<in> borel_measurable M"
  1.2331 -  shows "integrable M u"
  1.2332 -  and "integral\<^sup>L M u = x"
  1.2333 -proof -
  1.2334 -  have nn: "AE x in M. \<forall>i. 0 \<le> f i x"
  1.2335 -    using pos unfolding AE_all_countable by auto
  1.2336 -  with lim have u_nn: "AE x in M. 0 \<le> u x"
  1.2337 -    by eventually_elim (auto intro: LIMSEQ_le_const)
  1.2338 -  have [simp]: "0 \<le> x"
  1.2339 -    by (intro LIMSEQ_le_const[OF ilim] allI exI impI integral_nonneg_AE pos)
  1.2340 -  have "(\<integral>\<^sup>+ x. ennreal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ennreal (f n x) \<partial>M))"
  1.2341 -  proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
  1.2342 -    fix i
  1.2343 -    from mono nn show "AE x in M. ennreal (f i x) \<le> ennreal (f (Suc i) x)"
  1.2344 -      by eventually_elim (auto simp: mono_def)
  1.2345 -    show "(\<lambda>x. ennreal (f i x)) \<in> borel_measurable M"
  1.2346 -      using i by auto
  1.2347 -  next
  1.2348 -    show "(\<integral>\<^sup>+ x. ennreal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ennreal (f i x)) \<partial>M"
  1.2349 -      apply (rule nn_integral_cong_AE)
  1.2350 -      using lim mono nn u_nn
  1.2351 -      apply eventually_elim
  1.2352 -      apply (simp add: LIMSEQ_unique[OF _ LIMSEQ_SUP] incseq_def)
  1.2353 -      done
  1.2354 -  qed
  1.2355 -  also have "\<dots> = ennreal x"
  1.2356 -    using mono i nn unfolding nn_integral_eq_integral[OF i pos]
  1.2357 -    by (subst LIMSEQ_unique[OF LIMSEQ_SUP]) (auto simp: mono_def integral_nonneg_AE pos intro!: integral_mono_AE ilim)
  1.2358 -  finally have "(\<integral>\<^sup>+ x. ennreal (u x) \<partial>M) = ennreal x" .
  1.2359 -  moreover have "(\<integral>\<^sup>+ x. ennreal (- u x) \<partial>M) = 0"
  1.2360 -    using u u_nn by (subst nn_integral_0_iff_AE) (auto simp add: ennreal_neg)
  1.2361 -  ultimately show "integrable M u" "integral\<^sup>L M u = x"
  1.2362 -    by (auto simp: real_integrable_def real_lebesgue_integral_def u)
  1.2363 -qed
  1.2364 -
  1.2365 -lemma
  1.2366 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  1.2367 -  assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  1.2368 -  and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
  1.2369 -  and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) \<longlonglongrightarrow> x"
  1.2370 -  and u: "u \<in> borel_measurable M"
  1.2371 -  shows integrable_monotone_convergence: "integrable M u"
  1.2372 -    and integral_monotone_convergence: "integral\<^sup>L M u = x"
  1.2373 -    and has_bochner_integral_monotone_convergence: "has_bochner_integral M u x"
  1.2374 -proof -
  1.2375 -  have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
  1.2376 -    using f by auto
  1.2377 -  have 2: "AE x in M. mono (\<lambda>n. f n x - f 0 x)"
  1.2378 -    using mono by (auto simp: mono_def le_fun_def)
  1.2379 -  have 3: "\<And>n. AE x in M. 0 \<le> f n x - f 0 x"
  1.2380 -    using mono by (auto simp: field_simps mono_def le_fun_def)
  1.2381 -  have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) \<longlonglongrightarrow> u x - f 0 x"
  1.2382 -    using lim by (auto intro!: tendsto_diff)
  1.2383 -  have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) \<longlonglongrightarrow> x - integral\<^sup>L M (f 0)"
  1.2384 -    using f ilim by (auto intro!: tendsto_diff)
  1.2385 -  have 6: "(\<lambda>x. u x - f 0 x) \<in> borel_measurable M"
  1.2386 -    using f[of 0] u by auto
  1.2387 -  note diff = integral_monotone_convergence_nonneg[OF 1 2 3 4 5 6]
  1.2388 -  have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
  1.2389 -    using diff(1) f by (rule integrable_add)
  1.2390 -  with diff(2) f show "integrable M u" "integral\<^sup>L M u = x"
  1.2391 -    by auto
  1.2392 -  then show "has_bochner_integral M u x"
  1.2393 -    by (metis has_bochner_integral_integrable)
  1.2394 -qed
  1.2395 -
  1.2396 -lemma integral_norm_eq_0_iff:
  1.2397 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.2398 -  assumes f[measurable]: "integrable M f"
  1.2399 -  shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
  1.2400 -proof -
  1.2401 -  have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>x. norm (f x) \<partial>M)"
  1.2402 -    using f by (intro nn_integral_eq_integral integrable_norm) auto
  1.2403 -  then have "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) = 0"
  1.2404 -    by simp
  1.2405 -  also have "\<dots> \<longleftrightarrow> emeasure M {x\<in>space M. ennreal (norm (f x)) \<noteq> 0} = 0"
  1.2406 -    by (intro nn_integral_0_iff) auto
  1.2407 -  finally show ?thesis
  1.2408 -    by simp
  1.2409 -qed
  1.2410 -
  1.2411 -lemma integral_0_iff:
  1.2412 -  fixes f :: "'a \<Rightarrow> real"
  1.2413 -  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"
  1.2414 -  using integral_norm_eq_0_iff[of M f] by simp
  1.2415 -
  1.2416 -lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
  1.2417 -  using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong add: less_top[symmetric])
  1.2418 -
  1.2419 -lemma lebesgue_integral_const[simp]:
  1.2420 -  fixes a :: "'a :: {banach, second_countable_topology}"
  1.2421 -  shows "(\<integral>x. a \<partial>M) = measure M (space M) *\<^sub>R a"
  1.2422 -proof -
  1.2423 -  { assume "emeasure M (space M) = \<infinity>" "a \<noteq> 0"
  1.2424 -    then have ?thesis
  1.2425 -      by (auto simp add: not_integrable_integral_eq ennreal_mult_less_top measure_def integrable_iff_bounded) }
  1.2426 -  moreover
  1.2427 -  { assume "a = 0" then have ?thesis by simp }
  1.2428 -  moreover
  1.2429 -  { assume "emeasure M (space M) \<noteq> \<infinity>"
  1.2430 -    interpret finite_measure M
  1.2431 -      proof qed fact
  1.2432 -    have "(\<integral>x. a \<partial>M) = (\<integral>x. indicator (space M) x *\<^sub>R a \<partial>M)"
  1.2433 -      by (intro integral_cong) auto
  1.2434 -    also have "\<dots> = measure M (space M) *\<^sub>R a"
  1.2435 -      by (simp add: less_top[symmetric])
  1.2436 -    finally have ?thesis . }
  1.2437 -  ultimately show ?thesis by blast
  1.2438 -qed
  1.2439 -
  1.2440 -lemma (in finite_measure) integrable_const_bound:
  1.2441 -  fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  1.2442 -  shows "AE x in M. norm (f x) \<le> B \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> integrable M f"
  1.2443 -  apply (rule integrable_bound[OF integrable_const[of B], of f])
  1.2444 -  apply assumption
  1.2445 -  apply (cases "0 \<le> B")
  1.2446 -  apply auto
  1.2447 -  done
  1.2448 -
  1.2449 -lemma integral_indicator_finite_real:
  1.2450 -  fixes f :: "'a \<Rightarrow> real"
  1.2451 -  assumes [simp]: "finite A"
  1.2452 -  assumes [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"
  1.2453 -  assumes finite: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} < \<infinity>"
  1.2454 -  shows "(\<integral>x. f x * indicator A x \<partial>M) = (\<Sum>a\<in>A. f a * measure M {a})"
  1.2455 -proof -
  1.2456 -  have "(\<integral>x. f x * indicator A x \<partial>M) = (\<integral>x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
  1.2457 -  proof (intro integral_cong refl)
  1.2458 -    fix x show "f x * indicator A x = (\<Sum>a\<in>A. f a * indicator {a} x)"
  1.2459 -      by (auto split: split_indicator simp: eq_commute[of x] cong: conj_cong)
  1.2460 -  qed
  1.2461 -  also have "\<dots> = (\<Sum>a\<in>A. f a * measure M {a})"
  1.2462 -    using finite by (subst integral_setsum) (auto simp add: integrable_mult_left_iff)
  1.2463 -  finally show ?thesis .
  1.2464 -qed
  1.2465 -
  1.2466 -lemma (in finite_measure) ennreal_integral_real:
  1.2467 -  assumes [measurable]: "f \<in> borel_measurable M"
  1.2468 -  assumes ae: "AE x in M. f x \<le> ennreal B" "0 \<le> B"
  1.2469 -  shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1.2470 -proof (subst nn_integral_eq_integral[symmetric])
  1.2471 -  show "integrable M (\<lambda>x. enn2real (f x))"
  1.2472 -    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI enn2real_nonneg)
  1.2473 -  show "(\<integral>\<^sup>+ x. ennreal (enn2real (f x)) \<partial>M) = integral\<^sup>N M f"
  1.2474 -    using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
  1.2475 -qed (auto simp: enn2real_nonneg)
  1.2476 -
  1.2477 -lemma (in finite_measure) integral_less_AE:
  1.2478 -  fixes X Y :: "'a \<Rightarrow> real"
  1.2479 -  assumes int: "integrable M X" "integrable M Y"
  1.2480 -  assumes A: "(emeasure M) A \<noteq> 0" "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> X x \<noteq> Y x"
  1.2481 -  assumes gt: "AE x in M. X x \<le> Y x"
  1.2482 -  shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  1.2483 -proof -
  1.2484 -  have "integral\<^sup>L M X \<le> integral\<^sup>L M Y"
  1.2485 -    using gt int by (intro integral_mono_AE) auto
  1.2486 -  moreover
  1.2487 -  have "integral\<^sup>L M X \<noteq> integral\<^sup>L M Y"
  1.2488 -  proof
  1.2489 -    assume eq: "integral\<^sup>L M X = integral\<^sup>L M Y"
  1.2490 -    have "integral\<^sup>L M (\<lambda>x. \<bar>Y x - X x\<bar>) = integral\<^sup>L M (\<lambda>x. Y x - X x)"
  1.2491 -      using gt int by (intro integral_cong_AE) auto
  1.2492 -    also have "\<dots> = 0"
  1.2493 -      using eq int by simp
  1.2494 -    finally have "(emeasure M) {x \<in> space M. Y x - X x \<noteq> 0} = 0"
  1.2495 -      using int by (simp add: integral_0_iff)
  1.2496 -    moreover
  1.2497 -    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)"
  1.2498 -      using A by (intro nn_integral_mono_AE) auto
  1.2499 -    then have "(emeasure M) A \<le> (emeasure M) {x \<in> space M. Y x - X x \<noteq> 0}"
  1.2500 -      using int A by (simp add: integrable_def)
  1.2501 -    ultimately have "emeasure M A = 0"
  1.2502 -      by simp
  1.2503 -    with \<open>(emeasure M) A \<noteq> 0\<close> show False by auto
  1.2504 -  qed
  1.2505 -  ultimately show ?thesis by auto
  1.2506 -qed
  1.2507 -
  1.2508 -lemma (in finite_measure) integral_less_AE_space:
  1.2509 -  fixes X Y :: "'a \<Rightarrow> real"
  1.2510 -  assumes int: "integrable M X" "integrable M Y"
  1.2511 -  assumes gt: "AE x in M. X x < Y x" "emeasure M (space M) \<noteq> 0"
  1.2512 -  shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  1.2513 -  using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
  1.2514 -
  1.2515 -lemma tendsto_integral_at_top:
  1.2516 -  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
  1.2517 -  assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
  1.2518 -  shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) \<longlongrightarrow> \<integral> x. f x \<partial>M) at_top"
  1.2519 -proof (rule tendsto_at_topI_sequentially)
  1.2520 -  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
  1.2521 -  show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) \<longlonglongrightarrow> integral\<^sup>L M f"
  1.2522 -  proof (rule integral_dominated_convergence)
  1.2523 -    show "integrable M (\<lambda>x. norm (f x))"
  1.2524 -      by (rule integrable_norm) fact
  1.2525 -    show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
  1.2526 -    proof
  1.2527 -      fix x
  1.2528 -      from \<open>filterlim X at_top sequentially\<close>
  1.2529 -      have "eventually (\<lambda>n. x \<le> X n) sequentially"
  1.2530 -        unfolding filterlim_at_top_ge[where c=x] by auto
  1.2531 -      then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
  1.2532 -        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
  1.2533 -    qed
  1.2534 -    fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
  1.2535 -      by (auto split: split_indicator)
  1.2536 -  qed auto
  1.2537 -qed
  1.2538 -
  1.2539 -lemma
  1.2540 -  fixes f :: "real \<Rightarrow> real"
  1.2541 -  assumes M: "sets M = sets borel"
  1.2542 -  assumes nonneg: "AE x in M. 0 \<le> f x"
  1.2543 -  assumes borel: "f \<in> borel_measurable borel"
  1.2544 -  assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
  1.2545 -  assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) \<longlongrightarrow> x) at_top"
  1.2546 -  shows has_bochner_integral_monotone_convergence_at_top: "has_bochner_integral M f x"
  1.2547 -    and integrable_monotone_convergence_at_top: "integrable M f"
  1.2548 -    and integral_monotone_convergence_at_top:"integral\<^sup>L M f = x"
  1.2549 -proof -
  1.2550 -  from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
  1.2551 -    by (auto split: split_indicator intro!: monoI)
  1.2552 -  { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
  1.2553 -      by (rule eventually_sequentiallyI[of "nat \<lceil>x\<rceil>"])
  1.2554 -         (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
  1.2555 -  from filterlim_cong[OF refl refl this]
  1.2556 -  have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) \<longlonglongrightarrow> f x"
  1.2557 -    by simp
  1.2558 -  have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) \<longlonglongrightarrow> x"
  1.2559 -    using conv filterlim_real_sequentially by (rule filterlim_compose)
  1.2560 -  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
  1.2561 -    using M by (simp add: sets_eq_imp_space_eq measurable_def)
  1.2562 -  have "f \<in> borel_measurable M"
  1.2563 -    using borel by simp
  1.2564 -  show "has_bochner_integral M f x"
  1.2565 -    by (rule has_bochner_integral_monotone_convergence) fact+
  1.2566 -  then show "integrable M f" "integral\<^sup>L M f = x"
  1.2567 -    by (auto simp: _has_bochner_integral_iff)
  1.2568 -qed
  1.2569 -
  1.2570 -subsection \<open>Product measure\<close>
  1.2571 -
  1.2572 -lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
  1.2573 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2574 -  assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  1.2575 -  shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
  1.2576 -proof -
  1.2577 -  have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
  1.2578 -    unfolding integrable_iff_bounded by simp
  1.2579 -  show ?thesis
  1.2580 -    by (simp cong: measurable_cong)
  1.2581 -qed
  1.2582 -
  1.2583 -lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
  1.2584 -
  1.2585 -lemma (in sigma_finite_measure) measurable_measure[measurable (raw)]:
  1.2586 -  "(\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M) \<Longrightarrow>
  1.2587 -    {x \<in> space (N \<Otimes>\<^sub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^sub>M M) \<Longrightarrow>
  1.2588 -    (\<lambda>x. measure M (A x)) \<in> borel_measurable N"
  1.2589 -  unfolding measure_def by (intro measurable_emeasure borel_measurable_enn2real) auto
  1.2590 -
  1.2591 -lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
  1.2592 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2593 -  assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  1.2594 -  shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
  1.2595 -proof -
  1.2596 -  from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
  1.2597 -  then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
  1.2598 -    "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
  1.2599 -    "\<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)"
  1.2600 -    by (auto simp: space_pair_measure)
  1.2601 -
  1.2602 -  have [measurable]: "\<And>i. s i \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  1.2603 -    by (rule borel_measurable_simple_function) fact
  1.2604 -
  1.2605 -  have "\<And>i. s i \<in> measurable (N \<Otimes>\<^sub>M M) (count_space UNIV)"
  1.2606 -    by (rule measurable_simple_function) fact
  1.2607 -
  1.2608 -  define f' where [abs_def]: "f' i x =
  1.2609 -    (if integrable M (f x) then simple_bochner_integral M (\<lambda>y. s i (x, y)) else 0)" for i x
  1.2610 -
  1.2611 -  { fix i x assume "x \<in> space N"
  1.2612 -    then have "simple_bochner_integral M (\<lambda>y. s i (x, y)) =
  1.2613 -      (\<Sum>z\<in>s i ` (space N \<times> space M). measure M {y \<in> space M. s i (x, y) = z} *\<^sub>R z)"
  1.2614 -      using s(1)[THEN simple_functionD(1)]
  1.2615 -      unfolding simple_bochner_integral_def
  1.2616 -      by (intro setsum.mono_neutral_cong_left)
  1.2617 -         (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
  1.2618 -  note eq = this
  1.2619 -
  1.2620 -  show ?thesis
  1.2621 -  proof (rule borel_measurable_LIMSEQ_metric)
  1.2622 -    fix i show "f' i \<in> borel_measurable N"
  1.2623 -      unfolding f'_def by (simp_all add: eq cong: measurable_cong if_cong)
  1.2624 -  next
  1.2625 -    fix x assume x: "x \<in> space N"
  1.2626 -    { assume int_f: "integrable M (f x)"
  1.2627 -      have int_2f: "integrable M (\<lambda>y. 2 * norm (f x y))"
  1.2628 -        by (intro integrable_norm integrable_mult_right int_f)
  1.2629 -      have "(\<lambda>i. integral\<^sup>L M (\<lambda>y. s i (x, y))) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
  1.2630 -      proof (rule integral_dominated_convergence)
  1.2631 -        from int_f show "f x \<in> borel_measurable M" by auto
  1.2632 -        show "\<And>i. (\<lambda>y. s i (x, y)) \<in> borel_measurable M"
  1.2633 -          using x by simp
  1.2634 -        show "AE xa in M. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f x xa"
  1.2635 -          using x s(2) by auto
  1.2636 -        show "\<And>i. AE xa in M. norm (s i (x, xa)) \<le> 2 * norm (f x xa)"
  1.2637 -          using x s(3) by auto
  1.2638 -      qed fact
  1.2639 -      moreover
  1.2640 -      { fix i
  1.2641 -        have "simple_bochner_integrable M (\<lambda>y. s i (x, y))"
  1.2642 -        proof (rule simple_bochner_integrableI_bounded)
  1.2643 -          have "(\<lambda>y. s i (x, y)) ` space M \<subseteq> s i ` (space N \<times> space M)"
  1.2644 -            using x by auto
  1.2645 -          then show "simple_function M (\<lambda>y. s i (x, y))"
  1.2646 -            using simple_functionD(1)[OF s(1), of i] x
  1.2647 -            by (intro simple_function_borel_measurable)
  1.2648 -               (auto simp: space_pair_measure dest: finite_subset)
  1.2649 -          have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
  1.2650 -            using x s by (intro nn_integral_mono) auto
  1.2651 -          also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
  1.2652 -            using int_2f by (simp add: integrable_iff_bounded)
  1.2653 -          finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
  1.2654 -        qed
  1.2655 -        then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"
  1.2656 -          by (rule simple_bochner_integrable_eq_integral[symmetric]) }
  1.2657 -      ultimately have "(\<lambda>i. simple_bochner_integral M (\<lambda>y. s i (x, y))) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
  1.2658 -        by simp }
  1.2659 -    then
  1.2660 -    show "(\<lambda>i. f' i x) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
  1.2661 -      unfolding f'_def
  1.2662 -      by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
  1.2663 -  qed
  1.2664 -qed
  1.2665 -
  1.2666 -lemma (in pair_sigma_finite) integrable_product_swap:
  1.2667 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2668 -  assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.2669 -  shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
  1.2670 -proof -
  1.2671 -  interpret Q: pair_sigma_finite M2 M1 ..
  1.2672 -  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  1.2673 -  show ?thesis unfolding *
  1.2674 -    by (rule integrable_distr[OF measurable_pair_swap'])
  1.2675 -       (simp add: distr_pair_swap[symmetric] assms)
  1.2676 -qed
  1.2677 -
  1.2678 -lemma (in pair_sigma_finite) integrable_product_swap_iff:
  1.2679 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2680 -  shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.2681 -proof -
  1.2682 -  interpret Q: pair_sigma_finite M2 M1 ..
  1.2683 -  from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
  1.2684 -  show ?thesis by auto
  1.2685 -qed
  1.2686 -
  1.2687 -lemma (in pair_sigma_finite) integral_product_swap:
  1.2688 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2689 -  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  1.2690 -  shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  1.2691 -proof -
  1.2692 -  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  1.2693 -  show ?thesis unfolding *
  1.2694 -    by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
  1.2695 -qed
  1.2696 -
  1.2697 -lemma (in pair_sigma_finite) Fubini_integrable:
  1.2698 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2699 -  assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  1.2700 -    and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
  1.2701 -    and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  1.2702 -  shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.2703 -proof (rule integrableI_bounded)
  1.2704 -  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)"
  1.2705 -    by (simp add: M2.nn_integral_fst [symmetric])
  1.2706 -  also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
  1.2707 -    apply (intro nn_integral_cong_AE)
  1.2708 -    using integ2
  1.2709 -  proof eventually_elim
  1.2710 -    fix x assume "integrable M2 (\<lambda>y. f (x, y))"
  1.2711 -    then have f: "integrable M2 (\<lambda>y. norm (f (x, y)))"
  1.2712 -      by simp
  1.2713 -    then have "(\<integral>\<^sup>+y. ennreal (norm (f (x, y))) \<partial>M2) = ennreal (LINT y|M2. norm (f (x, y)))"
  1.2714 -      by (rule nn_integral_eq_integral) simp
  1.2715 -    also have "\<dots> = ennreal \<bar>LINT y|M2. norm (f (x, y))\<bar>"
  1.2716 -      using f by simp
  1.2717 -    finally show "(\<integral>\<^sup>+y. ennreal (norm (f (x, y))) \<partial>M2) = ennreal \<bar>LINT y|M2. norm (f (x, y))\<bar>" .
  1.2718 -  qed
  1.2719 -  also have "\<dots> < \<infinity>"
  1.2720 -    using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
  1.2721 -  finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
  1.2722 -qed fact
  1.2723 -
  1.2724 -lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
  1.2725 -  assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
  1.2726 -  shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
  1.2727 -proof -
  1.2728 -  from M2.emeasure_pair_measure_alt[OF A] finite
  1.2729 -  have "(\<integral>\<^sup>+ x. emeasure M2 (Pair x -` A) \<partial>M1) \<noteq> \<infinity>"
  1.2730 -    by simp
  1.2731 -  then have "AE x in M1. emeasure M2 (Pair x -` A) \<noteq> \<infinity>"
  1.2732 -    by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
  1.2733 -  moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> Pair x -` A = {y\<in>space M2. (x, y) \<in> A}"
  1.2734 -    using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
  1.2735 -  ultimately show ?thesis by (auto simp: less_top)
  1.2736 -qed
  1.2737 -
  1.2738 -lemma (in pair_sigma_finite) AE_integrable_fst':
  1.2739 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2740 -  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.2741 -  shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  1.2742 -proof -
  1.2743 -  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))"
  1.2744 -    by (rule M2.nn_integral_fst) simp
  1.2745 -  also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) \<noteq> \<infinity>"
  1.2746 -    using f unfolding integrable_iff_bounded by simp
  1.2747 -  finally have "AE x in M1. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
  1.2748 -    by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
  1.2749 -       (auto simp: measurable_split_conv)
  1.2750 -  with AE_space show ?thesis
  1.2751 -    by eventually_elim
  1.2752 -       (auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top)
  1.2753 -qed
  1.2754 -
  1.2755 -lemma (in pair_sigma_finite) integrable_fst':
  1.2756 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2757 -  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.2758 -  shows "integrable M1 (\<lambda>x. \<integral>y. f (x, y) \<partial>M2)"
  1.2759 -  unfolding integrable_iff_bounded
  1.2760 -proof
  1.2761 -  show "(\<lambda>x. \<integral> y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
  1.2762 -    by (rule M2.borel_measurable_lebesgue_integral) simp
  1.2763 -  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)"
  1.2764 -    using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ennreal)
  1.2765 -  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))"
  1.2766 -    by (rule M2.nn_integral_fst) simp
  1.2767 -  also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>"
  1.2768 -    using f unfolding integrable_iff_bounded by simp
  1.2769 -  finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
  1.2770 -qed
  1.2771 -
  1.2772 -lemma (in pair_sigma_finite) integral_fst':
  1.2773 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2774 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.2775 -  shows "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  1.2776 -using f proof induct
  1.2777 -  case (base A c)
  1.2778 -  have A[measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" by fact
  1.2779 -
  1.2780 -  have eq: "\<And>x y. x \<in> space M1 \<Longrightarrow> indicator A (x, y) = indicator {y\<in>space M2. (x, y) \<in> A} y"
  1.2781 -    using sets.sets_into_space[OF A] by (auto split: split_indicator simp: space_pair_measure)
  1.2782 -
  1.2783 -  have int_A: "integrable (M1 \<Otimes>\<^sub>M M2) (indicator A :: _ \<Rightarrow> real)"
  1.2784 -    using base by (rule integrable_real_indicator)
  1.2785 -
  1.2786 -  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)"
  1.2787 -  proof (intro integral_cong_AE, simp, simp)
  1.2788 -    from AE_integrable_fst'[OF int_A] AE_space
  1.2789 -    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"
  1.2790 -      by eventually_elim (simp add: eq integrable_indicator_iff)
  1.2791 -  qed
  1.2792 -  also have "\<dots> = measure (M1 \<Otimes>\<^sub>M M2) A *\<^sub>R c"
  1.2793 -  proof (subst integral_scaleR_left)
  1.2794 -    have "(\<integral>\<^sup>+x. ennreal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) =
  1.2795 -      (\<integral>\<^sup>+x. emeasure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1)"
  1.2796 -      using emeasure_pair_measure_finite[OF base]
  1.2797 -      by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ennreal_measure)
  1.2798 -    also have "\<dots> = emeasure (M1 \<Otimes>\<^sub>M M2) A"
  1.2799 -      using sets.sets_into_space[OF A]
  1.2800 -      by (subst M2.emeasure_pair_measure_alt)
  1.2801 -         (auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
  1.2802 -    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" .
  1.2803 -
  1.2804 -    from base * show "integrable M1 (\<lambda>x. measure M2 {y \<in> space M2. (x, y) \<in> A})"
  1.2805 -      by (simp add: integrable_iff_bounded)
  1.2806 -    then have "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) =
  1.2807 -      (\<integral>\<^sup>+x. ennreal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1)"
  1.2808 -      by (rule nn_integral_eq_integral[symmetric]) simp
  1.2809 -    also note *
  1.2810 -    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"
  1.2811 -      using base by (simp add: emeasure_eq_ennreal_measure)
  1.2812 -  qed
  1.2813 -  also have "\<dots> = (\<integral> a. indicator A a *\<^sub>R c \<partial>(M1 \<Otimes>\<^sub>M M2))"
  1.2814 -    using base by simp
  1.2815 -  finally show ?case .
  1.2816 -next
  1.2817 -  case (add f g)
  1.2818 -  then have [measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" "g \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  1.2819 -    by auto
  1.2820 -  have "(\<integral> x. \<integral> y. f (x, y) + g (x, y) \<partial>M2 \<partial>M1) =
  1.2821 -    (\<integral> x. (\<integral> y. f (x, y) \<partial>M2) + (\<integral> y. g (x, y) \<partial>M2) \<partial>M1)"
  1.2822 -    apply (rule integral_cong_AE)
  1.2823 -    apply simp_all
  1.2824 -    using AE_integrable_fst'[OF add(1)] AE_integrable_fst'[OF add(3)]
  1.2825 -    apply eventually_elim
  1.2826 -    apply simp
  1.2827 -    done
  1.2828 -  also have "\<dots> = (\<integral> x. f x \<partial>(M1 \<Otimes>\<^sub>M M2)) + (\<integral> x. g x \<partial>(M1 \<Otimes>\<^sub>M M2))"
  1.2829 -    using integrable_fst'[OF add(1)] integrable_fst'[OF add(3)] add(2,4) by simp
  1.2830 -  finally show ?case
  1.2831 -    using add by simp
  1.2832 -next
  1.2833 -  case (lim f s)
  1.2834 -  then have [measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" "\<And>i. s i \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  1.2835 -    by auto
  1.2836 -
  1.2837 -  show ?case
  1.2838 -  proof (rule LIMSEQ_unique)
  1.2839 -    show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) \<longlonglongrightarrow> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  1.2840 -    proof (rule integral_dominated_convergence)
  1.2841 -      show "integrable (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. 2 * norm (f x))"
  1.2842 -        using lim(5) by auto
  1.2843 -    qed (insert lim, auto)
  1.2844 -    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"
  1.2845 -    proof (rule integral_dominated_convergence)
  1.2846 -      have "AE x in M1. \<forall>i. integrable M2 (\<lambda>y. s i (x, y))"
  1.2847 -        unfolding AE_all_countable using AE_integrable_fst'[OF lim(1)] ..
  1.2848 -      with AE_space AE_integrable_fst'[OF lim(5)]
  1.2849 -      show "AE x in M1. (\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) \<longlonglongrightarrow> \<integral> y. f (x, y) \<partial>M2"
  1.2850 -      proof eventually_elim
  1.2851 -        fix x assume x: "x \<in> space M1" and
  1.2852 -          s: "\<forall>i. integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
  1.2853 -        show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) \<longlonglongrightarrow> \<integral> y. f (x, y) \<partial>M2"
  1.2854 -        proof (rule integral_dominated_convergence)
  1.2855 -          show "integrable M2 (\<lambda>y. 2 * norm (f (x, y)))"
  1.2856 -             using f by auto
  1.2857 -          show "AE xa in M2. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f (x, xa)"
  1.2858 -            using x lim(3) by (auto simp: space_pair_measure)
  1.2859 -          show "\<And>i. AE xa in M2. norm (s i (x, xa)) \<le> 2 * norm (f (x, xa))"
  1.2860 -            using x lim(4) by (auto simp: space_pair_measure)
  1.2861 -        qed (insert x, measurable)
  1.2862 -      qed
  1.2863 -      show "integrable M1 (\<lambda>x. (\<integral> y. 2 * norm (f (x, y)) \<partial>M2))"
  1.2864 -        by (intro integrable_mult_right integrable_norm integrable_fst' lim)
  1.2865 -      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)"
  1.2866 -        using AE_space AE_integrable_fst'[OF lim(1), of i] AE_integrable_fst'[OF lim(5)]
  1.2867 -      proof eventually_elim
  1.2868 -        fix x assume x: "x \<in> space M1"
  1.2869 -          and s: "integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
  1.2870 -        from s have "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral>\<^sup>+y. norm (s i (x, y)) \<partial>M2)"
  1.2871 -          by (rule integral_norm_bound_ennreal)
  1.2872 -        also have "\<dots> \<le> (\<integral>\<^sup>+y. 2 * norm (f (x, y)) \<partial>M2)"
  1.2873 -          using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
  1.2874 -        also have "\<dots> = (\<integral>y. 2 * norm (f (x, y)) \<partial>M2)"
  1.2875 -          using f by (intro nn_integral_eq_integral) auto
  1.2876 -        finally show "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
  1.2877 -          by simp
  1.2878 -      qed
  1.2879 -    qed simp_all
  1.2880 -    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"
  1.2881 -      using lim by simp
  1.2882 -  qed
  1.2883 -qed
  1.2884 -
  1.2885 -lemma (in pair_sigma_finite)
  1.2886 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2887 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  1.2888 -  shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
  1.2889 -    and integrable_fst: "integrable M1 (\<lambda>x. \<integral>y. f x y \<partial>M2)" (is "?INT")
  1.2890 -    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")
  1.2891 -  using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto
  1.2892 -
  1.2893 -lemma (in pair_sigma_finite)
  1.2894 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2895 -  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  1.2896 -  shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
  1.2897 -    and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
  1.2898 -    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")
  1.2899 -proof -
  1.2900 -  interpret Q: pair_sigma_finite M2 M1 ..
  1.2901 -  have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
  1.2902 -    using f unfolding integrable_product_swap_iff[symmetric] by simp
  1.2903 -  show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
  1.2904 -  show ?INT using Q.integrable_fst'[OF Q_int] by simp
  1.2905 -  show ?EQ using Q.integral_fst'[OF Q_int]
  1.2906 -    using integral_product_swap[of "case_prod f"] by simp
  1.2907 -qed
  1.2908 -
  1.2909 -lemma (in pair_sigma_finite) Fubini_integral:
  1.2910 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1.2911 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  1.2912 -  shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
  1.2913 -  unfolding integral_snd[OF assms] integral_fst[OF assms] ..
  1.2914 -
  1.2915 -lemma (in product_sigma_finite) product_integral_singleton:
  1.2916 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2917 -  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"
  1.2918 -  apply (subst distr_singleton[symmetric])
  1.2919 -  apply (subst integral_distr)
  1.2920 -  apply simp_all
  1.2921 -  done
  1.2922 -
  1.2923 -lemma (in product_sigma_finite) product_integral_fold:
  1.2924 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2925 -  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  1.2926 -  and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
  1.2927 -  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)"
  1.2928 -proof -
  1.2929 -  interpret I: finite_product_sigma_finite M I by standard fact
  1.2930 -  interpret J: finite_product_sigma_finite M J by standard fact
  1.2931 -  have "finite (I \<union> J)" using fin by auto
  1.2932 -  interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
  1.2933 -  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
  1.2934 -  let ?M = "merge I J"
  1.2935 -  let ?f = "\<lambda>x. f (?M x)"
  1.2936 -  from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
  1.2937 -    by auto
  1.2938 -  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)"
  1.2939 -    using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
  1.2940 -  have f_int: "integrable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) ?f"
  1.2941 -    by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
  1.2942 -  show ?thesis
  1.2943 -    apply (subst distr_merge[symmetric, OF IJ fin])
  1.2944 -    apply (subst integral_distr[OF measurable_merge f_borel])
  1.2945 -    apply (subst P.integral_fst'[symmetric, OF f_int])
  1.2946 -    apply simp
  1.2947 -    done
  1.2948 -qed
  1.2949 -
  1.2950 -lemma (in product_sigma_finite) product_integral_insert:
  1.2951 -  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.2952 -  assumes I: "finite I" "i \<notin> I"
  1.2953 -    and f: "integrable (Pi\<^sub>M (insert i I) M) f"
  1.2954 -  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)"
  1.2955 -proof -
  1.2956 -  have "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = integral\<^sup>L (Pi\<^sub>M (I \<union> {i}) M) f"
  1.2957 -    by simp
  1.2958 -  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)"
  1.2959 -    using f I by (intro product_integral_fold) auto
  1.2960 -  also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^sub>M I M)"
  1.2961 -  proof (rule integral_cong[OF refl], subst product_integral_singleton[symmetric])
  1.2962 -    fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
  1.2963 -    have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
  1.2964 -      using f by auto
  1.2965 -    show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
  1.2966 -      using measurable_comp[OF measurable_component_update f_borel, OF x \<open>i \<notin> I\<close>]
  1.2967 -      unfolding comp_def .
  1.2968 -    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)"
  1.2969 -      by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
  1.2970 -  qed
  1.2971 -  finally show ?thesis .
  1.2972 -qed
  1.2973 -
  1.2974 -lemma (in product_sigma_finite) product_integrable_setprod:
  1.2975 -  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  1.2976 -  assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1.2977 -  shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
  1.2978 -proof (unfold integrable_iff_bounded, intro conjI)
  1.2979 -  interpret finite_product_sigma_finite M I by standard fact
  1.2980 -
  1.2981 -  show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
  1.2982 -    using assms by simp
  1.2983 -  have "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) =
  1.2984 -      (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ennreal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
  1.2985 -    by (simp add: setprod_norm setprod_ennreal)
  1.2986 -  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ennreal (norm (f i x)) \<partial>M i)"
  1.2987 -    using assms by (intro product_nn_integral_setprod) auto
  1.2988 -  also have "\<dots> < \<infinity>"
  1.2989 -    using integrable by (simp add: less_top[symmetric] ennreal_setprod_eq_top integrable_iff_bounded)
  1.2990 -  finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
  1.2991 -qed
  1.2992 -
  1.2993 -lemma (in product_sigma_finite) product_integral_setprod:
  1.2994 -  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  1.2995 -  assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1.2996 -  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))"
  1.2997 -using assms proof induct
  1.2998 -  case empty
  1.2999 -  interpret finite_measure "Pi\<^sub>M {} M"
  1.3000 -    by rule (simp add: space_PiM)
  1.3001 -  show ?case by (simp add: space_PiM measure_def)
  1.3002 -next
  1.3003 -  case (insert i I)
  1.3004 -  then have iI: "finite (insert i I)" by auto
  1.3005 -  then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
  1.3006 -    integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
  1.3007 -    by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
  1.3008 -  interpret I: finite_product_sigma_finite M I by standard fact
  1.3009 -  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))"
  1.3010 -    using \<open>i \<notin> I\<close> by (auto intro!: setprod.cong)
  1.3011 -  show ?case
  1.3012 -    unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
  1.3013 -    by (simp add: * insert prod subset_insertI)
  1.3014 -qed
  1.3015 -
  1.3016 -lemma integrable_subalgebra:
  1.3017 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.3018 -  assumes borel: "f \<in> borel_measurable N"
  1.3019 -  and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  1.3020 -  shows "integrable N f \<longleftrightarrow> integrable M f" (is ?P)
  1.3021 -proof -
  1.3022 -  have "f \<in> borel_measurable M"
  1.3023 -    using assms by (auto simp: measurable_def)
  1.3024 -  with assms show ?thesis
  1.3025 -    using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
  1.3026 -qed
  1.3027 -
  1.3028 -lemma integral_subalgebra:
  1.3029 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.3030 -  assumes borel: "f \<in> borel_measurable N"
  1.3031 -  and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  1.3032 -  shows "integral\<^sup>L N f = integral\<^sup>L M f"
  1.3033 -proof cases
  1.3034 -  assume "integrable N f"
  1.3035 -  then show ?thesis
  1.3036 -  proof induct
  1.3037 -    case base with assms show ?case by (auto simp: subset_eq measure_def)
  1.3038 -  next
  1.3039 -    case (add f g)
  1.3040 -    then have "(\<integral> a. f a + g a \<partial>N) = integral\<^sup>L M f + integral\<^sup>L M g"
  1.3041 -      by simp
  1.3042 -    also have "\<dots> = (\<integral> a. f a + g a \<partial>M)"
  1.3043 -      using add integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of g] by simp
  1.3044 -    finally show ?case .
  1.3045 -  next
  1.3046 -    case (lim f s)
  1.3047 -    then have M: "\<And>i. integrable M (s i)" "integrable M f"
  1.3048 -      using integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of "s i" for i] by simp_all
  1.3049 -    show ?case
  1.3050 -    proof (intro LIMSEQ_unique)
  1.3051 -      show "(\<lambda>i. integral\<^sup>L N (s i)) \<longlonglongrightarrow> integral\<^sup>L N f"
  1.3052 -        apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  1.3053 -        using lim
  1.3054 -        apply auto
  1.3055 -        done
  1.3056 -      show "(\<lambda>i. integral\<^sup>L N (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
  1.3057 -        unfolding lim
  1.3058 -        apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
  1.3059 -        using lim M N(2)
  1.3060 -        apply auto
  1.3061 -        done
  1.3062 -    qed
  1.3063 -  qed
  1.3064 -qed (simp add: not_integrable_integral_eq integrable_subalgebra[OF assms])
  1.3065 -
  1.3066 -hide_const (open) simple_bochner_integral
  1.3067 -hide_const (open) simple_bochner_integrable
  1.3068 -
  1.3069 -end