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