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