src/HOL/Probability/Lebesgue.thy
author hoelzl
Mon, 03 May 2010 14:35:10 +0200
changeset 36624 25153c08655e
parent 35977 30d42bfd0174
child 36725 34c36a5cb808
permissions -rw-r--r--
Cleanup information theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     1
header {*Lebesgue Integration*}
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     2
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     3
theory Lebesgue
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     4
imports Measure Borel
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     5
begin
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     6
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     7
text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*}
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     8
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
     9
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    10
  "pos_part f = (\<lambda>x. max 0 (f x))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    11
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    12
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    13
  "neg_part f = (\<lambda>x. - min 0 (f x))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    14
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    15
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    16
  "nonneg f = (\<forall>x. 0 \<le> f x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    17
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    18
lemma nonneg_pos_part[intro!]:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    19
  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,zero}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    20
  shows "nonneg (pos_part f)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    21
  unfolding nonneg_def pos_part_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    22
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    23
lemma nonneg_neg_part[intro!]:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    24
  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,ordered_ab_group_add}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    25
  shows "nonneg (neg_part f)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    26
  unfolding nonneg_def neg_part_def min_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    27
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    28
lemma pos_neg_part_abs:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    29
  fixes f :: "'a \<Rightarrow> real"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    30
  shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    31
unfolding real_abs_def pos_part_def neg_part_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    32
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    33
lemma pos_part_abs:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    34
  fixes f :: "'a \<Rightarrow> real"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    35
  shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    36
unfolding pos_part_def real_abs_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    37
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    38
lemma neg_part_abs:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    39
  fixes f :: "'a \<Rightarrow> real"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    40
  shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    41
unfolding neg_part_def real_abs_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    42
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    43
lemma (in measure_space)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    44
  assumes "f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    45
  shows pos_part_borel_measurable: "pos_part f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    46
  and neg_part_borel_measurable: "neg_part f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    47
