src/HOL/Probability/Lebesgue_Integration.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 38642 src/HOL/Probability/Lebesgue.thy@8fa437809c67
child 38705 aaee86c0e237
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
hoelzl@38656
     1
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
hoelzl@38656
     2
hoelzl@35582
     3
header {*Lebesgue Integration*}
hoelzl@35582
     4
hoelzl@38656
     5
theory Lebesgue_Integration
hoelzl@35582
     6
imports Measure Borel
hoelzl@35582
     7
begin
hoelzl@35582
     8
hoelzl@38656
     9
section "@{text \<mu>}-null sets"
hoelzl@35582
    10
hoelzl@38656
    11
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
hoelzl@35582
    12
hoelzl@38656
    13
lemma sums_If_finite:
hoelzl@38656
    14
  assumes finite: "finite {r. P r}"
hoelzl@38656
    15
  shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")
hoelzl@38656
    16
proof cases
hoelzl@38656
    17
  assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto
hoelzl@38656
    18
  thus ?thesis by (simp add: sums_zero)
hoelzl@38656
    19
next
hoelzl@38656
    20
  assume not_empty: "{r. P r} \<noteq> {}"
hoelzl@38656
    21
  have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"
hoelzl@38656
    22
    by (rule series_zero)
hoelzl@38656
    23
       (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])
hoelzl@38656
    24
  also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"
hoelzl@38656
    25
    by (subst setsum_cases)
hoelzl@38656
    26
       (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)
hoelzl@38656
    27
  finally show ?thesis .
hoelzl@38656
    28
qed
hoelzl@35582
    29
hoelzl@38656
    30
lemma sums_single:
hoelzl@38656
    31
  "(\<lambda>r. if r = i then f r else 0) sums f i"
hoelzl@38656
    32
  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
hoelzl@38656
    33
hoelzl@38656
    34
section "Simple function"
hoelzl@35582
    35
hoelzl@38656
    36
text {*
hoelzl@38656
    37
hoelzl@38656
    38
Our simple functions are not restricted to positive real numbers. Instead
hoelzl@38656
    39
they are just functions with a finite range and are measurable when singleton
hoelzl@38656
    40
sets are measurable.
hoelzl@35582
    41
hoelzl@38656
    42
*}
hoelzl@38656
    43
hoelzl@38656
    44
definition (in sigma_algebra) "simple_function g \<longleftrightarrow>
hoelzl@38656
    45
    finite (g ` space M) \<and>
hoelzl@38656
    46
    (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"
hoelzl@36624
    47
hoelzl@38656
    48
lemma (in sigma_algebra) simple_functionD:
hoelzl@38656
    49
  assumes "simple_function g"
hoelzl@38656
    50
  shows "finite (g ` space M)"
hoelzl@38656
    51
  "x \<in> g ` space M \<Longrightarrow> g -` {x} \<inter> space M \<in> sets M"
hoelzl@38656
    52
  using assms unfolding simple_function_def by auto
hoelzl@36624
    53
hoelzl@38656
    54
lemma (in sigma_algebra) simple_function_indicator_representation:
hoelzl@38656
    55
  fixes f ::"'a \<Rightarrow> pinfreal"
hoelzl@38656
    56
  assumes f: "simple_function f" and x: "x \<in> space M"
hoelzl@38656
    57
  shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
hoelzl@38656
    58
  (is "?l = ?r")
hoelzl@38656
    59
proof -
hoelzl@38656
    60
  have "?r = (\<Sum>y \<in> f ` space M. 
hoelzl@38656
    61
    (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
hoelzl@38656
    62
    by (auto intro!: setsum_cong2)
hoelzl@38656
    63
  also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
hoelzl@38656
    64
    using assms by (auto dest: simple_functionD simp: setsum_delta)
hoelzl@38656
    65
  also have "... = f x" using x by (auto simp: indicator_def)
hoelzl@38656
    66
  finally show ?thesis by auto
hoelzl@38656
    67
qed
hoelzl@36624
    68
hoelzl@38656
    69
lemma (in measure_space) simple_function_notspace:
hoelzl@38656
    70
  "simple_function (\<lambda>x. h x * indicator (- space M) x::pinfreal)" (is "simple_function ?h")
hoelzl@35692
    71
proof -
hoelzl@38656
    72
  have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto
hoelzl@38656
    73
  hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
hoelzl@38656
    74
  have "?h -` {0} \<inter> space M = space M" by auto
hoelzl@38656
    75
  thus ?thesis unfolding simple_function_def by auto
hoelzl@38656
    76
qed
hoelzl@38656
    77
hoelzl@38656
    78
lemma (in sigma_algebra) simple_function_cong:
hoelzl@38656
    79
  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
hoelzl@38656
    80
  shows "simple_function f \<longleftrightarrow> simple_function g"
hoelzl@38656
    81
proof -
hoelzl@38656
    82
  have "f ` space M = g ` space M"
hoelzl@38656
    83
    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
hoelzl@38656
    84
    using assms by (auto intro!: image_eqI)
hoelzl@38656
    85
  thus ?thesis unfolding simple_function_def using assms by simp
hoelzl@38656
    86
qed
hoelzl@38656
    87
hoelzl@38656
    88
lemma (in sigma_algebra) borel_measurable_simple_function:
hoelzl@38656
    89
  assumes "simple_function f"
hoelzl@38656
    90
  shows "f \<in> borel_measurable M"
hoelzl@38656
    91
proof (rule borel_measurableI)
hoelzl@38656
    92
  fix S
hoelzl@38656
    93
  let ?I = "f ` (f -` S \<inter> space M)"
hoelzl@38656
    94
  have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto
hoelzl@38656
    95
  have "finite ?I"
hoelzl@38656
    96
    using assms unfolding simple_function_def by (auto intro: finite_subset)
hoelzl@38656
    97
  hence "?U \<in> sets M"
hoelzl@38656
    98
    apply (rule finite_UN)
hoelzl@38656
    99
    using assms unfolding simple_function_def by auto
hoelzl@38656
   100
  thus "f -` S \<inter> space M \<in> sets M" unfolding * .
hoelzl@35692
   101
qed
hoelzl@35692
   102
hoelzl@38656
   103
lemma (in sigma_algebra) simple_function_borel_measurable:
hoelzl@38656
   104
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
hoelzl@38656
   105
  assumes "f \<in> borel_measurable M" and "finite (f ` space M)"
hoelzl@38656
   106
  shows "simple_function f"
hoelzl@38656
   107
  using assms unfolding simple_function_def
hoelzl@38656
   108
  by (auto intro: borel_measurable_vimage)
hoelzl@38656
   109
hoelzl@38656
   110
lemma (in sigma_algebra) simple_function_const[intro, simp]:
hoelzl@38656
   111
  "simple_function (\<lambda>x. c)"
hoelzl@38656
   112
  by (auto intro: finite_subset simp: simple_function_def)
hoelzl@38656
   113
hoelzl@38656
   114
lemma (in sigma_algebra) simple_function_compose[intro, simp]:
hoelzl@38656
   115
  assumes "simple_function f"
hoelzl@38656
   116
  shows "simple_function (g \<circ> f)"
hoelzl@38656
   117
  unfolding simple_function_def
hoelzl@38656
   118
proof safe
hoelzl@38656
   119
  show "finite ((g \<circ> f) ` space M)"
hoelzl@38656
   120
    using assms unfolding simple_function_def by (auto simp: image_compose)
hoelzl@38656
   121
next
hoelzl@38656
   122
  fix x assume "x \<in> space M"
hoelzl@38656
   123
  let ?G = "g -` {g (f x)} \<inter> (f`space M)"
hoelzl@38656
   124
  have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M =
hoelzl@38656
   125
    (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
hoelzl@38656
   126
  show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
hoelzl@38656
   127
    using assms unfolding simple_function_def *
hoelzl@38656
   128
    by (rule_tac finite_UN) (auto intro!: finite_UN)
hoelzl@38656
   129
qed
hoelzl@38656
   130
hoelzl@38656
   131
lemma (in sigma_algebra) simple_function_indicator[intro, simp]:
hoelzl@38656
   132
  assumes "A \<in> sets M"
hoelzl@38656
   133
  shows "simple_function (indicator A)"
hoelzl@35692
   134
proof -
hoelzl@38656
   135
  have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")
hoelzl@38656
   136
    by (auto simp: indicator_def)
hoelzl@38656
   137
  hence "finite ?S" by (rule finite_subset) simp
hoelzl@38656
   138
  moreover have "- A \<inter> space M = space M - A" by auto
hoelzl@38656
   139
  ultimately show ?thesis unfolding simple_function_def
hoelzl@38656
   140
    using assms by (auto simp: indicator_def_raw)
hoelzl@35692
   141
qed
hoelzl@35692
   142
hoelzl@38656
   143
lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
hoelzl@38656
   144
  assumes "simple_function f"
hoelzl@38656
   145
  assumes "simple_function g"
hoelzl@38656
   146
  shows "simple_function (\<lambda>x. (f x, g x))" (is "simple_function ?p")
hoelzl@38656
   147
  unfolding simple_function_def
hoelzl@38656
   148
proof safe
hoelzl@38656
   149
  show "finite (?p ` space M)"
hoelzl@38656
   150
    using assms unfolding simple_function_def
hoelzl@38656
   151
    by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto
hoelzl@38656
   152
next
hoelzl@38656
   153
  fix x assume "x \<in> space M"
hoelzl@38656
   154
  have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M =
hoelzl@38656
   155
      (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"
hoelzl@38656
   156
    by auto
hoelzl@38656
   157
  with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M"
hoelzl@38656
   158
    using assms unfolding simple_function_def by auto
hoelzl@38656
   159
qed
hoelzl@35692
   160
hoelzl@38656
   161
lemma (in sigma_algebra) simple_function_compose1:
hoelzl@38656
   162
  assumes "simple_function f"
hoelzl@38656
   163
  shows "simple_function (\<lambda>x. g (f x))"
hoelzl@38656
   164
  using simple_function_compose[OF assms, of g]
hoelzl@38656
   165
  by (simp add: comp_def)
hoelzl@35582
   166
hoelzl@38656
   167
lemma (in sigma_algebra) simple_function_compose2:
hoelzl@38656
   168
  assumes "simple_function f" and "simple_function g"
hoelzl@38656
   169
  shows "simple_function (\<lambda>x. h (f x) (g x))"
hoelzl@38656
   170
proof -
hoelzl@38656
   171
  have "simple_function ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"
hoelzl@38656
   172
    using assms by auto
hoelzl@38656
   173
  thus ?thesis by (simp_all add: comp_def)
hoelzl@38656
   174
qed
hoelzl@35582
   175
hoelzl@38656
   176
lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]
hoelzl@38656
   177
  and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]
hoelzl@38656
   178
  and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
hoelzl@38656
   179
  and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]
hoelzl@38656
   180
  and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]
hoelzl@38656
   181
  and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
hoelzl@38656
   182
hoelzl@38656
   183
lemma (in sigma_algebra) simple_function_setsum[intro, simp]:
hoelzl@38656
   184
  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"
hoelzl@38656
   185
  shows "simple_function (\<lambda>x. \<Sum>i\<in>P. f i x)"
hoelzl@38656
   186
proof cases
hoelzl@38656
   187
  assume "finite P" from this assms show ?thesis by induct auto
hoelzl@38656
   188
qed auto
hoelzl@35582
   189
hoelzl@38656
   190
lemma (in sigma_algebra) simple_function_le_measurable:
hoelzl@38656
   191
  assumes "simple_function f" "simple_function g"
hoelzl@38656
   192
  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
hoelzl@38656
   193
proof -
hoelzl@38656
   194
  have *: "{x \<in> space M. f x \<le> g x} =
hoelzl@38656
   195
    (\<Union>(F, G)\<in>f`space M \<times> g`space M.
hoelzl@38656
   196
      if F \<le> G then (f -` {F} \<inter> space M) \<inter> (g -` {G} \<inter> space M) else {})"
hoelzl@38656
   197
    apply (auto split: split_if_asm)
hoelzl@38656
   198
    apply (rule_tac x=x in bexI)
hoelzl@38656
   199
    apply (rule_tac x=x in bexI)
hoelzl@38656
   200
    by simp_all
hoelzl@38656
   201
  have **: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow>
hoelzl@38656
   202
    (f -` {f x} \<inter> space M) \<inter> (g -` {g y} \<inter> space M) \<in> sets M"
hoelzl@38656
   203
    using assms unfolding simple_function_def by auto
hoelzl@38656
   204
  have "finite (f`space M \<times> g`space M)"
hoelzl@38656
   205
    using assms unfolding simple_function_def by auto
hoelzl@38656
   206
  thus ?thesis unfolding *
hoelzl@38656
   207
    apply (rule finite_UN)
hoelzl@38656
   208
    using assms unfolding simple_function_def
hoelzl@38656
   209
    by (auto intro!: **)
hoelzl@35582
   210
qed
hoelzl@35582
   211
hoelzl@38656
   212
lemma setsum_indicator_disjoint_family:
hoelzl@38656
   213
  fixes f :: "'d \<Rightarrow> 'e::semiring_1"
hoelzl@38656
   214
  assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
hoelzl@38656
   215
  shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
hoelzl@38656
   216
proof -
hoelzl@38656
   217
  have "P \<inter> {i. x \<in> A i} = {j}"
hoelzl@38656
   218
    using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
hoelzl@38656
   219
    by auto
hoelzl@38656
   220
  thus ?thesis
hoelzl@38656
   221
    unfolding indicator_def
hoelzl@38656
   222
    by (simp add: if_distrib setsum_cases[OF `finite P`])
hoelzl@38656
   223
qed
hoelzl@35692
   224
hoelzl@38656
   225
lemma LeastI2_wellorder:
hoelzl@38656
   226
  fixes a :: "_ :: wellorder"
hoelzl@38656
   227
  assumes "P a"
hoelzl@38656
   228
  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
hoelzl@38656
   229
  shows "Q (Least P)"
hoelzl@38656
   230
proof (rule LeastI2_order)
hoelzl@38656
   231
  show "P (Least P)" using `P a` by (rule LeastI)
hoelzl@38656
   232
next
hoelzl@38656
   233
  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
hoelzl@38656
   234
next
hoelzl@38656
   235
  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
hoelzl@35582
   236
qed
hoelzl@35582
   237
hoelzl@38656
   238
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
hoelzl@38656
   239
  fixes u :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
   240
  assumes u: "u \<in> borel_measurable M"
