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