src/HOL/Probability/Lebesgue_Integration.thy
author hoelzl
Mon, 23 Aug 2010 19:35:57 +0200
changeset 38656 d5d342611edb
parent 38642 src/HOL/Probability/Lebesgue.thy@8fa437809c67
child 38705 aaee86c0e237
permissions -rw-r--r--
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
     1
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
     2
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     3
header {*Lebesgue Integration*}
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     4
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
     5
theory Lebesgue_Integration
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     6
imports Measure Borel
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     7
begin
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     8
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
     9
section "@{text \<mu>}-null sets"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    10
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    11
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    12
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    13
lemma sums_If_finite:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    14
  assumes finite: "finite {r. P r}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    15
  shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    16
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    17
  assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    18
  thus ?thesis by (simp add: sums_zero)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    19
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    20
  assume not_empty: "{r. P r} \<noteq> {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    21
  have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    22
    by (rule series_zero)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    23
       (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    24
  also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    25
    by (subst setsum_cases)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    26
       (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    27
  finally show ?thesis .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    28
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    29
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    30
lemma sums_single:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    31
  "(\<lambda>r. if r = i then f r else 0) sums f i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    32
  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    33
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    34
section "Simple function"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    35
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    36
text {*
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    37
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    38
Our simple functions are not restricted to positive real numbers. Instead
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    39
they are just functions with a finite range and are measurable when singleton
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    40
sets are measurable.
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    41
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    42
*}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    43
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    44
definition (in sigma_algebra) "simple_function g \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    45
    finite (g ` space M) \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    46
    (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    47
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    48
lemma (in sigma_algebra) simple_functionD:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    49
  assumes "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    50
  shows "finite (g ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    51
  "x \<in> g ` space M \<Longrightarrow> g -` {x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    52
  using assms unfolding simple_function_def by auto
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    53
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    54
lemma (in sigma_algebra) simple_function_indicator_representation:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    55
  fixes f ::"'a \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    56
  assumes f: "simple_function f" and x: "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    57
  shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    58
  (is "?l = ?r")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    59
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    60
  have "?r = (\<Sum>y \<in> f ` space M. 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    61
    (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    62
    by (auto intro!: setsum_cong2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    63
  also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    64
    using assms by (auto dest: simple_functionD simp: setsum_delta)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    65
  also have "... = f x" using x by (auto simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    66
  finally show ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    67
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    68
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    69
lemma (in measure_space) simple_function_notspace:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    70
  "simple_function (\<lambda>x. h x * indicator (- space M) x::pinfreal)" (is "simple_function ?h")
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    71
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    72
  have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    73
  hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    74
  have "?h -` {0} \<inter> space M = space M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    75
  thus ?thesis unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    76
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    77
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    78
lemma (in sigma_algebra) simple_function_cong:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    79
  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    80
  shows "simple_function f \<longleftrightarrow> simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    81
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    82
  have "f ` space M = g ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    83
    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    84
    using assms by (auto intro!: image_eqI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    85
  thus ?thesis unfolding simple_function_def using assms by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    86
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    87
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    88
lemma (in sigma_algebra) borel_measurable_simple_function:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    89
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    90
  shows "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    91
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    92
  fix S
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    93
  let ?I = "f ` (f -` S \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    94
  have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    95
  have "finite ?I"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    96
    using assms unfolding simple_function_def by (auto intro: finite_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    97
  hence "?U \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    98
    apply (rule finite_UN)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    99
    using assms unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   100
  thus "f -` S \<inter> space M \<in> sets M" unfolding * .
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   101
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   102
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   103
lemma (in sigma_algebra) simple_function_borel_measurable:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   104
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   105
  assumes "f \<in> borel_measurable M" and "finite (f ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   106
  shows "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   107
  using assms unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   108
  by (auto intro: borel_measurable_vimage)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   109
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   110
lemma (in sigma_algebra) simple_function_const[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   111
  "simple_function (\<lambda>x. c)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   112
  by (auto intro: finite_subset simp: simple_function_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   113
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   114
lemma (in sigma_algebra) simple_function_compose[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   115
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   116
  shows "simple_function (g \<circ> f)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   117
  unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   118
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   119
  show "finite ((g \<circ> f) ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   120
    using assms unfolding simple_function_def by (auto simp: image_compose)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   121
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   122
  fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   123
  let ?G = "g -` {g (f x)} \<inter> (f`space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   124
  have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   125
    (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   126
  show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   127
    using assms unfolding simple_function_def *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   128
    by (rule_tac finite_UN) (auto intro!: finite_UN)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   129
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   130
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   131
lemma (in sigma_algebra) simple_function_indicator[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   132
  assumes "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   133
  shows "simple_function (indicator A)"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   134
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   135
  have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   136
    by (auto simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   137
  hence "finite ?S" by (rule finite_subset) simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   138
  moreover have "- A \<inter> space M = space M - A" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   139
  ultimately show ?thesis unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   140
    using assms by (auto simp: indicator_def_raw)
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   141
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   142
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   143
lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   144
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   145
  assumes "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   146
  shows "simple_function (\<lambda>x. (f x, g x))" (is "simple_function ?p")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   147
  unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   148
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   149
  show "finite (?p ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   150
    using assms unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   151
    by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   152
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   153
  fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   154
  have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   155
      (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   156
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   157
  with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   158
    using assms unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   159
qed
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   160
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   161
lemma (in sigma_algebra) simple_function_compose1:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   162
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   163
  shows "simple_function (\<lambda>x. g (f x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   164
  using simple_function_compose[OF assms, of g]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   165
  by (simp add: comp_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   166
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   167
lemma (in sigma_algebra) simple_function_compose2:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   168
  assumes "simple_function f" and "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   169
  shows "simple_function (\<lambda>x. h (f x) (g x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   170
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   171
  have "simple_function ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   172
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   173
  thus ?thesis by (simp_all add: comp_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   174
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   175
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   176
lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   177
  and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   178
  and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   179
  and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   180
  and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   181
  and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   182
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   183
lemma (in sigma_algebra) simple_function_setsum[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   184
  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   185
  shows "simple_function (\<lambda>x. \<Sum>i\<in>P. f i x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   186
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   187
  assume "finite P" from this assms show ?thesis by induct auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   188
qed auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   189
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   190
lemma (in sigma_algebra) simple_function_le_measurable:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   191
  assumes "simple_function f" "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   192
  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   193
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   194
  have *: "{x \<in> space M. f x \<le> g x} =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   195
    (\<Union>(F, G)\<in>f`space M \<times> g`space M.
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   196
      if F \<le> G then (f -` {F} \<inter> space M) \<inter> (g -` {G} \<inter> space M) else {})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   197
    apply (auto split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   198
    apply (rule_tac x=x in bexI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   199
    apply (rule_tac x=x in bexI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   200
    by simp_all
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   201
  have **: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   202
    (f -` {f x} \<inter> space M) \<inter> (g -` {g y} \<inter> space M) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   203
    using assms unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   204
  have "finite (f`space M \<times> g`space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   205
    using assms unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   206
  thus ?thesis unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   207
    apply (rule finite_UN)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   208
    using assms unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   209
    by (auto intro!: **)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   210
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   211
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   212
lemma setsum_indicator_disjoint_family:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   213
  fixes f :: "'d \<Rightarrow> 'e::semiring_1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   214
  assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   215
  shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   216
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   217
  have "P \<inter> {i. x \<in> A i} = {j}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   218
    using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   219
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   220
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   221
    unfolding indicator_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   222
    by (simp add: if_distrib setsum_cases[OF `finite P`])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   223
qed
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   224
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   225
lemma LeastI2_wellorder:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   226
  fixes a :: "_ :: wellorder"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   227
  assumes "P a"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   228
  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   229
  shows "Q (Least P)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   230
proof (rule LeastI2_order)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   231
  show "P (Least P)" using `P a` by (rule LeastI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   232
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   233
  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   234
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   235
  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   236
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   237
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   238
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   239
  fixes u :: "'a \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   240
  assumes u: "u \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   241
  shows "\<exists>f. (\<forall>i. simple_function (f i) \<and> (\<forall>x\<in>space M. f i x \<noteq> \<omega>)) \<and> f \<up> u"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   242
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   243
  have "\<exists>f. \<forall>x j. (of_nat j \<le> u x \<longrightarrow> f x j = j*2^j) \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   244
    (u x < of_nat j \<longrightarrow> of_nat (f x j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f x j)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   245
    (is "\<exists>f. \<forall>x j. ?P x j (f x j)")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   246
  proof(rule choice, rule, rule choice, rule)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   247
    fix x j show "\<exists>n. ?P x j n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   248
    proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   249
      assume *: "u x < of_nat j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   250
      then obtain r where r: "u x = Real r" "0 \<le> r" by (cases "u x") auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   251
      from reals_Archimedean6a[of "r * 2^j"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   252
      obtain n :: nat where "real n \<le> r * 2 ^ j" "r * 2 ^ j < real (Suc n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   253
        using `0 \<le> r` by (auto simp: zero_le_power zero_le_mult_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   254
      thus ?thesis using r * by (auto intro!: exI[of _ n])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   255
    qed auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   256
  qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   257
  then obtain f where top: "\<And>j x. of_nat j \<le> u x \<Longrightarrow> f x j = j*2^j" and
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   258
    upper: "\<And>j x. u x < of_nat j \<Longrightarrow> of_nat (f x j) \<le> u x * 2^j" and
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   259
    lower: "\<And>j x. u x < of_nat j \<Longrightarrow> u x * 2^j < of_nat (Suc (f x j))" by blast
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   260
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   261
  { fix j x P
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   262
    assume 1: "of_nat j \<le> u x \<Longrightarrow> P (j * 2^j)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   263
    assume 2: "\<And>k. \<lbrakk> u x < of_nat j ; of_nat k \<le> u x * 2^j ; u x * 2^j < of_nat (Suc k) \<rbrakk> \<Longrightarrow> P k"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   264
    have "P (f x j)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   265
    proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   266
      assume "of_nat j \<le> u x" thus "P (f x j)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   267
        using top[of j x] 1 by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   268
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   269
      assume "\<not> of_nat j \<le> u x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   270
      hence "u x < of_nat j" "of_nat (f x j) \<le> u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   271
        using upper lower by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   272
      from 2[OF this] show "P (f x j)" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   273
    qed }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   274
  note fI = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   275
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   276
  { fix j x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   277
    have "f x j = j * 2 ^ j \<longleftrightarrow> of_nat j \<le> u x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   278
      by (rule fI, simp, cases "u x") (auto split: split_if_asm) }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   279
  note f_eq = this
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   280
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   281
  { fix j x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   282
    have "f x j \<le> j * 2 ^ j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   283
    proof (rule fI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   284
      fix k assume *: "u x < of_nat j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   285
      assume "of_nat k \<le> u x * 2 ^ j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   286
      also have "\<dots> \<le> of_nat (j * 2^j)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   287
        using * by (cases "u x") (auto simp: zero_le_mult_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   288
      finally show "k \<le> j*2^j" by (auto simp del: real_of_nat_mult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   289
    qed simp }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   290
  note f_upper = this
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   291
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   292
  let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   293
  show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   294
  proof (safe intro!: exI[of _ ?g])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   295
    fix j
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   296
    have *: "?g j ` space M \<subseteq> (\<lambda>x. of_nat x / 2^j) ` {..j * 2^j}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   297
      using f_upper by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   298
    thus "finite (?g j ` space M)" by (rule finite_subset) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   299
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   300
    fix j t assume "t \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   301
    have **: "?g j -` {?g j t} \<inter> space M = {x \<in> space M. f t j = f x j}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   302
      by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   303
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   304
    show "?g j -` {?g j t} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   305
    proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   306
      assume "of_nat j \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   307
      hence "?g j -` {?g j t} \<inter> space M = {x\<in>space M. of_nat j \<le> u x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   308
        unfolding ** f_eq[symmetric] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   309
      thus "?g j -` {?g j t} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   310
        using u by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   311
    next
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   312
      assume not_t: "\<not> of_nat j \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   313
      hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \<le> j*2^j` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   314
      have split_vimage: "?g j -` {?g j t} \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   315
          {x\<in>space M. of_nat (f t j)/2^j \<le> u x} \<inter> {x\<in>space M. u x < of_nat (Suc (f t j))/2^j}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   316
        unfolding **
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   317
      proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   318
        fix x assume [simp]: "f t j = f x j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   319
        have *: "\<not> of_nat j \<le> u x" using not_t f_eq[symmetric] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   320
        hence "of_nat (f t j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f t j))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   321
          using upper lower by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   322
        hence "of_nat (f t j) / 2^j \<le> u x \<and> u x < of_nat (Suc (f t j))/2^j" using *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   323
          by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   324
        thus "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   325
      next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   326
        fix x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   327
        assume "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   328
        hence "of_nat (f t j) \<le> u x * 2 ^ j \<and> u x * 2 ^ j < of_nat (Suc (f t j))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   329
          by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   330
        hence 1: "of_nat (f t j) \<le> u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   331
        note 2
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   332
        also have "\<dots> \<le> of_nat (j*2^j)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   333
          using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   334
        finally have bound_ux: "u x < of_nat j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   335
          by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   336
        show "f t j = f x j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   337
        proof (rule antisym)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   338
          from 1 lower[OF bound_ux]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   339
          show "f t j \<le> f x j" by (cases "u x") (auto split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   340
          from upper[OF bound_ux] 2
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   341
          show "f x j \<le> f t j" by (cases "u x") (auto split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   342
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   343
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   344
      show ?thesis unfolding split_vimage using u by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   345
    qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   346
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   347
    fix j t assume "?g j t = \<omega>" thus False by (auto simp: power_le_zero_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   348
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   349
    fix t
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   350
    { fix i
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   351
      have "f t i * 2 \<le> f t (Suc i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   352
      proof (rule fI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   353
        assume "of_nat (Suc i) \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   354
        hence "of_nat i \<le> u t" by (cases "u t") auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   355
        thus "f t i * 2 \<le> Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   356
      next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   357
        fix k
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   358
        assume *: "u t * 2 ^ Suc i < of_nat (Suc k)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   359
        show "f t i * 2 \<le> k"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   360
        proof (rule fI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   361
          assume "of_nat i \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   362
          hence "of_nat (i * 2^Suc i) \<le> u t * 2^Suc i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   363
            by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   364
          also have "\<dots> < of_nat (Suc k)" using * by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   365
          finally show "i * 2 ^ i * 2 \<le> k"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   366
            by (auto simp del: real_of_nat_mult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   367
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   368
          fix j assume "of_nat j \<le> u t * 2 ^ i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   369
          with * show "j * 2 \<le> k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   370
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   371
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   372
      thus "?g i t \<le> ?g (Suc i) t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   373
        by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   374
    hence mono: "mono (\<lambda>i. ?g i t)" unfolding mono_iff_le_Suc by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   375
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   376
    show "(SUP j. of_nat (f t j) / 2 ^ j) = u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   377
    proof (rule pinfreal_SUPI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   378
      fix j show "of_nat (f t j) / 2 ^ j \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   379
      proof (rule fI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   380
        assume "of_nat j \<le> u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   381
          by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   382
      next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   383
        fix k assume "of_nat k \<le> u t * 2 ^ j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   384
        thus "of_nat k / 2 ^ j \<le> u t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   385
          by (cases "u t")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   386
             (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   387
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   388
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   389
      fix y :: pinfreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   390
      show "u t \<le> y"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   391
      proof (cases "u t")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   392
        case (preal r)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   393
        show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   394
        proof (rule ccontr)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   395
          assume "\<not> u t \<le> y"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   396
          then obtain p where p: "y = Real p" "0 \<le> p" "p < r" using preal by (cases y) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   397
          with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r - p"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   398
          obtain n where n: "\<And>N. n \<le> N \<Longrightarrow> inverse (2^N) < r - p" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   399
          let ?N = "max n (natfloor r + 1)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   400
          have "u t < of_nat ?N" "n \<le> ?N"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   401
            using ge_natfloor_plus_one_imp_gt[of r n] preal
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   402
            by (auto simp: max_def real_Suc_natfloor)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   403
          from lower[OF this(1)]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   404
          have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   405
            using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   406
          hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   407
            using preal by (auto simp: field_simps divide_real_def[symmetric])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   408
          with n[OF `n \<le> ?N`] p preal *[of ?N]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   409
          show False
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   410
            by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   411
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   412
      next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   413
        case infinite
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   414
        { fix j have "f t j = j*2^j" using top[of j t] infinite by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   415
          hence "of_nat j \<le> y" using *[of j]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   416
            by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   417
        note all_less_y = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   418
        show ?thesis unfolding infinite
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   419
        proof (rule ccontr)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   420
          assume "\<not> \<omega> \<le> y" then obtain r where r: "y = Real r" "0 \<le> r" by (cases y) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   421
          moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   422
          with all_less_y[of n] r show False by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   423
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   424
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   425
    qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   426
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   427
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   428
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   429
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence':
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   430
  fixes u :: "'a \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   431
  assumes "u \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   432
  obtains (x) f where "f \<up> u" "\<And>i. simple_function (f i)" "\<And>i. \<omega>\<notin>f i`space M"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   433
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   434
  from borel_measurable_implies_simple_function_sequence[OF assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   435
  obtain f where x: "\<And>i. simple_function (f i)" "f \<up> u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   436
    and fin: "\<And>i. \<And>x. x\<in>space M \<Longrightarrow> f i x \<noteq> \<omega>" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   437
  { fix i from fin[of _ i] have "\<omega> \<notin> f i`space M" by fastsimp }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   438
  with x show thesis by (auto intro!: that[of f])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   439
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   440
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   441
section "Simple integral"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   442
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   443
definition (in measure_space)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   444
  "simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M))"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   445
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   446
lemma (in measure_space) simple_integral_cong:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   447
  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   448
  shows "simple_integral f = simple_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   449
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   450
  have "f ` space M = g ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   451
    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   452
    using assms by (auto intro!: image_eqI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   453
  thus ?thesis unfolding simple_integral_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   454
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   455
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   456
lemma (in measure_space) simple_integral_const[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   457
  "simple_integral (\<lambda>x. c) = c * \<mu> (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   458
proof (cases "space M = {}")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   459
  case True thus ?thesis unfolding simple_integral_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   460
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   461
  case False hence "(\<lambda>x. c) ` space M = {c}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   462
  thus ?thesis unfolding simple_integral_def by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   463
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   464
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   465
lemma (in measure_space) simple_function_partition:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   466
  assumes "simple_function f" and "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   467
  shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   468
    (is "_ = setsum _ (?p ` space M)")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   469
proof-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   470
  let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   471
  let ?SIGMA = "Sigma (f`space M) ?sub"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   472
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   473
  have [intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   474
    "finite (f ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   475
    "finite (g ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   476
    using assms unfolding simple_function_def by simp_all
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   477
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   478
  { fix A
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   479
    have "?p ` (A \<inter> space M) \<subseteq>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   480
      (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   481
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   482
    hence "finite (?p ` (A \<inter> space M))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   483
      by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   484
  note this[intro, simp]
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   485
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   486
  { fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   487
    have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   488
    moreover {
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   489
      fix x y
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   490
      have *: "f -` {f x} \<inter> g -` {g x} \<inter> space M
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   491
          = (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   492
      assume "x \<in> space M" "y \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   493
      hence "f -` {f x} \<inter> g -` {g x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   494
        using assms unfolding simple_function_def * by auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   495
    ultimately
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   496
    have "\<mu> (f -` {f x} \<inter> space M) = setsum (\<mu>) (?sub (f x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   497
      by (subst measure_finitely_additive) auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   498
  hence "simple_integral f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   499
    unfolding simple_integral_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   500
    by (subst setsum_Sigma[symmetric],
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   501
       auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   502
  also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   503
  proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   504
    have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   505
    have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   506
      = (\<lambda>x. (f x, ?p x)) ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   507
    proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   508
      fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   509
      thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   510
        by (auto intro!: image_eqI[of _ _ "?p x"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   511
    qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   512
    thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   513
      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   514
      apply (rule_tac x="xa" in image_eqI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   515
      by simp_all
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   516
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   517
  finally show ?thesis .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   518
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   519
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   520
lemma (in measure_space) simple_integral_add[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   521
  assumes "simple_function f" and "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   522
  shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   523
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   524
  { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   525
    assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   526
    hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   527
        "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   528
      by auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   529
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   530
    unfolding
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   531
      simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   532
      simple_function_partition[OF `simple_function f` `simple_function g`]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   533
      simple_function_partition[OF `simple_function g` `simple_function f`]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   534
    apply (subst (3) Int_commute)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   535
    by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   536
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   537
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   538
lemma (in measure_space) simple_integral_setsum[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   539
  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   540
  shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   541
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   542
  assume "finite P"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   543
  from this assms show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   544
    by induct (auto simp: simple_function_setsum simple_integral_add)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   545
qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   546
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   547
lemma (in measure_space) simple_integral_mult[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   548
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   549
  shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   550
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   551
  note mult = simple_function_mult[OF simple_function_const[of c] assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   552
  { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   553
    assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   554
    hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   555
      by auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   556
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   557
    unfolding simple_function_partition[OF mult assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   558
      simple_function_partition[OF assms mult]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   559
    by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   560
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   561
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   562
lemma (in measure_space) simple_integral_mono:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   563
  assumes "simple_function f" and "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   564
  and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   565
  shows "simple_integral f \<le> simple_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   566
  unfolding
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   567
    simple_function_partition[OF `simple_function f` `simple_function g`]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   568
    simple_function_partition[OF `simple_function g` `simple_function f`]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   569
  apply (subst Int_commute)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   570
proof (safe intro!: setsum_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   571
  fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   572
  assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   573
  hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   574
  thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   575
    using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   576
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   577
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   578
lemma (in measure_space) simple_integral_indicator:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   579
  assumes "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   580
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   581
  shows "simple_integral (\<lambda>x. f x * indicator A x) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   582
    (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   583
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   584
  assume "A = space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   585
  moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   586
    by (auto intro!: simple_integral_cong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   587
  moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   588
  ultimately show ?thesis by (simp add: simple_integral_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   589
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   590
  assume "A \<noteq> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   591
  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   592
  have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   593
  proof safe
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   594
    fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   595
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   596
    fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   597
      using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   598
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   599
    show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   600
  qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   601
  have *: "simple_integral (\<lambda>x. f x * indicator A x) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   602
    (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   603
    unfolding simple_integral_def I
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   604
  proof (rule setsum_mono_zero_cong_left)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   605
    show "finite (f ` space M \<union> {0})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   606
      using assms(2) unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   607
    show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   608
      using sets_into_space[OF assms(1)] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   609
    have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}" by (auto simp: image_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   610
    thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   611
      i * \<mu> (f -` {i} \<inter> space M \<inter> A) = 0" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   612
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   613
    fix x assume "x \<in> f`A \<union> {0}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   614
    hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   615
      by (auto simp: indicator_def split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   616
    thus "x * \<mu> (?I -` {x} \<inter> space M) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   617
      x * \<mu> (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   618
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   619
  show ?thesis unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   620
    using assms(2) unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   621
    by (auto intro!: setsum_mono_zero_cong_right)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   622
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   623
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   624
lemma (in measure_space) simple_integral_indicator_only[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   625
  assumes "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   626
  shows "simple_integral (indicator A) = \<mu> A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   627
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   628
  assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   629
  thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   630
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   631
  assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pinfreal}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   632
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   633
    using simple_integral_indicator[OF assms simple_function_const[of 1]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   634
    using sets_into_space[OF assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   635
    by (auto intro!: arg_cong[where f="\<mu>"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   636
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   637
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   638
lemma (in measure_space) simple_integral_null_set:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   639
  assumes "simple_function u" "N \<in> null_sets"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   640
  shows "simple_integral (\<lambda>x. u x * indicator N x) = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   641
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   642
  have "simple_integral (\<lambda>x. u x * indicator N x) \<le>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   643
    simple_integral (\<lambda>x. \<omega> * indicator N x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   644
    using assms
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   645
    by (safe intro!: simple_integral_mono simple_function_mult simple_function_indicator simple_function_const) simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   646
  also have "... = 0" apply(subst simple_integral_mult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   647
    using assms(2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   648
  finally show ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   649
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   650
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   651
lemma (in measure_space) simple_integral_cong':
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   652
  assumes f: "simple_function f" and g: "simple_function g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   653
  and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   654
  shows "simple_integral f = simple_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   655
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   656
  let ?h = "\<lambda>h. \<lambda>x. (h x * indicator {x\<in>space M. f x = g x} x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   657
    + h x * indicator {x\<in>space M. f x \<noteq> g x} x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   658
    + h x * indicator (-space M) x::pinfreal)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   659
  have *:"\<And>h. h = ?h h" unfolding indicator_def apply rule by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   660
  have mea_neq:"{x \<in> space M. f x \<noteq> g x} \<in> sets M" using f g by (auto simp: borel_measurable_simple_function)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   661
  then have mea_nullset: "{x \<in> space M. f x \<noteq> g x} \<in> null_sets" using mea by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   662
  have h1:"\<And>h::_=>pinfreal. simple_function h \<Longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   663
    simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x = g x} x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   664
    apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   665
    using f g by (auto simp: borel_measurable_simple_function)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   666
  have h2:"\<And>h::_\<Rightarrow>pinfreal. simple_function h \<Longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   667
    simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x \<noteq> g x} x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   668
    apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   669
    by(rule mea_neq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   670
  have **:"\<And>a b c d e f. a = b \<Longrightarrow> c = d \<Longrightarrow> e = f \<Longrightarrow> a+c+e = b+d+f" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   671
  note *** = simple_integral_add[OF simple_function_add[OF h1 h2] simple_function_notspace]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   672
    simple_integral_add[OF h1 h2]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   673
  show ?thesis apply(subst *[of g]) apply(subst *[of f])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   674
    unfolding ***[OF f f] ***[OF g g]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   675
  proof(rule **) case goal1 show ?case apply(rule arg_cong[where f=simple_integral]) apply rule 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   676
      unfolding indicator_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   677
  next note * = simple_integral_null_set[OF _ mea_nullset]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   678
    case goal2 show ?case unfolding *[OF f] *[OF g] ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   679
  next case goal3 show ?case apply(rule simple_integral_cong) by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   680
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   681
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   682
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   683
section "Continuous posititve integration"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   684
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   685
definition (in measure_space)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   686
  "positive_integral f =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   687
    (SUP g : {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. simple_integral g)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   688
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   689
lemma (in measure_space) positive_integral_alt1:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   690
  "positive_integral f =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   691
    (SUP g : {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}. simple_integral g)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   692
  unfolding positive_integral_def SUPR_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   693
proof (safe intro!: arg_cong[where f=Sup])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   694
  fix g let ?g = "\<lambda>x. if x \<in> space M then g x else f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   695
  assume "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   696
  hence "?g \<le> f" "simple_function ?g" "simple_integral g = simple_integral ?g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   697
    "\<omega> \<notin> g`space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   698
    unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   699
  thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   700
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   701
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   702
  fix g assume "simple_function g" "g \<le> f" "\<omega> \<notin> g`space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   703
  hence "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   704
    by (auto simp add: le_fun_def image_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   705
  thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   706
    by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   707
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   708
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   709
lemma (in measure_space) positive_integral_alt:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   710
  "positive_integral f =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   711
    (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   712
  apply(rule order_class.antisym) unfolding positive_integral_def 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   713
  apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   714
proof safe fix u assume u:"simple_function u" and uf:"u \<le> f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   715
  let ?u = "\<lambda>n x. if u x = \<omega> then Real (real (n::nat)) else u x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   716
  have su:"\<And>n. simple_function (?u n)" using simple_function_compose1[OF u] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   717
  show "\<exists>b. \<forall>n. b n \<in> {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   718
    (\<lambda>n. simple_integral (b n)) ----> simple_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   719
    apply(rule_tac x="?u" in exI, safe) apply(rule su)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   720
  proof- fix n::nat have "?u n \<le> u" unfolding le_fun_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   721
    also note uf finally show "?u n \<le> f" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   722
    let ?s = "{x \<in> space M. u x = \<omega>}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   723
    show "(\<lambda>n. simple_integral (?u n)) ----> simple_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   724
    proof(cases "\<mu> ?s = 0")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   725
      case True have *:"\<And>n. {x\<in>space M. ?u n x \<noteq> u x} = {x\<in>space M. u x = \<omega>}" by auto 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   726
      have *:"\<And>n. simple_integral (?u n) = simple_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   727
        apply(rule simple_integral_cong'[OF su u]) unfolding * True ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   728
      show ?thesis unfolding * by auto 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   729
    next case False note m0=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   730
      have s:"{x \<in> space M. u x = \<omega>} \<in> sets M" using u  by (auto simp: borel_measurable_simple_function)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   731
      have "\<omega> = simple_integral (\<lambda>x. \<omega> * indicator {x\<in>space M. u x = \<omega>} x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   732
        apply(subst simple_integral_mult) using s
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   733
        unfolding simple_integral_indicator_only[OF s] using False by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   734
      also have "... \<le> simple_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   735
        apply (rule simple_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   736
        apply (rule simple_function_mult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   737
        apply (rule simple_function_const)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   738
        apply(rule ) prefer 3 apply(subst indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   739
        using s u by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   740
      finally have *:"simple_integral u = \<omega>" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   741
      show ?thesis unfolding * Lim_omega_pos
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   742
      proof safe case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   743
        from real_arch_simple[of "B / real (\<mu> ?s)"] guess N0 .. note N=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   744
        def N \<equiv> "Suc N0" have N:"real N \<ge> B / real (\<mu> ?s)" "N > 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   745
          unfolding N_def using N by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   746
        show ?case apply-apply(rule_tac x=N in exI,safe) 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   747
        proof- case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   748
          have "Real B \<le> Real (real N) * \<mu> ?s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   749
          proof(cases "\<mu> ?s = \<omega>")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   750
            case True thus ?thesis using `B>0` N by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   751
          next case False
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   752
            have *:"B \<le> real N * real (\<mu> ?s)" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   753
              using N(1) apply-apply(subst (asm) pos_divide_le_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   754
              apply rule using m0 False by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   755
            show ?thesis apply(subst Real_real'[THEN sym,OF False])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   756
              apply(subst pinfreal_times,subst if_P) defer
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   757
              apply(subst pinfreal_less_eq,subst if_P) defer
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   758
              using * N `B>0` by(auto intro: mult_nonneg_nonneg)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   759
          qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   760
          also have "... \<le> Real (real n) * \<mu> ?s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   761
            apply(rule mult_right_mono) using goal1 by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   762
          also have "... = simple_integral (\<lambda>x. Real (real n) * indicator ?s x)" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   763
            apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   764
            unfolding simple_integral_indicator_only[OF s] ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   765
          also have "... \<le> simple_integral (\<lambda>x. if u x = \<omega> then Real (real n) else u x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   766
            apply(rule simple_integral_mono) apply(rule simple_function_mult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   767
            apply(rule simple_function_const)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   768
            apply(rule simple_function_indicator) apply(rule s su)+ by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   769
          finally show ?case .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   770
        qed qed qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   771
    fix x assume x:"\<omega> = (if u x = \<omega> then Real (real n) else u x)" "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   772
    hence "u x = \<omega>" apply-apply(rule ccontr) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   773
    hence "\<omega> = Real (real n)" using x by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   774
    thus False by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   775
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   776
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   777
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   778
lemma (in measure_space) positive_integral_cong:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   779
  assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   780
  shows "positive_integral f = positive_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   781
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   782
  have "\<And>h. (\<forall>x\<in>space M. h x \<le> f x \<and> h x \<noteq> \<omega>) = (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   783
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   784
  thus ?thesis unfolding positive_integral_alt1 by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   785
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   786
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   787
lemma (in measure_space) positive_integral_eq_simple_integral:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   788
  assumes "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   789
  shows "positive_integral f = simple_integral f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   790
  unfolding positive_integral_alt
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   791
proof (safe intro!: pinfreal_SUPI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   792
  fix g assume "simple_function g" "g \<le> f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   793
  with assms show "simple_integral g \<le> simple_integral f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   794
    by (auto intro!: simple_integral_mono simp: le_fun_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   795
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   796
  fix y assume "\<forall>x. x\<in>{g. simple_function g \<and> g \<le> f} \<longrightarrow> simple_integral x \<le> y"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   797
  with assms show "simple_integral f \<le> y" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   798
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   799
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   800
lemma (in measure_space) positive_integral_mono:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   801
  assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   802
  shows "positive_integral u \<le> positive_integral v"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   803
  unfolding positive_integral_alt1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   804
proof (safe intro!: SUPR_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   805
  fix a assume a: "simple_function a" and "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   806
  with mono have "\<forall>x\<in>space M. a x \<le> v x \<and> a x \<noteq> \<omega>" by fastsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   807
  with a show "\<exists>b\<in>{g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> v x \<and> g x \<noteq> \<omega>)}. simple_integral a \<le> simple_integral b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   808
    by (auto intro!: bexI[of _ a])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   809
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   810
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   811
lemma (in measure_space) positive_integral_SUP_approx:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   812
  assumes "f \<up> s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   813
  and f: "\<And>i. f i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   814
  and "simple_function u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   815
  and le: "u \<le> s" and real: "\<omega> \<notin> u`space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   816
  shows "simple_integral u \<le> (SUP i. positive_integral (f i))" (is "_ \<le> ?S")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   817
proof (rule pinfreal_le_mult_one_interval)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   818
  fix a :: pinfreal assume "0 < a" "a < 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   819
  hence "a \<noteq> 0" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   820
  let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   821
  have B: "\<And>i. ?B i \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   822
    using f `simple_function u` by (auto simp: borel_measurable_simple_function)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   823
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   824
  let "?uB i x" = "u x * indicator (?B i) x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   825
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   826
  { fix i have "?B i \<subseteq> ?B (Suc i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   827
    proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   828
      fix i x assume "a * u x \<le> f i x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   829
      also have "\<dots> \<le> f (Suc i) x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   830
        using `f \<up> s` unfolding isoton_def le_fun_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   831
      finally show "a * u x \<le> f (Suc i) x" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   832
    qed }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   833
  note B_mono = this
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   834
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   835
  have u: "\<And>x. x \<in> space M \<Longrightarrow> u -` {u x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   836
    using `simple_function u` by (auto simp add: simple_function_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   837
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   838
  { fix i
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   839
    have "(\<lambda>n. (u -` {i} \<inter> space M) \<inter> ?B n) \<up> (u -` {i} \<inter> space M)" using B_mono unfolding isoton_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   840
    proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   841
      fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   842
      show "x \<in> (\<Union>i. (u -` {u x} \<inter> space M) \<inter> ?B i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   843
      proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   844
        assume "u x = 0" thus ?thesis using `x \<in> space M` by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   845
      next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   846
        assume "u x \<noteq> 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   847
        with `a < 1` real `x \<in> space M`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   848
        have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   849
        also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   850
          unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   851
        finally obtain i where "a * u x < f i x" unfolding SUPR_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   852
          by (auto simp add: less_Sup_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   853
        hence "a * u x \<le> f i x" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   854
        thus ?thesis using `x \<in> space M` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   855
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   856
    qed auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   857
  note measure_conv = measure_up[OF u Int[OF u B] this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   858
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   859
  have "simple_integral u = (SUP i. simple_integral (?uB i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   860
    unfolding simple_integral_indicator[OF B `simple_function u`]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   861
  proof (subst SUPR_pinfreal_setsum, safe)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   862
    fix x n assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   863
    have "\<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x})
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   864
      \<le> \<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f (Suc n) x})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   865
      using B_mono Int[OF u[OF `x \<in> space M`] B] by (auto intro!: measure_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   866
    thus "u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B n)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   867
            \<le> u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B (Suc n))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   868
      by (auto intro: mult_left_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   869
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   870
    show "simple_integral u =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   871
      (\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (u -` {i} \<inter> space M \<inter> ?B n))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   872
      using measure_conv unfolding simple_integral_def isoton_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   873
      by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   874
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   875
  moreover
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   876
  have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   877
    unfolding pinfreal_SUP_cmult[symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   878
  proof (safe intro!: SUP_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   879
    fix i
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   880
    have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   881
      using B `simple_function u`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   882
      by (subst simple_integral_mult[symmetric]) (auto simp: field_simps)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   883
    also have "\<dots> \<le> positive_integral (f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   884
    proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   885
      have "\<And>x. a * ?uB i x \<le> f i x" unfolding indicator_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   886
      hence *: "simple_function (\<lambda>x. a * ?uB i x)" using B assms(3)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   887
        by (auto intro!: simple_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   888
      show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   889
        by (auto intro!: positive_integral_mono simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   890
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   891
    finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   892
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   893
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   894
  ultimately show "a * simple_integral u \<le> ?S" by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   895
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   896
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   897
text {* Beppo-Levi monotone convergence theorem *}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   898
lemma (in measure_space) positive_integral_isoton:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   899
  assumes "f \<up> u" "\<And>i. f i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   900
  shows "(\<lambda>i. positive_integral (f i)) \<up> positive_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   901
  unfolding isoton_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   902
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   903
  fix i show "positive_integral (f i) \<le> positive_integral (f (Suc i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   904
    apply (rule positive_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   905
    using `f \<up> u` unfolding isoton_def le_fun_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   906
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   907
  have "u \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   908
    using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   909
  have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   910
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   911
  show "(SUP i. positive_integral (f i)) = positive_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   912
  proof (rule antisym)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   913
    from `f \<up> u`[THEN isoton_Sup, unfolded le_fun_def]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   914
    show "(SUP j. positive_integral (f j)) \<le> positive_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   915
      by (auto intro!: SUP_leI positive_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   916
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   917
    show "positive_integral u \<le> (SUP i. positive_integral (f i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   918
      unfolding positive_integral_def[of u]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   919
      by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms])
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   920
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   921
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   922
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   923
lemma (in measure_space) SUP_simple_integral_sequences:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   924
  assumes f: "f \<up> u" "\<And>i. simple_function (f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   925
  and g: "g \<up> u" "\<And>i. simple_function (g i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   926
  shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   927
    (is "SUPR _ ?F = SUPR _ ?G")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   928
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   929
  have "(SUP i. ?F i) = (SUP i. positive_integral (f i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   930
    using assms by (simp add: positive_integral_eq_simple_integral)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   931
  also have "\<dots> = positive_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   932
    using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   933
    unfolding isoton_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   934
  also have "\<dots> = (SUP i. positive_integral (g i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   935
    using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   936
    unfolding isoton_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   937
  also have "\<dots> = (SUP i. ?G i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   938
    using assms by (simp add: positive_integral_eq_simple_integral)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   939
  finally show ?thesis .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   940
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   941
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   942
lemma (in measure_space) positive_integral_const[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   943
  "positive_integral (\<lambda>x. c) = c * \<mu> (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   944
  by (subst positive_integral_eq_simple_integral) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   945
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   946
lemma (in measure_space) positive_integral_isoton_simple:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   947
  assumes "f \<up> u" and e: "\<And>i. simple_function (f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   948
  shows "(\<lambda>i. simple_integral (f i)) \<up> positive_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   949
  using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   950
  unfolding positive_integral_eq_simple_integral[OF e] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   951
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   952
lemma (in measure_space) positive_integral_linear:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   953
  assumes f: "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   954
  and g: "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   955
  shows "positive_integral (\<lambda>x. a * f x + g x) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   956
      a * positive_integral f + positive_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   957
    (is "positive_integral ?L = _")
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   958
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   959
  from borel_measurable_implies_simple_function_sequence'[OF f] guess u .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   960
  note u = this positive_integral_isoton_simple[OF this(1-2)]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   961
  from borel_measurable_implies_simple_function_sequence'[OF g] guess v .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   962
  note v = this positive_integral_isoton_simple[OF this(1-2)]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   963
  let "?L' i x" = "a * u i x + v i x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   964
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   965
  have "?L \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   966
    using assms by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   967
  from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   968
  note positive_integral_isoton_simple[OF this(1-2)] and l = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   969
  moreover have
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   970
      "(SUP i. simple_integral (l i)) = (SUP i. simple_integral (?L' i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   971
  proof (rule SUP_simple_integral_sequences[OF l(1-2)])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   972
    show "?L' \<up> ?L" "\<And>i. simple_function (?L' i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   973
      using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   974
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   975
  moreover from u v have L'_isoton:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   976
      "(\<lambda>i. simple_integral (?L' i)) \<up> a * positive_integral f + positive_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   977
    by (simp add: isoton_add isoton_cmult_right)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   978
  ultimately show ?thesis by (simp add: isoton_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   979
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   980
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   981
lemma (in measure_space) positive_integral_cmult:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   982
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   983
  shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   984
  using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   985
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   986
lemma (in measure_space) positive_integral_indicator[simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   987
  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   988
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   989
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   990
lemma (in measure_space) positive_integral_cmult_indicator:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   991
  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. c * indicator A x) = c * \<mu> A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   992
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   993
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   994
lemma (in measure_space) positive_integral_add:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   995
  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   996
  shows "positive_integral (\<lambda>x. f x + g x) = positive_integral f + positive_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   997
  using positive_integral_linear[OF assms, of 1] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   998
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   999
lemma (in measure_space) positive_integral_setsum:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1000
  assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1001
  shows "positive_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1002
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1003
  assume "finite P"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1004
  from this assms show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1005
  proof induct
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1006
    case (insert i P)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1007
    have "f i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1008
      "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1009
      using insert by (auto intro!: borel_measurable_pinfreal_setsum)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1010
    from positive_integral_add[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1011
    show ?case using insert by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1012
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1013
qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1014
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1015
lemma (in measure_space) positive_integral_diff:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1016
  assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1017
  and fin: "positive_integral g \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1018
  and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1019
  shows "positive_integral (\<lambda>x. f x - g x) = positive_integral f - positive_integral g"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1020
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1021
  have borel: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1022
    using f g by (rule borel_measurable_pinfreal_diff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1023
  have "positive_integral (\<lambda>x. f x - g x) + positive_integral g =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1024
    positive_integral f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1025
    unfolding positive_integral_add[OF borel g, symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1026
  proof (rule positive_integral_cong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1027
    fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1028
    from mono[OF this] show "f x - g x + g x = f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1029
      by (cases "f x", cases "g x", simp, simp, cases "g x", auto)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1030
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1031
  with mono show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1032
    by (subst minus_pinfreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1033
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1034
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1035
lemma (in measure_space) positive_integral_psuminf:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1036
  assumes "\<And>i. f i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1037
  shows "positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1038
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1039
  have "(\<lambda>i. positive_integral (\<lambda>x. \<Sum>i<i. f i x)) \<up> positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity>i. f i x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1040
    by (rule positive_integral_isoton)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1041
       (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1042
                     arg_cong[where f=Sup]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1043
             simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1044
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1045
    by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1046
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1047
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1048
text {* Fatou's lemma: convergence theorem on limes inferior *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1049
lemma (in measure_space) positive_integral_lim_INF:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1050
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1051
  assumes "\<And>i. u i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1052
  shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1053
    (SUP n. INF m. positive_integral (u (m + n)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1054
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1055
  have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1056
    by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1057
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1058
  have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1059
  proof (unfold isoton_def, safe)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1060
    fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1061
      by (rule INF_mono[where N=Suc]) simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1062
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1063
  from positive_integral_isoton[OF this] assms
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1064
  have "positive_integral (SUP n. INF m. u (m + n)) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1065
    (SUP n. positive_integral (INF m. u (m + n)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1066
    unfolding isoton_def by (simp add: borel_measurable_INF)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1067
  also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1068
    by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1069
  finally show ?thesis .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1070
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1071
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1072
lemma (in measure_space) measure_space_density:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1073
  assumes borel: "u \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1074
  shows "measure_space M (\<lambda>A. positive_integral (\<lambda>x. u x * indicator A x))" (is "measure_space M ?v")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1075
proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1076
  show "?v {} = 0" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1077
  show "countably_additive M ?v"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1078
    unfolding countably_additive_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1079
  proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1080
    fix A :: "nat \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1081
    assume "range A \<subseteq> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1082
    hence "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1083
      using borel by (auto intro: borel_measurable_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1084
    moreover assume "disjoint_family A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1085
    note psuminf_indicator[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1086
    ultimately show "(\<Sum>\<^isub>\<infinity>n. ?v (A n)) = ?v (\<Union>x. A x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1087
      by (simp add: positive_integral_psuminf[symmetric])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1088
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1089
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1090
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1091
lemma (in measure_space) positive_integral_null_set:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1092
  assumes borel: "u \<in> borel_measurable M" and "N \<in> null_sets"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1093
  shows "positive_integral (\<lambda>x. u x * indicator N x) = 0" (is "?I = 0")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1094
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1095
  have "N \<in> sets M" using `N \<in> null_sets` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1096
  have "(\<lambda>i x. min (of_nat i) (u x) * indicator N x) \<up> (\<lambda>x. u x * indicator N x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1097
    unfolding isoton_fun_expand
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1098
  proof (safe intro!: isoton_cmult_left, unfold isoton_def, safe)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1099
    fix j i show "min (of_nat j) (u i) \<le> min (of_nat (Suc j)) (u i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1100
      by (rule min_max.inf_mono) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1101
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1102
    fix i show "(SUP j. min (of_nat j) (u i)) = u i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1103
    proof (cases "u i")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1104
      case infinite
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1105
      moreover hence "\<And>j. min (of_nat j) (u i) = of_nat j"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1106
        by (auto simp: min_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1107
      ultimately show ?thesis by (simp add: Sup_\<omega>)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1108
    next
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1109
      case (preal r)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1110
      obtain j where "r \<le> of_nat j" using ex_le_of_nat ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1111
      hence "u i \<le> of_nat j" using preal by (auto simp: real_of_nat_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1112
      show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1113
      proof (rule pinfreal_SUPI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1114
        fix y assume "\<And>j. j \<in> UNIV \<Longrightarrow> min (of_nat j) (u i) \<le> y"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1115
        note this[of j]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1116
        moreover have "min (of_nat j) (u i) = u i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1117
          using `u i \<le> of_nat j` by (auto simp: min_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1118
        ultimately show "u i \<le> y" by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1119
      qed simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1120
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1121
  qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1122
  from positive_integral_isoton[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1123
  have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1124
    unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1125
  also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1126
  proof (rule SUP_mono, rule positive_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1127
    fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1128
      by (cases "x \<in> N") auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1129
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1130
  also have "\<dots> = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1131
    using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1132
  finally show ?thesis by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1133
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1134
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1135
lemma (in measure_space) positive_integral_Markov_inequality:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1136
  assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1137
  shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * positive_integral (\<lambda>x. u x * indicator A x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1138
    (is "\<mu> ?A \<le> _ * ?PI")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1139
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1140
  have "?A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1141
    using `A \<in> sets M` borel by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1142
  hence "\<mu> ?A = positive_integral (\<lambda>x. indicator ?A x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1143
    using positive_integral_indicator by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1144
  also have "\<dots> \<le> positive_integral (\<lambda>x. c * (u x * indicator A x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1145
  proof (rule positive_integral_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1146
    fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1147
    show "indicator ?A x \<le> c * (u x * indicator A x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1148
      by (cases "x \<in> ?A") auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1149
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1150
  also have "\<dots> = c * positive_integral (\<lambda>x. u x * indicator A x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1151
    using assms
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1152
    by (auto intro!: positive_integral_cmult borel_measurable_indicator)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1153
  finally show ?thesis .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1154
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1155
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1156
lemma (in measure_space) positive_integral_0_iff:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1157
  assumes borel: "u \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1158
  shows "positive_integral u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1159
    (is "_ \<longleftrightarrow> \<mu> ?A = 0")
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1160
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1161
  have A: "?A \<in> sets M" using borel by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1162
  have u: "positive_integral (\<lambda>x. u x * indicator ?A x) = positive_integral u"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1163
    by (auto intro!: positive_integral_cong simp: indicator_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1164
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1165
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1166
  proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1167
    assume "\<mu> ?A = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1168
    hence "?A \<in> null_sets" using `?A \<in> sets M` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1169
    from positive_integral_null_set[OF borel this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1170
    have "0 = positive_integral (\<lambda>x. u x * indicator ?A x)" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1171
    thus "positive_integral u = 0" unfolding u by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1172
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1173
    assume *: "positive_integral u = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1174
    let "?M n" = "{x \<in> space M. 1 \<le> of_nat n * u x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1175
    have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1176
    proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1177
      { fix n
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1178
        from positive_integral_Markov_inequality[OF borel `?A \<in> sets M`, of "of_nat n"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1179
        have "\<mu> (?M n \<inter> ?A) = 0" unfolding * u by simp }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1180
      thus ?thesis by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1181
    qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1182
    also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1183
    proof (safe intro!: continuity_from_below)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1184
      fix n show "?M n \<inter> ?A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1185
        using borel by (auto intro!: Int)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1186
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1187
      fix n x assume "1 \<le> of_nat n * u x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1188
      also have "\<dots> \<le> of_nat (Suc n) * u x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1189
        by (subst (1 2) mult_commute) (auto intro!: pinfreal_mult_cancel)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1190
      finally show "1 \<le> of_nat (Suc n) * u x" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1191
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1192
    also have "\<dots> = \<mu> ?A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1193
    proof (safe intro!: arg_cong[where f="\<mu>"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1194
      fix x assume "u x \<noteq> 0" and [simp, intro]: "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1195
      show "x \<in> (\<Union>n. ?M n \<inter> ?A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1196
      proof (cases "u x")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1197
        case (preal r)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1198
        obtain j where "1 / r \<le> of_nat j" using ex_le_of_nat ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1199
        hence "1 / r * r \<le> of_nat j * r" using preal unfolding mult_le_cancel_right by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1200
        hence "1 \<le> of_nat j * r" using preal `u x \<noteq> 0` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1201
        thus ?thesis using `u x \<noteq> 0` preal by (auto simp: real_of_nat_def[symmetric])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1202
      qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1203
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1204
    finally show "\<mu> ?A = 0" by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1205
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1206
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1207
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1208
lemma (in measure_space) positive_integral_cong_on_null_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1209
  assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1210
  and measure: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1211
  shows "positive_integral f = positive_integral g"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1212
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1213
  let ?N = "{x\<in>space M. f x \<noteq> g x}" and ?E = "{x\<in>space M. f x = g x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1214
  let "?A h x" = "h x * indicator ?E x :: pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1215
  let "?B h x" = "h x * indicator ?N x :: pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1216
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1217
  have A: "positive_integral (?A f) = positive_integral (?A g)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1218
    by (auto intro!: positive_integral_cong simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1219
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1220
  have [intro]: "?N \<in> sets M" "?E \<in> sets M" using f g by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1221
  hence "?N \<in> null_sets" using measure by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1222
  hence B: "positive_integral (?B f) = positive_integral (?B g)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1223
    using f g by (simp add: positive_integral_null_set)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1224
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1225
  have "positive_integral f = positive_integral (\<lambda>x. ?A f x + ?B f x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1226
    by (auto intro!: positive_integral_cong simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1227
  also have "\<dots> = positive_integral (?A f) + positive_integral (?B f)"
d5d342611edb Rewrite the Probability