hoelzl@38656
   241
  shows "\<exists>f. (\<forall>i. simple_function (f i) \<and> (\<forall>x\<in>space M. f i x \<noteq> \<omega>)) \<and> f \<up> u"
hoelzl@35582
   242
proof -
hoelzl@38656
   243
  have "\<exists>f. \<forall>x j. (of_nat j \<le> u x \<longrightarrow> f x j = j*2^j) \<and>
hoelzl@38656
   244
    (u x < of_nat j \<longrightarrow> of_nat (f x j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f x j)))"
hoelzl@38656
   245
    (is "\<exists>f. \<forall>x j. ?P x j (f x j)")
hoelzl@38656
   246
  proof(rule choice, rule, rule choice, rule)
hoelzl@38656
   247
    fix x j show "\<exists>n. ?P x j n"
hoelzl@38656
   248
    proof cases
hoelzl@38656
   249
      assume *: "u x < of_nat j"
hoelzl@38656
   250
      then obtain r where r: "u x = Real r" "0 \<le> r" by (cases "u x") auto
hoelzl@38656
   251
      from reals_Archimedean6a[of "r * 2^j"]
hoelzl@38656
   252
      obtain n :: nat where "real n \<le> r * 2 ^ j" "r * 2 ^ j < real (Suc n)"
hoelzl@38656
   253
        using `0 \<le> r` by (auto simp: zero_le_power zero_le_mult_iff)
hoelzl@38656
   254
      thus ?thesis using r * by (auto intro!: exI[of _ n])
hoelzl@38656
   255
    qed auto
hoelzl@35582
   256
  qed
hoelzl@38656
   257
  then obtain f where top: "\<And>j x. of_nat j \<le> u x \<Longrightarrow> f x j = j*2^j" and
hoelzl@38656
   258
    upper: "\<And>j x. u x < of_nat j \<Longrightarrow> of_nat (f x j) \<le> u x * 2^j" and
hoelzl@38656
   259
    lower: "\<And>j x. u x < of_nat j \<Longrightarrow> u x * 2^j < of_nat (Suc (f x j))" by blast
hoelzl@35582
   260
hoelzl@38656
   261
  { fix j x P
hoelzl@38656
   262
    assume 1: "of_nat j \<le> u x \<Longrightarrow> P (j * 2^j)"
hoelzl@38656
   263
    assume 2: "\<And>k. \<lbrakk> u x < of_nat j ; of_nat k \<le> u x * 2^j ; u x * 2^j < of_nat (Suc k) \<rbrakk> \<Longrightarrow> P k"
hoelzl@38656
   264
    have "P (f x j)"
hoelzl@38656
   265
    proof cases
hoelzl@38656
   266
      assume "of_nat j \<le> u x" thus "P (f x j)"
hoelzl@38656
   267
        using top[of j x] 1 by auto
hoelzl@38656
   268
    next
hoelzl@38656
   269
      assume "\<not> of_nat j \<le> u x"
hoelzl@38656
   270
      hence "u x < of_nat j" "of_nat (f x j) \<le> u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))"
hoelzl@38656
   271
        using upper lower by auto
hoelzl@38656
   272
      from 2[OF this] show "P (f x j)" .
hoelzl@38656
   273
    qed }
hoelzl@38656
   274
  note fI = this
hoelzl@38656
   275
hoelzl@38656
   276
  { fix j x
hoelzl@38656
   277
    have "f x j = j * 2 ^ j \<longleftrightarrow> of_nat j \<le> u x"
hoelzl@38656
   278
      by (rule fI, simp, cases "u x") (auto split: split_if_asm) }
hoelzl@38656
   279
  note f_eq = this
hoelzl@35582
   280
hoelzl@38656
   281
  { fix j x
hoelzl@38656
   282
    have "f x j \<le> j * 2 ^ j"
hoelzl@38656
   283
    proof (rule fI)
hoelzl@38656
   284
      fix k assume *: "u x < of_nat j"
hoelzl@38656
   285
      assume "of_nat k \<le> u x * 2 ^ j"
hoelzl@38656
   286
      also have "\<dots> \<le> of_nat (j * 2^j)"
hoelzl@38656
   287
        using * by (cases "u x") (auto simp: zero_le_mult_iff)
hoelzl@38656
   288
      finally show "k \<le> j*2^j" by (auto simp del: real_of_nat_mult)
hoelzl@38656
   289
    qed simp }
hoelzl@38656
   290
  note f_upper = this
hoelzl@35582
   291
hoelzl@38656
   292
  let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal"
hoelzl@38656
   293
  show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def
hoelzl@38656
   294
  proof (safe intro!: exI[of _ ?g])
hoelzl@38656
   295
    fix j
hoelzl@38656
   296
    have *: "?g j ` space M \<subseteq> (\<lambda>x. of_nat x / 2^j) ` {..j * 2^j}"
hoelzl@38656
   297
      using f_upper by auto
hoelzl@38656
   298
    thus "finite (?g j ` space M)" by (rule finite_subset) auto
hoelzl@38656
   299
  next
hoelzl@38656
   300
    fix j t assume "t \<in> space M"
hoelzl@38656
   301
    have **: "?g j -` {?g j t} \<inter> space M = {x \<in> space M. f t j = f x j}"
hoelzl@38656
   302
      by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff)
hoelzl@35582
   303
hoelzl@38656
   304
    show "?g j -` {?g j t} \<inter> space M \<in> sets M"
hoelzl@38656
   305
    proof cases
hoelzl@38656
   306
      assume "of_nat j \<le> u t"
hoelzl@38656
   307
      hence "?g j -` {?g j t} \<inter> space M = {x\<in>space M. of_nat j \<le> u x}"
hoelzl@38656
   308
        unfolding ** f_eq[symmetric] by auto
hoelzl@38656
   309
      thus "?g j -` {?g j t} \<inter> space M \<in> sets M"
hoelzl@38656
   310
        using u by auto
hoelzl@35582
   311
    next
hoelzl@38656
   312
      assume not_t: "\<not> of_nat j \<le> u t"
hoelzl@38656
   313
      hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \<le> j*2^j` by auto
hoelzl@38656
   314
      have split_vimage: "?g j -` {?g j t} \<inter> space M =
hoelzl@38656
   315
          {x\<in>space M. of_nat (f t j)/2^j \<le> u x} \<inter> {x\<in>space M. u x < of_nat (Suc (f t j))/2^j}"
hoelzl@38656
   316
        unfolding **
hoelzl@38656
   317
      proof safe
hoelzl@38656
   318
        fix x assume [simp]: "f t j = f x j"
hoelzl@38656
   319
        have *: "\<not> of_nat j \<le> u x" using not_t f_eq[symmetric] by simp
hoelzl@38656
   320
        hence "of_nat (f t j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f t j))"
hoelzl@38656
   321
          using upper lower by auto
hoelzl@38656
   322
        hence "of_nat (f t j) / 2^j \<le> u x \<and> u x < of_nat (Suc (f t j))/2^j" using *
hoelzl@38656
   323
          by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps)
hoelzl@38656
   324
        thus "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" by auto
hoelzl@38656
   325
      next
hoelzl@38656
   326
        fix x
hoelzl@38656
   327
        assume "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j"
hoelzl@38656
   328
        hence "of_nat (f t j) \<le> u x * 2 ^ j \<and> u x * 2 ^ j < of_nat (Suc (f t j))"
hoelzl@38656
   329
          by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps)
hoelzl@38656
   330
        hence 1: "of_nat (f t j) \<le> u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto
hoelzl@38656
   331
        note 2
hoelzl@38656
   332
        also have "\<dots> \<le> of_nat (j*2^j)"
hoelzl@38656
   333
          using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult)
hoelzl@38656
   334
        finally have bound_ux: "u x < of_nat j"
hoelzl@38656
   335
          by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq)
hoelzl@38656
   336
        show "f t j = f x j"
hoelzl@38656
   337
        proof (rule antisym)
hoelzl@38656
   338
          from 1 lower[OF bound_ux]
hoelzl@38656
   339
          show "f t j \<le> f x j" by (cases "u x") (auto split: split_if_asm)
hoelzl@38656
   340
          from upper[OF bound_ux] 2
hoelzl@38656
   341
          show "f x j \<le> f t j" by (cases "u x") (auto split: split_if_asm)
hoelzl@38656
   342
        qed
hoelzl@38656
   343
      qed
hoelzl@38656
   344
      show ?thesis unfolding split_vimage using u by auto
hoelzl@35582
   345
    qed
hoelzl@38656
   346
  next
hoelzl@38656
   347
    fix j t assume "?g j t = \<omega>" thus False by (auto simp: power_le_zero_eq)
hoelzl@38656
   348
  next
hoelzl@38656
   349
    fix t
hoelzl@38656
   350
    { fix i
hoelzl@38656
   351
      have "f t i * 2 \<le> f t (Suc i)"
hoelzl@38656
   352
      proof (rule fI)
hoelzl@38656
   353
        assume "of_nat (Suc i) \<le> u t"
hoelzl@38656
   354
        hence "of_nat i \<le> u t" by (cases "u t") auto
hoelzl@38656
   355
        thus "f t i * 2 \<le> Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp
hoelzl@38656
   356
      next
hoelzl@38656
   357
        fix k
hoelzl@38656
   358
        assume *: "u t * 2 ^ Suc i < of_nat (Suc k)"
hoelzl@38656
   359
        show "f t i * 2 \<le> k"
hoelzl@38656
   360
        proof (rule fI)
hoelzl@38656
   361
          assume "of_nat i \<le> u t"
hoelzl@38656
   362
          hence "of_nat (i * 2^Suc i) \<le> u t * 2^Suc i"
hoelzl@38656
   363
            by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq)
hoelzl@38656
   364
          also have "\<dots> < of_nat (Suc k)" using * by auto
hoelzl@38656
   365
          finally show "i * 2 ^ i * 2 \<le> k"
hoelzl@38656
   366
            by (auto simp del: real_of_nat_mult)
hoelzl@38656
   367
        next
hoelzl@38656
   368
          fix j assume "of_nat j \<le> u t * 2 ^ i"
hoelzl@38656
   369
          with * show "j * 2 \<le> k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq)
hoelzl@38656
   370
        qed
hoelzl@38656
   371
      qed
hoelzl@38656
   372
      thus "?g i t \<le> ?g (Suc i) t"
hoelzl@38656
   373
        by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) }
hoelzl@38656
   374
    hence mono: "mono (\<lambda>i. ?g i t)" unfolding mono_iff_le_Suc by auto
hoelzl@35582
   375
hoelzl@38656
   376
    show "(SUP j. of_nat (f t j) / 2 ^ j) = u t"
hoelzl@38656
   377
    proof (rule pinfreal_SUPI)
hoelzl@38656
   378
      fix j show "of_nat (f t j) / 2 ^ j \<le> u t"
hoelzl@38656
   379
      proof (rule fI)
hoelzl@38656
   380
        assume "of_nat j \<le> u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \<le> u t"
hoelzl@38656
   381
          by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps)
hoelzl@38656
   382
      next
hoelzl@38656
   383
        fix k assume "of_nat k \<le> u t * 2 ^ j"
hoelzl@38656
   384
        thus "of_nat k / 2 ^ j \<le> u t"
hoelzl@38656
   385
          by (cases "u t")
hoelzl@38656
   386
             (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff)
hoelzl@38656
   387
      qed
hoelzl@38656
   388
    next
hoelzl@38656
   389
      fix y :: pinfreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y"
hoelzl@38656
   390
      show "u t \<le> y"
hoelzl@38656
   391
      proof (cases "u t")
hoelzl@38656
   392
        case (preal r)
hoelzl@38656
   393
        show ?thesis
hoelzl@38656
   394
        proof (rule ccontr)
hoelzl@38656
   395
          assume "\<not> u t \<le> y"
hoelzl@38656
   396
          then obtain p where p: "y = Real p" "0 \<le> p" "p < r" using preal by (cases y) auto
hoelzl@38656
   397
          with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r - p"]
hoelzl@38656
   398
          obtain n where n: "\<And>N. n \<le> N \<Longrightarrow> inverse (2^N) < r - p" by auto
hoelzl@38656
   399
          let ?N = "max n (natfloor r + 1)"
hoelzl@38656
   400
          have "u t < of_nat ?N" "n \<le> ?N"
hoelzl@38656
   401
            using ge_natfloor_plus_one_imp_gt[of r n] preal
hoelzl@38656
   402
            by (auto simp: max_def real_Suc_natfloor)
hoelzl@38656
   403
          from lower[OF this(1)]
hoelzl@38656
   404
          have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq
hoelzl@38656
   405
            using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)
hoelzl@38656
   406
          hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N"
hoelzl@38656
   407
            using preal by (auto simp: field_simps divide_real_def[symmetric])
hoelzl@38656
   408
          with n[OF `n \<le> ?N`] p preal *[of ?N]
hoelzl@38656
   409
          show False
hoelzl@38656
   410
            by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm)
hoelzl@38656
   411
        qed
hoelzl@38656
   412
      next
hoelzl@38656
   413
        case infinite
hoelzl@38656
   414
        { fix j have "f t j = j*2^j" using top[of j t] infinite by simp
hoelzl@38656
   415
          hence "of_nat j \<le> y" using *[of j]
hoelzl@38656
   416
            by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) }
hoelzl@38656
   417
        note all_less_y = this
hoelzl@38656
   418
        show ?thesis unfolding infinite
hoelzl@38656
   419
        proof (rule ccontr)
hoelzl@38656
   420
          assume "\<not> \<omega> \<le> y" then obtain r where r: "y = Real r" "0 \<le> r" by (cases y) auto
hoelzl@38656
   421
          moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat)
hoelzl@38656
   422
          with all_less_y[of n] r show False by auto
hoelzl@38656
   423
        qed
hoelzl@38656
   424
      qed
hoelzl@38656
   425
    qed
hoelzl@35582
   426
  qed
hoelzl@35582
   427
qed
hoelzl@35582
   428
hoelzl@38656
   429
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence':
hoelzl@38656
   430
  fixes u :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
   431
  assumes "u \<in> borel_measurable M"
hoelzl@38656
   432
  obtains (x) f where "f \<up> u" "\<And>i. simple_function (f i)" "\<And>i. \<omega>\<notin>f i`space M"
hoelzl@35582
   433
proof -
hoelzl@38656
   434
  from borel_measurable_implies_simple_function_sequence[OF assms]
hoelzl@38656
   435
  obtain f where x: "\<And>i. simple_function (f i)" "f \<up> u"
