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