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