hoelzl@38656
   436
    and fin: "\<And>i. \<And>x. x\<in>space M \<Longrightarrow> f i x \<noteq> \<omega>" by auto
hoelzl@38656
   437
  { fix i from fin[of _ i] have "\<omega> \<notin> f i`space M" by fastsimp }
hoelzl@38656
   438
  with x show thesis by (auto intro!: that[of f])
hoelzl@38656
   439
qed
hoelzl@38656
   440
hoelzl@38656
   441
section "Simple integral"
hoelzl@38656
   442
hoelzl@38656
   443
definition (in measure_space)
hoelzl@38656
   444
  "simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M))"
hoelzl@35582
   445
hoelzl@38656
   446
lemma (in measure_space) simple_integral_cong:
hoelzl@38656
   447
  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
hoelzl@38656
   448
  shows "simple_integral f = simple_integral g"
hoelzl@38656
   449
proof -
hoelzl@38656
   450
  have "f ` space M = g ` space M"
hoelzl@38656
   451
    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
hoelzl@38656
   452
    using assms by (auto intro!: image_eqI)
hoelzl@38656
   453
  thus ?thesis unfolding simple_integral_def by simp
hoelzl@38656
   454
qed
hoelzl@38656
   455
hoelzl@38656
   456
lemma (in measure_space) simple_integral_const[simp]:
hoelzl@38656
   457
  "simple_integral (\<lambda>x. c) = c * \<mu> (space M)"
hoelzl@38656
   458
proof (cases "space M = {}")
hoelzl@38656
   459
  case True thus ?thesis unfolding simple_integral_def by simp
hoelzl@38656
   460
next
hoelzl@38656
   461
  case False hence "(\<lambda>x. c) ` space M = {c}" by auto
hoelzl@38656
   462
  thus ?thesis unfolding simple_integral_def by simp
hoelzl@35582
   463
qed
hoelzl@35582
   464
hoelzl@38656
   465
lemma (in measure_space) simple_function_partition:
hoelzl@38656
   466
  assumes "simple_function f" and "simple_function g"
hoelzl@38656
   467
  shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"
hoelzl@38656
   468
    (is "_ = setsum _ (?p ` space M)")
hoelzl@38656
   469
proof-
hoelzl@38656
   470
  let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
hoelzl@38656
   471
  let ?SIGMA = "Sigma (f`space M) ?sub"
hoelzl@35582
   472
hoelzl@38656
   473
  have [intro]:
hoelzl@38656
   474
    "finite (f ` space M)"
hoelzl@38656
   475
    "finite (g ` space M)"
hoelzl@38656
   476
    using assms unfolding simple_function_def by simp_all
hoelzl@38656
   477
hoelzl@38656
   478
  { fix A
hoelzl@38656
   479
    have "?p ` (A \<inter> space M) \<subseteq>
hoelzl@38656
   480
      (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
hoelzl@38656
   481
      by auto
hoelzl@38656
   482
    hence "finite (?p ` (A \<inter> space M))"
hoelzl@38656
   483
      by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) }
hoelzl@38656
   484
  note this[intro, simp]
hoelzl@35582
   485
hoelzl@38656
   486
  { fix x assume "x \<in> space M"
hoelzl@38656
   487
    have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
hoelzl@38656
   488
    moreover {
hoelzl@38656
   489
      fix x y
hoelzl@38656
   490
      have *: "f -` {f x} \<inter> g -` {g x} \<inter> space M
hoelzl@38656
   491
          = (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" by auto
hoelzl@38656
   492
      assume "x \<in> space M" "y \<in> space M"
hoelzl@38656
   493
      hence "f -` {f x} \<inter> g -` {g x} \<inter> space M \<in> sets M"
hoelzl@38656
   494
        using assms unfolding simple_function_def * by auto }
hoelzl@38656
   495
    ultimately
hoelzl@38656
   496
    have "\<mu> (f -` {f x} \<inter> space M) = setsum (\<mu>) (?sub (f x))"
hoelzl@38656
   497
      by (subst measure_finitely_additive) auto }
hoelzl@38656
   498
  hence "simple_integral f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)"
hoelzl@38656
   499
    unfolding simple_integral_def
hoelzl@38656
   500
    by (subst setsum_Sigma[symmetric],
hoelzl@38656
   501
       auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])
hoelzl@38656
   502
  also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"
hoelzl@38656
   503
  proof -
hoelzl@38656
   504
    have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
hoelzl@38656
   505
    have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M
hoelzl@38656
   506
      = (\<lambda>x. (f x, ?p x)) ` space M"
hoelzl@38656
   507
    proof safe
hoelzl@38656
   508
      fix x assume "x \<in> space M"
hoelzl@38656
   509
      thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"
hoelzl@38656
   510
        by (auto intro!: image_eqI[of _ _ "?p x"])
hoelzl@38656
   511
    qed auto
hoelzl@38656
   512
    thus ?thesis
hoelzl@38656
   513
      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)
hoelzl@38656
   514
      apply (rule_tac x="xa" in image_eqI)
hoelzl@38656
   515
      by simp_all
hoelzl@38656
   516
  qed
hoelzl@38656
   517
  finally show ?thesis .
hoelzl@35582
   518
qed
hoelzl@35582
   519
hoelzl@38656
   520
lemma (in measure_space) simple_integral_add[simp]:
hoelzl@38656
   521
  assumes "simple_function f" and "simple_function g"
hoelzl@38656
   522
  shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g"
hoelzl@35582
   523
proof -
hoelzl@38656
   524
  { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
hoelzl@38656
   525
    assume "x \<in> space M"
hoelzl@38656
   526
    hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}"
hoelzl@38656
   527
        "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S"
hoelzl@38656
   528
      by auto }
hoelzl@38656
   529
  thus ?thesis
hoelzl@38656
   530
    unfolding
hoelzl@38656
   531
      simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]]
hoelzl@38656
   532
      simple_function_partition[OF `simple_function f` `simple_function g`]
hoelzl@38656
   533
      simple_function_partition[OF `simple_function g` `simple_function f`]
hoelzl@38656
   534
    apply (subst (3) Int_commute)
hoelzl@38656
   535
    by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong)
hoelzl@35582
   536
qed
hoelzl@35582
   537
hoelzl@38656
   538
lemma (in measure_space) simple_integral_setsum[simp]:
hoelzl@38656
   539
  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"
hoelzl@38656
   540
  shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"
hoelzl@38656
   541
proof cases
hoelzl@38656
   542
  assume "finite P"
hoelzl@38656
   543
  from this assms show ?thesis
hoelzl@38656
   544
    by induct (auto simp: simple_function_setsum simple_integral_add)
hoelzl@38656
   545
qed auto
hoelzl@38656
   546
hoelzl@38656
   547
lemma (in measure_space) simple_integral_mult[simp]:
hoelzl@38656
   548
  assumes "simple_function f"
hoelzl@38656
   549
  shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f"
hoelzl@38656
   550
proof -
hoelzl@38656
   551
  note mult = simple_function_mult[OF simple_function_const[of c] assms]
hoelzl@38656
   552
  { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
hoelzl@38656
   553
    assume "x \<in> space M"
hoelzl@38656
   554
    hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"
hoelzl@38656
   555
      by auto }
hoelzl@38656
   556
  thus ?thesis
hoelzl@38656
   557
    unfolding simple_function_partition[OF mult assms]
hoelzl@38656
   558
      simple_function_partition[OF assms mult]
hoelzl@38656
   559
    by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong)
hoelzl@35582
   560
qed
hoelzl@35582
   561
hoelzl@38656
   562
lemma (in measure_space) simple_integral_mono:
hoelzl@38656
   563
  assumes "simple_function f" and "simple_function g"
hoelzl@38656
   564
  and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
hoelzl@38656
   565
  shows "simple_integral f \<le> simple_integral g"
hoelzl@38656
   566
  unfolding
hoelzl@38656
   567
    simple_function_partition[OF `simple_function f` `simple_function g`]
hoelzl@38656
   568
    simple_function_partition[OF `simple_function g` `simple_function f`]
hoelzl@38656
   569
  apply (subst Int_commute)
hoelzl@38656
   570
proof (safe intro!: setsum_mono)
hoelzl@38656
   571
  fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
hoelzl@38656
   572
  assume "x \<in> space M"
hoelzl@38656
   573
  hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto
hoelzl@38656
   574
  thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"
hoelzl@38656
   575
    using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)
hoelzl@35582
   576
qed
hoelzl@35582
   577
hoelzl@38656
   578
lemma (in measure_space) simple_integral_indicator:
hoelzl@38656
   579
  assumes "A \<in> sets M"
hoelzl@38656
   580
  assumes "simple_function f"
hoelzl@38656
   581
  shows "simple_integral (\<lambda>x. f x * indicator A x) =
hoelzl@38656
   582
    (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
hoelzl@38656
   583
proof cases
hoelzl@38656
   584
  assume "A = space M"
hoelzl@38656
   585
  moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f"
hoelzl@38656
   586
    by (auto intro!: simple_integral_cong)
hoelzl@38656
   587
  moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
hoelzl@38656
   588
  ultimately show ?thesis by (simp add: simple_integral_def)
hoelzl@38656
   589
next
hoelzl@38656
   590
  assume "A \<noteq> space M"
hoelzl@38656
   591
  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
hoelzl@38656
   592
  have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
hoelzl@35582
   593
  proof safe
hoelzl@38656
   594
    fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
hoelzl@38656
   595
  next
hoelzl@38656
   596
    fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
hoelzl@38656
   597
      using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
hoelzl@38656
   598
  next
hoelzl@38656
   599
    show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
hoelzl@35582
   600
  qed
hoelzl@38656
   601
  have *: "simple_integral (\<lambda>x. f x * indicator A x) =
hoelzl@38656
   602
    (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
hoelzl@38656
   603
    unfolding simple_integral_def I
hoelzl@38656
   604
  proof (rule setsum_mono_zero_cong_left)
hoelzl@38656
   605
    show "finite (f ` space M \<union> {0})"
hoelzl@38656
   606
      using assms(2) unfolding simple_function_def by auto
hoelzl@38656
   607
    show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
hoelzl@38656
   608
      using sets_into_space[OF assms(1)] by auto
hoelzl@38656
   609
    have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}" by (auto simp: image_iff)
hoelzl@38656
   610
    thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
hoelzl@38656
   611
      i * \<mu> (f -` {i} \<inter> space M \<inter> A) = 0" by auto
hoelzl@38656
   612
  next
hoelzl@38656
   613
    fix x assume "x \<in> f`A \<union> {0}"
hoelzl@38656
   614
    hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A"
hoelzl@38656
   615
      by (auto simp: indicator_def split: split_if_asm)
hoelzl@38656
   616
    thus "x * \<mu> (?I -` {x} \<inter> space M) =
hoelzl@38656
   617
      x * \<mu> (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all
hoelzl@38656
   618
  qed
hoelzl@38656
   619
  show ?thesis unfolding *
hoelzl@38656
   620
    using assms(2) unfolding simple_function_def
hoelzl@38656
   621
    by (auto intro!: setsum_mono_zero_cong_right)
hoelzl@38656
   622
qed
hoelzl@35582
   623
hoelzl@38656
   624
lemma (in measure_space) simple_integral_indicator_only[simp]:
hoelzl@38656
   625
  assumes "A \<in> sets M"
hoelzl@38656
   626
  shows "simple_integral (indicator A) = \<mu> A"
hoelzl@38656
   627
proof cases
hoelzl@38656
   628
  assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
hoelzl@38656
   629
  thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
hoelzl@38656
   630
next
hoelzl@38656
   631
  assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pinfreal}" by auto
hoelzl@38656
   632
  thus ?thesis
hoelzl@38656
   633
    using simple_integral_indicator[OF assms simple_function_const[of 1]]
hoelzl@38656
   634
    using sets_into_space[OF assms]
hoelzl@38656
   635
    by (auto intro!: arg_cong[where f="\<mu>"])
hoelzl@38656
   636
qed
hoelzl@35582
   637
hoelzl@38656
   638
lemma (in measure_space) simple_integral_null_set:
hoelzl@38656
   639
  assumes "simple_function u" "N \<in> null_sets"
hoelzl@38656
   640
  shows "simple_integral (\<lambda>x. u x * indicator N x) = 0"
hoelzl@38656
   641
proof -
hoelzl@38656
   642
  have "simple_integral (\<lambda>x. u x * indicator N x) \<le>
hoelzl@38656
   643
    simple_integral (\<lambda>x. \<omega> * indicator N x)"
hoelzl@38656
   644
    using assms
hoelzl@38656
   645
    by (safe intro!: simple_integral_mono simple_function_mult simple_function_indicator simple_function_const) simp
hoelzl@38656
   646
  also have "... = 0" apply(subst simple_integral_mult)
hoelzl@38656
   647
    using assms(2) by auto
hoelzl@38656
   648
  finally show ?thesis by auto
hoelzl@38656
   649
qed
hoelzl@35582
   650
hoelzl@38656
   651
lemma (in measure_space) simple_integral_cong':
hoelzl@38656
   652
  assumes f: "simple_function f" and g: "simple_function g"
hoelzl@38656
   653
  and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"
hoelzl@38656
   654
  shows "simple_integral f = simple_integral g"
hoelzl@38656
   655
proof -
hoelzl@38656
   656
  let ?h = "\<lambda>h. \<lambda>x. (h x * indicator {x\<in>space M. f x = g x} x
hoelzl@38656
   657
    + h x * indicator {x\<in>space M. f x \<noteq> g x} x
hoelzl@38656
   658
    + h x * indicator (-space M) x::pinfreal)"
hoelzl@38656
   659
  have *:"\<And>h. h = ?h h" unfolding indicator_def apply rule by auto
hoelzl@38656
   660
  have mea_neq:"{x \<in> space M. f x \<noteq> g x} \<in> sets M" using f g by (auto simp: borel_measurable_simple_function)
hoelzl@38656
   661
  then have mea_nullset: "{x \<in> space M. f x \<noteq> g x} \<in> null_sets" using mea by auto
hoelzl@38656
   662
  have h1:"\<And>h::_=>pinfreal. simple_function h \<Longrightarrow>
hoelzl@38656
   663
    simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x = g x} x)"
hoelzl@38656
   664
    apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator)
hoelzl@38656
   665
    using f g by (auto simp: borel_measurable_simple_function)
hoelzl@38656
   666
  have h2:"\<And>h::_\<Rightarrow>pinfreal. simple_function h \<Longrightarrow>
hoelzl@38656
   667
    simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x \<noteq> g x} x)"
