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