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