hoelzl@38656
   668
    apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator)
hoelzl@38656
   669
    by(rule mea_neq)
hoelzl@38656
   670
  have **:"\<And>a b c d e f. a = b \<Longrightarrow> c = d \<Longrightarrow> e = f \<Longrightarrow> a+c+e = b+d+f" by auto
hoelzl@38656
   671
  note *** = simple_integral_add[OF simple_function_add[OF h1 h2] simple_function_notspace]
hoelzl@38656
   672
    simple_integral_add[OF h1 h2]
hoelzl@38656
   673
  show ?thesis apply(subst *[of g]) apply(subst *[of f])
hoelzl@38656
   674
    unfolding ***[OF f f] ***[OF g g]
hoelzl@38656
   675
  proof(rule **) case goal1 show ?case apply(rule arg_cong[where f=simple_integral]) apply rule 
hoelzl@38656
   676
      unfolding indicator_def by auto
hoelzl@38656
   677
  next note * = simple_integral_null_set[OF _ mea_nullset]
hoelzl@38656
   678
    case goal2 show ?case unfolding *[OF f] *[OF g] ..
hoelzl@38656
   679
  next case goal3 show ?case apply(rule simple_integral_cong) by auto
hoelzl@35582
   680
  qed
hoelzl@35582
   681
qed
hoelzl@35582
   682
hoelzl@35692
   683
section "Continuous posititve integration"
hoelzl@35692
   684
hoelzl@38656
   685
definition (in measure_space)
hoelzl@38656
   686
  "positive_integral f =
hoelzl@38656
   687
    (SUP g : {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. simple_integral g)"
hoelzl@35582
   688
hoelzl@38656
   689
lemma (in measure_space) positive_integral_alt1:
hoelzl@38656
   690
  "positive_integral f =
hoelzl@38656
   691
    (SUP g : {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}. simple_integral g)"
hoelzl@38656
   692
  unfolding positive_integral_def SUPR_def
hoelzl@38656
   693
proof (safe intro!: arg_cong[where f=Sup])
hoelzl@38656
   694
  fix g let ?g = "\<lambda>x. if x \<in> space M then g x else f x"
hoelzl@38656
   695
  assume "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>"
hoelzl@38656
   696
  hence "?g \<le> f" "simple_function ?g" "simple_integral g = simple_integral ?g"
hoelzl@38656
   697
    "\<omega> \<notin> g`space M"
hoelzl@38656
   698
    unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong)
hoelzl@38656
   699
  thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}"
hoelzl@38656
   700
    by auto
hoelzl@38656
   701
next
hoelzl@38656
   702
  fix g assume "simple_function g" "g \<le> f" "\<omega> \<notin> g`space M"
hoelzl@38656
   703
  hence "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>"
hoelzl@38656
   704
    by (auto simp add: le_fun_def image_iff)
hoelzl@38656
   705
  thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}"
hoelzl@38656
   706
    by auto
hoelzl@35582
   707
qed
hoelzl@35582
   708
hoelzl@38656
   709
lemma (in measure_space) positive_integral_alt:
hoelzl@38656
   710
  "positive_integral f =
hoelzl@38656
   711
    (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)"
hoelzl@38656
   712
  apply(rule order_class.antisym) unfolding positive_integral_def 
hoelzl@38656
   713
  apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim)
hoelzl@38656
   714
proof safe fix u assume u:"simple_function u" and uf:"u \<le> f"
hoelzl@38656
   715
  let ?u = "\<lambda>n x. if u x = \<omega> then Real (real (n::nat)) else u x"
hoelzl@38656
   716
  have su:"\<And>n. simple_function (?u n)" using simple_function_compose1[OF u] .
hoelzl@38656
   717
  show "\<exists>b. \<forall>n. b n \<in> {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} \<and>
hoelzl@38656
   718
    (\<lambda>n. simple_integral (b n)) ----> simple_integral u"
hoelzl@38656
   719
    apply(rule_tac x="?u" in exI, safe) apply(rule su)
hoelzl@38656
   720
  proof- fix n::nat have "?u n \<le> u" unfolding le_fun_def by auto
hoelzl@38656
   721
    also note uf finally show "?u n \<le> f" .
hoelzl@38656
   722
    let ?s = "{x \<in> space M. u x = \<omega>}"
hoelzl@38656
   723
    show "(\<lambda>n. simple_integral (?u n)) ----> simple_integral u"
hoelzl@38656
   724
    proof(cases "\<mu> ?s = 0")
hoelzl@38656
   725
      case True have *:"\<And>n. {x\<in>space M. ?u n x \<noteq> u x} = {x\<in>space M. u x = \<omega>}" by auto 
hoelzl@38656
   726
      have *:"\<And>n. simple_integral (?u n) = simple_integral u"
hoelzl@38656
   727
        apply(rule simple_integral_cong'[OF su u]) unfolding * True ..
hoelzl@38656
   728
      show ?thesis unfolding * by auto 
hoelzl@38656
   729
    next case False note m0=this
hoelzl@38656
   730
      have s:"{x \<in> space M. u x = \<omega>} \<in> sets M" using u  by (auto simp: borel_measurable_simple_function)
hoelzl@38656
   731
      have "\<omega> = simple_integral (\<lambda>x. \<omega> * indicator {x\<in>space M. u x = \<omega>} x)"
hoelzl@38656
   732
        apply(subst simple_integral_mult) using s
hoelzl@38656
   733
        unfolding simple_integral_indicator_only[OF s] using False by auto
hoelzl@38656
   734
      also have "... \<le> simple_integral u"
hoelzl@38656
   735
        apply (rule simple_integral_mono)
hoelzl@38656
   736
        apply (rule simple_function_mult)
hoelzl@38656
   737
        apply (rule simple_function_const)
hoelzl@38656
   738
        apply(rule ) prefer 3 apply(subst indicator_def)
hoelzl@38656
   739
        using s u by auto
hoelzl@38656
   740
      finally have *:"simple_integral u = \<omega>" by auto
hoelzl@38656
   741
      show ?thesis unfolding * Lim_omega_pos
hoelzl@38656
   742
      proof safe case goal1
hoelzl@38656
   743
        from real_arch_simple[of "B / real (\<mu> ?s)"] guess N0 .. note N=this
hoelzl@38656
   744
        def N \<equiv> "Suc N0" have N:"real N \<ge> B / real (\<mu> ?s)" "N > 0"
hoelzl@38656
   745
          unfolding N_def using N by auto
hoelzl@38656
   746
        show ?case apply-apply(rule_tac x=N in exI,safe) 
hoelzl@38656
   747
        proof- case goal1
hoelzl@38656
   748
          have "Real B \<le> Real (real N) * \<mu> ?s"
hoelzl@38656
   749
          proof(cases "\<mu> ?s = \<omega>")
hoelzl@38656
   750
            case True thus ?thesis using `B>0` N by auto
hoelzl@38656
   751
          next case False
hoelzl@38656
   752
            have *:"B \<le> real N * real (\<mu> ?s)" 
hoelzl@38656
   753
              using N(1) apply-apply(subst (asm) pos_divide_le_eq)
hoelzl@38656
   754
              apply rule using m0 False by auto
hoelzl@38656
   755
            show ?thesis apply(subst Real_real'[THEN sym,OF False])
hoelzl@38656
   756
              apply(subst pinfreal_times,subst if_P) defer
hoelzl@38656
   757
              apply(subst pinfreal_less_eq,subst if_P) defer
hoelzl@38656
   758
              using * N `B>0` by(auto intro: mult_nonneg_nonneg)
hoelzl@38656
   759
          qed
hoelzl@38656
   760
          also have "... \<le> Real (real n) * \<mu> ?s"
hoelzl@38656
   761
            apply(rule mult_right_mono) using goal1 by auto
hoelzl@38656
   762
          also have "... = simple_integral (\<lambda>x. Real (real n) * indicator ?s x)" 
hoelzl@38656
   763
            apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s])
hoelzl@38656
   764
            unfolding simple_integral_indicator_only[OF s] ..
hoelzl@38656
   765
          also have "... \<le> simple_integral (\<lambda>x. if u x = \<omega> then Real (real n) else u x)"
hoelzl@38656
   766
            apply(rule simple_integral_mono) apply(rule simple_function_mult)
hoelzl@38656
   767
            apply(rule simple_function_const)
hoelzl@38656
   768
            apply(rule simple_function_indicator) apply(rule s su)+ by auto
hoelzl@38656
   769
          finally show ?case .
hoelzl@38656
   770
        qed qed qed
hoelzl@38656
   771
    fix x assume x:"\<omega> = (if u x = \<omega> then Real (real n) else u x)" "x \<in> space M"
hoelzl@38656
   772
    hence "u x = \<omega>" apply-apply(rule ccontr) by auto
hoelzl@38656
   773
    hence "\<omega> = Real (real n)" using x by auto
hoelzl@38656
   774
    thus False by auto
hoelzl@35582
   775
  qed
hoelzl@35582
   776
qed
hoelzl@35582
   777
hoelzl@38656
   778
lemma (in measure_space) positive_integral_cong:
hoelzl@38656
   779
  assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
hoelzl@38656
   780
  shows "positive_integral f = positive_integral g"
hoelzl@38656
   781
proof -
hoelzl@38656
   782
  have "\<And>h. (\<forall>x\<in>space M. h x \<le> f x \<and> h x \<noteq> \<omega>) = (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>)"
hoelzl@38656
   783
    using assms by auto
hoelzl@38656
   784
  thus ?thesis unfolding positive_integral_alt1 by auto
hoelzl@38656
   785
qed
hoelzl@38656
   786
hoelzl@38656
   787
lemma (in measure_space) positive_integral_eq_simple_integral:
hoelzl@38656
   788
  assumes "simple_function f"
hoelzl@38656
   789
  shows "positive_integral f = simple_integral f"
hoelzl@38656
   790
  unfolding positive_integral_alt
hoelzl@38656
   791
proof (safe intro!: pinfreal_SUPI)
hoelzl@38656
   792
  fix g assume "simple_function g" "g \<le> f"
hoelzl@38656
   793
  with assms show "simple_integral g \<le> simple_integral f"
hoelzl@38656
   794
    by (auto intro!: simple_integral_mono simp: le_fun_def)
hoelzl@38656
   795
next
hoelzl@38656
   796
  fix y assume "\<forall>x. x\<in>{g. simple_function g \<and> g \<le> f} \<longrightarrow> simple_integral x \<le> y"
hoelzl@38656
   797
  with assms show "simple_integral f \<le> y" by auto
hoelzl@38656
   798
qed
hoelzl@35582
   799
hoelzl@38656
   800
lemma (in measure_space) positive_integral_mono:
hoelzl@38656
   801
  assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x"
hoelzl@38656
   802
  shows "positive_integral u \<le> positive_integral v"
hoelzl@38656
   803
  unfolding positive_integral_alt1
hoelzl@38656
   804
proof (safe intro!: SUPR_mono)
hoelzl@38656
   805
  fix a assume a: "simple_function a" and "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>"
hoelzl@38656
   806
  with mono have "\<forall>x\<in>space M. a x \<le> v x \<and> a x \<noteq> \<omega>" by fastsimp
hoelzl@38656
   807
  with a show "\<exists>b\<in>{g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> v x \<and> g x \<noteq> \<omega>)}. simple_integral a \<le> simple_integral b"
hoelzl@38656
   808
    by (auto intro!: bexI[of _ a])
hoelzl@38656
   809
qed
hoelzl@38656
   810
hoelzl@38656
   811
lemma (in measure_space) positive_integral_SUP_approx:
hoelzl@38656
   812
  assumes "f \<up> s"
hoelzl@38656
   813
  and f: "\<And>i. f i \<in> borel_measurable M"
hoelzl@38656
   814
  and "simple_function u"
hoelzl@38656
   815
  and le: "u \<le> s" and real: "\<omega> \<notin> u`space M"
hoelzl@38656
   816
  shows "simple_integral u \<le> (SUP i. positive_integral (f i))" (is "_ \<le> ?S")
hoelzl@38656
   817
proof (rule pinfreal_le_mult_one_interval)
hoelzl@38656
   818
  fix a :: pinfreal assume "0 < a" "a < 1"
hoelzl@38656
   819
  hence "a \<noteq> 0" by auto
hoelzl@38656
   820
  let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
hoelzl@38656
   821
  have B: "\<And>i. ?B i \<in> sets M"
hoelzl@38656
   822
    using f `simple_function u` by (auto simp: borel_measurable_simple_function)
hoelzl@38656
   823
hoelzl@38656
   824
  let "?uB i x" = "u x * indicator (?B i) x"
hoelzl@38656
   825
hoelzl@38656
   826
  { fix i have "?B i \<subseteq> ?B (Suc i)"
hoelzl@38656
   827
    proof safe
hoelzl@38656
   828
      fix i x assume "a * u x \<le> f i x"
hoelzl@38656
   829
      also have "\<dots> \<le> f (Suc i) x"
hoelzl@38656
   830
        using `f \<up> s` unfolding isoton_def le_fun_def by auto
hoelzl@38656
   831
      finally show "a * u x \<le> f (Suc i) x" .
hoelzl@38656
   832
    qed }
hoelzl@38656
   833
  note B_mono = this
hoelzl@35582
   834
hoelzl@38656
   835
  have u: "\<And>x. x \<in> space M \<Longrightarrow> u -` {u x} \<inter> space M \<in> sets M"
hoelzl@38656
   836
    using `simple_function u` by (auto simp add: simple_function_def)
hoelzl@38656
   837
hoelzl@38656
   838
  { fix i
hoelzl@38656
   839
    have "(\<lambda>n. (u -` {i} \<inter> space M) \<inter> ?B n) \<up> (u -` {i} \<inter> space M)" using B_mono unfolding isoton_def
hoelzl@38656
   840
    proof safe
hoelzl@38656
   841
      fix x assume "x \<in> space M"
hoelzl@38656
   842
      show "x \<in> (\<Union>i. (u -` {u x} \<inter> space M) \<inter> ?B i)"
hoelzl@38656
   843
      proof cases
hoelzl@38656
   844
        assume "u x = 0" thus ?thesis using `x \<in> space M` by simp
hoelzl@38656
   845
      next
hoelzl@38656
   846
        assume "u x \<noteq> 0"
hoelzl@38656
   847
        with `a < 1` real `x \<in> space M`
hoelzl@38656
   848
        have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff)
