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