src/HOL/Analysis/Set_Integral.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69737 ec3cc98c38db child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:      HOL/Analysis/Set_Integral.thy
```
```     2     Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
```
```     3     Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
```
```     4
```
```     5 Notation and useful facts for working with integrals over a set.
```
```     6
```
```     7 TODO: keep all these? Need unicode translations as well.
```
```     8 *)
```
```     9
```
```    10 theory Set_Integral
```
```    11   imports Radon_Nikodym
```
```    12 begin
```
```    13
```
```    14 (*
```
```    15     Notation
```
```    16 *)
```
```    17
```
```    18 definition%important "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
```
```    19
```
```    20 definition%important  "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```    21
```
```    22 definition%important  "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```    23
```
```    24 syntax
```
```    25   "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
```
```    26   ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
```
```    27
```
```    28 translations
```
```    29   "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
```
```    30
```
```    31 (*
```
```    32     Notation for integration wrt lebesgue measure on the reals:
```
```    33
```
```    34       LBINT x. f
```
```    35       LBINT x : A. f
```
```    36
```
```    37     TODO: keep all these? Need unicode.
```
```    38 *)
```
```    39
```
```    40 syntax
```
```    41   "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
```
```    42   ("(2LBINT _./ _)" [0,60] 60)
```
```    43
```
```    44 syntax
```
```    45   "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
```
```    46   ("(3LBINT _:_./ _)" [0,60,61] 60)
```
```    47
```
```    48 (*
```
```    49     Basic properties
```
```    50 *)
```
```    51
```
```    52 (*
```
```    53 lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
```
```    54   by (auto simp add: indicator_def)
```
```    55 *)
```
```    56
```
```    57 lemma set_integrable_cong:
```
```    58   assumes "M = M'" "A = A'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
```
```    59   shows   "set_integrable M A f = set_integrable M' A' f'"
```
```    60 proof -
```
```    61   have "(\<lambda>x. indicator A x *\<^sub>R f x) = (\<lambda>x. indicator A' x *\<^sub>R f' x)"
```
```    62     using assms by (auto simp: indicator_def)
```
```    63   thus ?thesis by (simp add: set_integrable_def assms)
```
```    64 qed
```
```    65
```
```    66 lemma set_borel_measurable_sets:
```
```    67   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
```
```    68   assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
```
```    69   shows "f -` B \<inter> X \<in> sets M"
```
```    70 proof -
```
```    71   have "f \<in> borel_measurable (restrict_space M X)"
```
```    72     using assms unfolding set_borel_measurable_def by (subst borel_measurable_restrict_space_iff) auto
```
```    73   then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
```
```    74     by (rule measurable_sets) fact
```
```    75   with \<open>X \<in> sets M\<close> show ?thesis
```
```    76     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
```
```    77 qed
```
```    78
```
```    79 lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\<lambda>x. 0) = 0"
```
```    80   by (auto simp: set_lebesgue_integral_def)
```
```    81
```
```    82 lemma set_lebesgue_integral_cong:
```
```    83   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
```
```    84   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
```
```    85   unfolding set_lebesgue_integral_def
```
```    86   using assms
```
```    87   by (metis indicator_simps(2) real_vector.scale_zero_left)
```
```    88
```
```    89 lemma set_lebesgue_integral_cong_AE:
```
```    90   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
```
```    91   assumes "AE x \<in> A in M. f x = g x"
```
```    92   shows "LINT x:A|M. f x = LINT x:A|M. g x"
```
```    93 proof-
```
```    94   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
```
```    95     using assms by auto
```
```    96   thus ?thesis
```
```    97   unfolding set_lebesgue_integral_def by (intro integral_cong_AE) auto
```
```    98 qed
```
```    99
```
```   100 lemma set_integrable_cong_AE:
```
```   101     "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
```
```   102     AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
```
```   103     set_integrable M A f = set_integrable M A g"
```
```   104   unfolding set_integrable_def
```
```   105   by (rule integrable_cong_AE) auto
```
```   106
```
```   107 lemma set_integrable_subset:
```
```   108   fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   109   assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
```
```   110   shows "set_integrable M B f"
```
```   111 proof -
```
```   112   have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```   113     using assms integrable_mult_indicator set_integrable_def by blast
```
```   114   with \<open>B \<subseteq> A\<close> show ?thesis
```
```   115     unfolding set_integrable_def
```
```   116     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
```
```   117 qed
```
```   118
```
```   119 lemma set_integrable_restrict_space:
```
```   120   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
```
```   121   assumes f: "set_integrable M S f" and T: "T \<in> sets (restrict_space M S)"
```
```   122   shows "set_integrable M T f"
```
```   123 proof -
```
```   124   obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M"
```
```   125     using T by (auto simp: sets_restrict_space)
```
```   126   have \<open>integrable M (\<lambda>x. indicator T' x *\<^sub>R (indicator S x *\<^sub>R f x))\<close>
```
```   127     using \<open>T' \<in> sets M\<close> f integrable_mult_indicator set_integrable_def by blast
```
```   128   then show ?thesis
```
```   129     unfolding set_integrable_def
```
```   130     unfolding T_eq indicator_inter_arith by (simp add: ac_simps)
```
```   131 qed
```
```   132
```
```   133 (* TODO: integral_cmul_indicator should be named set_integral_const *)
```
```   134 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
```
```   135
```
```   136 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
```
```   137   unfolding set_lebesgue_integral_def
```
```   138   by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
```
```   139
```
```   140 lemma set_integral_mult_right [simp]:
```
```   141   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   142   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
```
```   143   unfolding set_lebesgue_integral_def
```
```   144   by (subst integral_mult_right_zero[symmetric]) auto
```
```   145
```
```   146 lemma set_integral_mult_left [simp]:
```
```   147   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   148   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
```
```   149   unfolding set_lebesgue_integral_def
```
```   150   by (subst integral_mult_left_zero[symmetric]) auto
```
```   151
```
```   152 lemma set_integral_divide_zero [simp]:
```
```   153   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
```
```   154   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
```
```   155   unfolding set_lebesgue_integral_def
```
```   156   by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
```
```   157      (auto split: split_indicator)
```
```   158
```
```   159 lemma set_integrable_scaleR_right [simp, intro]:
```
```   160   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
```
```   161   unfolding set_integrable_def
```
```   162   unfolding scaleR_left_commute by (rule integrable_scaleR_right)
```
```   163
```
```   164 lemma set_integrable_scaleR_left [simp, intro]:
```
```   165   fixes a :: "_ :: {banach, second_countable_topology}"
```
```   166   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
```
```   167   unfolding set_integrable_def
```
```   168   using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
```
```   169
```
```   170 lemma set_integrable_mult_right [simp, intro]:
```
```   171   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   172   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
```
```   173   unfolding set_integrable_def
```
```   174   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
```
```   175
```
```   176 lemma set_integrable_mult_left [simp, intro]:
```
```   177   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   178   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
```
```   179   unfolding set_integrable_def
```
```   180   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
```
```   181
```
```   182 lemma set_integrable_divide [simp, intro]:
```
```   183   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
```
```   184   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
```
```   185   shows "set_integrable M A (\<lambda>t. f t / a)"
```
```   186 proof -
```
```   187   have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
```
```   188     using assms unfolding set_integrable_def by (rule integrable_divide_zero)
```
```   189   also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
```
```   190     by (auto split: split_indicator)
```
```   191   finally show ?thesis
```
```   192     unfolding set_integrable_def .
```
```   193 qed
```
```   194
```
```   195 lemma set_integral_add [simp, intro]:
```
```   196   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   197   assumes "set_integrable M A f" "set_integrable M A g"
```
```   198   shows "set_integrable M A (\<lambda>x. f x + g x)"
```
```   199     and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
```
```   200   using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
```
```   201
```
```   202 lemma set_integral_diff [simp, intro]:
```
```   203   assumes "set_integrable M A f" "set_integrable M A g"
```
```   204   shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
```
```   205     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
```
```   206   using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
```
```   207
```
```   208 (* question: why do we have this for negation, but multiplication by a constant
```
```   209    requires an integrability assumption? *)
```
```   210 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
```
```   211   unfolding set_integrable_def set_lebesgue_integral_def
```
```   212   by (subst integral_minus[symmetric]) simp_all
```
```   213
```
```   214 lemma set_integral_complex_of_real:
```
```   215   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
```
```   216   unfolding set_lebesgue_integral_def
```
```   217   by (subst integral_complex_of_real[symmetric])
```
```   218      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
```
```   219
```
```   220 lemma set_integral_mono:
```
```   221   fixes f g :: "_ \<Rightarrow> real"
```
```   222   assumes "set_integrable M A f" "set_integrable M A g"
```
```   223     "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
```
```   224   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
```
```   225   using assms unfolding set_integrable_def set_lebesgue_integral_def
```
```   226   by (auto intro: integral_mono split: split_indicator)
```
```   227
```
```   228 lemma set_integral_mono_AE:
```
```   229   fixes f g :: "_ \<Rightarrow> real"
```
```   230   assumes "set_integrable M A f" "set_integrable M A g"
```
```   231     "AE x \<in> A in M. f x \<le> g x"
```
```   232   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
```
```   233   using assms unfolding set_integrable_def set_lebesgue_integral_def
```
```   234   by (auto intro: integral_mono_AE split: split_indicator)
```
```   235
```
```   236 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
```
```   237   using integrable_abs[of M "\<lambda>x. f x * indicator A x"]unfolding set_integrable_def by (simp add: abs_mult ac_simps)
```
```   238
```
```   239 lemma set_integrable_abs_iff:
```
```   240   fixes f :: "_ \<Rightarrow> real"
```
```   241   shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
```
```   242   unfolding set_integrable_def set_borel_measurable_def
```
```   243   by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
```
```   244
```
```   245 lemma set_integrable_abs_iff':
```
```   246   fixes f :: "_ \<Rightarrow> real"
```
```   247   shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
```
```   248     set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
```
```   249   by (simp add: set_borel_measurable_def set_integrable_abs_iff)
```
```   250
```
```   251 lemma set_integrable_discrete_difference:
```
```   252   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
```
```   253   assumes "countable X"
```
```   254   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
```
```   255   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
```
```   256   shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
```
```   257   unfolding set_integrable_def
```
```   258 proof (rule integrable_discrete_difference[where X=X])
```
```   259   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
```
```   260     using diff by (auto split: split_indicator)
```
```   261 qed fact+
```
```   262
```
```   263 lemma set_integral_discrete_difference:
```
```   264   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
```
```   265   assumes "countable X"
```
```   266   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
```
```   267   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
```
```   268   shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
```
```   269   unfolding set_lebesgue_integral_def
```
```   270 proof (rule integral_discrete_difference[where X=X])
```
```   271   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
```
```   272     using diff by (auto split: split_indicator)
```
```   273 qed fact+
```
```   274
```
```   275 lemma set_integrable_Un:
```
```   276   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   277   assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
```
```   278     and [measurable]: "A \<in> sets M" "B \<in> sets M"
```
```   279   shows "set_integrable M (A \<union> B) f"
```
```   280 proof -
```
```   281   have "set_integrable M (A - B) f"
```
```   282     using f_A by (rule set_integrable_subset) auto
```
```   283   with f_B have "integrable M (\<lambda>x. indicator (A - B) x *\<^sub>R f x + indicator B x *\<^sub>R f x)"
```
```   284     unfolding set_integrable_def using integrable_add by blast
```
```   285   then show ?thesis
```
```   286     unfolding set_integrable_def
```
```   287     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
```
```   288 qed
```
```   289
```
```   290 lemma set_integrable_empty [simp]: "set_integrable M {} f"
```
```   291   by (auto simp: set_integrable_def)
```
```   292
```
```   293 lemma set_integrable_UN:
```
```   294   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   295   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
```
```   296     "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
```
```   297   shows "set_integrable M (\<Union>i\<in>I. A i) f"
```
```   298   using assms
```
```   299   by (induct I) (auto simp: set_integrable_Un sets.finite_UN)
```
```   300
```
```   301 lemma set_integral_Un:
```
```   302   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   303   assumes "A \<inter> B = {}"
```
```   304   and "set_integrable M A f"
```
```   305   and "set_integrable M B f"
```
```   306 shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
```
```   307   using assms
```
```   308   unfolding set_integrable_def set_lebesgue_integral_def
```
```   309   by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
```
```   310
```
```   311 lemma set_integral_cong_set:
```
```   312   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   313   assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
```
```   314     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
```
```   315   shows "LINT x:B|M. f x = LINT x:A|M. f x"
```
```   316   unfolding set_lebesgue_integral_def
```
```   317 proof (rule integral_cong_AE)
```
```   318   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
```
```   319     using ae by (auto simp: subset_eq split: split_indicator)
```
```   320 qed (use assms in \<open>auto simp: set_borel_measurable_def\<close>)
```
```   321
```
```   322 proposition set_borel_measurable_subset:
```
```   323   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   324   assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
```
```   325   shows "set_borel_measurable M B f"
```
```   326 proof-
```
```   327   have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```   328     using assms unfolding set_borel_measurable_def
```
```   329     using borel_measurable_indicator borel_measurable_scaleR by blast
```
```   330   moreover have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
```
```   331     using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
```
```   332   ultimately show ?thesis
```
```   333     unfolding set_borel_measurable_def by simp
```
```   334 qed
```
```   335
```
```   336 lemma set_integral_Un_AE:
```
```   337   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   338   assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
```
```   339   and "set_integrable M A f"
```
```   340   and "set_integrable M B f"
```
```   341   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
```
```   342 proof -
```
```   343   have f: "set_integrable M (A \<union> B) f"
```
```   344     by (intro set_integrable_Un assms)
```
```   345   then have f': "set_borel_measurable M (A \<union> B) f"
```
```   346     using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
```
```   347   have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
```
```   348   proof (rule set_integral_cong_set)
```
```   349     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
```
```   350       using ae by auto
```
```   351     show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
```
```   352       using f' by (rule set_borel_measurable_subset) auto
```
```   353   qed fact
```
```   354   also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
```
```   355     by (auto intro!: set_integral_Un set_integrable_subset[OF f])
```
```   356   also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
```
```   357     using ae
```
```   358     by (intro arg_cong2[where f="(+)"] set_integral_cong_set)
```
```   359        (auto intro!: set_borel_measurable_subset[OF f'])
```
```   360   finally show ?thesis .
```
```   361 qed
```
```   362
```
```   363 lemma set_integral_finite_Union:
```
```   364   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   365   assumes "finite I" "disjoint_family_on A I"
```
```   366     and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
```
```   367   shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
```
```   368   using assms
```
```   369 proof induction
```
```   370   case (insert x F)
```
```   371   then have "A x \<inter> \<Union>(A ` F) = {}"
```
```   372     by (meson disjoint_family_on_insert)
```
```   373   with insert show ?case
```
```   374     by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
```
```   375 qed (simp add: set_lebesgue_integral_def)
```
```   376
```
```   377 (* TODO: find a better name? *)
```
```   378 lemma pos_integrable_to_top:
```
```   379   fixes l::real
```
```   380   assumes "\<And>i. A i \<in> sets M" "mono A"
```
```   381   assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
```
```   382   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
```
```   383   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
```
```   384 shows "set_integrable M (\<Union>i. A i) f"
```
```   385     unfolding set_integrable_def
```
```   386   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
```
```   387   apply (rule intgbl [unfolded set_integrable_def])
```
```   388   prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
```
```   389   apply (rule AE_I2)
```
```   390   using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
```
```   391 proof (rule AE_I2)
```
```   392   { fix x assume "x \<in> space M"
```
```   393     show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
```
```   394     proof cases
```
```   395       assume "\<exists>i. x \<in> A i"
```
```   396       then guess i ..
```
```   397       then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
```
```   398         using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
```
```   399       show ?thesis
```
```   400         apply (intro Lim_eventually)
```
```   401         using *
```
```   402         apply eventually_elim
```
```   403         apply (auto split: split_indicator)
```
```   404         done
```
```   405     qed auto }
```
```   406   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
```
```   407     apply (rule borel_measurable_LIMSEQ_real)
```
```   408     apply assumption
```
```   409     using intgbl set_integrable_def by blast
```
```   410 qed
```
```   411
```
```   412 (* Proof from Royden Real Analysis, p. 91. *)
```
```   413 lemma lebesgue_integral_countable_add:
```
```   414   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   415   assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
```
```   416     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
```
```   417     and intgbl: "set_integrable M (\<Union>i. A i) f"
```
```   418   shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
```
```   419     unfolding set_lebesgue_integral_def
```
```   420 proof%unimportant (subst integral_suminf[symmetric])
```
```   421   show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
```
```   422     using intgbl unfolding set_integrable_def [symmetric]
```
```   423     by (rule set_integrable_subset) auto
```
```   424   { fix x assume "x \<in> space M"
```
```   425     have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
```
```   426       by (intro sums_scaleR_left indicator_sums) fact }
```
```   427   note sums = this
```
```   428
```
```   429   have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
```
```   430     using int_A[THEN integrable_norm] unfolding set_integrable_def by auto
```
```   431
```
```   432   show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
```
```   433     using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
```
```   434
```
```   435   show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
```
```   436   proof (rule summableI_nonneg_bounded)
```
```   437     fix n
```
```   438     show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
```
```   439       using norm_f by (auto intro!: integral_nonneg_AE)
```
```   440
```
```   441     have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) = (\<Sum>i<n. LINT x:A i|M. norm (f x))"
```
```   442       by (simp add: abs_mult set_lebesgue_integral_def)
```
```   443     also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
```
```   444       using norm_f
```
```   445       by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
```
```   446     also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
```
```   447       using intgbl[unfolded set_integrable_def, THEN integrable_norm] norm_f
```
```   448       unfolding set_lebesgue_integral_def set_integrable_def
```
```   449       apply (intro integral_mono set_integrable_UN[of "{..<n}", unfolded set_integrable_def])
```
```   450           apply (auto split: split_indicator)
```
```   451       done
```
```   452     finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
```
```   453       set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
```
```   454       by simp
```
```   455   qed
```
```   456   show "LINT x|M. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
```
```   457     apply (rule Bochner_Integration.integral_cong[OF refl])
```
```   458     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
```
```   459     using sums_unique[OF indicator_sums[OF disj]]
```
```   460     apply auto
```
```   461     done
```
```   462 qed
```
```   463
```
```   464 lemma set_integral_cont_up:
```
```   465   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   466   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
```
```   467   and intgbl: "set_integrable M (\<Union>i. A i) f"
```
```   468 shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
```
```   469   unfolding set_lebesgue_integral_def
```
```   470 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
```
```   471   have int_A: "\<And>i. set_integrable M (A i) f"
```
```   472     using intgbl by (rule set_integrable_subset) auto
```
```   473   show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
```
```   474     using int_A integrable_iff_bounded set_integrable_def by blast
```
```   475   show "(\<lambda>x. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
```
```   476     using integrable_iff_bounded intgbl set_integrable_def by blast
```
```   477   show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
```
```   478     using int_A intgbl integrable_norm unfolding set_integrable_def
```
```   479     by fastforce
```
```   480   { fix x i assume "x \<in> A i"
```
```   481     with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
```
```   482       by (intro filterlim_cong refl)
```
```   483          (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
```
```   484   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
```
```   485     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
```
```   486 qed (auto split: split_indicator)
```
```   487
```
```   488 (* Can the int0 hypothesis be dropped? *)
```
```   489 lemma set_integral_cont_down:
```
```   490   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   491   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
```
```   492   and int0: "set_integrable M (A 0) f"
```
```   493   shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
```
```   494   unfolding set_lebesgue_integral_def
```
```   495 proof (rule integral_dominated_convergence)
```
```   496   have int_A: "\<And>i. set_integrable M (A i) f"
```
```   497     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
```
```   498   have "integrable M (\<lambda>c. norm (indicat_real (A 0) c *\<^sub>R f c))"
```
```   499     by (metis (no_types) int0 integrable_norm set_integrable_def)
```
```   500   then show "integrable M (\<lambda>x. indicator (A 0) x *\<^sub>R norm (f x))"
```
```   501     by force
```
```   502   have "set_integrable M (\<Inter>i. A i) f"
```
```   503     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
```
```   504   with int_A show "(\<lambda>x. indicat_real (\<Inter>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
```
```   505                   "\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
```
```   506     by (auto simp: set_integrable_def)
```
```   507   show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
```
```   508     using A by (auto split: split_indicator simp: decseq_def)
```
```   509   { fix x i assume "x \<in> space M" "x \<notin> A i"
```
```   510     with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
```
```   511       by (intro filterlim_cong refl)
```
```   512          (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
```
```   513   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x *\<^sub>R f x"
```
```   514     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
```
```   515 qed
```
```   516
```
```   517 lemma set_integral_at_point:
```
```   518   fixes a :: real
```
```   519   assumes "set_integrable M {a} f"
```
```   520   and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
```
```   521   shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
```
```   522 proof-
```
```   523   have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
```
```   524     by (intro set_lebesgue_integral_cong) simp_all
```
```   525   then show ?thesis using assms
```
```   526     unfolding set_lebesgue_integral_def by simp
```
```   527 qed
```
```   528
```
```   529
```
```   530 abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
```
```   531   "complex_integrable M f \<equiv> integrable M f"
```
```   532
```
```   533 abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
```
```   534   "integral\<^sup>C M f == integral\<^sup>L M f"
```
```   535
```
```   536 syntax
```
```   537   "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
```
```   538  ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
```
```   539
```
```   540 translations
```
```   541   "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
```
```   542
```
```   543 syntax
```
```   544   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
```
```   545   ("(3CLINT _|_. _)" [0,110,60] 60)
```
```   546
```
```   547 translations
```
```   548   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
```
```   549
```
```   550 lemma complex_integrable_cnj [simp]:
```
```   551   "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
```
```   552 proof
```
```   553   assume "complex_integrable M (\<lambda>x. cnj (f x))"
```
```   554   then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
```
```   555     by (rule integrable_cnj)
```
```   556   then show "complex_integrable M f"
```
```   557     by simp
```
```   558 qed simp
```
```   559
```
```   560 lemma complex_of_real_integrable_eq:
```
```   561   "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
```
```   562 proof
```
```   563   assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
```
```   564   then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
```
```   565     by (rule integrable_Re)
```
```   566   then show "integrable M f"
```
```   567     by simp
```
```   568 qed simp
```
```   569
```
```   570
```
```   571 abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
```
```   572   "complex_set_integrable M A f \<equiv> set_integrable M A f"
```
```   573
```
```   574 abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
```
```   575   "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
```
```   576
```
```   577 syntax
```
```   578 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
```
```   579 ("(4CLINT _:_|_. _)" [0,60,110,61] 60)
```
```   580
```
```   581 translations
```
```   582 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
```
```   583
```
```   584 lemma set_measurable_continuous_on_ivl:
```
```   585   assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
```
```   586   shows "set_borel_measurable borel {a..b} f"
```
```   587   unfolding set_borel_measurable_def
```
```   588   by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
```
```   589
```
```   590
```
```   591 text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
```
```   592 notations in this file, they are more in line with sum, and more readable he thinks.\<close>
```
```   593
```
```   594 abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
```
```   595
```
```   596 syntax
```
```   597 "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
```
```   598 ("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
```
```   599
```
```   600 "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
```
```   601 ("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
```
```   602
```
```   603 translations
```
```   604 "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
```
```   605 "\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
```
```   606
```
```   607 lemma nn_integral_disjoint_pair:
```
```   608   assumes [measurable]: "f \<in> borel_measurable M"
```
```   609           "B \<in> sets M" "C \<in> sets M"
```
```   610           "B \<inter> C = {}"
```
```   611   shows "(\<integral>\<^sup>+x \<in> B \<union> C. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M) + (\<integral>\<^sup>+x \<in> C. f x \<partial>M)"
```
```   612 proof -
```
```   613   have mes: "\<And>D. D \<in> sets M \<Longrightarrow> (\<lambda>x. f x * indicator D x) \<in> borel_measurable M" by simp
```
```   614   have pos: "\<And>D. AE x in M. f x * indicator D x \<ge> 0" using assms(2) by auto
```
```   615   have "\<And>x. f x * indicator (B \<union> C) x = f x * indicator B x + f x * indicator C x" using assms(4)
```
```   616     by (auto split: split_indicator)
```
```   617   then have "(\<integral>\<^sup>+x. f x * indicator (B \<union> C) x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator B x + f x * indicator C x \<partial>M)"
```
```   618     by simp
```
```   619   also have "... = (\<integral>\<^sup>+x. f x * indicator B x \<partial>M) + (\<integral>\<^sup>+x. f x * indicator C x \<partial>M)"
```
```   620     by (rule nn_integral_add) (auto simp add: assms mes pos)
```
```   621   finally show ?thesis by simp
```
```   622 qed
```
```   623
```
```   624 lemma nn_integral_disjoint_pair_countspace:
```
```   625   assumes "B \<inter> C = {}"
```
```   626   shows "(\<integral>\<^sup>+x \<in> B \<union> C. f x \<partial>count_space UNIV) = (\<integral>\<^sup>+x \<in> B. f x \<partial>count_space UNIV) + (\<integral>\<^sup>+x \<in> C. f x \<partial>count_space UNIV)"
```
```   627 by (rule nn_integral_disjoint_pair) (simp_all add: assms)
```
```   628
```
```   629 lemma nn_integral_null_delta:
```
```   630   assumes "A \<in> sets M" "B \<in> sets M"
```
```   631           "(A - B) \<union> (B - A) \<in> null_sets M"
```
```   632   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M)"
```
```   633 proof (rule nn_integral_cong_AE, auto simp add: indicator_def)
```
```   634   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
```
```   635     using assms(3) AE_not_in by blast
```
```   636   then show "AE a in M. a \<notin> A \<longrightarrow> a \<in> B \<longrightarrow> f a = 0"
```
```   637     by auto
```
```   638   show "AE x\<in>A in M. x \<notin> B \<longrightarrow> f x = 0"
```
```   639     using * by auto
```
```   640 qed
```
```   641
```
```   642 proposition nn_integral_disjoint_family:
```
```   643   assumes [measurable]: "f \<in> borel_measurable M" "\<And>(n::nat). B n \<in> sets M"
```
```   644       and "disjoint_family B"
```
```   645   shows "(\<integral>\<^sup>+x \<in> (\<Union>n. B n). f x \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+x \<in> B n. f x \<partial>M))"
```
```   646 proof -
```
```   647   have "(\<integral>\<^sup>+ x. (\<Sum>n. f x * indicator (B n) x) \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+ x. f x * indicator (B n) x \<partial>M))"
```
```   648     by (rule nn_integral_suminf) simp
```
```   649   moreover have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (\<Union>n. B n) x" for x
```
```   650   proof (cases)
```
```   651     assume "x \<in> (\<Union>n. B n)"
```
```   652     then obtain n where "x \<in> B n" by blast
```
```   653     have a: "finite {n}" by simp
```
```   654     have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using \<open>x \<in> B n\<close> assms(3) disjoint_family_on_def
```
```   655       by (metis IntI UNIV_I empty_iff)
```
```   656     then have "\<And>i. i \<notin> {n} \<Longrightarrow> indicator (B i) x = (0::ennreal)" using indicator_def by simp
```
```   657     then have b: "\<And>i. i \<notin> {n} \<Longrightarrow> f x * indicator (B i) x = (0::ennreal)" by simp
```
```   658
```
```   659     define h where "h = (\<lambda>i. f x * indicator (B i) x)"
```
```   660     then have "\<And>i. i \<notin> {n} \<Longrightarrow> h i = 0" using b by simp
```
```   661     then have "(\<Sum>i. h i) = (\<Sum>i\<in>{n}. h i)"
```
```   662       by (metis sums_unique[OF sums_finite[OF a]])
```
```   663     then have "(\<Sum>i. h i) = h n" by simp
```
```   664     then have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
```
```   665     then have "(\<Sum>n. f x * indicator (B n) x) = f x" using \<open>x \<in> B n\<close> indicator_def by simp
```
```   666     then show ?thesis using \<open>x \<in> (\<Union>n. B n)\<close> by auto
```
```   667   next
```
```   668     assume "x \<notin> (\<Union>n. B n)"
```
```   669     then have "\<And>n. f x * indicator (B n) x = 0" by simp
```
```   670     have "(\<Sum>n. f x * indicator (B n) x) = 0"
```
```   671       by (simp add: \<open>\<And>n. f x * indicator (B n) x = 0\<close>)
```
```   672     then show ?thesis using \<open>x \<notin> (\<Union>n. B n)\<close> by auto
```
```   673   qed
```
```   674   ultimately show ?thesis by simp
```
```   675 qed
```
```   676
```
```   677 lemma nn_set_integral_add:
```
```   678   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
```
```   679           "A \<in> sets M"
```
```   680   shows "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x \<in> A. f x \<partial>M) + (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
```
```   681 proof -
```
```   682   have "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x. (f x * indicator A x + g x * indicator A x) \<partial>M)"
```
```   683     by (auto simp add: indicator_def intro!: nn_integral_cong)
```
```   684   also have "... = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + (\<integral>\<^sup>+x. g x * indicator A x \<partial>M)"
```
```   685     apply (rule nn_integral_add) using assms(1) assms(2) by auto
```
```   686   finally show ?thesis by simp
```
```   687 qed
```
```   688
```
```   689 lemma nn_set_integral_cong:
```
```   690   assumes "AE x in M. f x = g x"
```
```   691   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
```
```   692 apply (rule nn_integral_cong_AE) using assms(1) by auto
```
```   693
```
```   694 lemma nn_set_integral_set_mono:
```
```   695   "A \<subseteq> B \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+ x \<in> B. f x \<partial>M)"
```
```   696 by (auto intro!: nn_integral_mono split: split_indicator)
```
```   697
```
```   698 lemma nn_set_integral_mono:
```
```   699   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
```
```   700           "A \<in> sets M"
```
```   701       and "AE x\<in>A in M. f x \<le> g x"
```
```   702   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
```
```   703 by (auto intro!: nn_integral_mono_AE split: split_indicator simp: assms)
```
```   704
```
```   705 lemma nn_set_integral_space [simp]:
```
```   706   shows "(\<integral>\<^sup>+ x \<in> space M. f x \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
```
```   707 by (metis (mono_tags, lifting) indicator_simps(1) mult.right_neutral nn_integral_cong)
```
```   708
```
```   709 lemma nn_integral_count_compose_inj:
```
```   710   assumes "inj_on g A"
```
```   711   shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
```
```   712 proof -
```
```   713   have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+x. f (g x) \<partial>count_space A)"
```
```   714     by (auto simp add: nn_integral_count_space_indicator[symmetric])
```
```   715   also have "... = (\<integral>\<^sup>+y. f y \<partial>count_space (g`A))"
```
```   716     by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
```
```   717   also have "... = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
```
```   718     by (auto simp add: nn_integral_count_space_indicator[symmetric])
```
```   719   finally show ?thesis by simp
```
```   720 qed
```
```   721
```
```   722 lemma nn_integral_count_compose_bij:
```
```   723   assumes "bij_betw g A B"
```
```   724   shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> B. f y \<partial>count_space UNIV)"
```
```   725 proof -
```
```   726   have "inj_on g A" using assms bij_betw_def by auto
```
```   727   then have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
```
```   728     by (rule nn_integral_count_compose_inj)
```
```   729   then show ?thesis using assms by (simp add: bij_betw_def)
```
```   730 qed
```
```   731
```
```   732 lemma set_integral_null_delta:
```
```   733   fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   734   assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
```
```   735     and null: "(A - B) \<union> (B - A) \<in> null_sets M"
```
```   736   shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
```
```   737 proof (rule set_integral_cong_set)
```
```   738   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
```
```   739     using null AE_not_in by blast
```
```   740   then show "AE x in M. (x \<in> B) = (x \<in> A)"
```
```   741     by auto
```
```   742 qed (simp_all add: set_borel_measurable_def)
```
```   743
```
```   744 lemma set_integral_space:
```
```   745   assumes "integrable M f"
```
```   746   shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
```
```   747   by (metis (no_types, lifting) indicator_simps(1) integral_cong scaleR_one set_lebesgue_integral_def)
```
```   748
```
```   749 lemma null_if_pos_func_has_zero_nn_int:
```
```   750   fixes f::"'a \<Rightarrow> ennreal"
```
```   751   assumes [measurable]: "f \<in> borel_measurable M" "A \<in> sets M"
```
```   752     and "AE x\<in>A in M. f x > 0" "(\<integral>\<^sup>+x\<in>A. f x \<partial>M) = 0"
```
```   753   shows "A \<in> null_sets M"
```
```   754 proof -
```
```   755   have "AE x in M. f x * indicator A x = 0"
```
```   756     by (subst nn_integral_0_iff_AE[symmetric], auto simp add: assms(4))
```
```   757   then have "AE x\<in>A in M. False" using assms(3) by auto
```
```   758   then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
```
```   759 qed
```
```   760
```
```   761 lemma null_if_pos_func_has_zero_int:
```
```   762   assumes [measurable]: "integrable M f" "A \<in> sets M"
```
```   763       and "AE x\<in>A in M. f x > 0" "(\<integral>x\<in>A. f x \<partial>M) = (0::real)"
```
```   764   shows "A \<in> null_sets M"
```
```   765 proof -
```
```   766   have "AE x in M. indicator A x * f x = 0"
```
```   767     apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
```
```   768     using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)]
```
```   769     by (auto simp: set_lebesgue_integral_def)
```
```   770   then have "AE x\<in>A in M. f x = 0" by auto
```
```   771   then have "AE x\<in>A in M. False" using assms(3) by auto
```
```   772   then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
```
```   773 qed
```
```   774
```
```   775 text\<open>The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
```
```   776 for nonnegative set integrals introduced earlier.\<close>
```
```   777
```
```   778 lemma (in sigma_finite_measure) density_unique2:
```
```   779   assumes [measurable]: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
```
```   780   assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+ x \<in> A. f' x \<partial>M)"
```
```   781   shows "AE x in M. f x = f' x"
```
```   782 proof (rule density_unique)
```
```   783   show "density M f = density M f'"
```
```   784     by (intro measure_eqI) (auto simp: emeasure_density intro!: density_eq)
```
```   785 qed (auto simp add: assms)
```
```   786
```
```   787
```
```   788 text \<open>The next lemma implies the same statement for Banach-space valued functions
```
```   789 using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
```
```   790 only formulate it for real-valued functions.\<close>
```
```   791
```
```   792 lemma density_unique_real:
```
```   793   fixes f f'::"_ \<Rightarrow> real"
```
```   794   assumes M[measurable]: "integrable M f" "integrable M f'"
```
```   795   assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M)"
```
```   796   shows "AE x in M. f x = f' x"
```
```   797 proof -
```
```   798   define A where "A = {x \<in> space M. f x < f' x}"
```
```   799   then have [measurable]: "A \<in> sets M" by simp
```
```   800   have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
```
```   801     using \<open>A \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
```
```   802   then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
```
```   803   then have "A \<in> null_sets M"
```
```   804     using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
```
```   805   then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
```
```   806   then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
```
```   807
```
```   808   define B where "B = {x \<in> space M. f' x < f x}"
```
```   809   then have [measurable]: "B \<in> sets M" by simp
```
```   810   have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
```
```   811     using \<open>B \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
```
```   812   then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
```
```   813   then have "B \<in> null_sets M"
```
```   814     using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
```
```   815   then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
```
```   816   then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
```
```   817   then show ?thesis using * by auto
```
```   818 qed
```
```   819
```
```   820 text \<open>The next lemma shows that \<open>L\<^sup>1\<close> convergence of a sequence of functions follows from almost
```
```   821 everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
```
```   822 just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
```
```   823 variations) are known as Scheffe lemma.
```
```   824
```
```   825 The formalization is more painful as one should jump back and forth between reals and ereals and justify
```
```   826 all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\<close>
```
```   827
```
```   828 proposition Scheffe_lemma1:
```
```   829   assumes "\<And>n. integrable M (F n)" "integrable M f"
```
```   830           "AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
```
```   831           "limsup (\<lambda>n. \<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
```
```   832   shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
```
```   833 proof -
```
```   834   have [measurable]: "\<And>n. F n \<in> borel_measurable M" "f \<in> borel_measurable M"
```
```   835     using assms(1) assms(2) by simp_all
```
```   836   define G where "G = (\<lambda>n x. norm(f x) + norm(F n x) - norm(F n x - f x))"
```
```   837   have [measurable]: "\<And>n. G n \<in> borel_measurable M" unfolding G_def by simp
```
```   838   have G_pos[simp]: "\<And>n x. G n x \<ge> 0"
```
```   839     unfolding G_def by (metis ge_iff_diff_ge_0 norm_minus_commute norm_triangle_ineq4)
```
```   840   have finint: "(\<integral>\<^sup>+ x. norm(f x) \<partial>M) \<noteq> \<infinity>"
```
```   841     using has_bochner_integral_implies_finite_norm[OF has_bochner_integral_integrable[OF \<open>integrable M f\<close>]]
```
```   842     by simp
```
```   843   then have fin2: "2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M) \<noteq> \<infinity>"
```
```   844     by (auto simp: ennreal_mult_eq_top_iff)
```
```   845
```
```   846   {
```
```   847     fix x assume *: "(\<lambda>n. F n x) \<longlonglongrightarrow> f x"
```
```   848     then have "(\<lambda>n. norm(F n x)) \<longlonglongrightarrow> norm(f x)" using tendsto_norm by blast
```
```   849     moreover have "(\<lambda>n. norm(F n x - f x)) \<longlonglongrightarrow> 0" using * Lim_null tendsto_norm_zero_iff by fastforce
```
```   850     ultimately have a: "(\<lambda>n. norm(F n x) - norm(F n x - f x)) \<longlonglongrightarrow> norm(f x)" using tendsto_diff by fastforce
```
```   851     have "(\<lambda>n. norm(f x) + (norm(F n x) - norm(F n x - f x))) \<longlonglongrightarrow> norm(f x) + norm(f x)"
```
```   852       by (rule tendsto_add) (auto simp add: a)
```
```   853     moreover have "\<And>n. G n x = norm(f x) + (norm(F n x) - norm(F n x - f x))" unfolding G_def by simp
```
```   854     ultimately have "(\<lambda>n. G n x) \<longlonglongrightarrow> 2 * norm(f x)" by simp
```
```   855     then have "(\<lambda>n. ennreal(G n x)) \<longlonglongrightarrow> ennreal(2 * norm(f x))" by simp
```
```   856     then have "liminf (\<lambda>n. ennreal(G n x)) = ennreal(2 * norm(f x))"
```
```   857       using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
```
```   858   }
```
```   859   then have "AE x in M. liminf (\<lambda>n. ennreal(G n x)) = ennreal(2 * norm(f x))" using assms(3) by auto
```
```   860   then have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M) = (\<integral>\<^sup>+ x. 2 * ennreal(norm(f x)) \<partial>M)"
```
```   861     by (simp add: nn_integral_cong_AE ennreal_mult)
```
```   862   also have "... = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)" by (rule nn_integral_cmult) auto
```
```   863   finally have int_liminf: "(\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M) = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
```
```   864     by simp
```
```   865
```
```   866   have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) = (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(F n x) \<partial>M)" for n
```
```   867     by (rule nn_integral_add) (auto simp add: assms)
```
```   868   then have "limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M)) =
```
```   869       limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
```
```   870     by simp
```
```   871   also have "... = (\<integral>\<^sup>+x. norm(f x) \<partial>M) + limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
```
```   872     by (rule Limsup_const_add, auto simp add: finint)
```
```   873   also have "... \<le> (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
```
```   874     using assms(4) by (simp add: add_left_mono)
```
```   875   also have "... = 2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
```
```   876     unfolding one_add_one[symmetric] distrib_right by simp
```
```   877   ultimately have a: "limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M)) \<le>
```
```   878     2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)" by simp
```
```   879
```
```   880   have le: "ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))" for n x
```
```   881     by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus flip: ennreal_plus)
```
```   882   then have le2: "(\<integral>\<^sup>+ x. ennreal (norm (F n x - f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) \<partial>M)" for n
```
```   883     by (rule nn_integral_mono)
```
```   884
```
```   885   have "2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M) = (\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M)"
```
```   886     by (simp add: int_liminf)
```
```   887   also have "\<dots> \<le> liminf (\<lambda>n. (\<integral>\<^sup>+x. G n x \<partial>M))"
```
```   888     by (rule nn_integral_liminf) auto
```
```   889   also have "liminf (\<lambda>n. (\<integral>\<^sup>+x. G n x \<partial>M)) =
```
```   890     liminf (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M))"
```
```   891   proof (intro arg_cong[where f=liminf] ext)
```
```   892     fix n
```
```   893     have "\<And>x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))"
```
```   894       unfolding G_def by (simp add: ennreal_minus flip: ennreal_plus)
```
```   895     moreover have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \<partial>M)
```
```   896             = (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)"
```
```   897     proof (rule nn_integral_diff)
```
```   898       from le show "AE x in M. ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))"
```
```   899         by simp
```
```   900       from le2 have "(\<integral>\<^sup>+x. ennreal (norm (F n x - f x)) \<partial>M) < \<infinity>" using assms(1) assms(2)
```
```   901         by (metis has_bochner_integral_implies_finite_norm integrable.simps Bochner_Integration.integrable_diff)
```
```   902       then show "(\<integral>\<^sup>+x. ennreal (norm (F n x - f x)) \<partial>M) \<noteq> \<infinity>" by simp
```
```   903     qed (auto simp add: assms)
```
```   904     ultimately show "(\<integral>\<^sup>+x. G n x \<partial>M) = (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)"
```
```   905       by simp
```
```   906   qed
```
```   907   finally have "2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M) + limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)) \<le>
```
```   908     liminf (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)) +
```
```   909     limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M))"
```
```   910     by (intro add_mono) auto
```
```   911   also have "\<dots> \<le> (limsup (\<lambda>n. \<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - limsup (\<lambda>n. \<integral>\<^sup>+x. norm (F n x - f x) \<partial>M)) +
```
```   912     limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M))"
```
```   913     by (intro add_mono liminf_minus_ennreal le2) auto
```
```   914   also have "\<dots> = limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M))"
```
```   915     by (intro diff_add_cancel_ennreal Limsup_mono always_eventually allI le2)
```
```   916   also have "\<dots> \<le> 2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
```
```   917     by fact
```
```   918   finally have "limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)) = 0"
```
```   919     using fin2 by simp
```
```   920   then show ?thesis
```
```   921     by (rule tendsto_0_if_Limsup_eq_0_ennreal)
```
```   922 qed
```
```   923
```
```   924 proposition Scheffe_lemma2:
```
```   925   fixes F::"nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
```
```   926   assumes "\<And> n::nat. F n \<in> borel_measurable M" "integrable M f"
```
```   927           "AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
```
```   928           "\<And>n. (\<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
```
```   929   shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
```
```   930 proof (rule Scheffe_lemma1)
```
```   931   fix n::nat
```
```   932   have "(\<integral>\<^sup>+ x. norm(f x) \<partial>M) < \<infinity>" using assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.cases)
```
```   933   then have "(\<integral>\<^sup>+ x. norm(F n x) \<partial>M) < \<infinity>" using assms(4)[of n] by auto
```
```   934   then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
```
```   935 qed (auto simp add: assms Limsup_bounded)
```
```   936
```
```   937 lemma tendsto_set_lebesgue_integral_at_right:
```
```   938   fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
```
```   939   assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
```
```   940       and "set_integrable M {a<..b} f"
```
```   941   shows   "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
```
```   942              set_lebesgue_integral M {a<..b} f) (at_right a)"
```
```   943 proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
```
```   944   case (1 S)
```
```   945   have eq: "(\<Union>n. {S n..b}) = {a<..b}"
```
```   946   proof safe
```
```   947     fix x n assume "x \<in> {S n..b}"
```
```   948     with 1(1,2)[of n] show "x \<in> {a<..b}" by auto
```
```   949   next
```
```   950     fix x assume "x \<in> {a<..b}"
```
```   951     with order_tendstoD[OF \<open>S \<longlonglongrightarrow> a\<close>, of x] show "x \<in> (\<Union>n. {S n..b})"
```
```   952       by (force simp: eventually_at_top_linorder dest: less_imp_le)
```
```   953   qed
```
```   954   have "(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f"
```
```   955     by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
```
```   956   with eq show ?case by simp
```
```   957 qed
```
```   958
```
```   959
```
```   960 text \<open>
```
```   961   The next lemmas relate convergence of integrals over an interval to
```
```   962   improper integrals.
```
```   963 \<close>
```
```   964 lemma tendsto_set_lebesgue_integral_at_left:
```
```   965   fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
```
```   966   assumes "a < b" and sets: "\<And>b'. b' \<in> {a..<b} \<Longrightarrow> {a..b'} \<in> sets M"
```
```   967       and "set_integrable M {a..<b} f"
```
```   968   shows   "((\<lambda>b'. set_lebesgue_integral M {a..b'} f) \<longlongrightarrow>
```
```   969              set_lebesgue_integral M {a..<b} f) (at_left b)"
```
```   970 proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
```
```   971   case (1 S)
```
```   972   have eq: "(\<Union>n. {a..S n}) = {a..<b}"
```
```   973   proof safe
```
```   974     fix x n assume "x \<in> {a..S n}"
```
```   975     with 1(1,2)[of n] show "x \<in> {a..<b}" by auto
```
```   976   next
```
```   977     fix x assume "x \<in> {a..<b}"
```
```   978     with order_tendstoD[OF \<open>S \<longlonglongrightarrow> b\<close>, of x] show "x \<in> (\<Union>n. {a..S n})"
```
```   979       by (force simp: eventually_at_top_linorder dest: less_imp_le)
```
```   980   qed
```
```   981   have "(\<lambda>n. set_lebesgue_integral M {a..S n} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {a..S n}) f"
```
```   982     by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
```
```   983   with eq show ?case by simp
```
```   984 qed
```
```   985
```
```   986 proposition tendsto_set_lebesgue_integral_at_top:
```
```   987   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
```
```   988   assumes sets: "\<And>b. b \<ge> a \<Longrightarrow> {a..b} \<in> sets M"
```
```   989       and int: "set_integrable M {a..} f"
```
```   990   shows "((\<lambda>b. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {a..} f) at_top"
```
```   991 proof (rule tendsto_at_topI_sequentially)
```
```   992   fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
```
```   993   show "(\<lambda>n. set_lebesgue_integral M {a..X n} f) \<longlonglongrightarrow> set_lebesgue_integral M {a..} f"
```
```   994     unfolding set_lebesgue_integral_def
```
```   995   proof (rule integral_dominated_convergence)
```
```   996     show "integrable M (\<lambda>x. indicat_real {a..} x *\<^sub>R norm (f x))"
```
```   997       using integrable_norm[OF int[unfolded set_integrable_def]] by simp
```
```   998     show "AE x in M. (\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
```
```   999     proof
```
```  1000       fix x
```
```  1001       from \<open>filterlim X at_top sequentially\<close>
```
```  1002       have "eventually (\<lambda>n. x \<le> X n) sequentially"
```
```  1003         unfolding filterlim_at_top_ge[where c=x] by auto
```
```  1004       then show "(\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
```
```  1005         by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
```
```  1006     qed
```
```  1007     fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \<le>
```
```  1008                              indicator {a..} x *\<^sub>R norm (f x)"
```
```  1009       by (auto split: split_indicator)
```
```  1010   next
```
```  1011     from int show "(\<lambda>x. indicat_real {a..} x *\<^sub>R f x) \<in> borel_measurable M"
```
```  1012       by (simp add: set_integrable_def)
```
```  1013   next
```
```  1014     fix n :: nat
```
```  1015     from sets have "{a..X n} \<in> sets M" by (cases "X n \<ge> a") auto
```
```  1016     with int have "set_integrable M {a..X n} f"
```
```  1017       by (rule set_integrable_subset) auto
```
```  1018     thus "(\<lambda>x. indicat_real {a..X n} x *\<^sub>R f x) \<in> borel_measurable M"
```
```  1019       by (simp add: set_integrable_def)
```
```  1020   qed
```
```  1021 qed
```
```  1022
```
```  1023 proposition tendsto_set_lebesgue_integral_at_bot:
```
```  1024   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
```
```  1025   assumes sets: "\<And>a. a \<le> b \<Longrightarrow> {a..b} \<in> sets M"
```
```  1026       and int: "set_integrable M {..b} f"
```
```  1027     shows "((\<lambda>a. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {..b} f) at_bot"
```
```  1028 proof (rule tendsto_at_botI_sequentially)
```
```  1029   fix X :: "nat \<Rightarrow> real" assume "filterlim X at_bot sequentially"
```
```  1030   show "(\<lambda>n. set_lebesgue_integral M {X n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {..b} f"
```
```  1031     unfolding set_lebesgue_integral_def
```
```  1032   proof (rule integral_dominated_convergence)
```
```  1033     show "integrable M (\<lambda>x. indicat_real {..b} x *\<^sub>R norm (f x))"
```
```  1034       using integrable_norm[OF int[unfolded set_integrable_def]] by simp
```
```  1035     show "AE x in M. (\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
```
```  1036     proof
```
```  1037       fix x
```
```  1038       from \<open>filterlim X at_bot sequentially\<close>
```
```  1039       have "eventually (\<lambda>n. x \<ge> X n) sequentially"
```
```  1040         unfolding filterlim_at_bot_le[where c=x] by auto
```
```  1041       then show "(\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
```
```  1042         by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
```
```  1043     qed
```
```  1044     fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \<le>
```
```  1045                              indicator {..b} x *\<^sub>R norm (f x)"
```
```  1046       by (auto split: split_indicator)
```
```  1047   next
```
```  1048     from int show "(\<lambda>x. indicat_real {..b} x *\<^sub>R f x) \<in> borel_measurable M"
```
```  1049       by (simp add: set_integrable_def)
```
```  1050   next
```
```  1051     fix n :: nat
```
```  1052     from sets have "{X n..b} \<in> sets M" by (cases "X n \<le> b") auto
```
```  1053     with int have "set_integrable M {X n..b} f"
```
```  1054       by (rule set_integrable_subset) auto
```
```  1055     thus "(\<lambda>x. indicat_real {X n..b} x *\<^sub>R f x) \<in> borel_measurable M"
```
```  1056       by (simp add: set_integrable_def)
```
```  1057   qed
```
```  1058 qed
```
```  1059
```
```  1060 end
```