hoelzl@38656
   849
        also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s`
hoelzl@38656
   850
          unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def)
hoelzl@38656
   851
        finally obtain i where "a * u x < f i x" unfolding SUPR_def
hoelzl@38656
   852
          by (auto simp add: less_Sup_iff)
hoelzl@38656
   853
        hence "a * u x \<le> f i x" by auto
hoelzl@38656
   854
        thus ?thesis using `x \<in> space M` by auto
hoelzl@38656
   855
      qed
hoelzl@38656
   856
    qed auto }
hoelzl@38656
   857
  note measure_conv = measure_up[OF u Int[OF u B] this]
hoelzl@38656
   858
hoelzl@38656
   859
  have "simple_integral u = (SUP i. simple_integral (?uB i))"
hoelzl@38656
   860
    unfolding simple_integral_indicator[OF B `simple_function u`]
hoelzl@38656
   861
  proof (subst SUPR_pinfreal_setsum, safe)
hoelzl@38656
   862
    fix x n assume "x \<in> space M"
hoelzl@38656
   863
    have "\<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x})
hoelzl@38656
   864
      \<le> \<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f (Suc n) x})"
hoelzl@38656
   865
      using B_mono Int[OF u[OF `x \<in> space M`] B] by (auto intro!: measure_mono)
hoelzl@38656
   866
    thus "u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B n)
hoelzl@38656
   867
            \<le> u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B (Suc n))"
hoelzl@38656
   868
      by (auto intro: mult_left_mono)
hoelzl@38656
   869
  next
hoelzl@38656
   870
    show "simple_integral u =
hoelzl@38656
   871
      (\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (u -` {i} \<inter> space M \<inter> ?B n))"
hoelzl@38656
   872
      using measure_conv unfolding simple_integral_def isoton_def
hoelzl@38656
   873
      by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult)
hoelzl@38656
   874
  qed
hoelzl@38656
   875
  moreover
hoelzl@38656
   876
  have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"
hoelzl@38656
   877
    unfolding pinfreal_SUP_cmult[symmetric]
hoelzl@38656
   878
  proof (safe intro!: SUP_mono)
hoelzl@38656
   879
    fix i
hoelzl@38656
   880
    have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
hoelzl@38656
   881
      using B `simple_function u`
hoelzl@38656
   882
      by (subst simple_integral_mult[symmetric]) (auto simp: field_simps)
hoelzl@38656
   883
    also have "\<dots> \<le> positive_integral (f i)"
hoelzl@38656
   884
    proof -
hoelzl@38656
   885
      have "\<And>x. a * ?uB i x \<le> f i x" unfolding indicator_def by auto
hoelzl@38656
   886
      hence *: "simple_function (\<lambda>x. a * ?uB i x)" using B assms(3)
hoelzl@38656
   887
        by (auto intro!: simple_integral_mono)
hoelzl@38656
   888
      show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric]
hoelzl@38656
   889
        by (auto intro!: positive_integral_mono simp: indicator_def)
hoelzl@38656
   890
    qed
hoelzl@38656
   891
    finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"
hoelzl@38656
   892
      by auto
hoelzl@38656
   893
  qed
hoelzl@38656
   894
  ultimately show "a * simple_integral u \<le> ?S" by simp
hoelzl@35582
   895
qed
hoelzl@35582
   896
hoelzl@35582
   897
text {* Beppo-Levi monotone convergence theorem *}
hoelzl@38656
   898
lemma (in measure_space) positive_integral_isoton:
hoelzl@38656
   899
  assumes "f \<up> u" "\<And>i. f i \<in> borel_measurable M"
hoelzl@38656
   900
  shows "(\<lambda>i. positive_integral (f i)) \<up> positive_integral u"
hoelzl@38656
   901
  unfolding isoton_def
hoelzl@38656
   902
proof safe
hoelzl@38656
   903
  fix i show "positive_integral (f i) \<le> positive_integral (f (Suc i))"
hoelzl@38656
   904
    apply (rule positive_integral_mono)
hoelzl@38656
   905
    using `f \<up> u` unfolding isoton_def le_fun_def by auto
hoelzl@38656
   906
next
hoelzl@38656
   907
  have "u \<in> borel_measurable M"
hoelzl@38656
   908
    using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
hoelzl@38656
   909
  have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
hoelzl@35582
   910
hoelzl@38656
   911
  show "(SUP i. positive_integral (f i)) = positive_integral u"
hoelzl@38656
   912
  proof (rule antisym)
hoelzl@38656
   913
    from `f \<up> u`[THEN isoton_Sup, unfolded le_fun_def]
hoelzl@38656
   914
    show "(SUP j. positive_integral (f j)) \<le> positive_integral u"
hoelzl@38656
   915
      by (auto intro!: SUP_leI positive_integral_mono)
hoelzl@38656
   916
  next
hoelzl@38656
   917
    show "positive_integral u \<le> (SUP i. positive_integral (f i))"
hoelzl@38656
   918
      unfolding positive_integral_def[of u]
hoelzl@38656
   919
      by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms])
hoelzl@35582
   920
  qed
hoelzl@35582
   921
qed
hoelzl@35582
   922
hoelzl@38656
   923
lemma (in measure_space) SUP_simple_integral_sequences:
hoelzl@38656
   924
  assumes f: "f \<up> u" "\<And>i. simple_function (f i)"
hoelzl@38656
   925
  and g: "g \<up> u" "\<And>i. simple_function (g i)"
hoelzl@38656
   926
  shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))"
hoelzl@38656
   927
    (is "SUPR _ ?F = SUPR _ ?G")
hoelzl@38656
   928
proof -
hoelzl@38656
   929
  have "(SUP i. ?F i) = (SUP i. positive_integral (f i))"
hoelzl@38656
   930
    using assms by (simp add: positive_integral_eq_simple_integral)
hoelzl@38656
   931
  also have "\<dots> = positive_integral u"
hoelzl@38656
   932
    using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]]
hoelzl@38656
   933
    unfolding isoton_def by simp
hoelzl@38656
   934
  also have "\<dots> = (SUP i. positive_integral (g i))"
hoelzl@38656
   935
    using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]]
hoelzl@38656
   936
    unfolding isoton_def by simp
hoelzl@38656
   937
  also have "\<dots> = (SUP i. ?G i)"
hoelzl@38656
   938
    using assms by (simp add: positive_integral_eq_simple_integral)
hoelzl@38656
   939
  finally show ?thesis .
hoelzl@38656
   940
qed
hoelzl@38656
   941
hoelzl@38656
   942
lemma (in measure_space) positive_integral_const[simp]:
hoelzl@38656
   943
  "positive_integral (\<lambda>x. c) = c * \<mu> (space M)"
hoelzl@38656
   944
  by (subst positive_integral_eq_simple_integral) auto
hoelzl@38656
   945
hoelzl@38656
   946
lemma (in measure_space) positive_integral_isoton_simple:
hoelzl@38656
   947
  assumes "f \<up> u" and e: "\<And>i. simple_function (f i)"
hoelzl@38656
   948
  shows "(\<lambda>i. simple_integral (f i)) \<up> positive_integral u"
hoelzl@38656
   949
  using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
hoelzl@38656
   950
  unfolding positive_integral_eq_simple_integral[OF e] .
hoelzl@38656
   951
hoelzl@38656
   952
lemma (in measure_space) positive_integral_linear:
hoelzl@38656
   953
  assumes f: "f \<in> borel_measurable M"
hoelzl@38656
   954
  and g: "g \<in> borel_measurable M"
hoelzl@38656
   955
  shows "positive_integral (\<lambda>x. a * f x + g x) =
hoelzl@38656
   956
      a * positive_integral f + positive_integral g"
hoelzl@38656
   957
    (is "positive_integral ?L = _")
hoelzl@35582
   958
proof -
hoelzl@38656
   959
  from borel_measurable_implies_simple_function_sequence'[OF f] guess u .
hoelzl@38656
   960
  note u = this positive_integral_isoton_simple[OF this(1-2)]
hoelzl@38656
   961
  from borel_measurable_implies_simple_function_sequence'[OF g] guess v .
hoelzl@38656
   962
  note v = this positive_integral_isoton_simple[OF this(1-2)]
hoelzl@38656
   963
  let "?L' i x" = "a * u i x + v i x"
hoelzl@38656
   964
hoelzl@38656
   965
  have "?L \<in> borel_measurable M"
hoelzl@38656
   966
    using assms by simp
hoelzl@38656
   967
  from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
hoelzl@38656
   968
  note positive_integral_isoton_simple[OF this(1-2)] and l = this
hoelzl@38656
   969
  moreover have
hoelzl@38656
   970
      "(SUP i. simple_integral (l i)) = (SUP i. simple_integral (?L' i))"
hoelzl@38656
   971
  proof (rule SUP_simple_integral_sequences[OF l(1-2)])
hoelzl@38656
   972
    show "?L' \<up> ?L" "\<And>i. simple_function (?L' i)"
hoelzl@38656
   973
      using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right)
hoelzl@38656
   974
  qed
hoelzl@38656
   975
  moreover from u v have L'_isoton:
hoelzl@38656
   976
      "(\<lambda>i. simple_integral (?L' i)) \<up> a * positive_integral f + positive_integral g"
hoelzl@38656
   977
    by (simp add: isoton_add isoton_cmult_right)
hoelzl@38656
   978
  ultimately show ?thesis by (simp add: isoton_def)
hoelzl@38656
   979
qed
hoelzl@38656
   980
hoelzl@38656
   981
lemma (in measure_space) positive_integral_cmult:
hoelzl@38656
   982
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   983
  shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
hoelzl@38656
   984
  using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
hoelzl@38656
   985
hoelzl@38656
   986
lemma (in measure_space) positive_integral_indicator[simp]:
hoelzl@38656
   987
  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
hoelzl@38656
   988
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
hoelzl@38656
   989
hoelzl@38656
   990
lemma (in measure_space) positive_integral_cmult_indicator:
hoelzl@38656
   991
  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. c * indicator A x) = c * \<mu> A"
hoelzl@38656
   992
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
hoelzl@38656
   993
hoelzl@38656
   994
lemma (in measure_space) positive_integral_add:
hoelzl@38656
   995
  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@38656
   996
  shows "positive_integral (\<lambda>x. f x + g x) = positive_integral f + positive_integral g"
hoelzl@38656
   997
  using positive_integral_linear[OF assms, of 1] by simp
hoelzl@38656
   998
hoelzl@38656
   999
lemma (in measure_space) positive_integral_setsum:
hoelzl@38656
  1000
  assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M"
hoelzl@38656
  1001
  shows "positive_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"
hoelzl@38656
  1002
proof cases
hoelzl@38656
  1003
  assume "finite P"
hoelzl@38656
  1004
  from this assms show ?thesis
hoelzl@38656
  1005
  proof induct
hoelzl@38656
  1006
    case (insert i P)
hoelzl@38656
  1007
    have "f i \<in> borel_measurable M"
hoelzl@38656
  1008
      "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M"
hoelzl@38656
  1009
      using insert by (auto intro!: borel_measurable_pinfreal_setsum)
hoelzl@38656
  1010
    from positive_integral_add[OF this]
hoelzl@38656
  1011
    show ?case using insert by auto
hoelzl@38656
  1012
  qed simp
hoelzl@38656
  1013
qed simp
hoelzl@38656
  1014
hoelzl@38656
  1015
lemma (in measure_space) positive_integral_diff:
hoelzl@38656
  1016
  assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"
hoelzl@38656
  1017
  and fin: "positive_integral g \<noteq> \<omega>"
hoelzl@38656
  1018
  and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x"
hoelzl@38656
  1019
  shows "positive_integral (\<lambda>x. f x - g x) = positive_integral f - positive_integral g"
hoelzl@38656
  1020
proof -
hoelzl@38656
  1021
  have borel: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
hoelzl@38656
  1022
    using f g by (rule borel_measurable_pinfreal_diff)
hoelzl@38656
  1023
  have "positive_integral (\<lambda>x. f x - g x) + positive_integral g =
hoelzl@38656
  1024
    positive_integral f"
hoelzl@38656
  1025
    unfolding positive_integral_add[OF borel g, symmetric]
hoelzl@38656
  1026
  proof (rule positive_integral_cong)
hoelzl@38656
  1027
    fix x assume "x \<in> space M"
hoelzl@38656
  1028
    from mono[OF this] show "f x - g x + g x = f x"
hoelzl@38656
  1029
      by (cases "f x", cases "g x", simp, simp, cases "g x", auto)
hoelzl@38656
  1030
  qed
hoelzl@38656
  1031
  with mono show ?thesis
hoelzl@38656
  1032
    by (subst minus_pinfreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono)
hoelzl@38656
  1033
qed
hoelzl@38656
  1034
hoelzl@38656
  1035
lemma (in measure_space) positive_integral_psuminf:
hoelzl@38656
  1036
  assumes "\<And>i. f i \<in> borel_measurable M"
hoelzl@38656
  1037
  shows "positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"
hoelzl@38656
  1038
proof -
hoelzl@38656
  1039
  have "(\<lambda>i. positive_integral (\<lambda>x. \<Sum>i<i. f i x)) \<up> positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity>i. f i x)"
hoelzl@38656
  1040
    by (rule positive_integral_isoton)
hoelzl@38656
  1041
       (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono
hoelzl@38656
  1042
                     arg_cong[where f=Sup]
hoelzl@38656
  1043
             simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def)
hoelzl@38656
  1044
  thus ?thesis
hoelzl@38656
  1045
    by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms])
hoelzl@38656
  1046
qed
hoelzl@38656
  1047
hoelzl@38656
  1048
text {* Fatou's lemma: convergence theorem on limes inferior *}
hoelzl@38656
  1049
lemma (in measure_space) positive_integral_lim_INF:
hoelzl@38656
  1050
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pinfreal"
hoelzl@38656
  1051
  assumes "\<And>i. u i \<in> borel_measurable M"
hoelzl@38656
  1052
  shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
hoelzl@38656
  1053
    (SUP n. INF m. positive_integral (u (m + n)))"
hoelzl@38656
  1054
proof -
hoelzl@38656
  1055
  have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
hoelzl@38656
  1056
    by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
hoelzl@38656
  1057
hoelzl@38656
  1058
  have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
hoelzl@38656
  1059
  proof (unfold isoton_def, safe)
hoelzl@38656
  1060
    fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"
hoelzl@38656
  1061
      by (rule INF_mono[where N=Suc]) simp
hoelzl@38656
  1062
  qed
hoelzl@38656
  1063
  from positive_integral_isoton[OF this] assms
hoelzl@38656
  1064
  have "positive_integral (SUP n. INF m. u (m + n)) =
hoelzl@38656
  1065
    (SUP n. positive_integral (INF m. u (m + n)))"
hoelzl@38656
  1066
    unfolding isoton_def by (simp add: borel_measurable_INF)
hoelzl@38656
  1067
  also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
hoelzl@38656
  1068
    by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)
