src/HOL/Probability/Lebesgue_Integration.thy
author nipkow
Fri, 11 Apr 2014 13:36:57 +0200
changeset 56536 aefb4a8da31f
parent 56218 1c3f1f2431f9
child 56537 01caba82e1d2
permissions -rw-r--r--
made mult_nonneg_nonneg a simp rule
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42067
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     1
(*  Title:      HOL/Probability/Lebesgue_Integration.thy
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     2
    Author:     Johannes Hölzl, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     3
    Author:     Armin Heller, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     4
*)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
     5
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     6
header {*Lebesgue Integration*}
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     7
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
     8
theory Lebesgue_Integration
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
     9
  imports Measure_Space Borel_Space
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    10
begin
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    11
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    12
lemma tendsto_real_max:
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    13
  fixes x y :: real
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    14
  assumes "(X ---> x) net"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    15
  assumes "(Y ---> y) net"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    16
  shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    17
proof -
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    18
  have *: "\<And>x y :: real. max x y = y + ((x - y) + norm (x - y)) / 2"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    19
    by (auto split: split_max simp: field_simps)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    20
  show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    21
    unfolding *
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    22
    by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    23
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    24
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    25
lemma measurable_sets2[intro]:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    26
  assumes "f \<in> measurable M M'" "g \<in> measurable M M''"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    27
  and "A \<in> sets M'" "B \<in> sets M''"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    28
  shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    29
proof -
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    30
  have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    31
    by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    32
  then show ?thesis using assms by (auto intro: measurable_sets)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    33
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    34
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    35
section "Simple function"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    36
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    37
text {*
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    38
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    39
Our simple functions are not restricted to positive real numbers. Instead
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    40
they are just functions with a finite range and are measurable when singleton
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    41
sets are measurable.
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    42
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    43
*}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    44
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
    45
definition "simple_function M g \<longleftrightarrow>
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    46
    finite (g ` space M) \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    47
    (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    48
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    49
lemma simple_functionD:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
    50
  assumes "simple_function M g"
40875
9a9d33f6fb46 generalized simple_functionD
hoelzl
parents: 40873
diff changeset
    51
  shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M"
40871
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
    52
proof -
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
    53
  show "finite (g ` space M)"
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
    54
    using assms unfolding simple_function_def by auto
40875
9a9d33f6fb46 generalized simple_functionD
hoelzl
parents: 40873
diff changeset
    55
  have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
9a9d33f6fb46 generalized simple_functionD
hoelzl
parents: 40873
diff changeset
    56
  also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
9a9d33f6fb46 generalized simple_functionD
hoelzl
parents: 40873
diff changeset
    57
  finally show "g -` X \<inter> space M \<in> sets M" using assms
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    58
    by (auto simp del: UN_simps simp: simple_function_def)
40871
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
    59
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    60
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    61
lemma simple_function_measurable2[intro]:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    62
  assumes "simple_function M f" "simple_function M g"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    63
  shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    64
proof -
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    65
  have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    66
    by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    67
  then show ?thesis using assms[THEN simple_functionD(2)] by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    68
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    69
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    70
lemma simple_function_indicator_representation:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
    71
  fixes f ::"'a \<Rightarrow> ereal"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
    72
  assumes f: "simple_function M f" and x: "x \<in> space M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    73
  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
    74
  (is "?l = ?r")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    75
