src/HOL/Analysis/Set_Integral.thy
 author hoelzl Fri Sep 16 13:56:51 2016 +0200 (2016-09-16) changeset 63886 685fb01256af parent 63627 6ddb43c6b711 child 63941 f353674c2528 permissions -rw-r--r--
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
```     1 (*  Title:      HOL/Analysis/Set_Integral.thy
```
```     2     Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
```
```     3
```
```     4 Notation and useful facts for working with integrals over a set.
```
```     5
```
```     6 TODO: keep all these? Need unicode translations as well.
```
```     7 *)
```
```     8
```
```     9 theory Set_Integral
```
```    10   imports Equivalence_Lebesgue_Henstock_Integration
```
```    11 begin
```
```    12
```
```    13 (*
```
```    14     Notation
```
```    15 *)
```
```    16
```
```    17 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
```
```    18
```
```    19 abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```    20
```
```    21 abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```    22
```
```    23 syntax
```
```    24 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
```
```    25 ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
```
```    26
```
```    27 translations
```
```    28 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
```
```    29
```
```    30 abbreviation
```
```    31   "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
```
```    32
```
```    33 syntax
```
```    34   "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
```
```    35 ("AE _\<in>_ in _./ _" [0,0,0,10] 10)
```
```    36
```
```    37 translations
```
```    38   "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
```
```    39
```
```    40 (*
```
```    41     Notation for integration wrt lebesgue measure on the reals:
```
```    42
```
```    43       LBINT x. f
```
```    44       LBINT x : A. f
```
```    45
```
```    46     TODO: keep all these? Need unicode.
```
```    47 *)
```
```    48
```
```    49 syntax
```
```    50 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
```
```    51 ("(2LBINT _./ _)" [0,60] 60)
```
```    52
```
```    53 translations
```
```    54 "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
```
```    55
```
```    56 syntax
```
```    57 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
```
```    58 ("(3LBINT _:_./ _)" [0,60,61] 60)
```
```    59
```
```    60 translations
```
```    61 "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
```
```    62
```
```    63 (*
```
```    64     Basic properties
```
```    65 *)
```
```    66
```
```    67 (*
```
```    68 lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
```
```    69   by (auto simp add: indicator_def)
```
```    70 *)
```
```    71
```
```    72 lemma set_borel_measurable_sets:
```
```    73   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
```
```    74   assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
```
```    75   shows "f -` B \<inter> X \<in> sets M"
```
```    76 proof -
```
```    77   have "f \<in> borel_measurable (restrict_space M X)"
```
```    78     using assms by (subst borel_measurable_restrict_space_iff) auto
```
```    79   then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
```
```    80     by (rule measurable_sets) fact
```
```    81   with \<open>X \<in> sets M\<close> show ?thesis
```
```    82     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
```
```    83 qed
```
```    84
```
```    85 lemma set_lebesgue_integral_cong:
```
```    86   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
```
```    87   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
```
```    88   using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
```
```    89
```
```    90 lemma set_lebesgue_integral_cong_AE:
```
```    91   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
```
```    92   assumes "AE x \<in> A in M. f x = g x"
```
```    93   shows "LINT x:A|M. f x = LINT x:A|M. g x"
```
```    94 proof-
```
```    95   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
```
```    96     using assms by auto
```
```    97   thus ?thesis 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   by (rule integrable_cong_AE) auto
```
```   105
```
```   106 lemma set_integrable_subset:
```
```   107   fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   108   assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
```
```   109   shows "set_integrable M B f"
```
```   110 proof -
```
```   111   have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```   112     by (rule integrable_mult_indicator) fact+
```
```   113   with \<open>B \<subseteq> A\<close> show ?thesis
```
```   114     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
```
```   115 qed
```
```   116
```
```   117 (* TODO: integral_cmul_indicator should be named set_integral_const *)
```
```   118 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
```
```   119
```
```   120 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
```
```   121   by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
```
```   122
```
```   123 lemma set_integral_mult_right [simp]:
```
```   124   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   125   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
```
```   126   by (subst integral_mult_right_zero[symmetric]) auto
```
```   127
```
```   128 lemma set_integral_mult_left [simp]:
```
```   129   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   130   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
```
```   131   by (subst integral_mult_left_zero[symmetric]) auto
```
```   132
```
```   133 lemma set_integral_divide_zero [simp]:
```
```   134   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
```
```   135   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
```
```   136   by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
```
```   137      (auto split: split_indicator)
```
```   138
```
```   139 lemma set_integrable_scaleR_right [simp, intro]:
```
```   140   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
```
```   141   unfolding scaleR_left_commute by (rule integrable_scaleR_right)
```
```   142
```
```   143 lemma set_integrable_scaleR_left [simp, intro]:
```
```   144   fixes a :: "_ :: {banach, second_countable_topology}"
```
```   145   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
```
```   146   using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
```
```   147
```
```   148 lemma set_integrable_mult_right [simp, intro]:
```
```   149   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   150   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
```
```   151   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
```
```   152
```
```   153 lemma set_integrable_mult_left [simp, intro]:
```
```   154   fixes a :: "'a::{real_normed_field, second_countable_topology}"
```
```   155   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
```
```   156   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
```
```   157
```
```   158 lemma set_integrable_divide [simp, intro]:
```
```   159   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
```
```   160   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
```
```   161   shows "set_integrable M A (\<lambda>t. f t / a)"
```
```   162 proof -
```
```   163   have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
```
```   164     using assms by (rule integrable_divide_zero)
```
```   165   also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
```
```   166     by (auto split: split_indicator)
```
```   167   finally show ?thesis .
```
```   168 qed
```
```   169
```
```   170 lemma set_integral_add [simp, intro]:
```
```   171   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   172   assumes "set_integrable M A f" "set_integrable M A g"
```
```   173   shows "set_integrable M A (\<lambda>x. f x + g x)"
```
```   174     and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
```
```   175   using assms by (simp_all add: scaleR_add_right)
```
```   176
```
```   177 lemma set_integral_diff [simp, intro]:
```
```   178   assumes "set_integrable M A f" "set_integrable M A g"
```
```   179   shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
```
```   180     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
```
```   181   using assms by (simp_all add: scaleR_diff_right)
```
```   182
```
```   183 lemma set_integral_reflect:
```
```   184   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   185   shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
```
```   186   by (subst lborel_integral_real_affine[where c="-1" and t=0])
```
```   187      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
```
```   188
```
```   189 (* question: why do we have this for negation, but multiplication by a constant
```
```   190    requires an integrability assumption? *)
```
```   191 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
```
```   192   by (subst integral_minus[symmetric]) simp_all
```
```   193
```
```   194 lemma set_integral_complex_of_real:
```
```   195   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
```
```   196   by (subst integral_complex_of_real[symmetric])
```
```   197      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
```
```   198
```
```   199 lemma set_integral_mono:
```
```   200   fixes f g :: "_ \<Rightarrow> real"
```
```   201   assumes "set_integrable M A f" "set_integrable M A g"
```
```   202     "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
```
```   203   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
```
```   204 using assms by (auto intro: integral_mono split: split_indicator)
```
```   205
```
```   206 lemma set_integral_mono_AE:
```
```   207   fixes f g :: "_ \<Rightarrow> real"
```
```   208   assumes "set_integrable M A f" "set_integrable M A g"
```
```   209     "AE x \<in> A in M. f x \<le> g x"
```
```   210   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
```
```   211 using assms by (auto intro: integral_mono_AE split: split_indicator)
```
```   212
```
```   213 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
```
```   214   using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
```
```   215
```
```   216 lemma set_integrable_abs_iff:
```
```   217   fixes f :: "_ \<Rightarrow> real"
```
```   218   shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
```
```   219   by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
```
```   220
```
```   221 lemma set_integrable_abs_iff':
```
```   222   fixes f :: "_ \<Rightarrow> real"
```
```   223   shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
```
```   224     set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
```
```   225 by (intro set_integrable_abs_iff) auto
```
```   226
```
```   227 lemma set_integrable_discrete_difference:
```
```   228   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
```
```   229   assumes "countable X"
```
```   230   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
```
```   231   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
```
```   232   shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
```
```   233 proof (rule integrable_discrete_difference[where X=X])
```
```   234   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"
```
```   235     using diff by (auto split: split_indicator)
```
```   236 qed fact+
```
```   237
```
```   238 lemma set_integral_discrete_difference:
```
```   239   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
```
```   240   assumes "countable X"
```
```   241   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
```
```   242   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
```
```   243   shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
```
```   244 proof (rule integral_discrete_difference[where X=X])
```
```   245   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"
```
```   246     using diff by (auto split: split_indicator)
```
```   247 qed fact+
```
```   248
```
```   249 lemma set_integrable_Un:
```
```   250   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   251   assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
```
```   252     and [measurable]: "A \<in> sets M" "B \<in> sets M"
```
```   253   shows "set_integrable M (A \<union> B) f"
```
```   254 proof -
```
```   255   have "set_integrable M (A - B) f"
```
```   256     using f_A by (rule set_integrable_subset) auto
```
```   257   from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
```
```   258     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
```
```   259 qed
```
```   260
```
```   261 lemma set_integrable_UN:
```
```   262   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   263   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
```
```   264     "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
```
```   265   shows "set_integrable M (\<Union>i\<in>I. A i) f"
```
```   266 using assms by (induct I) (auto intro!: set_integrable_Un)
```
```   267
```
```   268 lemma set_integral_Un:
```
```   269   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   270   assumes "A \<inter> B = {}"
```
```   271   and "set_integrable M A f"
```
```   272   and "set_integrable M B f"
```
```   273   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
```
```   274 by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
```
```   275       scaleR_add_left assms)
```
```   276
```
```   277 lemma set_integral_cong_set:
```
```   278   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   279   assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
```
```   280     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
```
```   281   shows "LINT x:B|M. f x = LINT x:A|M. f x"
```
```   282 proof (rule integral_cong_AE)
```
```   283   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
```
```   284     using ae by (auto simp: subset_eq split: split_indicator)
```
```   285 qed fact+
```
```   286
```
```   287 lemma set_borel_measurable_subset:
```
```   288   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   289   assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
```
```   290   shows "set_borel_measurable M B f"
```
```   291 proof -
```
```   292   have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
```
```   293     by measurable
```
```   294   also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
```
```   295     using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
```
```   296   finally show ?thesis .
```
```   297 qed
```
```   298
```
```   299 lemma set_integral_Un_AE:
```
```   300   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   301   assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
```
```   302   and "set_integrable M A f"
```
```   303   and "set_integrable M B f"
```
```   304   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
```
```   305 proof -
```
```   306   have f: "set_integrable M (A \<union> B) f"
```
```   307     by (intro set_integrable_Un assms)
```
```   308   then have f': "set_borel_measurable M (A \<union> B) f"
```
```   309     by (rule borel_measurable_integrable)
```
```   310   have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
```
```   311   proof (rule set_integral_cong_set)
```
```   312     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
```
```   313       using ae by auto
```
```   314     show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
```
```   315       using f' by (rule set_borel_measurable_subset) auto
```
```   316   qed fact
```
```   317   also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
```
```   318     by (auto intro!: set_integral_Un set_integrable_subset[OF f])
```
```   319   also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
```
```   320     using ae
```
```   321     by (intro arg_cong2[where f="op+"] set_integral_cong_set)
```
```   322        (auto intro!: set_borel_measurable_subset[OF f'])
```
```   323   finally show ?thesis .
```
```   324 qed
```
```   325
```
```   326 lemma set_integral_finite_Union:
```
```   327   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
```
```   328   assumes "finite I" "disjoint_family_on A I"
```
```   329     and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
```
```   330   shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
```
```   331   using assms
```
```   332   apply induct
```
```   333   apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
```
```   334 by (subst set_integral_Un, auto intro: set_integrable_UN)
```
```   335
```
```   336 (* TODO: find a better name? *)
```
```   337 lemma pos_integrable_to_top:
```
```   338   fixes l::real
```
```   339   assumes "\<And>i. A i \<in> sets M" "mono A"
```
```   340   assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
```
```   341   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
```
```   342   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
```
```   343   shows "set_integrable M (\<Union>i. A i) f"
```
```   344   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
```
```   345   apply (rule intgbl)
```
```   346   prefer 3 apply (rule lim)
```
```   347   apply (rule AE_I2)
```
```   348   using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
```
```   349 proof (rule AE_I2)
```
```   350   { fix x assume "x \<in> space M"
```
```   351     show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
```
```   352     proof cases
```
```   353       assume "\<exists>i. x \<in> A i"
```
```   354       then guess i ..
```
```   355       then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
```
```   356         using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
```
```   357       show ?thesis
```
```   358         apply (intro Lim_eventually)
```
```   359         using *
```
```   360         apply eventually_elim
```
```   361         apply (auto split: split_indicator)
```
```   362         done
```
```   363     qed auto }
```
```   364   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
```
```   365     apply (rule borel_measurable_LIMSEQ_real)
```
```   366     apply assumption
```
```   367     apply (intro borel_measurable_integrable intgbl)
```
```   368     done
```
```   369 qed
```
```   370
```
```   371 (* Proof from Royden Real Analysis, p. 91. *)
```
```   372 lemma lebesgue_integral_countable_add:
```
```   373   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   374   assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
```
```   375     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
```
```   376     and intgbl: "set_integrable M (\<Union>i. A i) f"
```
```   377   shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
```
```   378 proof (subst integral_suminf[symmetric])
```
```   379   show int_A: "\<And>i. set_integrable M (A i) f"
```
```   380     using intgbl by (rule set_integrable_subset) auto
```
```   381   { fix x assume "x \<in> space M"
```
```   382     have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
```
```   383       by (intro sums_scaleR_left indicator_sums) fact }
```
```   384   note sums = this
```
```   385
```
```   386   have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
```
```   387     using int_A[THEN integrable_norm] by auto
```
```   388
```
```   389   show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
```
```   390     using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
```
```   391
```
```   392   show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
```
```   393   proof (rule summableI_nonneg_bounded)
```
```   394     fix n
```
```   395     show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
```
```   396       using norm_f by (auto intro!: integral_nonneg_AE)
```
```   397
```
```   398     have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
```
```   399       (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
```
```   400       by (simp add: abs_mult)
```
```   401     also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
```
```   402       using norm_f
```
```   403       by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
```
```   404     also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
```
```   405       using intgbl[THEN integrable_norm]
```
```   406       by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
```
```   407          (auto split: split_indicator)
```
```   408     finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
```
```   409       set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
```
```   410       by simp
```
```   411   qed
```
```   412   show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
```
```   413     apply (rule Bochner_Integration.integral_cong[OF refl])
```
```   414     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
```
```   415     using sums_unique[OF indicator_sums[OF disj]]
```
```   416     apply auto
```
```   417     done
```
```   418 qed
```
```   419
```
```   420 lemma set_integral_cont_up:
```
```   421   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   422   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
```
```   423   and intgbl: "set_integrable M (\<Union>i. A i) f"
```
```   424   shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
```
```   425 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
```
```   426   have int_A: "\<And>i. set_integrable M (A i) f"
```
```   427     using intgbl by (rule set_integrable_subset) auto
```
```   428   then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
```
```   429     "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
```
```   430     using intgbl integrable_norm[OF intgbl] by auto
```
```   431
```
```   432   { fix x i assume "x \<in> A i"
```
```   433     with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
```
```   434       by (intro filterlim_cong refl)
```
```   435          (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
```
```   436   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"
```
```   437     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
```
```   438 qed (auto split: split_indicator)
```
```   439
```
```   440 (* Can the int0 hypothesis be dropped? *)
```
```   441 lemma set_integral_cont_down:
```
```   442   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
```
```   443   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
```
```   444   and int0: "set_integrable M (A 0) f"
```
```   445   shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
```
```   446 proof (rule integral_dominated_convergence)
```
```   447   have int_A: "\<And>i. set_integrable M (A i) f"
```
```   448     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
```
```   449   show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
```
```   450     using int0[THEN integrable_norm] by simp
```
```   451   have "set_integrable M (\<Inter>i. A i) f"
```
```   452     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
```
```   453   with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
```
```   454     by auto
```
```   455   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)"
```
```   456     using A by (auto split: split_indicator simp: decseq_def)
```
```   457   { fix x i assume "x \<in> space M" "x \<notin> A i"
```
```   458     with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
```
```   459       by (intro filterlim_cong refl)
```
```   460          (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
```
```   461   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"
```
```   462     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
```
```   463 qed
```
```   464
```
```   465 lemma set_integral_at_point:
```
```   466   fixes a :: real
```
```   467   assumes "set_integrable M {a} f"
```
```   468   and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
```
```   469   shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
```
```   470 proof-
```
```   471   have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
```
```   472     by (intro set_lebesgue_integral_cong) simp_all
```
```   473   then show ?thesis using assms by simp
```
```   474 qed
```
```   475
```
```   476
```
```   477 abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
```
```   478   "complex_integrable M f \<equiv> integrable M f"
```
```   479
```
```   480 abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
```
```   481   "integral\<^sup>C M f == integral\<^sup>L M f"
```
```   482
```
```   483 syntax
```
```   484   "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
```
```   485  ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
```
```   486
```
```   487 translations
```
```   488   "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
```
```   489
```
```   490 syntax
```
```   491   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
```
```   492   ("(3CLINT _|_. _)" [0,110,60] 60)
```
```   493
```
```   494 translations
```
```   495   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
```
```   496
```
```   497 lemma complex_integrable_cnj [simp]:
```
```   498   "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
```
```   499 proof
```
```   500   assume "complex_integrable M (\<lambda>x. cnj (f x))"
```
```   501   then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
```
```   502     by (rule integrable_cnj)
```
```   503   then show "complex_integrable M f"
```
```   504     by simp
```
```   505 qed simp
```
```   506
```
```   507 lemma complex_of_real_integrable_eq:
```
```   508   "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
```
```   509 proof
```
```   510   assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
```
```   511   then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
```
```   512     by (rule integrable_Re)
```
```   513   then show "integrable M f"
```
```   514     by simp
```
```   515 qed simp
```
```   516
```
```   517
```
```   518 abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
```
```   519   "complex_set_integrable M A f \<equiv> set_integrable M A f"
```
```   520
```
```   521 abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
```
```   522   "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
```
```   523
```
```   524 syntax
```
```   525 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
```
```   526 ("(4CLINT _:_|_. _)" [0,60,110,61] 60)
```
```   527
```
```   528 translations
```
```   529 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
```
```   530
```
```   531 (*
```
```   532 lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
```
```   533   apply (simp add: norm_mult)
```
```   534   by (subst norm_mult, auto)
```
```   535 *)
```
```   536
```
```   537 lemma borel_integrable_atLeastAtMost':
```
```   538   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
```
```   539   assumes f: "continuous_on {a..b} f"
```
```   540   shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
```
```   541   by (intro borel_integrable_compact compact_Icc f)
```
```   542
```
```   543 lemma integral_FTC_atLeastAtMost:
```
```   544   fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
```
```   545   assumes "a \<le> b"
```
```   546     and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
```
```   547     and f: "continuous_on {a .. b} f"
```
```   548   shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
```
```   549 proof -
```
```   550   let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
```
```   551   have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
```
```   552     using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
```
```   553   moreover
```
```   554   have "(f has_integral F b - F a) {a .. b}"
```
```   555     by (intro fundamental_theorem_of_calculus ballI assms) auto
```
```   556   then have "(?f has_integral F b - F a) {a .. b}"
```
```   557     by (subst has_integral_cong[where g=f]) auto
```
```   558   then have "(?f has_integral F b - F a) UNIV"
```
```   559     by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
```
```   560   ultimately show "integral\<^sup>L lborel ?f = F b - F a"
```
```   561     by (rule has_integral_unique)
```
```   562 qed
```
```   563
```
```   564 lemma set_borel_integral_eq_integral:
```
```   565   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
```
```   566   assumes "set_integrable lborel S f"
```
```   567   shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
```
```   568 proof -
```
```   569   let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
```
```   570   have "(?f has_integral LINT x : S | lborel. f x) UNIV"
```
```   571     by (rule has_integral_integral_lborel) fact
```
```   572   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
```
```   573     apply (subst has_integral_restrict_univ [symmetric])
```
```   574     apply (rule has_integral_eq)
```
```   575     by auto
```
```   576   thus "f integrable_on S"
```
```   577     by (auto simp add: integrable_on_def)
```
```   578   with 1 have "(f has_integral (integral S f)) S"
```
```   579     by (intro integrable_integral, auto simp add: integrable_on_def)
```
```   580   thus "LINT x : S | lborel. f x = integral S f"
```
```   581     by (intro has_integral_unique [OF 1])
```
```   582 qed
```
```   583
```
```   584 lemma set_borel_measurable_continuous:
```
```   585   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
```
```   586   assumes "S \<in> sets borel" "continuous_on S f"
```
```   587   shows "set_borel_measurable borel S f"
```
```   588 proof -
```
```   589   have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
```
```   590     by (intro assms borel_measurable_continuous_on_if continuous_on_const)
```
```   591   also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
```
```   592     by auto
```
```   593   finally show ?thesis .
```
```   594 qed
```
```   595
```
```   596 lemma set_measurable_continuous_on_ivl:
```
```   597   assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
```
```   598   shows "set_borel_measurable borel {a..b} f"
```
```   599   by (rule set_borel_measurable_continuous[OF _ assms]) simp
```
```   600
```
```   601 end
```
```   602
```