hoelzl@38656
  1069
  finally show ?thesis .
hoelzl@35582
  1070
qed
hoelzl@35582
  1071
hoelzl@38656
  1072
lemma (in measure_space) measure_space_density:
hoelzl@38656
  1073
  assumes borel: "u \<in> borel_measurable M"
hoelzl@38656
  1074
  shows "measure_space M (\<lambda>A. positive_integral (\<lambda>x. u x * indicator A x))" (is "measure_space M ?v")
hoelzl@38656
  1075
proof
hoelzl@38656
  1076
  show "?v {} = 0" by simp
hoelzl@38656
  1077
  show "countably_additive M ?v"
hoelzl@38656
  1078
    unfolding countably_additive_def
hoelzl@38656
  1079
  proof safe
hoelzl@38656
  1080
    fix A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
  1081
    assume "range A \<subseteq> sets M"
hoelzl@38656
  1082
    hence "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M"
hoelzl@38656
  1083
      using borel by (auto intro: borel_measurable_indicator)
hoelzl@38656
  1084
    moreover assume "disjoint_family A"
hoelzl@38656
  1085
    note psuminf_indicator[OF this]
hoelzl@38656
  1086
    ultimately show "(\<Sum>\<^isub>\<infinity>n. ?v (A n)) = ?v (\<Union>x. A x)"
hoelzl@38656
  1087
      by (simp add: positive_integral_psuminf[symmetric])
hoelzl@38656
  1088
  qed
hoelzl@38656
  1089
qed
hoelzl@35582
  1090
hoelzl@38656
  1091
lemma (in measure_space) positive_integral_null_set:
hoelzl@38656
  1092
  assumes borel: "u \<in> borel_measurable M" and "N \<in> null_sets"
hoelzl@38656
  1093
  shows "positive_integral (\<lambda>x. u x * indicator N x) = 0" (is "?I = 0")
hoelzl@38656
  1094
proof -
hoelzl@38656
  1095
  have "N \<in> sets M" using `N \<in> null_sets` by auto
hoelzl@38656
  1096
  have "(\<lambda>i x. min (of_nat i) (u x) * indicator N x) \<up> (\<lambda>x. u x * indicator N x)"
hoelzl@38656
  1097
    unfolding isoton_fun_expand
hoelzl@38656
  1098
  proof (safe intro!: isoton_cmult_left, unfold isoton_def, safe)
hoelzl@38656
  1099
    fix j i show "min (of_nat j) (u i) \<le> min (of_nat (Suc j)) (u i)"
hoelzl@38656
  1100
      by (rule min_max.inf_mono) auto
hoelzl@38656
  1101
  next
hoelzl@38656
  1102
    fix i show "(SUP j. min (of_nat j) (u i)) = u i"
hoelzl@38656
  1103
    proof (cases "u i")
hoelzl@38656
  1104
      case infinite
hoelzl@38656
  1105
      moreover hence "\<And>j. min (of_nat j) (u i) = of_nat j"
hoelzl@38656
  1106
        by (auto simp: min_def)
hoelzl@38656
  1107
      ultimately show ?thesis by (simp add: Sup_\<omega>)
hoelzl@35582
  1108
    next
hoelzl@38656
  1109
      case (preal r)
hoelzl@38656
  1110
      obtain j where "r \<le> of_nat j" using ex_le_of_nat ..
hoelzl@38656
  1111
      hence "u i \<le> of_nat j" using preal by (auto simp: real_of_nat_def)
hoelzl@38656
  1112
      show ?thesis
hoelzl@38656
  1113
      proof (rule pinfreal_SUPI)
hoelzl@38656
  1114
        fix y assume "\<And>j. j \<in> UNIV \<Longrightarrow> min (of_nat j) (u i) \<le> y"
hoelzl@38656
  1115
        note this[of j]
hoelzl@38656
  1116
        moreover have "min (of_nat j) (u i) = u i"
hoelzl@38656
  1117
          using `u i \<le> of_nat j` by (auto simp: min_def)
hoelzl@38656
  1118
        ultimately show "u i \<le> y" by simp
hoelzl@35582
  1119
      qed simp
hoelzl@35582
  1120
    qed
hoelzl@35582
  1121
  qed
hoelzl@38656
  1122
  from positive_integral_isoton[OF this]
hoelzl@38656
  1123
  have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"
hoelzl@38656
  1124
    unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)
hoelzl@38656
  1125
  also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"
hoelzl@38656
  1126
  proof (rule SUP_mono, rule positive_integral_mono)
hoelzl@38656
  1127
    fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"
hoelzl@38656
  1128
      by (cases "x \<in> N") auto
hoelzl@38656
  1129
  qed
hoelzl@38656
  1130
  also have "\<dots> = 0"
hoelzl@38656
  1131
    using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)
hoelzl@38656
  1132
  finally show ?thesis by simp
hoelzl@38656
  1133
qed
hoelzl@35582
  1134
hoelzl@38656
  1135
lemma (in measure_space) positive_integral_Markov_inequality:
hoelzl@38656
  1136
  assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>"
hoelzl@38656
  1137
  shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * positive_integral (\<lambda>x. u x * indicator A x)"
hoelzl@38656
  1138
    (is "\<mu> ?A \<le> _ * ?PI")
hoelzl@38656
  1139
proof -
hoelzl@38656
  1140
  have "?A \<in> sets M"
hoelzl@38656
  1141
    using `A \<in> sets M` borel by auto
hoelzl@38656
  1142
  hence "\<mu> ?A = positive_integral (\<lambda>x. indicator ?A x)"
hoelzl@38656
  1143
    using positive_integral_indicator by simp
hoelzl@38656
  1144
  also have "\<dots> \<le> positive_integral (\<lambda>x. c * (u x * indicator A x))"
hoelzl@38656
  1145
  proof (rule positive_integral_mono)
hoelzl@38656
  1146
    fix x assume "x \<in> space M"
hoelzl@38656
  1147
    show "indicator ?A x \<le> c * (u x * indicator A x)"
hoelzl@38656
  1148
      by (cases "x \<in> ?A") auto
hoelzl@38656
  1149
  qed
hoelzl@38656
  1150
  also have "\<dots> = c * positive_integral (\<lambda>x. u x * indicator A x)"
hoelzl@38656
  1151
    using assms
hoelzl@38656
  1152
    by (auto intro!: positive_integral_cmult borel_measurable_indicator)
hoelzl@38656
  1153
  finally show ?thesis .
hoelzl@35582
  1154
qed
hoelzl@35582
  1155
hoelzl@38656
  1156
lemma (in measure_space) positive_integral_0_iff:
hoelzl@38656
  1157
  assumes borel: "u \<in> borel_measurable M"
hoelzl@38656
  1158
  shows "positive_integral u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0"
hoelzl@38656
  1159
    (is "_ \<longleftrightarrow> \<mu> ?A = 0")
hoelzl@35582
  1160
proof -
hoelzl@38656
  1161
  have A: "?A \<in> sets M" using borel by auto
hoelzl@38656
  1162
  have u: "positive_integral (\<lambda>x. u x * indicator ?A x) = positive_integral u"
hoelzl@38656
  1163
    by (auto intro!: positive_integral_cong simp: indicator_def)
hoelzl@35582
  1164
hoelzl@38656
  1165
  show ?thesis
hoelzl@38656
  1166
  proof
hoelzl@38656
  1167
    assume "\<mu> ?A = 0"
hoelzl@38656
  1168
    hence "?A \<in> null_sets" using `?A \<in> sets M` by auto
hoelzl@38656
  1169
    from positive_integral_null_set[OF borel this]
hoelzl@38656
  1170
    have "0 = positive_integral (\<lambda>x. u x * indicator ?A x)" by simp
hoelzl@38656
  1171
    thus "positive_integral u = 0" unfolding u by simp
hoelzl@38656
  1172
  next
hoelzl@38656
  1173
    assume *: "positive_integral u = 0"
hoelzl@38656
  1174
    let "?M n" = "{x \<in> space M. 1 \<le> of_nat n * u x}"
hoelzl@38656
  1175
    have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
hoelzl@38656
  1176
    proof -
hoelzl@38656
  1177
      { fix n
hoelzl@38656
  1178
        from positive_integral_Markov_inequality[OF borel `?A \<in> sets M`, of "of_nat n"]
hoelzl@38656
  1179
        have "\<mu> (?M n \<inter> ?A) = 0" unfolding * u by simp }
hoelzl@38656
  1180
      thus ?thesis by simp
hoelzl@35582
  1181
    qed
hoelzl@38656
  1182
    also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)"
hoelzl@38656
  1183
    proof (safe intro!: continuity_from_below)
hoelzl@38656
  1184
      fix n show "?M n \<inter> ?A \<in> sets M"
hoelzl@38656
  1185
        using borel by (auto intro!: Int)
hoelzl@38656
  1186
    next
hoelzl@38656
  1187
      fix n x assume "1 \<le> of_nat n * u x"
hoelzl@38656
  1188
      also have "\<dots> \<le> of_nat (Suc n) * u x"
hoelzl@38656
  1189
        by (subst (1 2) mult_commute) (auto intro!: pinfreal_mult_cancel)
hoelzl@38656
  1190
      finally show "1 \<le> of_nat (Suc n) * u x" .
hoelzl@38656
  1191
    qed
hoelzl@38656
  1192
    also have "\<dots> = \<mu> ?A"
hoelzl@38656
  1193
    proof (safe intro!: arg_cong[where f="\<mu>"])
hoelzl@38656
  1194
      fix x assume "u x \<noteq> 0" and [simp, intro]: "x \<in> space M"
hoelzl@38656
  1195
      show "x \<in> (\<Union>n. ?M n \<inter> ?A)"
hoelzl@38656
  1196
      proof (cases "u x")
hoelzl@38656
  1197
        case (preal r)
hoelzl@38656
  1198
        obtain j where "1 / r \<le> of_nat j" using ex_le_of_nat ..
hoelzl@38656
  1199
        hence "1 / r * r \<le> of_nat j * r" using preal unfolding mult_le_cancel_right by auto
hoelzl@38656
  1200
        hence "1 \<le> of_nat j * r" using preal `u x \<noteq> 0` by auto
hoelzl@38656
  1201
        thus ?thesis using `u x \<noteq> 0` preal by (auto simp: real_of_nat_def[symmetric])
hoelzl@38656
  1202
      qed auto
hoelzl@38656
  1203
    qed
hoelzl@38656
  1204
    finally show "\<mu> ?A = 0" by simp
hoelzl@35582
  1205
  qed
hoelzl@35582
  1206
qed
hoelzl@35582
  1207
hoelzl@38656
  1208
lemma (in measure_space) positive_integral_cong_on_null_sets:
hoelzl@38656
  1209
  assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"
hoelzl@38656
  1210
  and measure: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"
hoelzl@38656
  1211
  shows "positive_integral f = positive_integral g"
hoelzl@35582
  1212
proof -
hoelzl@38656
  1213
  let ?N = "{x\<in>space M. f x \<noteq> g x}" and ?E = "{x\<in>space M. f x = g x}"
hoelzl@38656
  1214
  let "?A h x" = "h x * indicator ?E x :: pinfreal"
hoelzl@38656
  1215
  let "?B h x" = "h x * indicator ?N x :: pinfreal"
hoelzl@38656
  1216
hoelzl@38656
  1217
  have A: "positive_integral (?A f) = positive_integral (?A g)"
hoelzl@38656
  1218
    by (auto intro!: positive_integral_cong simp: indicator_def)
hoelzl@38656
  1219
hoelzl@38656
  1220
  have [intro]: "?N \<in> sets M" "?E \<in> sets M" using f g by auto
hoelzl@38656
  1221
  hence "?N \<in> null_sets" using measure by auto
hoelzl@38656
  1222
  hence B: "positive_integral (?B f) = positive_integral (?B g)"
hoelzl@38656
  1223
    using f g by (simp add: positive_integral_null_set)
hoelzl@38656
  1224
hoelzl@38656
  1225
  have "positive_integral f = positive_integral (\<lambda>x. ?A f x + ?B f x)"
hoelzl@38656
  1226
    by (auto intro!: positive_integral_cong simp: indicator_def)
hoelzl@38656
  1227
  also have "\<dots> = positive_integral (?A f) + positive_integral (?B f)"
hoelzl@38656
  1228
    using f g by (auto intro!: positive_integral_add borel_measurable_indicator)
hoelzl@38656
  1229
  also have "\<dots> = positive_integral (\<lambda>x. ?A g x + ?B g x)"
hoelzl@38656
  1230
    unfolding A B using f g by (auto intro!: positive_integral_add[symmetric] borel_measurable_indicator)
hoelzl@38656
  1231
  also have "\<dots> = positive_integral g"
hoelzl@38656
  1232
    by (auto intro!: positive_integral_cong simp: indicator_def)
hoelzl@38656
  1233
  finally show ?thesis by simp
hoelzl@35582
  1234
qed
hoelzl@35582
  1235
hoelzl@35692
  1236
section "Lebesgue Integral"
hoelzl@35692
  1237
hoelzl@38656
  1238
definition (in measure_space) integrable where
hoelzl@38656
  1239
  "integrable f \<longleftrightarrow> f \<in> borel_measurable M \<and>
hoelzl@38656
  1240
    positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega> \<and>
hoelzl@38656
  1241
    positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>"
hoelzl@35692
  1242
hoelzl@38656
  1243
lemma (in measure_space) integrableD[dest]:
hoelzl@38656
  1244
  assumes "integrable f"
hoelzl@38656
  1245
  shows "f \<in> borel_measurable M"
hoelzl@38656
  1246
  "positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega>"
hoelzl@38656
  1247
  "positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>"
hoelzl@38656
  1248
  using assms unfolding integrable_def by auto
hoelzl@35692
  1249
hoelzl@38656
  1250
definition (in measure_space) integral where
hoelzl@38656
  1251
  "integral f =
hoelzl@38656
  1252
    real (positive_integral (\<lambda>x. Real (f x))) -
hoelzl@38656
  1253
    real (positive_integral (\<lambda>x. Real (- f x)))"
hoelzl@38656
  1254
hoelzl@38656
  1255
