src/HOL/Analysis/Set_Integral.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (8 months ago)
changeset 69313 b021008c5397
parent 69173 38beaaebe736
child 69566 c41954ee87cf
permissions -rw-r--r--
removed legacy input syntax
     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 lemma%important 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%unimportant-
   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%important 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%unimportant 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%important 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 lemma 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 $L^1$ 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 lemma%important 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%unimportant -
   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 lemma%important 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%unimportant (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%important 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%unimportant (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%important 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%unimportant (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 lemma%important 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%unimportant (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 lemma%important 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%unimportant (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