proof -
38705
aaee86c0e237 moved generic lemmas in Probability to HOL
hoelzl
parents: 38656
diff changeset
    76
  have "?r = (\<Sum>y \<in> f ` space M.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    77
    (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
    78
    by (auto intro!: setsum_cong2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    79
  also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    80
    using assms by (auto dest: simple_functionD simp: setsum_delta)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    81
  also have "... = f x" using x by (auto simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    82
  finally show ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    83
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    84
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    85
lemma simple_function_notspace:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
    86
  "simple_function M (\<lambda>x. h x * indicator (- space M) x::ereal)" (is "simple_function M ?h")
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    87
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    88
  have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    89
  hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    90
  have "?h -` {0} \<inter> space M = space M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    91
  thus ?thesis unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    92
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    93
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    94
lemma simple_function_cong:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    95
  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
    96
  shows "simple_function M f \<longleftrightarrow> simple_function M g"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    97
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    98
  have "f ` space M = g ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
    99
    "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   100
    using assms by (auto intro!: image_eqI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   101
  thus ?thesis unfolding simple_function_def using assms by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   102
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   103
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   104
lemma simple_function_cong_algebra:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   105
  assumes "sets N = sets M" "space N = space M"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   106
  shows "simple_function M f \<longleftrightarrow> simple_function N f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   107
  unfolding simple_function_def assms ..
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   108
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   109
lemma borel_measurable_simple_function[measurable_dest]:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   110
  assumes "simple_function M f"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   111
  shows "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   112
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   113
  fix S
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   114
  let ?I = "f ` (f -` S \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   115
  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
   116
  have "finite ?I"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   117
    using assms unfolding simple_function_def
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   118
    using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   119
  hence "?U \<in> sets M"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   120
    apply (rule sets.finite_UN)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   121
    using assms unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   122
  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
   123
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   124
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   125
lemma simple_function_borel_measurable:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   126
  fixes f :: "'a \<Rightarrow> 'x::{t2_space}"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   127
  assumes "f \<in> borel_measurable M" and "finite (f ` space M)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   128
  shows "simple_function M f"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   129
  using assms unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   130
  by (auto intro: borel_measurable_vimage)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   131
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   132
lemma simple_function_eq_borel_measurable:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   133
  fixes f :: "'a \<Rightarrow> ereal"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   134
  shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   135
  using simple_function_borel_measurable[of f] borel_measurable_simple_function[of M f]
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44666
diff changeset
   136
  by (fastforce simp: simple_function_def)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   137
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   138
lemma simple_function_const[intro, simp]:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   139
  "simple_function M (\<lambda>x. c)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   140
  by (auto intro: finite_subset simp: simple_function_def)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   141
lemma simple_function_compose[intro, simp]:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   142
  assumes "simple_function M f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   143
  shows "simple_function M (g \<circ> f)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   144
  unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   145
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   146
  show "finite ((g \<circ> f) ` space M)"
56154
f0a927235162 more complete set of lemmas wrt. image and composition
haftmann
parents: 54611
diff changeset
   147
    using assms unfolding simple_function_def by (auto simp: image_comp [symmetric])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   148
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   149
  fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   150
  let ?G = "g -` {g (f x)} \<inter> (f`space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   151
  have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   152
    (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   153
  show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   154
    using assms unfolding simple_function_def *
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   155
    by (rule_tac sets.finite_UN) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   156
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   157
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   158
lemma simple_function_indicator[intro, simp]:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   159
  assumes "A \<in> sets M"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   160
  shows "simple_function M (indicator A)"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   161
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   162
  have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   163
    by (auto simp: indicator_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   164
  hence "finite ?S" by (rule finite_subset) simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   165
  moreover have "- A \<inter> space M = space M - A" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   166
  ultimately show ?thesis unfolding simple_function_def
46905
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
   167
    using assms by (auto simp: indicator_def [abs_def])
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   168
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   169
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   170
lemma simple_function_Pair[intro, simp]:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   171
  assumes "simple_function M f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   172
  assumes "simple_function M g"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   173
  shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p")
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   174
  unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   175
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   176
  show "finite (?p ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   177
    using assms unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   178
    by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   179
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   180
  fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   181
  have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   182
      (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   183
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   184
  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
   185
    using assms unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   186
qed
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   187
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   188
lemma simple_function_compose1:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   189
  assumes "simple_function M f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   190
  shows "simple_function M (\<lambda>x. g (f x))"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   191
  using simple_function_compose[OF assms, of g]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   192
  by (simp add: comp_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   193
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   194
lemma simple_function_compose2:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   195
  assumes "simple_function M f" and "simple_function M g"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   196
  shows "simple_function M (\<lambda>x. h (f x) (g x))"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   197
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   198
  have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   199
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   200
  thus ?thesis by (simp_all add: comp_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   201
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   202
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   203
lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   204
  and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   205
  and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   206
  and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   207
  and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   208
  and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   209
  and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   210
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   211
lemma simple_function_setsum[intro, simp]:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   212
  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   213
  shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   214
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   215
  assume "finite P" from this assms show ?thesis by induct auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   216
qed auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   217
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   218
lemma
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   219
  fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   220
  shows simple_function_ereal[intro, simp]: "simple_function M (\<lambda>x. ereal (f x))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   221
  by (auto intro!: simple_function_compose1[OF sf])
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   222
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   223
lemma
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   224
  fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   225
  shows simple_function_real_of_nat[intro, simp]: "simple_function M (\<lambda>x. real (f x))"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   226
  by (auto intro!: simple_function_compose1[OF sf])
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   227
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   228
lemma borel_measurable_implies_simple_function_sequence:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   229
  fixes u :: "'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   230
  assumes u: "u \<in> borel_measurable M"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   231
  shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   232
             (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   233
proof -
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   234
  def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   235
  { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   236
    proof (split split_if, intro conjI impI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   237
      assume "\<not> real j \<le> u x"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   238
      then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56218
diff changeset
   239
         by (cases "u x") (auto intro!: natfloor_mono)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   240
      moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56218
diff changeset
   241
        by (intro real_natfloor_le) auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   242
      ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   243
        unfolding real_of_nat_le_iff by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   244
    qed auto }
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   245
  note f_upper = this
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   246
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   247
  have real_f:
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   248
    "\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   249
    unfolding f_def by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   250
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   251
  let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   252
  show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   253
  proof (intro exI[of _ ?g] conjI allI ballI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   254
    fix i
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   255
    have "simple_function M (\<lambda>x. real (f x i))"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   256
    proof (intro simple_function_borel_measurable)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   257
      show "(\<lambda>x. real (f x i)) \<in> borel_measurable M"
50021
d96a3f468203 add support for function application to measurability prover
hoelzl
parents: 50003
diff changeset
   258
        using u by (auto simp: real_f)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   259
      have "(\<lambda>x. real (f x i))`space M \<subseteq> real`{..i*2^i}"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   260
        using f_upper[of _ i] by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   261
      then show "finite ((\<lambda>x. real (f x i))`space M)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   262
        by (rule finite_subset) auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   263
    qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   264
    then show "simple_function M (?g i)"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   265
      by (auto intro: simple_function_ereal simple_function_div)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   266
  next
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   267
    show "incseq ?g"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   268
    proof (intro incseq_ereal incseq_SucI le_funI)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   269
      fix x and i :: nat
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   270
      have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   271
      proof ((split split_if)+, intro conjI impI)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   272
        assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   273
        then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   274
          by (cases "u x") (auto intro!: le_natfloor)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   275
      next
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   276
        assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   277
        then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   278
          by (cases "u x") auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   279
      next
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   280
        assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   281
        have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   282
          by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   283
        also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   284
        proof cases
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   285
          assume "0 \<le> u x" then show ?thesis
46671
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45342
diff changeset
   286
            by (intro le_mult_natfloor) 
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   287
        next
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   288
          assume "\<not> 0 \<le> u x" then show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   289
            by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   290
        qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   291
        also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   292
          by (simp add: ac_simps)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   293
        finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" .
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   294
      qed simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   295
      then show "?g i x \<le> ?g (Suc i) x"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   296
        by (auto simp: field_simps)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   297
    qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   298
  next
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   299
    fix x show "(SUP i. ?g i x) = max 0 (u x)"
51000
c9adb50f74ad use order topology for extended reals
hoelzl
parents: 50384
diff changeset
   300
    proof (rule SUP_eqI)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   301
      fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   302
        by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56218
diff changeset
   303
                                     mult_nonpos_nonneg)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   304
    next
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   305
      fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   306
      have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   307
      from order_trans[OF this *] have "0 \<le> y" by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   308
      show "max 0 (u x) \<le> y"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   309
      proof (cases y)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   310
        case (real r)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   311
        with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
44666
8670a39d4420 remove more duplicate lemmas
huffman
parents: 44568
diff changeset
   312
        from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   313
        then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   314
        then guess p .. note ux = this
44666
8670a39d4420 remove more duplicate lemmas
huffman
parents: 44568
diff changeset
   315
        obtain m :: nat where m: "p < real m" using reals_Archimedean2 ..
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   316
        have "p \<le> r"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   317
        proof (rule ccontr)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   318
          assume "\<not> p \<le> r"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   319
          with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"]
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56218
diff changeset
   320
          obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   321
          then have "r * 2^max N m < p * 2^max N m - 1" by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   322
          moreover
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   323
          have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   324
            using *[of "max N m"] m unfolding real_f using ux
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56218
diff changeset
   325
            by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   326
          then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   327
            by (metis real_natfloor_gt_diff_one less_le_trans)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   328
          ultimately show False by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   329
        qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   330
        then show "max 0 (u x) \<le> y" using real ux by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   331
      qed (insert `0 \<le> y`, auto)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   332
    qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   333
  qed (auto simp: divide_nonneg_pos)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   334
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   335
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   336
lemma borel_measurable_implies_simple_function_sequence':
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   337
  fixes u :: "'a \<Rightarrow> ereal"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   338
  assumes u: "u \<in> borel_measurable M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   339
  obtains f where "\<And>i. simple_function M (f i)" "incseq f" "\<And>i. \<infinity> \<notin> range (f i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   340
    "\<And>x. (SUP i. f i x) = max 0 (u x)" "\<And>i x. 0 \<le> f i x"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   341
  using borel_measurable_implies_simple_function_sequence[OF u] by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   342
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   343
lemma simple_function_induct[consumes 1, case_names cong set mult add, induct set: simple_function]:
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   344
  fixes u :: "'a \<Rightarrow> ereal"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   345
  assumes u: "simple_function M u"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   346
  assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   347
  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   348
  assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   349
  assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   350
  shows "P u"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   351
proof (rule cong)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   352
  from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   353
  proof eventually_elim
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   354
    fix x assume x: "x \<in> space M"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   355
    from simple_function_indicator_representation[OF u x]
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   356
    show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" ..
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   357
  qed
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   358
next
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   359
  from u have "finite (u ` space M)"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   360
    unfolding simple_function_def by auto
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   361
  then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   362
  proof induct
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   363
    case empty show ?case
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   364
      using set[of "{}"] by (simp add: indicator_def[abs_def])
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   365
  qed (auto intro!: add mult set simple_functionD u)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   366
next
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   367
  show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   368
    apply (subst simple_function_cong)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   369
    apply (rule simple_function_indicator_representation[symmetric])
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   370
    apply (auto intro: u)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   371
    done
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   372
qed fact
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   373
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   374
lemma simple_function_induct_nn[consumes 2, case_names cong set mult add]:
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   375
  fixes u :: "'a \<Rightarrow> ereal"
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   376
  assumes u: "simple_function M u" and nn: "\<And>x. 0 \<le> u x"
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   377
  assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   378
  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
49797
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   379
  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   380
  assumes add: "\<And>u v. simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> simple_function M v \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   381
  shows "P u"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   382
proof -
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   383
  show ?thesis
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   384
  proof (rule cong)
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   385
    fix x assume x: "x \<in> space M"
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   386
    from simple_function_indicator_representation[OF u x]
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   387
    show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" ..
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   388
  next
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   389
    show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   390
      apply (subst simple_function_cong)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   391
      apply (rule simple_function_indicator_representation[symmetric])
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   392
      apply (auto intro: u)
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   393
      done
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   394
  next
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   395
    from u nn have "finite (u ` space M)" "\<And>x. x \<in> u ` space M \<Longrightarrow> 0 \<le> x"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   396
      unfolding simple_function_def by auto
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   397
    then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   398
    proof induct
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   399
      case empty show ?case
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   400
        using set[of "{}"] by (simp add: indicator_def[abs_def])
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   401
    qed (auto intro!: add mult set simple_functionD u setsum_nonneg
49797
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   402
       simple_function_setsum)
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   403
  qed fact
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   404
qed
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   405
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   406
lemma borel_measurable_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   407
  fixes u :: "'a \<Rightarrow> ereal"
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   408
  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   409
  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   410
  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
49797
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   411
  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   412
  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   413
  assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow>  (\<And>i x. 0 \<le> U i x) \<Longrightarrow>  (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P (SUP i. U i)"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   414
  shows "P u"
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   415
  using u
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   416
proof (induct rule: borel_measurable_implies_simple_function_sequence')
49797
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   417
  fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   418
    sup: "\<And>x. (SUP i. U i x) = max 0 (u x)" and nn: "\<And>i x. 0 \<le> U i x"
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   419
  have u_eq: "u = (SUP i. U i)"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   420
    using nn u sup by (auto simp: max_def)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   421
  
49797
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   422
  from U have "\<And>i. U i \<in> borel_measurable M"
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   423
    by (simp add: borel_measurable_simple_function)
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   424
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   425
  show "P u"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   426
    unfolding u_eq
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   427
  proof (rule seq)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   428
    fix i show "P (U i)"
49799
15ea98537c76 strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents: 49798
diff changeset
   429
      using `simple_function M (U i)` nn
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   430
      by (induct rule: simple_function_induct_nn)
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   431
         (auto intro: set mult add cong dest!: borel_measurable_simple_function)
49797
28066863284c add induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49796
diff changeset
   432
  qed fact+
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   433
qed
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   434
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   435
lemma simple_function_If_set:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   436
  assumes sf: "simple_function M f" "simple_function M g" and A: "A \<inter> space M \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   437
  shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF")
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   438
proof -
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   439
  def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   440
  show ?thesis unfolding simple_function_def
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   441
  proof safe
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   442
    have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   443
    from finite_subset[OF this] assms
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   444
    show "finite (?IF ` space M)" unfolding simple_function_def by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   445
  next
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   446
    fix x assume "x \<in> space M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   447
    then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   448
      then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   449
      else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   450
      using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   451
    have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   452
      unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   453
    show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   454
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   455
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   456
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   457
lemma simple_function_If:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   458
  assumes sf: "simple_function M f" "simple_function M g" and P: "{x\<in>space M. P x} \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   459
  shows "simple_function M (\<lambda>x. if P x then f x else g x)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   460
proof -
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   461
  have "{x\<in>space M. P x} = {x. P x} \<inter> space M" by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   462
  with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   463
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   464
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   465
lemma simple_function_subalgebra:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   466
  assumes "simple_function N f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   467
  and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   468
  shows "simple_function M f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   469
  using assms unfolding simple_function_def by auto
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 38705
diff changeset
   470
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   471
lemma simple_function_comp:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   472
  assumes T: "T \<in> measurable M M'"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   473
    and f: "simple_function M' f"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   474
  shows "simple_function M (\<lambda>x. f (T x))"
41661
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   475
proof (intro simple_function_def[THEN iffD2] conjI ballI)
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   476
  have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   477
    using T unfolding measurable_def by auto
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   478
  then show "finite ((\<lambda>x. f (T x)) ` space M)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   479
    using f unfolding simple_function_def by (auto intro: finite_subset)
41661
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   480
  fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   481
  then have "i \<in> f ` space M'"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   482
    using T unfolding measurable_def by auto
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   483
  then have "f -` {i} \<inter> space M' \<in> sets M'"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   484
    using f unfolding simple_function_def by auto
41661
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   485
  then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   486
    using T unfolding measurable_def by auto
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   487
  also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   488
    using T unfolding measurable_def by auto
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41545
diff changeset
   489
  finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   490
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   491
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   492
section "Simple integral"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   493
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   494
definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>S") where
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   495
  "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   496
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   497
syntax
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   498
  "_simple_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110)
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   499
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   500
translations
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   501
  "\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   502
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   503
lemma simple_integral_cong:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   504
  assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   505
  shows "integral\<^sup>S M f = integral\<^sup>S M g"
38656
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
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   513
lemma simple_integral_const[simp]:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   514
  "(\<integral>\<^sup>Sx. c \<partial>M) = c * (emeasure M) (space M)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   515
proof (cases "space M = {}")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   516
  case True thus ?thesis unfolding simple_integral_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   517
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   518
  case False hence "(\<lambda>x. c) ` space M = {c}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   519
  thus ?thesis unfolding simple_integral_def by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   520
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   521
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   522
lemma simple_function_partition:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   523
  assumes f: "simple_function M f" and g: "simple_function M g"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   524
  shows "integral\<^sup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * (emeasure M) A)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   525
    (is "_ = setsum _ (?p ` space M)")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   526
proof-
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   527
  let ?sub = "\<lambda>x. ?p ` (f -` {x} \<inter> space M)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   528
  let ?SIGMA = "Sigma (f`space M) ?sub"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   529
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   530
  have [intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   531
    "finite (f ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   532
    "finite (g ` space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   533
    using assms unfolding simple_function_def by simp_all
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   534
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   535
  { fix A
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   536
    have "?p ` (A \<inter> space M) \<subseteq>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   537
      (\<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
   538
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   539
    hence "finite (?p ` (A \<inter> space M))"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 39910
diff changeset
   540
      by (rule finite_subset) auto }
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   541
  note this[intro, simp]
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   542
  note sets = simple_function_measurable2[OF f g]
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   543
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   544
  { fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   545
    have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   546
    with sets have "(emeasure M) (f -` {f x} \<inter> space M) = setsum (emeasure M) (?sub (f x))"
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   547
      by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) }
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   548
  hence "integral\<^sup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * (emeasure M) A)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   549
    unfolding simple_integral_def using f sets
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   550
    by (subst setsum_Sigma[symmetric])
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   551
       (auto intro!: setsum_cong setsum_ereal_right_distrib)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   552
  also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * (emeasure M) A)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   553
  proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   554
    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
   555
    have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   556
      = (\<lambda>x. (f x, ?p x)) ` space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   557
    proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   558
      fix x assume "x \<in> space M"
39910
10097e0a9dbd constant `contents` renamed to `the_elem`
haftmann
parents: 39302
diff changeset
   559
      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
   560
        by (auto intro!: image_eqI[of _ _ "?p x"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   561
    qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   562
    thus ?thesis
39910
10097e0a9dbd constant `contents` renamed to `the_elem`
haftmann
parents: 39302
diff changeset
   563
      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
   564
      apply (rule_tac x="xa" in image_eqI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   565
      by simp_all
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   566
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   567
  finally show ?thesis .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   568
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   569
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   570
lemma simple_integral_add[simp]:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   571
  assumes f: "simple_function M f" and "\<And>x. 0 \<le> f x" and g: "simple_function M g" and "\<And>x. 0 \<le> g x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   572
  shows "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = integral\<^sup>S M f + integral\<^sup>S M g"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   573
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   574
  { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   575
    assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   576
    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
   577
        "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   578
      by auto }
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   579
  with assms show ?thesis
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   580
    unfolding
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   581
      simple_function_partition[OF simple_function_add[OF f g] simple_function_Pair[OF f g]]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   582
      simple_function_partition[OF f g]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   583
      simple_function_partition[OF g f]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   584
    by (subst (3) Int_commute)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   585
       (auto simp add: ereal_left_distrib setsum_addf[symmetric] intro!: setsum_cong)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   586
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   587
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   588
lemma simple_integral_setsum[simp]:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   589
  assumes "\<And>i x. i \<in> P \<Longrightarrow> 0 \<le> f i x"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   590
  assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   591
  shows "(\<integral>\<^sup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>S M (f i))"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   592
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   593
  assume "finite P"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   594
  from this assms show ?thesis
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   595
    by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   596
qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   597
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   598
lemma simple_integral_mult[simp]:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   599
  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   600
  shows "(\<integral>\<^sup>Sx. c * f x \<partial>M) = c * integral\<^sup>S M f"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   601
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   602
  note mult = simple_function_mult[OF simple_function_const[of _ c] f(1)]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   603
  { 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
   604
    assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   605
    hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   606
      by auto }
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   607
  with assms show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   608
    unfolding simple_function_partition[OF mult f(1)]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   609
              simple_function_partition[OF f(1) mult]
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   610
    by (subst setsum_ereal_right_distrib)
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   611
       (auto intro!: ereal_0_le_mult setsum_cong simp: mult_assoc)
40871
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
   612
qed
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
   613
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   614
lemma simple_integral_mono_AE:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   615
  assumes f: "simple_function M f" and g: "simple_function M g"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   616
  and mono: "AE x in M. f x \<le> g x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   617
  shows "integral\<^sup>S M f \<le> integral\<^sup>S M g"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   618
proof -
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   619
  let ?S = "\<lambda>x. (g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   620
  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
   621
    "\<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
   622
  show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   623
    unfolding *
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   624
      simple_function_partition[OF f g]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   625
      simple_function_partition[OF g f]
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   626
  proof (safe intro!: setsum_mono)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   627
    fix x assume "x \<in> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   628
    then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   629
    show "the_elem (f`?S x) * (emeasure M) (?S x) \<le> the_elem (g`?S x) * (emeasure M) (?S x)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   630
    proof (cases "f x \<le> g x")
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   631
      case True then show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   632
        using * assms(1,2)[THEN simple_functionD(2)]
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   633
        by (auto intro!: ereal_mult_right_mono)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   634
    next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   635
      case False
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   636
      obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "(emeasure M) N = 0"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   637
        using mono by (auto elim!: AE_E)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   638
      have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
40871
688f6ff859e1 Generalized simple_functionD and less_SUP_iff.
hoelzl
parents: 40859
diff changeset
   639
      moreover have "?S x \<in> sets M" using assms
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   640
        by (rule_tac sets.Int) (auto intro!: simple_functionD)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   641
      ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   642
        using `N \<in> sets M` by (auto intro!: emeasure_mono)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   643
      moreover have "0 \<le> (emeasure M) (?S x)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   644
        using assms(1,2)[THEN simple_functionD(2)] by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   645
      ultimately have "(emeasure M) (?S x) = 0" using `(emeasure M) N = 0` by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   646
      then show ?thesis by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   647
    qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   648
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   649
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   650
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   651
lemma simple_integral_mono:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   652
  assumes "simple_function M f" and "simple_function M g"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   653
  and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   654
  shows "integral\<^sup>S M f \<le> integral\<^sup>S M g"
41705
1100512e16d8 add auto support for AE_mp
hoelzl
parents: 41689
diff changeset
   655
  using assms by (intro simple_integral_mono_AE) auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   656
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   657
lemma simple_integral_cong_AE:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   658
  assumes "simple_function M f" and "simple_function M g"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   659
  and "AE x in M. f x = g x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   660
  shows "integral\<^sup>S M f = integral\<^sup>S M g"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   661
  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
   662
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   663
lemma simple_integral_cong':
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   664
  assumes sf: "simple_function M f" "simple_function M g"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   665
  and mea: "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   666
  shows "integral\<^sup>S M f = integral\<^sup>S M g"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   667
proof (intro simple_integral_cong_AE sf AE_I)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   668
  show "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" by fact
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   669
  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
   670
    using sf[THEN borel_measurable_simple_function] by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   671
qed simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   672
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   673
lemma simple_integral_indicator:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   674
  assumes "A \<in> sets M"
49796
182fa22e7ee8 introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents: 49795
diff changeset
   675
  assumes f: "simple_function M f"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   676
  shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   677
    (\<Sum>x \<in> f ` space M. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   678
proof (cases "A = space M")
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   679
  case True
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   680
  then have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   681
    by (auto intro!: simple_integral_cong)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   682
  with True show ?thesis by (simp add: simple_integral_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   683
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   684
  assume "A \<noteq> space M"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   685
  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   686
  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
   687
  proof safe
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   688
    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
   689
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   690
    fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   691
      using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   692
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   693
    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
   694
  qed
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   695
  have *: "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   696
    (\<Sum>x \<in> f ` space M \<union> {0}. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   697
    unfolding simple_integral_def I
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   698
  proof (rule setsum_mono_zero_cong_left)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   699
    show "finite (f ` space M \<union> {0})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   700
      using assms(2) unfolding simple_function_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   701
    show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   702
      using sets.sets_into_space[OF assms(1)] by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   703
    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
   704
      by (auto simp: image_iff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   705
    thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   706
      i * (emeasure M) (f -` {i} \<inter> space M \<inter> A) = 0" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   707
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   708
    fix x assume "x \<in> f`A \<union> {0}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   709
    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
   710
      by (auto simp: indicator_def split: split_if_asm)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   711
    thus "x * (emeasure M) (?I -` {x} \<inter> space M) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   712
      x * (emeasure M) (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   713
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   714
  show ?thesis unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   715
    using assms(2) unfolding simple_function_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   716
    by (auto intro!: setsum_mono_zero_cong_right)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   717
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   718
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   719
lemma simple_integral_indicator_only[simp]:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   720
  assumes "A \<in> sets M"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   721
  shows "integral\<^sup>S M (indicator A) = emeasure M A"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   722
proof cases
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   723
  assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   724
  thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   725
next
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   726
  assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   727
  thus ?thesis
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   728
    using simple_integral_indicator[OF assms simple_function_const[of _ 1]]
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   729
    using sets.sets_into_space[OF assms]
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   730
    by (auto intro!: arg_cong[where f="(emeasure M)"])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   731
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   732
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   733
lemma simple_integral_null_set:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   734
  assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets M"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   735
  shows "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = 0"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   736
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   737
  have "AE x in M. indicator N x = (0 :: ereal)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   738
    using `N \<in> null_sets M` by (auto simp: indicator_def intro!: AE_I[of _ _ N])
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   739
  then have "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^sup>Sx. 0 \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   740
    using assms apply (intro simple_integral_cong_AE) by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   741
  then show ?thesis by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   742
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   743
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   744
lemma simple_integral_cong_AE_mult_indicator:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   745
  assumes sf: "simple_function M f" and eq: "AE x in M. x \<in> S" and "S \<in> sets M"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   746
  shows "integral\<^sup>S M f = (\<integral>\<^sup>Sx. f x * indicator S x \<partial>M)"
41705
1100512e16d8 add auto support for AE_mp
hoelzl
parents: 41689
diff changeset
   747
  using assms by (intro simple_integral_cong_AE) auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   748
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   749
lemma simple_integral_cmult_indicator:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   750
  assumes A: "A \<in> sets M"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   751
  shows "(\<integral>\<^sup>Sx. c * indicator A x \<partial>M) = c * (emeasure M) A"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   752
  using simple_integral_mult[OF simple_function_indicator[OF A]]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   753
  unfolding simple_integral_indicator_only[OF A] by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   754
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   755
lemma simple_integral_positive:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   756
  assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   757
  shows "0 \<le> integral\<^sup>S M f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   758
proof -
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   759
  have "integral\<^sup>S M (\<lambda>x. 0) \<le> integral\<^sup>S M f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   760
    using simple_integral_mono_AE[OF _ f ae] by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   761
  then show ?thesis by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   762
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   763
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   764
section "Continuous positive integration"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   765
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   766
definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   767
  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   768
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   769
syntax
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   770
  "_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   771
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   772
translations
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   773
  "\<integral>\<^sup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)"
40872
7c556a9240de Move SUP_commute, SUP_less_iff to HOL image;
hoelzl
parents: 40871
diff changeset
   774
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   775
lemma positive_integral_positive:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   776
  "0 \<le> integral\<^sup>P M f"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   777
  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
40873
1ef85f4e7097 Shorter definition for positive_integral.
hoelzl
parents: 40872
diff changeset
   778
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   779
lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \<noteq> -\<infinity>"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   780
  using positive_integral_positive[of M f] by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   781
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   782
lemma positive_integral_def_finite:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   783
  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56213
diff changeset
   784
    (is "_ = SUPREMUM ?A ?f")
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   785
  unfolding positive_integral_def
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   786
proof (safe intro!: antisym SUP_least)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   787
  fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   788
  let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   789
  note gM = g(1)[THEN borel_measurable_simple_function]
50252
4aa34bd43228 eliminated slightly odd identifiers;
wenzelm
parents: 50244
diff changeset
   790
  have \<mu>_G_pos: "0 \<le> (emeasure M) ?G" using gM by auto
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   791
  let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   792
  from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   793
    apply (safe intro!: simple_function_max simple_function_If)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   794
    apply (force simp: max_def le_fun_def split: split_if_asm)+
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   795
    done
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56213
diff changeset
   796
  show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   797
  proof cases
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   798
    have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   799
    assume "(emeasure M) ?G = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   800
    with gM have "AE x in M. x \<notin> ?G"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   801
      by (auto simp add: AE_iff_null intro!: null_setsI)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   802
    with gM g show ?thesis
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   803
      by (intro SUP_upper2[OF g0] simple_integral_mono_AE)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   804
         (auto simp: max_def intro!: simple_function_If)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   805
  next
50252
4aa34bd43228 eliminated slightly odd identifiers;
wenzelm
parents: 50244
diff changeset
   806
    assume \<mu>_G: "(emeasure M) ?G \<noteq> 0"
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56213
diff changeset
   807
    have "SUPREMUM ?A (integral\<^sup>S M) = \<infinity>"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   808
    proof (intro SUP_PInfty)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   809
      fix n :: nat
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   810
      let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)"
50252
4aa34bd43228 eliminated slightly odd identifiers;
wenzelm
parents: 50244
diff changeset
   811
      have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>_G \<mu>_G_pos by (auto simp: ereal_divide_eq)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   812
      then have "?g ?y \<in> ?A" by (rule g_in_A)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   813
      have "real n \<le> ?y * (emeasure M) ?G"
50252
4aa34bd43228 eliminated slightly odd identifiers;
wenzelm
parents: 50244
diff changeset
   814
        using \<mu>_G \<mu>_G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   815
      also have "\<dots> = (\<integral>\<^sup>Sx. ?y * indicator ?G x \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   816
        using `0 \<le> ?y` `?g ?y \<in> ?A` gM
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   817
        by (subst simple_integral_cmult_indicator) auto
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   818
      also have "\<dots> \<le> integral\<^sup>S M (?g ?y)" using `?g ?y \<in> ?A` gM
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   819
        by (intro simple_integral_mono) auto
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   820
      finally show "\<exists>i\<in>?A. real n \<le> integral\<^sup>S M i"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   821
        using `?g ?y \<in> ?A` by blast
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   822
    qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   823
    then show ?thesis by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   824
  qed
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   825
qed (auto intro: SUP_upper)
40873
1ef85f4e7097 Shorter definition for positive_integral.
hoelzl
parents: 40872
diff changeset
   826
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   827
lemma positive_integral_mono_AE:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   828
  assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>P M u \<le> integral\<^sup>P M v"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   829
  unfolding positive_integral_def
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   830
proof (safe intro!: SUP_mono)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   831
  fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   832
  from ae[THEN AE_E] guess N . note N = this
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   833
  then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in)
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   834
  let ?n = "\<lambda>x. n x * indicator (space M - N) x"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   835
  have "AE x in M. n x \<le> ?n x" "simple_function M ?n"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   836
    using n N ae_N by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   837
  moreover
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   838
  { fix x have "?n x \<le> max 0 (v x)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   839
    proof cases
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   840
      assume x: "x \<in> space M - N"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   841
      with N have "u x \<le> v x" by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   842
      with n(2)[THEN le_funD, of x] x show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   843
        by (auto simp: max_def split: split_if_asm)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   844
    qed simp }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   845
  then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   846
  moreover have "integral\<^sup>S M n \<le> integral\<^sup>S M ?n"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   847
    using ae_N N n by (auto intro!: simple_integral_mono_AE)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   848
  ultimately show "\<exists>m\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> v}. integral\<^sup>S M n \<le> integral\<^sup>S M m"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   849
    by force
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   850
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   851
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   852
lemma positive_integral_mono:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   853
  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>P M u \<le> integral\<^sup>P M v"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   854
  by (auto intro: positive_integral_mono_AE)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   855
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   856
lemma positive_integral_cong_AE:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   857
  "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   858
  by (auto simp: eq_iff intro!: positive_integral_mono_AE)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   859
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   860
lemma positive_integral_cong:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   861
  "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   862
  by (auto intro: positive_integral_cong_AE)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   863
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   864
lemma positive_integral_eq_simple_integral:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   865
  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   866
proof -
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   867
  let ?f = "\<lambda>x. f x * indicator (space M) x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   868
  have f': "simple_function M ?f" using f by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   869
  with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   870
    by (auto simp: fun_eq_iff max_def split: split_indicator)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   871
  have "integral\<^sup>P M ?f \<le> integral\<^sup>S M ?f" using f'
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   872
    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   873
  moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>P M ?f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   874
    unfolding positive_integral_def
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   875
    using f' by (auto intro!: SUP_upper)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   876
  ultimately show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   877
    by (simp cong: positive_integral_cong simple_integral_cong)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   878
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   879
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   880
lemma positive_integral_eq_simple_integral_AE:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   881
  assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   882
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   883
  have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   884
  with f have "integral\<^sup>P M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   885
    by (simp cong: positive_integral_cong_AE simple_integral_cong_AE
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   886
             add: positive_integral_eq_simple_integral)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   887
  with assms show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   888
    by (auto intro!: simple_integral_cong_AE split: split_max)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   889
qed
40873
1ef85f4e7097 Shorter definition for positive_integral.
hoelzl
parents: 40872
diff changeset
   890
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   891
lemma positive_integral_SUP_approx:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   892
  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   893
  and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   894
  shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>P M (f i))" (is "_ \<le> ?S")
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   895
proof (rule ereal_le_mult_one_interval)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   896
  have "0 \<le> (SUP i. integral\<^sup>P M (f i))"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   897
    using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   898
  then show "(SUP i. integral\<^sup>P M (f i)) \<noteq> -\<infinity>" by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   899
  have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   900
    using u(3) by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   901
  fix a :: ereal assume "0 < a" "a < 1"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   902
  hence "a \<noteq> 0" by auto
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   903
  let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   904
  have B: "\<And>i. ?B i \<in> sets M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   905
    using f `simple_function M u` by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   906
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   907
  let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   908
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   909
  { fix i have "?B i \<subseteq> ?B (Suc i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   910
    proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   911
      fix i x assume "a * u x \<le> f i x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   912
      also have "\<dots> \<le> f (Suc i) x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   913
        using `incseq f`[THEN incseq_SucD] unfolding le_fun_def by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   914
      finally show "a * u x \<le> f (Suc i) x" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   915
    qed }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   916
  note B_mono = this
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   917
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   918
  note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   919
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
   920
  let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   921
  have measure_conv: "\<And>i. (emeasure M) (u -` {i} \<inter> space M) = (SUP n. (emeasure M) (?B' i n))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   922
  proof -
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   923
    fix i
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   924
    have 1: "range (?B' i) \<subseteq> sets M" using B_u by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   925
    have 2: "incseq (?B' i)" using B_mono by (auto intro!: incseq_SucI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   926
    have "(\<Union>n. ?B' i n) = u -` {i} \<inter> space M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   927
    proof safe
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   928
      fix x i assume x: "x \<in> space M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   929
      show "x \<in> (\<Union>i. ?B' (u x) i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   930
      proof cases
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   931
        assume "u x = 0" thus ?thesis using `x \<in> space M` f(3) by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   932
      next
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   933
        assume "u x \<noteq> 0"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   934
        with `a < 1` u_range[OF `x \<in> space M`]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   935
        have "a * u x < 1 * u x"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
   936
          by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
46884
154dc6ec0041 tuned proofs
noschinl
parents: 46731
diff changeset
   937
        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   938
        finally obtain i where "a * u x < f i x" unfolding SUP_def
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   939
          by (auto simp add: less_SUP_iff)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   940
        hence "a * u x \<le> f i x" by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   941
        thus ?thesis using `x \<in> space M` by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   942
      qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
   943
    qed
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   944
    then show "?thesis i" using SUP_emeasure_incseq[OF 1 2] by simp
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   945
  qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   946
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   947
  have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB i))"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   948
    unfolding simple_integral_indicator[OF B `simple_function M u`]
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56193
diff changeset
   949
  proof (subst SUP_ereal_setsum, safe)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   950
    fix x n assume "x \<in> space M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   951
    with u_range show "incseq (\<lambda>i. u x * (emeasure M) (?B' (u x) i))" "\<And>i. 0 \<le> u x * (emeasure M) (?B' (u x) i)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   952
      using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   953
  next
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   954
    show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   955
      using measure_conv u_range B_u unfolding simple_integral_def
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56193
diff changeset
   956
      by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   957
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   958
  moreover
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   959
  have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56193
diff changeset
   960
    apply (subst SUP_ereal_cmult [symmetric])
38705
aaee86c0e237 moved generic lemmas in Probability to HOL
hoelzl
parents: 38656
diff changeset
   961
  proof (safe intro!: SUP_mono bexI)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   962
    fix i
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   963
    have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   964
      using B `simple_function M u` u_range
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   965
      by (subst simple_integral_mult) (auto split: split_indicator)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   966
    also have "\<dots> \<le> integral\<^sup>P M (f i)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   967
    proof -
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   968
      have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   969
      show ?thesis using f(3) * u_range `0 < a`
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   970
        by (subst positive_integral_eq_simple_integral[symmetric])
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   971
           (auto intro!: positive_integral_mono split: split_indicator)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   972
    qed
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   973
    finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>P M (f i)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   974
      by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   975
  next
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   976
    fix i show "0 \<le> \<integral>\<^sup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   977
      by (intro simple_integral_positive) (auto split: split_indicator)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   978
  qed (insert `0 < a`, auto)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   979
  ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   980
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   981
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   982
lemma incseq_positive_integral:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   983
  assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>P M (f i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   984
proof -
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   985
  have "\<And>i x. f i x \<le> f (Suc i) x"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   986
    using assms by (auto dest!: incseq_SucD simp: le_fun_def)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   987
  then show ?thesis
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   988
    by (auto intro!: incseq_SucI positive_integral_mono)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   989
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   990
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   991
text {* Beppo-Levi monotone convergence theorem *}
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   992
lemma positive_integral_monotone_convergence_SUP:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   993
  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   994
  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   995
proof (rule antisym)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   996
  show "(SUP j. integral\<^sup>P M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
   997
    by (auto intro!: SUP_least SUP_upper positive_integral_mono)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   998
next
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
   999
  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>P M (f j))"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1000
    unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
  1001
  proof (safe intro!: SUP_least)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1002
    fix g assume g: "simple_function M g"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
  1003
      and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
  1004
    then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44890
diff changeset
  1005
      using f by (auto intro!: SUP_upper2)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
  1006
    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1007
      by (intro  positive_integral_SUP_approx[OF f g _ g'])
46884
154dc6ec0041 tuned proofs
noschinl
parents: 46731
diff changeset
  1008
         (auto simp: le_fun_def max_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1009
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1010
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1011
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1012
lemma positive_integral_monotone_convergence_SUP_AE:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1013
  assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1014
  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
  1015
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1016
  from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1017
    by (simp add: AE_all_countable)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1018
  from this[THEN AE_E] guess N . note N = this
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
  1019
  let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1020
  have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1021
  then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1022
    by (auto intro!: positive_integral_cong_AE)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1023
  also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1024
  proof (rule positive_integral_monotone_convergence_SUP)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1025
    show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1026
    { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1027
        using f N(3) by (intro measurable_If_set) auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1028
      fix x show "0 \<le> ?f i x"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1029
        using N(1) by auto }
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
  1030
  qed
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1031
  also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56213
diff changeset
  1032
    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1033
  finally show ?thesis .
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1034
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1035
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1036
lemma positive_integral_monotone_convergence_SUP_AE_incseq:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1037
  assumes f: "incseq f" "\<And>i. AE x in M. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1038
  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1039
  using f[unfolded incseq_Suc_iff le_fun_def]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1040
  by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1041
     auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1042
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1043
lemma positive_integral_monotone_convergence_simple:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1044
  assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1045
  shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1046
  using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1047
    f(3)[THEN borel_measurable_simple_function] f(2)]
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56213
diff changeset
  1048
  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1049
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1050
lemma positive_integral_max_0:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1051
  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1052
  by (simp add: le_fun_def positive_integral_def)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1053
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1054
lemma positive_integral_cong_pos:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1055
  assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1056
  shows "integral\<^sup>P M f = integral\<^sup>P M g"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1057
proof -
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1058
  have "integral\<^sup>P M (\<lambda>x. max 0 (f x)) = integral\<^sup>P M (\<lambda>x. max 0 (g x))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1059
  proof (intro positive_integral_cong)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1060
    fix x assume "x \<in> space M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1061
    from assms[OF this] show "max 0 (f x) = max 0 (g x)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1062
      by (auto split: split_max)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1063
  qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1064
  then show ?thesis by (simp add: positive_integral_max_0)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
  1065
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40786
diff changeset
  1066
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1067
lemma SUP_simple_integral_sequences:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1068
  assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1069
  and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1070
  and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1071
  shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))"
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56213
diff changeset
  1072
    (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1073
proof -
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1074
  have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1075
    using f by (rule positive_integral_monotone_convergence_simple)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1076
  also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1077
    unfolding eq[THEN positive_integral_cong_AE] ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1078
  also have "\<dots> = (SUP i. ?G i)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1079
    using g by (rule positive_integral_monotone_convergence_simple[symmetric])
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1080
  finally show ?thesis by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1081
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1082
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1083
lemma positive_integral_const[simp]:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1084
  "0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1085
  by (subst positive_integral_eq_simple_integral) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1086
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1087
lemma positive_integral_linear:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1088
  assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1089
  and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1090
  shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>P M f + integral\<^sup>P M g"
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1091
    (is "integral\<^sup>P M ?L = _")
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1092
proof -
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1093
  from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1094
  note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1095
  from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1096
  note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 46671
diff changeset
  1097
  let ?L' = "\<lambda>i x. a * u i x + v i x"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1098
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1099
  have "?L \<in> borel_measurable M" using assms by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
  1100
  from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1101
  note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1102
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1103
  have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1104
    using u v `0 \<le> a`
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1105
    by (auto simp: incseq_Suc_iff le_fun_def
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
  1106
             intro!: add_mono ereal_mult_left_mono simple_integral_mono)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1107
  have pos: "\<And>i. 0 \<le> integral\<^sup>S M (u i)" "\<And>i. 0 \<le> integral\<^sup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^sup>S M (u i)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1108
    using u v `0 \<le> a` by (auto simp: simple_integral_positive)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1109
  { fix i from pos[of i] have "a * integral\<^sup>S M (u i) \<noteq> -\<infinity>" "integral\<^sup>S M (v i) \<noteq> -\<infinity>"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1110
      by (auto split: split_if_asm) }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1111
  note not_MInf = this
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1112
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51340
diff changeset
  1113
  have l': "(SUP i. integral\<^sup>S M (l i)) = (SUP i. integral\<^sup>S M (?L' i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1114
  proof (rule SUP_simple_integral_sequences[OF l(3,6,2)])
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1115
    show "incseq ?L'" "\<And>i x. 0 \<le> ?L' i x" "\<And>i. simple_function M (?L' i)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1116
      using u v  `0 \<le> a` unfolding incseq_Suc_iff le_fun_def
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43339
diff changeset
  1117
      by (auto intro!: add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1118
    { fix x
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1119
      { fix i have "a * u i x \<noteq> -\<infinity>" "v i x \<noteq> -\<infinity>" "u i x \<noteq> -\<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x]
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1120
          by auto }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1121
      then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
  1122
        using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56193
diff changeset