lemma (in measure_space) integral_cong:
hoelzl@35582
  1256
  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
hoelzl@35582
  1257
  shows "integral f = integral g"
hoelzl@38656
  1258
  using assms by (simp cong: positive_integral_cong add: integral_def)
hoelzl@35582
  1259
hoelzl@38656
  1260
lemma (in measure_space) integrable_cong:
hoelzl@38656
  1261
  "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable f \<longleftrightarrow> integrable g"
hoelzl@38656
  1262
  by (simp cong: positive_integral_cong measurable_cong add: integrable_def)
hoelzl@38656
  1263
hoelzl@38656
  1264
lemma (in measure_space) integral_eq_positive_integral:
hoelzl@38656
  1265
  assumes "\<And>x. 0 \<le> f x"
hoelzl@38656
  1266
  shows "integral f = real (positive_integral (\<lambda>x. Real (f x)))"
hoelzl@35582
  1267
proof -
hoelzl@38656
  1268
  have "\<And>x. Real (- f x) = 0" using assms by simp
hoelzl@38656
  1269
  thus ?thesis by (simp del: Real_eq_0 add: integral_def)
hoelzl@35582
  1270
qed
hoelzl@35582
  1271
hoelzl@38656
  1272
lemma (in measure_space) integral_minus[intro, simp]:
hoelzl@38656
  1273
  assumes "integrable f"
hoelzl@38656
  1274
  shows "integrable (\<lambda>x. - f x)" "integral (\<lambda>x. - f x) = - integral f"
hoelzl@38656
  1275
  using assms by (auto simp: integrable_def integral_def)
hoelzl@38656
  1276
hoelzl@38656
  1277
lemma (in measure_space) integral_of_positive_diff:
hoelzl@38656
  1278
  assumes integrable: "integrable u" "integrable v"
hoelzl@38656
  1279
  and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x"
hoelzl@38656
  1280
  shows "integrable f" and "integral f = integral u - integral v"
hoelzl@35582
  1281
proof -
hoelzl@38656
  1282
  let ?PI = positive_integral
hoelzl@38656
  1283
  let "?f x" = "Real (f x)"
hoelzl@38656
  1284
  let "?mf x" = "Real (- f x)"
hoelzl@38656
  1285
  let "?u x" = "Real (u x)"
hoelzl@38656
  1286
  let "?v x" = "Real (v x)"
hoelzl@38656
  1287
hoelzl@38656
  1288
  from borel_measurable_diff[of u v] integrable
hoelzl@38656
  1289
  have f_borel: "?f \<in> borel_measurable M" and
hoelzl@38656
  1290
    mf_borel: "?mf \<in> borel_measurable M" and
hoelzl@38656
  1291
    v_borel: "?v \<in> borel_measurable M" and
hoelzl@38656
  1292
    u_borel: "?u \<in> borel_measurable M" and
hoelzl@38656
  1293
    "f \<in> borel_measurable M"
hoelzl@38656
  1294
    by (auto simp: f_def[symmetric] integrable_def)
hoelzl@35582
  1295
hoelzl@38656
  1296
  have "?PI (\<lambda>x. Real (u x - v x)) \<le> ?PI ?u"
hoelzl@38656
  1297
    using pos by (auto intro!: positive_integral_mono)
hoelzl@38656
  1298
  moreover have "?PI (\<lambda>x. Real (v x - u x)) \<le> ?PI ?v"
hoelzl@38656
  1299
    using pos by (auto intro!: positive_integral_mono)
hoelzl@38656
  1300
  ultimately show f: "integrable f"
hoelzl@38656
  1301
    using `integrable u` `integrable v` `f \<in> borel_measurable M`
hoelzl@38656
  1302
    by (auto simp: integrable_def f_def)
hoelzl@38656
  1303
  hence mf: "integrable (\<lambda>x. - f x)" ..
hoelzl@38656
  1304
hoelzl@38656
  1305
  have *: "\<And>x. Real (- v x) = 0" "\<And>x. Real (- u x) = 0"
hoelzl@38656
  1306
    using pos by auto
hoelzl@35582
  1307
hoelzl@38656
  1308
  have "\<And>x. ?u x + ?mf x = ?v x + ?f x"
hoelzl@38656
  1309
    unfolding f_def using pos by simp
hoelzl@38656
  1310
  hence "?PI (\<lambda>x. ?u x + ?mf x) = ?PI (\<lambda>x. ?v x + ?f x)" by simp
hoelzl@38656
  1311
  hence "real (?PI ?u + ?PI ?mf) = real (?PI ?v + ?PI ?f)"
hoelzl@38656
  1312
    using positive_integral_add[OF u_borel mf_borel]
hoelzl@38656
  1313
    using positive_integral_add[OF v_borel f_borel]
hoelzl@38656
  1314
    by auto
hoelzl@38656
  1315
  then show "integral f = integral u - integral v"
hoelzl@38656
  1316
    using f mf `integrable u` `integrable v`
hoelzl@38656
  1317
    unfolding integral_def integrable_def *
hoelzl@38656
  1318
    by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?v", cases "?PI ?u")
hoelzl@38656
  1319
       (auto simp add: field_simps)
hoelzl@35582
  1320
qed
hoelzl@35582
  1321
hoelzl@38656
  1322
lemma (in measure_space) integral_linear:
hoelzl@38656
  1323
  assumes "integrable f" "integrable g" and "0 \<le> a"
hoelzl@38656
  1324
  shows "integrable (\<lambda>t. a * f t + g t)"
hoelzl@38656
  1325
  and "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g"
hoelzl@38656
  1326
proof -
hoelzl@38656
  1327
  let ?PI = positive_integral
hoelzl@38656
  1328
  let "?f x" = "Real (f x)"
hoelzl@38656
  1329
  let "?g x" = "Real (g x)"
hoelzl@38656
  1330
  let "?mf x" = "Real (- f x)"
hoelzl@38656
  1331
  let "?mg x" = "Real (- g x)"
hoelzl@38656
  1332
  let "?p t" = "max 0 (a * f t) + max 0 (g t)"
hoelzl@38656
  1333
  let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)"
hoelzl@38656
  1334
hoelzl@38656
  1335
  have pos: "?f \<in> borel_measurable M" "?g \<in> borel_measurable M"
hoelzl@38656
  1336
    and neg: "?mf \<in> borel_measurable M" "?mg \<in> borel_measurable M"
hoelzl@38656
  1337
    and p: "?p \<in> borel_measurable M"
hoelzl@38656
  1338
    and n: "?n \<in> borel_measurable M"
hoelzl@38656
  1339
    using assms by (simp_all add: integrable_def)
hoelzl@35582
  1340
hoelzl@38656
  1341
  have *: "\<And>x. Real (?p x) = Real a * ?f x + ?g x"
hoelzl@38656
  1342
          "\<And>x. Real (?n x) = Real a * ?mf x + ?mg x"
hoelzl@38656
  1343
          "\<And>x. Real (- ?p x) = 0"
hoelzl@38656
  1344
          "\<And>x. Real (- ?n x) = 0"
hoelzl@38656
  1345
    using `0 \<le> a` by (auto simp: max_def min_def zero_le_mult_iff mult_le_0_iff add_nonpos_nonpos)
hoelzl@38656
  1346
hoelzl@38656
  1347
  note linear =
hoelzl@38656
  1348
    positive_integral_linear[OF pos]
hoelzl@38656
  1349
    positive_integral_linear[OF neg]
hoelzl@35582
  1350
hoelzl@38656
  1351
  have "integrable ?p" "integrable ?n"
hoelzl@38656
  1352
      "\<And>t. a * f t + g t = ?p t - ?n t" "\<And>t. 0 \<le> ?p t" "\<And>t. 0 \<le> ?n t"
hoelzl@38656
  1353
    using assms p n unfolding integrable_def * linear by auto
hoelzl@38656
  1354
  note diff = integral_of_positive_diff[OF this]
hoelzl@38656
  1355
hoelzl@38656
  1356
  show "integrable (\<lambda>t. a * f t + g t)" by (rule diff)
hoelzl@38656
  1357
hoelzl@38656
  1358
  from assms show "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g"
hoelzl@38656
  1359
    unfolding diff(2) unfolding integral_def * linear integrable_def
hoelzl@38656
  1360
    by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?g", cases "?PI ?mg")
hoelzl@38656
  1361
       (auto simp add: field_simps zero_le_mult_iff)
hoelzl@38656
  1362
qed
hoelzl@38656
  1363
hoelzl@38656
  1364
lemma (in measure_space) integral_add[simp, intro]:
hoelzl@38656
  1365
  assumes "integrable f" "integrable g"
hoelzl@35582
  1366
  shows "integrable (\<lambda>t. f t + g t)"
hoelzl@35582
  1367
  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
hoelzl@38656
  1368
  using assms integral_linear[where a=1] by auto
hoelzl@38656
  1369
hoelzl@38656
  1370
lemma (in measure_space) integral_zero[simp, intro]:
hoelzl@38656
  1371
  shows "integrable (\<lambda>x. 0)"
hoelzl@38656
  1372
  and "integral (\<lambda>x. 0) = 0"
hoelzl@38656
  1373
  unfolding integrable_def integral_def
hoelzl@38656
  1374
  by (auto simp add: borel_measurable_const)
hoelzl@35582
  1375
hoelzl@38656
  1376
lemma (in measure_space) integral_cmult[simp, intro]:
hoelzl@38656
  1377
  assumes "integrable f"
hoelzl@38656
  1378
  shows "integrable (\<lambda>t. a * f t)" (is ?P)
hoelzl@38656
  1379
  and "integral (\<lambda>t. a * f t) = a * integral f" (is ?I)
hoelzl@38656
  1380
proof -
hoelzl@38656
  1381
  have "integrable (\<lambda>t. a * f t) \<and> integral (\<lambda>t. a * f t) = a * integral f"
hoelzl@38656
  1382
  proof (cases rule: le_cases)
hoelzl@38656
  1383
    assume "0 \<le> a" show ?thesis
hoelzl@38656
  1384
      using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
hoelzl@38656
  1385
      by (simp add: integral_zero)
hoelzl@38656
  1386
  next
hoelzl@38656
  1387
    assume "a \<le> 0" hence "0 \<le> - a" by auto
hoelzl@38656
  1388
    have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
hoelzl@38656
  1389
    show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
hoelzl@38656
  1390
        integral_minus(1)[of "\<lambda>t. - a * f t"]
hoelzl@38656
  1391
      unfolding * integral_zero by simp
hoelzl@38656
  1392
  qed
hoelzl@38656
  1393
  thus ?P ?I by auto
hoelzl@35582
  1394
qed
hoelzl@35582
  1395
hoelzl@38656
  1396
lemma (in measure_space) integral_mono:
hoelzl@38656
  1397
  assumes fg: "integrable f" "integrable g"
hoelzl@35582
  1398
  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
hoelzl@35582
  1399
  shows "integral f \<le> integral g"
hoelzl@38656
  1400
  using fg unfolding integral_def integrable_def diff_minus
hoelzl@38656
  1401
proof (safe intro!: add_mono real_of_pinfreal_mono le_imp_neg_le positive_integral_mono)
hoelzl@38656
  1402
  fix x assume "x \<in> space M" from mono[OF this]
hoelzl@38656
  1403
  show "Real (f x) \<le> Real (g x)" "Real (- g x) \<le> Real (- f x)" by auto
hoelzl@35582
  1404
qed
hoelzl@35582
  1405
hoelzl@38656
  1406
lemma (in measure_space) integral_diff[simp, intro]:
hoelzl@38656
  1407
  assumes f: "integrable f" and g: "integrable g"
hoelzl@38656
  1408
  shows "integrable (\<lambda>t. f t - g t)"
hoelzl@38656
  1409
  and "integral (\<lambda>t. f t - g t) = integral f - integral g"
hoelzl@38656
  1410
  using integral_add[OF f integral_minus(1)[OF g]]
hoelzl@38656
  1411
  unfolding diff_minus integral_minus(2)[OF g]
hoelzl@38656
  1412
  by auto
hoelzl@38656
  1413
hoelzl@38656
  1414
lemma (in measure_space) integral_indicator[simp, intro]:
hoelzl@38656
  1415
  assumes "a \<in> sets M" and "\<mu> a \<noteq> \<omega>"
hoelzl@38656
  1416
  shows "integral (indicator a) = real (\<mu> a)" (is ?int)
hoelzl@38656
  1417
  and "integrable (indicator a)" (is ?able)
hoelzl@35582
  1418
proof -
hoelzl@38656
  1419
  have *:
hoelzl@38656
  1420
    "\<And>A x. Real (indicator A x) = indicator A x"
hoelzl@38656
  1421
    "\<And>A x. Real (- indicator A x) = 0" unfolding indicator_def by auto
hoelzl@38656
  1422
  show ?int ?able
hoelzl@38656
  1423
    using assms unfolding integral_def integrable_def
hoelzl@38656
  1424
    by (auto simp: * positive_integral_indicator borel_measurable_indicator)
hoelzl@35582
  1425
qed
hoelzl@35582
  1426
hoelzl@38656
  1427
lemma (in measure_space) integral_cmul_indicator:
hoelzl@38656
  1428
  assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<omega>"
hoelzl@38656
  1429
  shows "integrable (\<lambda>x. c * indicator A x)" (is ?P)
hoelzl@38656
  1430
  and "integral (\<lambda>x. c * indicator A x) = c * real (\<mu> A)" (is ?I)
hoelzl@38656
  1431
proof -
hoelzl@38656
  1432
  show ?P
hoelzl@38656
  1433
  proof (cases "c = 0")
hoelzl@38656
  1434
    case False with assms show ?thesis by simp
hoelzl@38656
  1435
  qed simp
hoelzl@35582
  1436
hoelzl@38656
  1437
  show ?I
hoelzl@38656
  1438
  proof (cases "c = 0")
hoelzl@38656
  1439
    case False with assms show ?thesis by simp
hoelzl@38656
  1440
  qed simp
hoelzl@38656
  1441
qed
hoelzl@35582
  1442
hoelzl@38656
  1443
lemma (in measure_space) integral_setsum[simp, intro]:
hoelzl@35582
  1444
  assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
hoelzl@35582
  1445
  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
hoelzl@38656
  1446
    and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S")
hoelzl@35582
  1447
proof -
hoelzl@38656
  1448
  have "?int S \<and> ?I S"
hoelzl@38656
  1449
  proof (cases "finite S")
hoelzl@38656
  1450
    assume "finite S"
hoelzl@38656
  1451
    from this assms show ?thesis by (induct S) simp_all