using assms
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    48
proof -
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    49
  { fix a :: real
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    50
    { assume asm: "0 \<le> a"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    51
      from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    52
      have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    53
        unfolding pos_part_def using assms borel_measurable_le_iff by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    54
      hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    55
    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    56
      unfolding pos_part_def using empty_sets by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    57
    ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    58
      using le_less_linear by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    59
  } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    60
  { fix a :: real
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    61
    { assume asm: "0 \<le> a"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    62
      from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    63
      have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    64
        unfolding neg_part_def using assms borel_measurable_ge_iff by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    65
      hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    66
    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    67
    moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    68
    ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    69
      using le_less_linear by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    70
  } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    71
  from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    72
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    73
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    74
lemma (in measure_space) pos_part_neg_part_borel_measurable_iff:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    75
  "f \<in> borel_measurable M \<longleftrightarrow>
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    76
  pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    77
proof -
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    78
  { fix x
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    79
    have "f x = pos_part f x - neg_part f x"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    80
      unfolding pos_part_def neg_part_def unfolding max_def min_def
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    81
      by auto }
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    82
  hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    83
  hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    84
  from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f]
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    85
    borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    86
    this
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    87
  show ?thesis by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    88
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    89
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    90
context measure_space
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    91
begin
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    92
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    93
section "Simple discrete step function"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
    94
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    95
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    96
 "pos_simple f =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    97
  { (s :: nat set, a, x).
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    98
    finite s \<and> nonneg f \<and> nonneg x \<and> a ` s \<subseteq> sets M \<and>
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    99
    (\<forall>t \<in> space M. (\<exists>!i\<in>s. t\<in>a i) \<and> (\<forall>i\<in>s. t \<in> a i \<longrightarrow> f t = x i)) }"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   100
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   101
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   102
  "pos_simple_integral \<equiv> \<lambda>(s, a, x). \<Sum> i \<in> s. x i * measure M (a i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   103
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   104
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   105
  "psfis f = pos_simple_integral ` (pos_simple f)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   106
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   107
lemma pos_simpleE[consumes 1]:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   108
  assumes ps: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   109
  obtains "finite s" and "nonneg f" and "nonneg x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   110
    and "a ` s \<subseteq> sets M" and "(\<Union>i\<in>s. a i) = space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   111
    and "disjoint_family_on a s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   112
    and "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   113
    and "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   114
proof
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   115
  show "finite s" and "nonneg f" and "nonneg x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   116
    and as_in_M: "a ` s \<subseteq> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   117
    and *: "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   118
    and **: "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   119
    using ps unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   120
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   121
  thus t: "(\<Union>i\<in>s. a i) = space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   122
  proof safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   123
    fix x assume "x \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   124
    from *[OF this] show "x \<in> (\<Union>i\<in>s. a i)" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   125
  next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   126
    fix t i assume "i \<in> s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   127
    hence "a i \<in> sets M" using as_in_M by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   128
    moreover assume "t \<in> a i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   129
    ultimately show "t \<in> space M" using sets_into_space by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   130
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   131
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   132
  show "disjoint_family_on a s" unfolding disjoint_family_on_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   133
  proof safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   134
    fix i j and t assume "i \<in> s" "t \<in> a i" and "j \<in> s" "t \<in> a j" and "i \<noteq> j"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   135
    with t * show "t \<in> {}" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   136
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   137
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   138
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   139
lemma pos_simple_cong:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   140
  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   141
  shows "pos_simple f = pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   142
  unfolding pos_simple_def using assms by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   143
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   144
lemma psfis_cong:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   145
  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   146
  shows "psfis f = psfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   147
  unfolding psfis_def using pos_simple_cong[OF assms] by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   148
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   149
lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   150
  unfolding psfis_def pos_simple_def pos_simple_integral_def
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   151
  by (auto simp: nonneg_def
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   152
      intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   153
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   154
lemma pos_simple_setsum_indicator_fn:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   155
  assumes ps: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   156
  and "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   157
  shows "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) = f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   158
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   159
  from assms obtain i where *: "i \<in> s" "t \<in> a i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   160
    and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   161
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   162
  have **: "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   163
    (\<Sum>j\<in>s. if j \<in> {i} then x i else 0)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   164
    unfolding indicator_fn_def using assms *
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   165
    by (auto intro!: setsum_cong elim!: pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   166
  show ?thesis unfolding ** setsum_cases[OF `finite s`] xi
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   167
    using `i \<in> s` by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   168
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   169
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   170
lemma pos_simple_common_partition:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   171
  assumes psf: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   172
  assumes psg: "(s', b, y) \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   173
  obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   174
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   175
  (* definitions *)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   176
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   177
  def k == "{0 ..< card (s \<times> s')}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   178
  have fs: "finite s" "finite s'" "finite k" unfolding k_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   179
    using psf psg unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   180
  hence "finite (s \<times> s')" by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   181
  then obtain p where p: "p ` k = s \<times> s'" "inj_on p k"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   182
    using ex_bij_betw_nat_finite[of "s \<times> s'"] unfolding bij_betw_def k_def by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   183
  def c == "\<lambda> i. a (fst (p i)) \<inter> b (snd (p i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   184
  def z == "\<lambda> i. x (fst (p i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   185
  def z' == "\<lambda> i. y (snd (p i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   186
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   187
  have "finite k" unfolding k_def by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   188
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   189
  have "nonneg z" and "nonneg z'"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   190
    using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   191
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   192
  have ck_subset_M: "c ` k \<subseteq> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   193
  proof
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   194
    fix x assume "x \<in> c ` k"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   195
    then obtain j where "j \<in> k" and "x = c j" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   196
    hence "p j \<in> s \<times> s'" using p(1) by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   197
    hence "a (fst (p j)) \<in> sets M" (is "?a \<in> _")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   198
      and "b (snd (p j)) \<in> sets M" (is "?b \<in> _")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   199
      using psf psg unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   200
    thus "x \<in> sets M" unfolding `x = c j` c_def using Int by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   201
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   202
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   203
  { fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   204
    hence ex1s: "\<exists>!i\<in>s. t \<in> a i" and ex1s': "\<exists>!i\<in>s'. t \<in> b i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   205
      using psf psg unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   206
    then obtain j j' where j: "j \<in> s" "t \<in> a j" and j': "j' \<in> s'" "t \<in> b j'"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   207
      by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   208
    then obtain i :: nat where i: "(j,j') = p i" and "i \<in> k" using p by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   209
    have "\<exists>!i\<in>k. t \<in> c i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   210
    proof (rule ex1I[of _ i])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   211
      show "\<And>x. x \<in> k \<Longrightarrow> t \<in> c x \<Longrightarrow> x = i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   212
      proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   213
        fix l assume "l \<in> k" "t \<in> c l"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   214
        hence "p l \<in> s \<times> s'" and t_in: "t \<in> a (fst (p l))" "t \<in> b (snd (p l))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   215
          using p unfolding c_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   216
        hence "fst (p l) \<in> s" and "snd (p l) \<in> s'" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   217
        with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   218
        thus "l = i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   219
          using `(j, j') = p i` p(2)[THEN inj_onD] `l \<in> k` `i \<in> k` by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   220
      qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   221
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   222
      show "i \<in> k \<and> t \<in> c i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   223
        using `i \<in> k` `t \<in> a j` `t \<in> b j'` c_def i[symmetric] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   224
    qed auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   225
  } note ex1 = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   226
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   227
  show thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   228
  proof (rule that)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   229
    { fix t i assume "t \<in> space M" and "i \<in> k"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   230
      hence "p i \<in> s \<times> s'" using p(1) by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   231
      hence "fst (p i) \<in> s" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   232
      moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   233
      assume "t \<in> c i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   234
      hence "t \<in> a (fst (p i))" unfolding c_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   235
      ultimately have "f t = z i" using psf `t \<in> space M`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   236
        unfolding z_def pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   237
    }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   238
    thus "(k, c, z) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   239
      using psf `finite k` `nonneg z` ck_subset_M ex1
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   240
      unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   241
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   242
    { fix t i assume "t \<in> space M" and "i \<in> k"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   243
      hence "p i \<in> s \<times> s'" using p(1) by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   244
      hence "snd (p i) \<in> s'" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   245
      moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   246
      assume "t \<in> c i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   247
      hence "t \<in> b (snd (p i))" unfolding c_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   248
      ultimately have "g t = z' i" using psg `t \<in> space M`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   249
        unfolding z'_def pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   250
    }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   251
    thus "(k, c, z') \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   252
      using psg `finite k` `nonneg z'` ck_subset_M ex1
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   253
      unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   254
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   255
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   256
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   257
lemma pos_simple_integral_equal:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   258
  assumes psx: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   259
  assumes psy: "(s', b, y) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   260
  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   261
  unfolding pos_simple_integral_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   262
proof simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   263
  have "(\<Sum>i\<in>s. x i * measure M (a i)) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   264
    (\<Sum>i\<in>s. (\<Sum>j \<in> s'. x i * measure M (a i \<inter> b j)))" (is "?left = _")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   265
    using psy psx unfolding setsum_right_distrib[symmetric]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   266
    by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   267
  also have "... = (\<Sum>i\<in>s. (\<Sum>j \<in> s'. y j * measure M (a i \<inter> b j)))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   268
  proof (rule setsum_cong, simp, rule setsum_cong, simp_all)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   269
    fix i j assume i: "i \<in> s" and j: "j \<in> s'"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   270
    hence "a i \<in> sets M" using psx by (auto elim!: pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   271
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   272
    show "measure M (a i \<inter> b j) = 0 \<or> x i = y j"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   273
    proof (cases "a i \<inter> b j = {}")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   274
      case True thus ?thesis using empty_measure by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   275
    next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   276
      case False then obtain t where t: "t \<in> a i" "t \<in> b j" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   277
      hence "t \<in> space M" using `a i \<in> sets M` sets_into_space by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   278
      with psx psy t i j have "x i = f t" and "y j = f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   279
        unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   280
      thus ?thesis by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   281
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   282
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   283
  also have "... = (\<Sum>j\<in>s'. (\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   284
    by (subst setsum_commute) simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   285
  also have "... = (\<Sum>i\<in>s'. y i * measure M (b i))" (is "?sum_sum = ?right")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   286
  proof (rule setsum_cong)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   287
    fix j assume "j \<in> s'"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   288
    have "y j * measure M (b j) = (\<Sum>i\<in>s. y j * measure M (b j \<inter> a i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   289
      using psx psy `j \<in> s'` unfolding setsum_right_distrib[symmetric]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   290
      by (auto intro!: measure_setsum_split elim!: pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   291
    thus "(\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)) = y j * measure M (b j)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   292
      by (auto intro!: setsum_cong arg_cong[where f="measure M"])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   293
  qed simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   294
  finally show "?left = ?right" .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   295
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   296
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   297
lemma psfis_present:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   298
  assumes "A \<in> psfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   299
  assumes "B \<in> psfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   300
  obtains z z' c k where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   301
  "A = pos_simple_integral (k, c, z)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   302
  "B = pos_simple_integral (k, c, z')"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   303
  "(k, c, z) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   304
  "(k, c, z') \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   305
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   306
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   307
  from assms obtain s a x s' b y where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   308
    ps: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   309
    A: "A = pos_simple_integral (s, a, x)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   310
    B: "B = pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   311
    unfolding psfis_def pos_simple_integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   312
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   313
  guess z z' c k using pos_simple_common_partition[OF ps] . note part = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   314
  show thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   315
  proof (rule that[of k c z z', OF _ _ part])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   316
    show "A = pos_simple_integral (k, c, z)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   317
      unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   318
    show "B = pos_simple_integral (k, c, z')"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   319
      unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   320
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   321
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   322
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   323
lemma pos_simple_integral_add:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   324
  assumes "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   325
  assumes "(s', b, y) \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   326
  obtains s'' c z where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   327
    "(s'', c, z) \<in> pos_simple (\<lambda>x. f x + g x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   328
    "(pos_simple_integral (s, a, x) +
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   329
      pos_simple_integral (s', b, y) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   330
      pos_simple_integral (s'', c, z))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   331
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   332
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   333
  guess z z' c k
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   334
    by (rule pos_simple_common_partition[OF `(s, a, x) \<in> pos_simple f ` `(s', b, y) \<in> pos_simple g`])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   335
  note kczz' = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   336
  have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   337
    by (rule pos_simple_integral_equal) (fact, fact)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   338
  have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   339
    by (rule pos_simple_integral_equal) (fact, fact)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   340
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   341
  have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   342
    = (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   343
    unfolding pos_simple_integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   344
  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   345
  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   346
  also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   347
  finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   348
    pos_simple_integral (k, c, (\<lambda> x. z x + z' x))" using x y by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   349
  show ?thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   350
    apply (rule that[of k c "(\<lambda> x. z x + z' x)", OF _ ths])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   351
    using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   352
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   353
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   354
lemma psfis_add:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   355
  assumes "a \<in> psfis f" "b \<in> psfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   356
  shows "a + b \<in> psfis (\<lambda>x. f x + g x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   357
using assms pos_simple_integral_add
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   358
unfolding psfis_def by auto blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   359
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   360
lemma pos_simple_integral_mono_on_mspace:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   361
  assumes f: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   362
  assumes g: "(s', b, y) \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   363
  assumes mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   364
  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   365
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   366
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   367
  guess z z' c k by (rule pos_simple_common_partition[OF f g])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   368
  note kczz' = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   369
  (* w = z and w' = z'  except where c _ = {} or undef *)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   370
  def w == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   371
  def w' == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z' i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   372
  { fix i
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   373
    have "w i \<le> w' i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   374
    proof (cases "i \<notin> k \<or> c i = {}")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   375
      case False hence "i \<in> k" "c i \<noteq> {}" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   376
      then obtain v where v: "v \<in> c i" and "c i \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   377
        using kczz'(1) unfolding pos_simple_def by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   378
      hence "v \<in> space M" using sets_into_space by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   379
      with mono[OF `v \<in> space M`] kczz' `i \<in> k` `v \<in> c i`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   380
      have "z i \<le> z' i" unfolding pos_simple_def by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   381
      thus ?thesis unfolding w_def w'_def using False by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   382
    next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   383
      case True thus ?thesis unfolding w_def w'_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   384
   qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   385
  } note w_mn = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   386
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   387
  (* some technical stuff for the calculation*)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   388
  have "\<And> i. i \<in> k \<Longrightarrow> c i \<in> sets M" using kczz' unfolding pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   389
  hence "\<And> i. i \<in> k \<Longrightarrow> measure M (c i) \<ge> 0" using positive by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   390
  hence w_mono: "\<And> i. i \<in> k \<Longrightarrow> w i * measure M (c i) \<le> w' i * measure M (c i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   391
    using mult_right_mono w_mn by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   392
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   393
  { fix i have "\<lbrakk>i \<in> k ; z i \<noteq> w i\<rbrakk> \<Longrightarrow> measure M (c i) = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   394
      unfolding w_def by (cases "c i = {}") auto }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   395
  hence zw: "\<And> i. i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   396
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   397
  { fix i have "i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   398
      unfolding w_def by (cases "c i = {}") simp_all }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   399
  note zw = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   400
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   401
  { fix i have "i \<in> k \<Longrightarrow> z' i * measure M (c i) = w' i * measure M (c i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   402
      unfolding w'_def by (cases "c i = {}") simp_all }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   403
  note z'w' = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   404
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   405
  (* the calculation *)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   406
  have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   407
    using f kczz'(1) by (rule pos_simple_integral_equal)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   408
  also have "\<dots> = (\<Sum> i \<in> k. z i * measure M (c i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   409
    unfolding pos_simple_integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   410
  also have "\<dots> = (\<Sum> i \<in> k. w i * measure M (c i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   411
    using setsum_cong2[of k, OF zw] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   412
  also have "\<dots> \<le> (\<Sum> i \<in> k. w' i * measure M (c i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   413
    using setsum_mono[OF w_mono, of k] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   414
  also have "\<dots> = (\<Sum> i \<in> k. z' i * measure M (c i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   415
    using setsum_cong2[of k, OF z'w'] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   416
  also have "\<dots> = pos_simple_integral (k, c, z')"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   417
    unfolding pos_simple_integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   418
  also have "\<dots> = pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   419
    using kczz'(2) g by (rule pos_simple_integral_equal)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   420
  finally show "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   421
    by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   422
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   423
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   424
lemma pos_simple_integral_mono:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   425
  assumes a: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   426
  assumes "\<And> z. f z \<le> g z"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   427
  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   428
using assms pos_simple_integral_mono_on_mspace by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   429
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   430
lemma psfis_mono:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   431
  assumes "a \<in> psfis f" "b \<in> psfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   432
  assumes "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   433
  shows "a \<le> b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   434
using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   435
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   436
lemma pos_simple_fn_integral_unique:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   437
  assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   438
  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   439
using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   440
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   441
lemma psfis_unique:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   442
  assumes "a \<in> psfis f" "b \<in> psfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   443
  shows "a = b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   444
using assms real_le_antisym real_le_refl psfis_mono by metis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   445
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   446
lemma pos_simple_integral_indicator:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   447
  assumes "A \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   448
  obtains s a x where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   449
  "(s, a, x) \<in> pos_simple (indicator_fn A)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   450
  "measure M A = pos_simple_integral (s, a, x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   451
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   452
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   453
  def s == "{0, 1} :: nat set"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   454
  def a == "\<lambda> i :: nat. if i = 0 then A else space M - A"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   455
  def x == "\<lambda> i :: nat. if i = 0 then 1 else (0 :: real)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   456
  have eq: "pos_simple_integral (s, a, x) = measure M A"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   457
    unfolding s_def a_def x_def pos_simple_integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   458
  have "(s, a, x) \<in> pos_simple (indicator_fn A)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   459
    unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   460
    using assms sets_into_space by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   461
   from that[OF this] eq show thesis by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   462
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   463
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   464
lemma psfis_indicator:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   465
  assumes "A \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   466
  shows "measure M A \<in> psfis (indicator_fn A)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   467
using pos_simple_integral_indicator[OF assms]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   468
  unfolding psfis_def image_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   469
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   470
lemma pos_simple_integral_mult:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   471
  assumes f: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   472
  assumes "0 \<le> z"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   473
  obtains s' b y where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   474
  "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   475
  "pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   476
  using assms that[of s a "\<lambda>i. z * x i"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   477
  by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   478
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   479
lemma psfis_mult:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   480
  assumes "r \<in> psfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   481
  assumes "0 \<le> z"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   482
  shows "z * r \<in> psfis (\<lambda>x. z * f x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   483
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   484
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   485
  from assms obtain s a x
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   486
    where sax: "(s, a, x) \<in> pos_simple f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   487
    and r: "r = pos_simple_integral (s, a, x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   488
    unfolding psfis_def image_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   489
  obtain s' b y where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   490
    "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   491
    "z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   492
    using pos_simple_integral_mult[OF sax `0 \<le> z`, of thesis] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   493
  thus ?thesis using r unfolding psfis_def image_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   494
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   495
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   496
lemma psfis_setsum_image:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   497
  assumes "finite P"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   498
  assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   499
  shows "(setsum a P) \<in> psfis (\<lambda>t. \<Sum>i \<in> P. f i t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   500
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   501
proof (induct P)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   502
  case empty
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   503
  let ?s = "{0 :: nat}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   504
  let ?a = "\<lambda> i. if i = (0 :: nat) then space M else {}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   505
  let ?x = "\<lambda> (i :: nat). (0 :: real)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   506
  have "(?s, ?a, ?x) \<in> pos_simple (\<lambda> t. (0 :: real))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   507
    unfolding pos_simple_def image_def nonneg_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   508
  moreover have "(\<Sum> i \<in> ?s. ?x i * measure M (?a i)) = 0" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   509
  ultimately have "0 \<in> psfis (\<lambda> t. 0)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   510
    unfolding psfis_def image_def pos_simple_integral_def nonneg_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   511
    by (auto intro!:bexI[of _ "(?s, ?a, ?x)"])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   512
  thus ?case by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   513
next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   514
  case (insert x P) note asms = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   515
  have "finite P" by fact
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   516
  have "x \<notin> P" by fact
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   517
  have "(\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)) \<Longrightarrow>
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   518
    setsum a P \<in> psfis (\<lambda>t. \<Sum>i\<in>P. f i t)" by fact
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   519
  have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \<notin> P` by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   520
  also have "\<dots> \<in> psfis (\<lambda> t. f x t + (\<Sum> i \<in> P. f i t))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   521
    using asms psfis_add by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   522
  also have "\<dots> = psfis (\<lambda> t. \<Sum> i \<in> insert x P. f i t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   523
    using `x \<notin> P` `finite P` by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   524
  finally show ?case by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   525
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   526
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   527
lemma psfis_intro:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   528
  assumes "a ` P \<subseteq> sets M" and "nonneg x" and "finite P"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   529
  shows "(\<Sum>i\<in>P. x i * measure M (a i)) \<in> psfis (\<lambda>t. \<Sum>i\<in>P. x i * indicator_fn (a i) t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   530
using assms psfis_mult psfis_indicator
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   531
unfolding image_def nonneg_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   532
by (auto intro!:psfis_setsum_image)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   533
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   534
lemma psfis_nonneg: "a \<in> psfis f \<Longrightarrow> nonneg f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   535
unfolding psfis_def pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   536
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   537
lemma pos_psfis: "r \<in> psfis f \<Longrightarrow> 0 \<le> r"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   538
unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   539
using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   540
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   541
lemma psfis_borel_measurable:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   542
  assumes "a \<in> psfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   543
  shows "f \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   544
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   545
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   546
  from assms obtain s a' x where sa'x: "(s, a', x) \<in> pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   547
    and fs: "finite s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   548
    unfolding psfis_def pos_simple_integral_def image_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   549
    by (auto elim:pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   550
  { fix w assume "w \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   551
    hence "(f w \<le> a) = ((\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   552
      using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   553
  } hence "\<And> w. (w \<in> space M \<and> f w \<le> a) = (w \<in> space M \<and> (\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   554
    by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   555
  { fix i assume "i \<in> s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   556
    hence "indicator_fn (a' i) \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   557
      using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   558
    hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   559
      using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   560
        real_mult_commute by auto }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   561
  from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   562
  have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   563
  from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   564
  show ?thesis by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   565
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   566
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   567
lemma psfis_mono_conv_mono:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   568
  assumes mono: "mono_convergent u f (space M)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   569
  and ps_u: "\<And>n. x n \<in> psfis (u n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   570
  and "x ----> y"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   571
  and "r \<in> psfis s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   572
  and f_upper_bound: "\<And>t. t \<in> space M \<Longrightarrow> s t \<le> f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   573
  shows "r <= y"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   574
proof (rule field_le_mult_one_interval)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   575
  fix z :: real assume "0 < z" and "z < 1"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   576
  hence "0 \<le> z" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   577
  let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   578
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   579
  have "incseq x" unfolding incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   580
  proof safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   581
    fix m n :: nat assume "m \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   582
    show "x m \<le> x n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   583
    proof (rule psfis_mono[OF `x m \<in> psfis (u m)` `x n \<in> psfis (u n)`])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   584
      fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   585
      with mono_convergentD[OF mono this] `m \<le> n` show "u m t \<le> u n t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   586
        unfolding incseq_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   587
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   588
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   589
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   590
  from `r \<in> psfis s`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   591
  obtain s' a x' where r: "r = pos_simple_integral (s', a, x')"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   592
    and ps_s: "(s', a, x') \<in> pos_simple s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   593
    unfolding psfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   594
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   595
  { fix t i assume "i \<in> s'" "t \<in> a i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   596
    hence "t \<in> space M" using ps_s by (auto elim!: pos_simpleE) }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   597
  note t_in_space = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   598
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   599
  { fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   600
    from psfis_borel_measurable[OF `r \<in> psfis s`]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   601
       psfis_borel_measurable[OF ps_u]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   602
    have "?B' n \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   603
      by (auto intro!:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   604
        borel_measurable_leq_borel_measurable
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   605
        borel_measurable_times_borel_measurable
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   606
        borel_measurable_const) }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   607
  note B'_in_M = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   608
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   609
  { fix n have "(\<lambda>i. a i \<inter> ?B' n) ` s' \<subseteq> sets M" using B'_in_M ps_s
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   610
      by (auto intro!: Int elim!: pos_simpleE) }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   611
  note B'_inter_a_in_M = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   612
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   613
  let "?sum n" = "(\<Sum>i\<in>s'. x' i * measure M (a i \<inter> ?B' n))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   614
  { fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   615
    have "z * ?sum n \<le> x n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   616
    proof (rule psfis_mono[OF _ ps_u])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   617
      have *: "\<And>i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   618
        x' i * indicator_fn (a i \<inter> ?B' n) t" unfolding indicator_fn_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   619
      have ps': "?sum n \<in> psfis (\<lambda>t. indicator_fn (?B' n) t * (\<Sum>i\<in>s'. x' i * indicator_fn (a i) t))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   620
        unfolding setsum_right_distrib * using B'_in_M ps_s
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   621
        by (auto intro!: psfis_intro Int elim!: pos_simpleE)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   622
      also have "... = psfis (\<lambda>t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   623
      proof (rule psfis_cong)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   624
        show "nonneg ?l" using psfis_nonneg[OF ps'] .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   625
        show "nonneg ?r" using psfis_nonneg[OF `r \<in> psfis s`] unfolding nonneg_def indicator_fn_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   626
        fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   627
        show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \<in> space M`] ..
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   628
      qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   629
      finally show "z * ?sum n \<in> psfis (\<lambda>t. z * ?r t)" using psfis_mult[OF _ `0 \<le> z`] by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   630
    next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   631
      fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   632
      show "z * (indicator_fn (?B' n) t * s t) \<le> u n t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   633
         using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   634
    qed }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   635
  hence *: "\<exists>N. \<forall>n\<ge>N. z * ?sum n \<le> x n" by (auto intro!: exI[of _ 0])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   636
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   637
  show "z * r \<le> y" unfolding r pos_simple_integral_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   638
  proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x ----> y` *],
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   639
         simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   640
    fix i assume "i \<in> s'"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   641
    from psfis_nonneg[OF `r \<in> psfis s`, unfolded nonneg_def]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   642
    have "\<And>t. 0 \<le> s t" by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   643
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   644
    have *: "(\<Union>j. a i \<inter> ?B' j) = a i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   645
    proof (safe, simp, safe)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   646
      fix t assume "t \<in> a i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   647
      thus "t \<in> space M" using t_in_space[OF `i \<in> s'`] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   648
      show "\<exists>j. z * s t \<le> u j t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   649
      proof (cases "s t = 0")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   650
        case True thus ?thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   651
          using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   652
      next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   653
        case False with `0 \<le> s t`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   654
        have "0 < s t" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   655
        hence "z * s t < 1 * s t" using `0 < z` `z < 1`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   656
          by (auto intro!: mult_strict_right_mono simp del: mult_1_left)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   657
        also have "... \<le> f t" using f_upper_bound `t \<in> space M` by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   658
        finally obtain b where "\<And>j. b \<le> j \<Longrightarrow> z * s t < u j t" using `t \<in> space M`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   659
          using mono_conv_outgrow[of "\<lambda>n. u n t" "f t" "z * s t"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   660
          using mono_convergentD[OF mono] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   661
        from this[of b] show ?thesis by (auto intro!: exI[of _ b])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   662
      qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   663
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   664
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   665
    show "(\<lambda>n. measure M (a i \<inter> ?B' n)) ----> measure M (a i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   666
    proof (safe intro!:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   667
        monotone_convergence[of "\<lambda>n. a i \<inter> ?B' n", unfolded comp_def *])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   668
      fix n show "a i \<inter> ?B' n \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   669
        using B'_inter_a_in_M[of n] `i \<in> s'` by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   670
    next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   671
      fix j t assume "t \<in> space M" and "z * s t \<le> u j t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   672
      thus "z * s t \<le> u (Suc j) t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   673
        using mono_convergentD(1)[OF mono, unfolded incseq_def,
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   674
          rule_format, of t j "Suc j"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   675
        by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   676
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   677
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   678
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   679
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   680
section "Continuous posititve integration"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   681
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   682
definition
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   683
  "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   684
                        (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   685
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   686
lemma psfis_nnfis:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   687
  "a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   688
  unfolding nnfis_def mono_convergent_def incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   689
  by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   690
35748
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
   691
lemma nnfis_0: "0 \<in> nnfis (\<lambda> x. 0)"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
   692
  by (rule psfis_nnfis[OF psfis_0])
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
   693
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   694
lemma nnfis_times:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   695
  assumes "a \<in> nnfis f" and "0 \<le> z"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   696
  shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   697
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   698
  obtain u x where "mono_convergent u f (space M)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   699
    "\<And>n. x n \<in> psfis (u n)" "x ----> a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   700
    using `a \<in> nnfis f` unfolding nnfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   701
  with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   702
    by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   703
      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   704
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   705
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   706
lemma nnfis_add:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   707
  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   708
  shows "a + b \<in> nnfis (\<lambda>t. f t + g t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   709
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   710
  obtain u x w y
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   711
    where "mono_convergent u f (space M)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   712
    "\<And>n. x n \<in> psfis (u n)" "x ----> a" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   713
    "mono_convergent w g (space M)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   714
    "\<And>n. y n \<in> psfis (w n)" "y ----> b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   715
    using `a \<in> nnfis f` `b \<in> nnfis g` unfolding nnfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   716
  thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   717
    by (auto intro!: exI[of _ "\<lambda>n a. u n a + w n a"] exI[of _ "\<lambda>n. x n + y n"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   718
      LIMSEQ_add LIMSEQ_const psfis_add add_mono)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   719
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   720
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   721
lemma nnfis_mono:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   722
  assumes nnfis: "a \<in> nnfis f" "b \<in> nnfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   723
  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   724
  shows "a \<le> b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   725
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   726
  obtain u x w y where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   727
    mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   728
    psfis: "\<And>n. x n \<in> psfis (u n)" "\<And>n. y n \<in> psfis (w n)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   729
    limseq: "x ----> a" "y ----> b" using nnfis unfolding nnfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   730
  show ?thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   731
  proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   732
    fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   733
    show "x n \<le> b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   734
    proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   735
      fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   736
      from mono_convergent_le[OF mc(1) this] mono[OF this]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   737
      show "u n t \<le> g t" by (rule order_trans)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   738
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   739
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   740
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   741
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   742
lemma nnfis_unique:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   743
  assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   744
  shows "a = b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   745
  using nnfis_mono[OF a b] nnfis_mono[OF b a]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   746
  by (auto intro!: real_le_antisym[of a b])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   747
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   748
lemma psfis_equiv:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   749
  assumes "a \<in> psfis f" and "nonneg g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   750
  and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   751
  shows "a \<in> psfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   752
  using assms unfolding psfis_def pos_simple_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   753
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   754
lemma psfis_mon_upclose:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   755
  assumes "\<And>m. a m \<in> psfis (u m)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   756
  shows "\<exists>c. c \<in> psfis (mon_upclose n u)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   757
proof (induct n)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   758
  case 0 thus ?case unfolding mon_upclose.simps using assms ..
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   759
next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   760
  case (Suc n)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   761
  then obtain sn an xn where ps: "(sn, an, xn) \<in> pos_simple (mon_upclose n u)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   762
    unfolding psfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   763
  obtain ss as xs where ps': "(ss, as, xs) \<in> pos_simple (u (Suc n))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   764
    using assms[of "Suc n"] unfolding psfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   765
  from pos_simple_common_partition[OF ps ps'] guess x x' a s .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   766
  hence "(s, a, upclose x x') \<in> pos_simple (mon_upclose (Suc n) u)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   767
    by (simp add: upclose_def pos_simple_def nonneg_def max_def)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   768
  thus ?case unfolding psfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   769
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   770
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   771
text {* Beppo-Levi monotone convergence theorem *}
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   772
lemma nnfis_mon_conv:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   773
  assumes mc: "mono_convergent f h (space M)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   774
  and nnfis: "\<And>n. x n \<in> nnfis (f n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   775
  and "x ----> z"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   776
  shows "z \<in> nnfis h"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   777
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   778
  have "\<forall>n. \<exists>u y. mono_convergent u (f n) (space M) \<and> (\<forall>m. y m \<in> psfis (u m)) \<and>
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   779
    y ----> x n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   780
    using nnfis unfolding nnfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   781
  from choice[OF this] guess u ..
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   782
  from choice[OF this] guess y ..
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   783
  hence mc_u: "\<And>n. mono_convergent (u n) (f n) (space M)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   784
    and psfis: "\<And>n m. y n m \<in> psfis (u n m)" and "\<And>n. y n ----> x n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   785
    by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   786
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   787
  let "?upclose n" = "mon_upclose n (\<lambda>m. u m n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   788
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   789
  have "\<exists>c. \<forall>n. c n \<in> psfis (?upclose n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   790
    by (safe intro!: choice psfis_mon_upclose) (rule psfis)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   791
  then guess c .. note c = this[rule_format]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   792
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   793
  show ?thesis unfolding nnfis_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   794
  proof (safe intro!: exI)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   795
    show mc_upclose: "mono_convergent ?upclose h (space M)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   796
      by (rule mon_upclose_mono_convergent[OF mc_u mc])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   797
    show psfis_upclose: "\<And>n. c n \<in> psfis (?upclose n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   798
      using c .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   799
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   800
    { fix n m :: nat assume "n \<le> m"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   801
      hence "c n \<le> c m"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   802
        using psfis_mono[OF c c]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   803
        using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   804
        by auto }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   805
    hence "incseq c" unfolding incseq_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   806
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   807
    { fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   808
      have c_nnfis: "c n \<in> nnfis (?upclose n)" using c by (rule psfis_nnfis)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   809
      from nnfis_mono[OF c_nnfis nnfis]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   810
        mon_upclose_le_mono_convergent[OF mc_u]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   811
        mono_convergentD(1)[OF mc]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   812
      have "c n \<le> x n" by fast }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   813
    note c_less_x = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   814
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   815
    { fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   816
      note c_less_x[of n]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   817
      also have "x n \<le> z"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   818
      proof (rule incseq_le)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   819
        show "x ----> z" by fact
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   820
        from mono_convergentD(1)[OF mc]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   821
        show "incseq x" unfolding incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   822
          by (auto intro!: nnfis_mono[OF nnfis nnfis])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   823
      qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   824
      finally have "c n \<le> z" . }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   825
    note c_less_z = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   826
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   827
    have "convergent c"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   828
    proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   829
      show "Bseq c"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   830
        using pos_psfis[OF c] c_less_z
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   831
        by (auto intro!: BseqI'[of _ z])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   832
      show "incseq c" by fact
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   833
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   834
    then obtain l where l: "c ----> l" unfolding convergent_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   835
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   836
    have "l \<le> z" using c_less_x l
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   837
      by (auto intro!: LIMSEQ_le[OF _ `x ----> z`])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   838
    moreover have "z \<le> l"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   839
    proof (rule LIMSEQ_le_const2[OF `x ----> z`], safe intro!: exI[of _ 0])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   840
      fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   841
      have "l \<in> nnfis h"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   842
        unfolding nnfis_def using l mc_upclose psfis_upclose by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   843
      from nnfis this mono_convergent_le[OF mc]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   844
      show "x n \<le> l" by (rule nnfis_mono)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   845
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   846
    ultimately have "l = z" by (rule real_le_antisym)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   847
    thus "c ----> z" using `c ----> l` by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   848
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   849
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   850
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   851
lemma nnfis_pos_on_mspace:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   852
  assumes "a \<in> nnfis f" and "x \<in>space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   853
  shows "0 \<le> f x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   854
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   855
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   856
  from assms[unfolded nnfis_def] guess u y by auto note uy = this
35748
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
   857
  hence "\<And> n. 0 \<le> u n x"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   858
    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   859
    by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   860
  thus "0 \<le> f x" using uy[rule_format]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   861
    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   862
    using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   863
    by fast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   864
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   865
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   866
lemma nnfis_borel_measurable:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   867
  assumes "a \<in> nnfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   868
  shows "f \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   869
using assms unfolding nnfis_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   870
apply auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   871
apply (rule mono_convergent_borel_measurable)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   872
using psfis_borel_measurable
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   873
by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   874
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   875
lemma borel_measurable_mon_conv_psfis:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   876
  assumes f_borel: "f \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   877
  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   878
  shows"\<exists>u x. mono_convergent u f (space M) \<and> (\<forall>n. x n \<in> psfis (u n))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   879
proof (safe intro!: exI)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   880
  let "?I n" = "{0<..<n * 2^n}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   881
  let "?A n i" = "{w \<in> space M. real (i :: nat) / 2^(n::nat) \<le> f w \<and> f w < real (i + 1) / 2^n}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   882
  let "?u n t" = "\<Sum>i\<in>?I n. real i / 2^n * indicator_fn (?A n i) t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   883
  let "?x n" = "\<Sum>i\<in>?I n. real i / 2^n * measure M (?A n i)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   884
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   885
  let "?w n t" = "if f t < real n then real (natfloor (f t * 2^n)) / 2^n else 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   886
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   887
  { fix t n assume t: "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   888
    have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   889
    proof (cases "f t < real n")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   890
      case True
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   891
      with nonneg t
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   892
      have i: "?i < n * 2^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   893
        by (auto simp: real_of_nat_power[symmetric]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   894
                 intro!: less_natfloor mult_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   895
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   896
      hence t_in_A: "t \<in> ?A n ?i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   897
        unfolding divide_le_eq less_divide_eq
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   898
        using nonneg t True
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   899
        by (auto intro!: real_natfloor_le
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   900
          real_natfloor_gt_diff_one[unfolded diff_less_eq]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   901
          simp: real_of_nat_Suc zero_le_mult_iff)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   902
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   903
      hence *: "real ?i / 2^n \<le> f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   904
        "f t < real (?i + 1) / 2^n" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   905
      { fix j assume "t \<in> ?A n j"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   906
        hence "real j / 2^n \<le> f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   907
          and "f t < real (j + 1) / 2^n" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   908
        with * have "j \<in> {?i}" unfolding divide_le_eq less_divide_eq
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   909
          by auto }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   910
      hence *: "\<And>j. t \<in> ?A n j \<longleftrightarrow> j \<in> {?i}" using t_in_A by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   911
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   912
      have "?u n t = real ?i / 2^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   913
        unfolding indicator_fn_def if_distrib *
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   914
          setsum_cases[OF finite_greaterThanLessThan]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   915
        using i by (cases "?i = 0") simp_all
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   916
      thus ?thesis using True by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   917
    next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   918
      case False
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   919
      have "?u n t = (\<Sum>i \<in> {0 <..< n*2^n}. 0)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   920
      proof (rule setsum_cong)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   921
        fix i assume "i \<in> {0 <..< n*2^n}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   922
        hence "i + 1 \<le> n * 2^n" by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   923
        hence "real (i + 1) \<le> real n * 2^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   924
          unfolding real_of_nat_le_iff[symmetric]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   925
          by (auto simp: real_of_nat_power[symmetric])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   926
        also have "... \<le> f t * 2^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   927
          using False by (auto intro!: mult_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   928
        finally have "t \<notin> ?A n i"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   929
          by (auto simp: divide_le_eq less_divide_eq)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   930
        thus "real i / 2^n * indicator_fn (?A n i) t = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   931
          unfolding indicator_fn_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   932
      qed simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   933
      thus ?thesis using False by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   934
    qed }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   935
  note u_at_t = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   936
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   937
  show "mono_convergent ?u f (space M)" unfolding mono_convergent_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   938
  proof safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   939
    fix t assume t: "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   940
    { fix m n :: nat assume "m \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   941
      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   942
      have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   943
        apply (subst *)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   944
        apply (subst class_semiring.mul_a)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   945
        apply (subst real_of_nat_le_iff)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   946
        apply (rule le_mult_natfloor)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   947
        using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   948
      hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   949
        apply (subst *)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   950
        apply (subst (3) class_semiring.mul_c)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   951
        apply (subst class_semiring.mul_a)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   952
        by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   953
    thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   954
      by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   955
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   956
    show "(\<lambda>i. ?u i t) ----> f t" unfolding u_at_t[OF t]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   957
    proof (rule LIMSEQ_I, safe intro!: exI)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   958
      fix r :: real and n :: nat
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   959
      let ?N = "natfloor (1/r) + 1"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   960
      assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   961
      hence "?N \<le> n" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   962
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   963
      have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   964
        by (simp add: real_of_nat_Suc)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   965
      also have "... < 2^?N" by (rule two_realpow_gt)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   966
      finally have less_r: "1 / 2^?N < r" using `0 < r`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   967
        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   968
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   969
      have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   970
      also have "... \<le> real n" unfolding real_of_nat_le_iff using N by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   971
      finally have "f t < real n" .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   972
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   973
      have "real (natfloor (f t * 2^n)) \<le> f t * 2^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   974
        using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   975
      hence less: "real (natfloor (f t * 2^n)) / 2^n \<le> f t" unfolding divide_le_eq by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   976
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   977
      have "f t * 2 ^ n - 1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   978
      hence "f t - real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   979
        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   980
      also have "... \<le> 1 / 2^?N" using `?N \<le> n`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   981
        by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   982
      also have "... < r" using less_r .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   983
      finally show "norm (?w n t - f t) < r" using `f t < real n` less by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   984
    qed
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
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   987
  fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   988
  show "?x n \<in> psfis (?u n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   989
  proof (rule psfis_intro)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   990
    show "?A n ` ?I n \<subseteq> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   991
    proof safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   992
      fix i :: nat
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   993
      from Int[OF
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   994
        f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   995
        f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   996
      show "?A n i \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   997
        by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   998
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   999
    show "nonneg (\<lambda>i :: nat. real i / 2 ^ n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1000
      unfolding nonneg_def by (auto intro!: divide_nonneg_pos)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1001
  qed auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1002
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1003
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1004
lemma nnfis_dom_conv:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1005
  assumes borel: "f \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1006
  and nnfis: "b \<in> nnfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1007
  and ord: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1008
  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1009
  shows "\<exists>a. a \<in> nnfis f \<and> a \<le> b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1010
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1011
  obtain u x where mc_f: "mono_convergent u f (space M)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1012
    psfis: "\<And>n. x n \<in> psfis (u n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1013
    using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1014
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1015
  { fix n
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1016
    { fix t assume t: "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1017
      note mono_convergent_le[OF mc_f this, of n]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1018
      also note ord[OF t]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1019
      finally have "u n t \<le> g t" . }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1020
    from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1021
    have "x n \<le> b" by simp }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1022
  note x_less_b = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1023
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1024
  have "convergent x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1025
  proof (safe intro!: Bseq_mono_convergent)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1026
    from x_less_b pos_psfis[OF psfis]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1027
    show "Bseq x" by (auto intro!: BseqI'[of _ b])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1028
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1029
    fix n m :: nat assume *: "n \<le> m"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1030
    show "x n \<le> x m"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1031
    proof (rule psfis_mono[OF `x n \<in> psfis (u n)` `x m \<in> psfis (u m)`])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1032
      fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1033
      from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1034
      show "u n t \<le> u m t" using * by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1035
    qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1036
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1037
  then obtain a where "x ----> a" unfolding convergent_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1038
  with LIMSEQ_le_const2[OF `x ----> a`] x_less_b mc_f psfis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1039
  show ?thesis unfolding nnfis_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1040
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1041
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1042
lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1043
  by (auto intro: the_equality nnfis_unique)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1044
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1045
lemma nnfis_cong:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1046
  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1047
  shows "nnfis f = nnfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1048
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1049
  { fix f g :: "'a \<Rightarrow> real" assume cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1050
    fix x assume "x \<in> nnfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1051
    then guess u y unfolding nnfis_def by safe note x = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1052
    hence "mono_convergent u g (space M)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1053
      unfolding mono_convergent_def using cong by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1054
    with x(2,3) have "x \<in> nnfis g" unfolding nnfis_def by auto }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1055
  from this[OF cong] this[OF cong[symmetric]]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1056
  show ?thesis by safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1057
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1058
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1059
section "Lebesgue Integral"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1060
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1061
definition
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1062
  "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1063
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1064
definition
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1065
  "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1066
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1067
lemma integral_cong:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1068
  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1069
  shows "integral f = integral g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1070
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1071
  have "nnfis (pos_part f) = nnfis (pos_part g)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1072
    using cong by (auto simp: pos_part_def intro!: nnfis_cong)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1073
  moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1074
  have "nnfis (neg_part f) = nnfis (neg_part g)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1075
    using cong by (auto simp: neg_part_def intro!: nnfis_cong)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1076
  ultimately show ?thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1077
    unfolding integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1078
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1079
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1080
lemma nnfis_integral:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1081
  assumes "a \<in> nnfis f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1082
  shows "integrable f" and "integral f = a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1083
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1084
  have a: "a \<in> nnfis (pos_part f)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1085
    using assms nnfis_pos_on_mspace[OF assms]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1086
    by (auto intro!: nnfis_mon_conv[of "\<lambda>i. f" _ "\<lambda>i. a"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1087
      LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1088
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1089
  have "\<And>t. t \<in> space M \<Longrightarrow> neg_part f t = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1090
    unfolding neg_part_def min_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1091
    using nnfis_pos_on_mspace[OF assms] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1092
  hence 0: "0 \<in> nnfis (neg_part f)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1093
    by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1094
          intro!: LIMSEQ_const exI[of _ "\<lambda> x n. 0"] exI[of _ "\<lambda> n. 0"])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1095
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1096
  from 0 a show "integrable f" "integral f = a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1097
    unfolding integrable_def integral_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1098
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1099
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1100
lemma nnfis_minus_nnfis_integral:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1101
  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1102
  shows "integrable (\<lambda>t. f t - g t)" and "integral (\<lambda>t. f t - g t) = a - b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1103
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1104
  have borel: "(\<lambda>t. f t - g t) \<in> borel_measurable M" using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1105
    by (blast intro:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1106
      borel_measurable_diff_borel_measurable nnfis_borel_measurable)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1107
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1108
  have "\<exists>x. x \<in> nnfis (pos_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1109
    (is "\<exists>x. x \<in> nnfis ?pp \<and> _")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1110
  proof (rule nnfis_dom_conv)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1111
    show "?pp \<in> borel_measurable M"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1112
      using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1113
    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1114
    fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1115
    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1116
    show "?pp t \<le> f t + g t" unfolding pos_part_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1117
    show "0 \<le> ?pp t" using nonneg_pos_part[of "\<lambda>t. f t - g t"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1118
      unfolding nonneg_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1119
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1120
  then obtain x where x: "x \<in> nnfis ?pp" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1121
  moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1122
  have "\<exists>x. x \<in> nnfis (neg_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1123
    (is "\<exists>x. x \<in> nnfis ?np \<and> _")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1124
  proof (rule nnfis_dom_conv)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1125
    show "?np \<in> borel_measurable M"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1126
      using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1127
    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1128
    fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1129
    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1130
    show "?np t \<le> f t + g t" unfolding neg_part_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1131
    show "0 \<le> ?np t" using nonneg_neg_part[of "\<lambda>t. f t - g t"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1132
      unfolding nonneg_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1133
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1134
  then obtain y where y: "y \<in> nnfis ?np" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1135
  ultimately show "integrable (\<lambda>t. f t - g t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1136
    unfolding integrable_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1137
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1138
  from x and y
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1139
  have "a + y \<in> nnfis (\<lambda>t. f t + ?np t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1140
    and "b + x \<in> nnfis (\<lambda>t. g t + ?pp t)" using assms by (auto intro: nnfis_add)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1141
  moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1142
  have "\<And>t. f t + ?np t = g t + ?pp t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1143
    unfolding pos_part_def neg_part_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1144
  ultimately have "a - b = x - y"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1145
    using nnfis_unique by (auto simp: algebra_simps)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1146
  thus "integral (\<lambda>t. f t - g t) = a - b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1147
    unfolding integral_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1148
    using the_nnfis[OF x] the_nnfis[OF y] by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1149
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1150
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1151
lemma integral_borel_measurable:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1152
  "integrable f \<Longrightarrow> f \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1153
  unfolding integrable_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1154
  by (subst pos_part_neg_part_borel_measurable_iff)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1155
   (auto intro: nnfis_borel_measurable)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1156
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1157
lemma integral_indicator_fn:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1158
  assumes "a \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1159
  shows "integral (indicator_fn a) = measure M a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1160
  and "integrable (indicator_fn a)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1161
  using psfis_indicator[OF assms, THEN psfis_nnfis]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1162
  by (auto intro!: nnfis_integral)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1163
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1164
lemma integral_add:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1165
  assumes "integrable f" and "integrable g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1166
  shows "integrable (\<lambda>t. f t + g t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1167
  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1168
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1169
  { fix t
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1170
    have "pos_part f t + pos_part g t - (neg_part f t + neg_part g t) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1171
      f t + g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1172
      unfolding pos_part_def neg_part_def by auto }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1173
  note part_sum = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1174
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1175
  from assms obtain a b c d where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1176
    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1177
    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1178
    unfolding integrable_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1179
  note sums = nnfis_add[OF a c] nnfis_add[OF b d]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1180
  note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1181
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1182
  show "integrable (\<lambda>t. f t + g t)" using int(1) .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1183
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1184
  show "integral (\<lambda>t. f t + g t) = integral f + integral g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1185
    using int(2) sums a b c d by (simp add: the_nnfis integral_def)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1186
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1187
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1188
lemma integral_mono:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1189
  assumes "integrable f" and "integrable g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1190
  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1191
  shows "integral f \<le> integral g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1192
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1193
  from assms obtain a b c d where
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1194
    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1195
    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1196
    unfolding integrable_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1197
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1198
  have "a \<le> c"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1199
  proof (rule nnfis_mono[OF a c])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1200
    fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1201
    from mono[OF this] show "pos_part f t \<le> pos_part g t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1202
      unfolding pos_part_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1203
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1204
  moreover have "d \<le> b"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1205
  proof (rule nnfis_mono[OF d b])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1206
    fix t assume "t \<in> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1207
    from mono[OF this] show "neg_part g t \<le> neg_part f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1208
      unfolding neg_part_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1209
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1210
  ultimately have "a - b \<le> c - d" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1211
  thus ?thesis unfolding integral_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1212
    using a b c d by (simp add: the_nnfis)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1213
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1214
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1215
lemma integral_uminus:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1216
  assumes "integrable f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1217
  shows "integrable (\<lambda>t. - f t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1218
  and "integral (\<lambda>t. - f t) = - integral f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1219
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1220
  have "pos_part f = neg_part (\<lambda>t.-f t)" and "neg_part f = pos_part (\<lambda>t.-f t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1221
    unfolding pos_part_def neg_part_def by (auto intro!: ext)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1222
  with assms show "integrable (\<lambda>t.-f t)" and "integral (\<lambda>t.-f t) = -integral f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1223
    unfolding integrable_def integral_def by simp_all
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1224
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1225
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1226
lemma integral_times_const:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1227
  assumes "integrable f"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1228
  shows "integrable (\<lambda>t. a * f t)" (is "?P a")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1229
  and "integral (\<lambda>t. a * f t) = a * integral f" (is "?I a")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1230
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1231
  { fix a :: real assume "0 \<le> a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1232
    hence "pos_part (\<lambda>t. a * f t) = (\<lambda>t. a * pos_part f t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1233
      and "neg_part (\<lambda>t. a * f t) = (\<lambda>t. a * neg_part f t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1234
      unfolding pos_part_def neg_part_def max_def min_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1235
      by (auto intro!: ext simp: zero_le_mult_iff)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1236
    moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1237
    obtain x y where x: "x \<in> nnfis (pos_part f)" and y: "y \<in> nnfis (neg_part f)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1238
      using assms unfolding integrable_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1239
    ultimately
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1240
    have "a * x \<in> nnfis (pos_part (\<lambda>t. a * f t))" and
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1241
      "a * y \<in> nnfis (neg_part (\<lambda>t. a * f t))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1242
      using nnfis_times[OF _ `0 \<le> a`] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1243
    with x y have "?P a \<and> ?I a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1244
      unfolding integrable_def integral_def by (auto simp: algebra_simps) }
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1245
  note int = this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1246
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1247
  have "?P a \<and> ?I a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1248
  proof (cases "0 \<le> a")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1249
    case True from int[OF this] show ?thesis .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1250
  next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1251
    case False with int[of "- a"] integral_uminus[of "\<lambda>t. - a * f t"]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1252
    show ?thesis by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1253
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1254
  thus "integrable (\<lambda>t. a * f t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1255
    and "integral (\<lambda>t. a * f t) = a * integral f" by simp_all
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1256
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1257
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1258
lemma integral_cmul_indicator:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1259
  assumes "s \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1260
  shows "integral (\<lambda>x. c * indicator_fn s x) = c * (measure M s)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1261
  and "integrable (\<lambda>x. c * indicator_fn s x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1262
using assms integral_times_const integral_indicator_fn by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1263
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1264
lemma integral_zero:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1265
  shows "integral (\<lambda>x. 0) = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1266
  and "integrable (\<lambda>x. 0)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1267
  using integral_cmul_indicator[OF empty_sets, of 0]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1268
  unfolding indicator_fn_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1269
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1270
lemma integral_setsum:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1271
  assumes "finite S"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1272
  assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1273
  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1274
    and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I s")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1275
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1276
  from assms have "?int S \<and> ?I S"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1277
  proof (induct S)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1278
    case empty thus ?case by (simp add: integral_zero)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1279
  next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1280
    case (insert i S)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1281
    thus ?case
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1282
      apply simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1283
      apply (subst integral_add)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1284
      using assms apply auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1285
      apply (subst integral_add)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1286
      using assms by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1287
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1288
  thus "?int S" and "?I S" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1289
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1290
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1291
lemma (in measure_space) integrable_abs:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1292
  assumes "integrable f"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1293
  shows "integrable (\<lambda> x. \<bar>f x\<bar>)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1294
using assms
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1295
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1296
  from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1297
    unfolding integrable_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1298
  hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1299
    using nnfis_add by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1300
  hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1301
  thus ?thesis unfolding integrable_def
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1302
    using ext[OF pos_part_abs[of f], of "\<lambda> y. y"]
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1303
      ext[OF neg_part_abs[of f], of "\<lambda> y. y"]
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1304
    using nnfis_0 by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1305
qed
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1306
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1307
lemma markov_ineq:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1308
  assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1309
  shows "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1310
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1311
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1312
  from assms have "0 < a ^ n" using real_root_pow_pos by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1313
  from assms have "f \<in> borel_measurable M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1314
    using integral_borel_measurable[OF `integrable f`] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1315
  hence w: "{w . w \<in> space M \<and> a \<le> f w} \<in> sets M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1316
    using borel_measurable_ge_iff by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1317
  have i: "integrable (indicator_fn {w . w \<in> space M \<and> a \<le> f w})"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1318
    using integral_indicator_fn[OF w] by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1319
  have v1: "\<And> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t 
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1320
            \<le> (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1321
    unfolding indicator_fn_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1322
    using `0 < a` power_mono[of a] assms by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1323
  have v2: "\<And> t. (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t \<le> \<bar>f t\<bar> ^ n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1324
    unfolding indicator_fn_def 
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1325
    using power_mono[of a _ n] abs_ge_self `a > 0` 
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1326
    by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1327
  have "{w \<in> space M. a \<le> f w} \<inter> space M = {w . a \<le> f w} \<inter> space M"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1328
    using Collect_eq by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1329
  from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1330
  have "(a ^ n) * (measure M ((f -` {y . a \<le> y}) \<inter> space M)) =
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1331
        (a ^ n) * measure M {w . w \<in> space M \<and> a \<le> f w}"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1332
    unfolding vimage_Collect_eq[of f] by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1333
  also have "\<dots> = integral (\<lambda> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1334
    using integral_cmul_indicator[OF w] i by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1335
  also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1336
    apply (rule integral_mono)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1337
    using integral_cmul_indicator[OF w]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1338
      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1339
  finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1340
    unfolding atLeast_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1341
    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1342
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
  1343
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1344
lemma (in measure_space) integral_0:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1345
  fixes f :: "'a \<Rightarrow> real"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1346
  assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1347
  shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1348
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1349
  have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1350
  moreover
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1351
  { fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1352
    hence "\<bar> f y \<bar> > 0" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1353
    hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1354
      using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1355
    hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1356
      by auto }
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1357
  moreover
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1358
  { fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1359
    then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1360
    hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1361
    hence "\<bar>f y\<bar> > 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1362
      using real_of_nat_Suc_gt_zero
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1363
        positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1364
    hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto }
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1365
  ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1366
    by blast
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1367
  { fix n
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1368
    have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using integrable_abs assms by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1369
    have "measure M (f -` {inverse (real (Suc n))..} \<inter> space M)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1370
           \<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1371
      using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1372
    hence le0: "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) \<le> 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1373
      using assms unfolding nonneg_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1374
    have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1375
      apply (subst Int_commute) unfolding Int_def
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1376
      using borel[unfolded borel_measurable_ge_iff] by simp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1377
    hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and>
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1378
      {x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1379
      using positive le0 unfolding atLeast_def by fastsimp }
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1380
  moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1381
    by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1382
  moreover
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1383
  { fix n
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1384
    have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1385
      using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1386
    hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1387
    hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1388
         \<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto }
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1389
  ultimately have "(\<lambda> x. 0) ----> measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1390
    using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"]
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1391
    unfolding o_def by (simp del: of_nat_Suc)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1392
  hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1393
    using LIMSEQ_const[of 0] LIMSEQ_unique by simp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1394
  hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1395
    using assms unfolding nonneg_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1396
  thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1397
qed
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
  1398
35748
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1399
section "Lebesgue integration on countable spaces"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1400
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1401
lemma nnfis_on_countable:
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1402
  assumes borel: "f \<in> borel_measurable M"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1403
  and bij: "bij_betw enum S (f ` space M - {0})"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1404
  and enum_zero: "enum ` (-S) \<subseteq> {0}"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1405
  and nn_enum: "\<And>n. 0 \<le> enum n"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1406
  and sums: "(\<lambda>r. enum r * measure M (f -` {enum r} \<inter> space M)) sums x" (is "?sum sums x")
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1407
  shows "x \<in> nnfis f"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1408
proof -
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1409
  have inj_enum: "inj_on enum S"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1410
    and range_enum: "enum ` S = f ` space M - {0}"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1411
    using bij by (auto simp: bij_betw_def)
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1412
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1413
  let "?x n z" = "\<Sum>i = 0..<n. enum i * indicator_fn (f -` {enum i} \<inter> space M) z"
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1414
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1415
  show ?thesis
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1416
  proof (rule nnfis_mon_conv)
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1417
    show "(\<lambda>n. \<Sum>i = 0..<n. ?sum i) ----> x" using sums unfolding sums_def .
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35692
diff changeset
  1418
  next