hoelzl@38656
  1452
  qed simp
hoelzl@35582
  1453
  thus "?int S" and "?I S" by auto
hoelzl@35582
  1454
qed
hoelzl@35582
  1455
hoelzl@36624
  1456
lemma (in measure_space) integrable_abs:
hoelzl@36624
  1457
  assumes "integrable f"
hoelzl@36624
  1458
  shows "integrable (\<lambda> x. \<bar>f x\<bar>)"
hoelzl@36624
  1459
proof -
hoelzl@38656
  1460
  have *:
hoelzl@38656
  1461
    "\<And>x. Real \<bar>f x\<bar> = Real (f x) + Real (- f x)"
hoelzl@38656
  1462
    "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto
hoelzl@38656
  1463
  have abs: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" and
hoelzl@38656
  1464
    f: "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
hoelzl@38656
  1465
        "(\<lambda>x. Real (- f x)) \<in> borel_measurable M"
hoelzl@38656
  1466
    using assms unfolding integrable_def by auto
hoelzl@38656
  1467
  from abs assms show ?thesis unfolding integrable_def *
hoelzl@38656
  1468
    using positive_integral_linear[OF f, of 1] by simp
hoelzl@38656
  1469
qed
hoelzl@38656
  1470
hoelzl@38656
  1471
lemma (in measure_space) integrable_bound:
hoelzl@38656
  1472
  assumes "integrable f"
hoelzl@38656
  1473
  and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
hoelzl@38656
  1474
    "\<And>x. x \<in> space M \<Longrightarrow> \<bar>g x\<bar> \<le> f x"
hoelzl@38656
  1475
  assumes borel: "g \<in> borel_measurable M"
hoelzl@38656
  1476
  shows "integrable g"
hoelzl@38656
  1477
proof -
hoelzl@38656
  1478
  have "positive_integral (\<lambda>x. Real (g x)) \<le> positive_integral (\<lambda>x. Real \<bar>g x\<bar>)"
hoelzl@38656
  1479
    by (auto intro!: positive_integral_mono)
hoelzl@38656
  1480
  also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))"
hoelzl@38656
  1481
    using f by (auto intro!: positive_integral_mono)
hoelzl@38656
  1482
  also have "\<dots> < \<omega>"
hoelzl@38656
  1483
    using `integrable f` unfolding integrable_def by (auto simp: pinfreal_less_\<omega>)
hoelzl@38656
  1484
  finally have pos: "positive_integral (\<lambda>x. Real (g x)) < \<omega>" .
hoelzl@38656
  1485
hoelzl@38656
  1486
  have "positive_integral (\<lambda>x. Real (- g x)) \<le> positive_integral (\<lambda>x. Real (\<bar>g x\<bar>))"
hoelzl@38656
  1487
    by (auto intro!: positive_integral_mono)
hoelzl@38656
  1488
  also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))"
hoelzl@38656
  1489
    using f by (auto intro!: positive_integral_mono)
hoelzl@38656
  1490
  also have "\<dots> < \<omega>"
hoelzl@38656
  1491
    using `integrable f` unfolding integrable_def by (auto simp: pinfreal_less_\<omega>)
hoelzl@38656
  1492
  finally have neg: "positive_integral (\<lambda>x. Real (- g x)) < \<omega>" .
hoelzl@38656
  1493
hoelzl@38656
  1494
  from neg pos borel show ?thesis
hoelzl@36624
  1495
    unfolding integrable_def by auto
hoelzl@38656
  1496
qed
hoelzl@38656
  1497
hoelzl@38656
  1498
lemma (in measure_space) integrable_abs_iff:
hoelzl@38656
  1499
  "f \<in> borel_measurable M \<Longrightarrow> integrable (\<lambda> x. \<bar>f x\<bar>) \<longleftrightarrow> integrable f"
hoelzl@38656
  1500
  by (auto intro!: integrable_bound[where g=f] integrable_abs)
hoelzl@38656
  1501
hoelzl@38656
  1502
lemma (in measure_space) integrable_max:
hoelzl@38656
  1503
  assumes int: "integrable f" "integrable g"
hoelzl@38656
  1504
  shows "integrable (\<lambda> x. max (f x) (g x))"
hoelzl@38656
  1505
proof (rule integrable_bound)
hoelzl@38656
  1506
  show "integrable (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
hoelzl@38656
  1507
    using int by (simp add: integrable_abs)
hoelzl@38656
  1508
  show "(\<lambda>x. max (f x) (g x)) \<in> borel_measurable M"
hoelzl@38656
  1509
    using int unfolding integrable_def by auto
hoelzl@38656
  1510
next
hoelzl@38656
  1511
  fix x assume "x \<in> space M"
hoelzl@38656
  1512
  show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>max (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
hoelzl@38656
  1513
    by auto
hoelzl@38656
  1514
qed
hoelzl@38656
  1515
hoelzl@38656
  1516
lemma (in measure_space) integrable_min:
hoelzl@38656
  1517
  assumes int: "integrable f" "integrable g"
hoelzl@38656
  1518
  shows "integrable (\<lambda> x. min (f x) (g x))"
hoelzl@38656
  1519
proof (rule integrable_bound)
hoelzl@38656
  1520
  show "integrable (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
hoelzl@38656
  1521
    using int by (simp add: integrable_abs)
hoelzl@38656
  1522
  show "(\<lambda>x. min (f x) (g x)) \<in> borel_measurable M"
hoelzl@38656
  1523
    using int unfolding integrable_def by auto
hoelzl@38656
  1524
next
hoelzl@38656
  1525
  fix x assume "x \<in> space M"
hoelzl@38656
  1526
  show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>min (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
hoelzl@38656
  1527
    by auto
hoelzl@38656
  1528
qed
hoelzl@38656
  1529
hoelzl@38656
  1530
lemma (in measure_space) integral_triangle_inequality:
hoelzl@38656
  1531
  assumes "integrable f"
hoelzl@38656
  1532
  shows "\<bar>integral f\<bar> \<le> integral (\<lambda>x. \<bar>f x\<bar>)"
hoelzl@38656
  1533
proof -
hoelzl@38656
  1534
  have "\<bar>integral f\<bar> = max (integral f) (- integral f)" by auto
hoelzl@38656
  1535
  also have "\<dots> \<le> integral (\<lambda>x. \<bar>f x\<bar>)"
hoelzl@38656
  1536
      using assms integral_minus(2)[of f, symmetric]
hoelzl@38656
  1537
      by (auto intro!: integral_mono integrable_abs simp del: integral_minus)
hoelzl@38656
  1538
  finally show ?thesis .
hoelzl@36624
  1539
qed
hoelzl@36624
  1540
hoelzl@38656
  1541
lemma (in measure_space) integral_positive:
hoelzl@38656
  1542
  assumes "integrable f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
hoelzl@38656
  1543
  shows "0 \<le> integral f"
hoelzl@38656
  1544
proof -
hoelzl@38656
  1545
  have "0 = integral (\<lambda>x. 0)" by (auto simp: integral_zero)
hoelzl@38656
  1546
  also have "\<dots> \<le> integral f"
hoelzl@38656
  1547
    using assms by (rule integral_mono[OF integral_zero(1)])
hoelzl@38656
  1548
  finally show ?thesis .
hoelzl@38656
  1549
qed
hoelzl@38656
  1550
hoelzl@38656
  1551
lemma (in measure_space) integral_monotone_convergence_pos:
hoelzl@38656
  1552
  assumes i: "\<And>i. integrable (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
hoelzl@38656
  1553
  and pos: "\<And>x i. 0 \<le> f i x"
hoelzl@38656
  1554
  and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
hoelzl@38656
  1555
  and ilim: "(\<lambda>i. integral (f i)) ----> x"
hoelzl@38656
  1556
  shows "integrable u"
hoelzl@38656
  1557
  and "integral u = x"
hoelzl@35582
  1558
proof -
hoelzl@38656
  1559
  { fix x have "0 \<le> u x"
hoelzl@38656
  1560
      using mono pos[of 0 x] incseq_le[OF _ lim, of x 0]
hoelzl@38656
  1561
      by (simp add: mono_def incseq_def) }
hoelzl@38656
  1562
  note pos_u = this
hoelzl@38656
  1563
hoelzl@38656
  1564
  hence [simp]: "\<And>i x. Real (- f i x) = 0" "\<And>x. Real (- u x) = 0"
hoelzl@38656
  1565
    using pos by auto
hoelzl@38656
  1566
hoelzl@38656
  1567
  have SUP_F: "\<And>x. (SUP n. Real (f n x)) = Real (u x)"
hoelzl@38656
  1568
    using mono pos pos_u lim by (rule SUP_eq_LIMSEQ[THEN iffD2])
hoelzl@38656
  1569
hoelzl@38656
  1570
  have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M"
hoelzl@38656
  1571
    using i unfolding integrable_def by auto
hoelzl@38656
  1572
  hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M"
hoelzl@35582
  1573
    by auto
hoelzl@38656
  1574
  hence borel_u: "u \<in> borel_measurable M"
hoelzl@38656
  1575
    using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F)
hoelzl@38656
  1576
hoelzl@38656
  1577
  have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
hoelzl@38656
  1578
    using i unfolding integral_def integrable_def by (auto simp: Real_real)
hoelzl@38656
  1579
hoelzl@38656
  1580
  have pos_integral: "\<And>n. 0 \<le> integral (f n)"
hoelzl@38656
  1581
    using pos i by (auto simp: integral_positive)
hoelzl@38656
  1582
  hence "0 \<le> x"
hoelzl@38656
  1583
    using LIMSEQ_le_const[OF ilim, of 0] by auto
hoelzl@38656
  1584
hoelzl@38656
  1585
  have "(\<lambda>i. positive_integral (\<lambda>x. Real (f i x))) \<up> positive_integral (\<lambda>x. Real (u x))"
hoelzl@38656
  1586
  proof (rule positive_integral_isoton)
hoelzl@38656
  1587
    from SUP_F mono pos
hoelzl@38656
  1588
    show "(\<lambda>i x. Real (f i x)) \<up> (\<lambda>x. Real (u x))"
hoelzl@38656
  1589
      unfolding isoton_fun_expand by (auto simp: isoton_def mono_def)
hoelzl@38656
  1590
  qed (rule borel_f)
hoelzl@38656
  1591
  hence pI: "positive_integral (\<lambda>x. Real (u x)) =
hoelzl@38656
  1592
      (SUP n. positive_integral (\<lambda>x. Real (f n x)))"
hoelzl@38656
  1593
    unfolding isoton_def by simp
hoelzl@38656
  1594
  also have "\<dots> = Real x" unfolding integral_eq
hoelzl@38656
  1595
  proof (rule SUP_eq_LIMSEQ[THEN iffD2])
hoelzl@38656
  1596
    show "mono (\<lambda>n. integral (f n))"
hoelzl@38656
  1597
      using mono i by (auto simp: mono_def intro!: integral_mono)
hoelzl@38656
  1598
    show "\<And>n. 0 \<le> integral (f n)" using pos_integral .
hoelzl@38656
  1599
    show "0 \<le> x" using `0 \<le> x` .
hoelzl@38656
  1600
    show "(\<lambda>n. integral (f n)) ----> x" using ilim .
hoelzl@38656
  1601
  qed
hoelzl@38656
  1602
  finally show  "integrable u" "integral u = x" using borel_u `0 \<le> x`
hoelzl@38656
  1603
    unfolding integrable_def integral_def by auto
hoelzl@38656
  1604
qed
hoelzl@38656
  1605
hoelzl@38656
  1606
lemma (in measure_space) integral_monotone_convergence:
hoelzl@38656
  1607
  assumes f: "\<And>i. integrable (f i)" and "mono f"
hoelzl@38656
  1608
  and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
hoelzl@38656
  1609
  and ilim: "(\<lambda>i. integral (f i)) ----> x"
hoelzl@38656
  1610
  shows "integrable u"
hoelzl@38656
  1611
  and "integral u = x"
hoelzl@38656
  1612
proof -
hoelzl@38656
  1613
  have 1: "\<And>i. integrable (\<lambda>x. f i x - f 0 x)"
hoelzl@38656
  1614
      using f by (auto intro!: integral_diff)
hoelzl@38656
  1615
  have 2: "\<And>x. mono (\<lambda>n. f n x - f 0 x)" using `mono f`
hoelzl@38656
  1616
      unfolding mono_def le_fun_def by auto
hoelzl@38656
  1617
  have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
hoelzl@38656
  1618
      unfolding mono_def le_fun_def by (auto simp: field_simps)
hoelzl@38656
  1619
  have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
hoelzl@38656
  1620
    using lim by (auto intro!: LIMSEQ_diff)
hoelzl@38656
  1621
  have 5: "(\<lambda>i. integral (\<lambda>x. f i x - f 0 x)) ----> x - integral (f 0)"
hoelzl@38656
  1622
    using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
hoelzl@38656
  1623
  note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
hoelzl@38656
  1624
  have "integrable (\<lambda>x. (u x - f 0 x) + f 0 x)"
hoelzl@38656
  1625
    using diff(1) f by (rule integral_add(1))
hoelzl@38656
  1626
  with diff(2) f show "integrable u" "integral u = x"
hoelzl@38656
  1627
    by (auto simp: integral_diff)
hoelzl@38656
  1628
qed
hoelzl@38656
  1629
hoelzl@38656
  1630
lemma (in measure_space) integral_0_iff:
hoelzl@38656
  1631
  assumes "integrable f"
hoelzl@38656
  1632
  shows "integral (\<lambda>x. \<bar>f x\<bar>) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
hoelzl@38656
  1633
proof -
hoelzl@38656
  1634
  have *: "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto
hoelzl@38656
  1635
  have "integrable (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs)
hoelzl@38656
  1636
  hence "(\<lambda>x. Real (\<bar>f x\<bar>)) \<in> borel_measurable M"
hoelzl@38656
  1637
    "positive_integral (\<lambda>x. Real \<bar>f x\<bar>) \<noteq> \<omega>" unfolding integrable_def by auto
hoelzl@38656
  1638
  from positive_integral_0_iff[OF this(1)] this(2)
hoelzl@38656
  1639
  show ?thesis unfolding integral_def *
hoelzl@38656
  1640
    by (simp add: real_of_pinfreal_eq_0)
hoelzl@35582
  1641
qed
hoelzl@35582
  1642
hoelzl@38656
  1643
lemma LIMSEQ_max:
hoelzl@38656
  1644
  "u ----> (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) ----> max x 0"
hoelzl@38656
  1645
  by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D)