src/HOL/Probability/Borel.thy
author hoelzl
Mon, 08 Mar 2010 11:30:55 +0100
changeset 35692 f1315bbf1bc9
parent 35582 b16d99a72dc9
child 35704 5007843dae33
permissions -rw-r--r--
Moved theorems in Lebesgue to the right places
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     1
header {*Borel Sets*}
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     2
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     3
theory Borel
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     4
  imports Measure
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     5
begin
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     6
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     7
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     8
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     9
definition borel_space where
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    10
  "borel_space = sigma (UNIV::real set) (range (\<lambda>a::real. {x. x \<le> a}))"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    11
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    12
definition borel_measurable where
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    13
  "borel_measurable a = measurable a borel_space"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    14
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    15
definition indicator_fn where
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    16
  "indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    17
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    18
lemma in_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    19
   "f \<in> borel_measurable M \<longleftrightarrow>
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    20
    sigma_algebra M \<and>
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    21
    (\<forall>s \<in> sets (sigma UNIV (range (\<lambda>a::real. {x. x \<le> a}))).
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    22
      f -` s \<inter> space M \<in> sets M)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    23
apply (auto simp add: borel_measurable_def measurable_def borel_space_def) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    24
apply (metis PowD UNIV_I Un_commute sigma_algebra_sigma subset_Pow_Union subset_UNIV subset_Un_eq) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    25
done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    26
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    27
lemma (in sigma_algebra) borel_measurable_const:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    28
   "(\<lambda>x. c) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    29
  by (auto simp add: in_borel_measurable prems)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    30
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    31
lemma (in sigma_algebra) borel_measurable_indicator:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    32
  assumes a: "a \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    33
  shows "indicator_fn a \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    34
apply (auto simp add: in_borel_measurable indicator_fn_def prems)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    35
apply (metis Diff_eq Int_commute a compl_sets) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    36
done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    37
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    38
lemma Collect_eq: "{w \<in> X. f w \<le> a} = {w. f w \<le> a} \<inter> X"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    39
  by (metis Collect_conj_eq Collect_mem_eq Int_commute)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    40
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    41
lemma (in measure_space) borel_measurable_le_iff:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    42
   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    43
proof 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    44
  assume f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    45
  { fix a
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    46
    have "{w \<in> space M. f w \<le> a} \<in> sets M" using f
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    47
      apply (auto simp add: in_borel_measurable sigma_def Collect_eq)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    48
      apply (drule_tac x="{x. x \<le> a}" in bspec, auto)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    49
      apply (metis equalityE rangeI subsetD sigma_sets.Basic)  
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    50
      done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    51
    }
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    52
  thus "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" by blast
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    53
next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    54
  assume "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    55
  thus "f \<in> borel_measurable M" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    56
    apply (simp add: borel_measurable_def borel_space_def Collect_eq) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    57
    apply (rule measurable_sigma, auto) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    58
    done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    59
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    60
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    61
lemma Collect_less_le:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    62
     "{w \<in> X. f w < g w} = (\<Union>n. {w \<in> X. f w \<le> g w - inverse(real(Suc n))})"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    63
  proof auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    64
    fix w
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    65
    assume w: "f w < g w"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    66
    hence nz: "g w - f w \<noteq> 0"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    67
      by arith
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    68
    with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    69
      by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff)       hence "inverse(real(Suc(natceiling(inverse(g w - f w)))))
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    70
             < inverse(inverse(g w - f w))" 
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 33657
diff changeset
    71
      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    72
    hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    73
      by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    74
    thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    75
      by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    76
  next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    77
    fix w n
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    78
    assume le: "f w \<le> g w - inverse(real(Suc n))"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    79
    hence "0 < inverse(real(Suc n))"
35347
be0c69c06176 remove redundant simp rules from RealPow.thy
huffman
parents: 35050
diff changeset
    80
      by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    81
    thus "f w < g w" using le
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    82
      by arith 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    83
  qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    84
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    85
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    86
lemma (in sigma_algebra) sigma_le_less:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    87
  assumes M: "!!a::real. {w \<in> space M. f w \<le> a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    88
  shows "{w \<in> space M. f w < a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    89
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    90
  show ?thesis using Collect_less_le [of "space M" f "\<lambda>x. a"]
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    91
    by (auto simp add: countable_UN M) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    92
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    93
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    94
lemma (in sigma_algebra) sigma_less_ge:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    95
  assumes M: "!!a::real. {w \<in> space M. f w < a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    96
  shows "{w \<in> space M. a \<le> f w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    97
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    98
  have "{w \<in> space M. a \<le> f w} = space M - {w \<in> space M. f w < a}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    99
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   100
  thus ?thesis using M
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   101
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   102
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   103
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   104
lemma (in sigma_algebra) sigma_ge_gr:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   105
  assumes M: "!!a::real. {w \<in> space M. a \<le> f w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   106
  shows "{w \<in> space M. a < f w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   107
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   108
  show ?thesis using Collect_less_le [of "space M" "\<lambda>x. a" f]
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   109
    by (auto simp add: countable_UN le_diff_eq M) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   110
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   111
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   112
lemma (in sigma_algebra) sigma_gr_le:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   113
  assumes M: "!!a::real. {w \<in> space M. a < f w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   114
  shows "{w \<in> space M. f w \<le> a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   115
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   116
  have "{w \<in> space M. f w \<le> a} = space M - {w \<in> space M. a < f w}" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   117
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   118
  thus ?thesis
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   119
    by (simp add: M compl_sets)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   120
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   121
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   122
lemma (in measure_space) borel_measurable_gr_iff:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   123
   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   124
proof (auto simp add: borel_measurable_le_iff sigma_gr_le) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   125
  fix u
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   126
  assume M: "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   127
  have "{w \<in> space M. u < f w} = space M - {w \<in> space M. f w \<le> u}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   128
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   129
  thus "{w \<in> space M. u < f w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   130
    by (force simp add: compl_sets countable_UN M)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   131
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   132
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   133
lemma (in measure_space) borel_measurable_less_iff:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   134
   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   135
proof (auto simp add: borel_measurable_le_iff sigma_le_less) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   136
  fix u
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   137
  assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   138
  have "{w \<in> space M. f w \<le> u} = space M - {w \<in> space M. u < f w}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   139
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   140
  thus "{w \<in> space M. f w \<le> u} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   141
    using Collect_less_le [of "space M" "\<lambda>x. u" f] 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   142
    by (force simp add: compl_sets countable_UN le_diff_eq sigma_less_ge M)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   143
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   144
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   145
lemma (in measure_space) borel_measurable_ge_iff:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   146
   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   147
proof (auto simp add: borel_measurable_less_iff sigma_le_less sigma_ge_gr sigma_gr_le) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   148
  fix u
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   149
  assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   150
  have "{w \<in> space M. u \<le> f w} = space M - {w \<in> space M. f w < u}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   151
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   152
  thus "{w \<in> space M. u \<le> f w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   153
    by (force simp add: compl_sets countable_UN M)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   154
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   155
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   156
lemma (in measure_space) affine_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   157
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   158
  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   159
proof (cases rule: linorder_cases [of b 0])
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   160
  case equal thus ?thesis
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   161
    by (simp add: borel_measurable_const)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   162
next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   163
  case less
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   164
    {
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   165
      fix w c
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   166
      have "a + g w * b \<le> c \<longleftrightarrow> g w * b \<le> c - a"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   167
        by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   168
      also have "... \<longleftrightarrow> (c-a)/b \<le> g w" using less
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   169
        by (metis divide_le_eq less less_asym)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   170
      finally have "a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   171
    }
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   172
    hence "\<And>w c. a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   173
    thus ?thesis using less g
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   174
      by (simp add: borel_measurable_ge_iff [of g]) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   175
         (simp add: borel_measurable_le_iff)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   176
next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   177
  case greater
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   178
    hence 0: "\<And>x c. (g x * b \<le> c - a) \<longleftrightarrow> (g x \<le> (c - a) / b)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   179
      by (metis mult_imp_le_div_pos le_divide_eq) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   180
    have 1: "\<And>x c. (a + g x * b \<le> c) \<longleftrightarrow> (g x * b \<le> c - a)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   181
      by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   182
    from greater g
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   183
    show ?thesis
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   184
      by (simp add: borel_measurable_le_iff 0 1) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   185
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   186
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   187
definition
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   188
  nat_to_rat_surj :: "nat \<Rightarrow> rat" where
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   189
 "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   190
                       in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   191
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   192
lemma nat_to_rat_surj: "surj nat_to_rat_surj"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   193
proof (auto simp add: surj_def nat_to_rat_surj_def) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   194
  fix y
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   195
  show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   196
  proof (cases y)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   197
    case (Fract a b)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   198
      obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   199
        by (metis surj_def) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   200
      obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   201
        by (metis surj_def)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   202
      obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   203
        by (metis surj_def)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   204
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   205
      from Fract i j n show ?thesis
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   206
        by (metis prod.cases prod_case_split)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   207
  qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   208
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   209
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   210
lemma rats_enumeration: "\<rat> = range (of_rat o nat_to_rat_surj)" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   211
  using nat_to_rat_surj
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   212
  by (auto simp add: image_def surj_def) (metis Rats_cases) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   213
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   214
lemma (in measure_space) borel_measurable_less_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   215
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   216
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   217
  shows "{w \<in> space M. f w < g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   218
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   219
  have "{w \<in> space M. f w < g w} =
33536
fd28b7399f2b eliminated hard tabulators;
wenzelm
parents: 33535
diff changeset
   220
        (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   221
    by (auto simp add: Rats_dense_in_real)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   222
  thus ?thesis using f g 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   223
    by (simp add: borel_measurable_less_iff [of f]  
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   224
                  borel_measurable_gr_iff [of g]) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   225
       (blast intro: gen_countable_UN [OF rats_enumeration])
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   226
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   227
 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   228
lemma (in measure_space) borel_measurable_leq_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   229
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   230
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   231
  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   232
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   233
  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   234
    by auto 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   235
  thus ?thesis using f g 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   236
    by (simp add: borel_measurable_less_borel_measurable compl_sets)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   237
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   238
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   239
lemma (in measure_space) borel_measurable_eq_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   240
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   241
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   242
  shows "{w \<in> space M. f w = g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   243
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   244
  have "{w \<in> space M. f w = g w} =
33536
fd28b7399f2b eliminated hard tabulators;
wenzelm
parents: 33535
diff changeset
   245
        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   246
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   247
  thus ?thesis using f g 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   248
    by (simp add: borel_measurable_leq_borel_measurable Int) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   249
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   250
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   251
lemma (in measure_space) borel_measurable_neq_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   252
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   253
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   254
  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   255
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   256
  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   257
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   258
  thus ?thesis using f g 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   259
    by (simp add: borel_measurable_eq_borel_measurable compl_sets) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   260
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   261
33535
b233f48a4d3d fixed some inappropriate names
paulson
parents: 33533
diff changeset
   262
lemma (in measure_space) borel_measurable_add_borel_measurable:
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   263
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   264
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   265
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   266
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   267
  have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * -1 \<le> f w}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   268
    by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   269
  have "!!a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   270
    by (rule affine_borel_measurable [OF g]) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   271
  hence "!!a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   272
    by (rule borel_measurable_leq_borel_measurable) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   273
  hence "!!a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   274
    by (simp add: 1) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   275
  thus ?thesis
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   276
    by (simp add: borel_measurable_ge_iff) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   277
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   278
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   279
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   280
lemma (in measure_space) borel_measurable_square:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   281
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   282
  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   283
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   284
  {
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   285
    fix a
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   286
    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   287
    proof (cases rule: linorder_cases [of a 0])
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   288
      case less
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   289
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   290
        by auto (metis less order_le_less_trans power2_less_0)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   291
      also have "... \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   292
        by (rule empty_sets) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   293
      finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   294
    next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   295
      case equal
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   296
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   297
             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   298
        by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   299
      also have "... \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   300
        apply (insert f) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   301
        apply (rule Int) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   302
        apply (simp add: borel_measurable_le_iff)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   303
        apply (simp add: borel_measurable_ge_iff)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   304
        done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   305
      finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   306
    next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   307
      case greater
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   308
      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   309
        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   310
                  real_sqrt_le_iff real_sqrt_power)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   311
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   312
             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   313
        using greater by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   314
      also have "... \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   315
        apply (insert f) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   316
        apply (rule Int) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   317
        apply (simp add: borel_measurable_ge_iff)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   318
        apply (simp add: borel_measurable_le_iff)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   319
        done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   320
      finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   321
    qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   322
  }
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   323
  thus ?thesis by (auto simp add: borel_measurable_le_iff) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   324
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   325
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   326
lemma times_eq_sum_squares:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   327
   fixes x::real
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   328
   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   329
by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   330
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   331
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   332
lemma (in measure_space) borel_measurable_uminus_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   333
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   334
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   335
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   336
  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   337
    by simp
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   338
  also have "... \<in> borel_measurable M" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   339
    by (fast intro: affine_borel_measurable g) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   340
  finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   341
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   342
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   343
lemma (in measure_space) borel_measurable_times_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   344
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   345
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   346
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   347
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   348
  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   349
    by (fast intro: affine_borel_measurable borel_measurable_square 
33535
b233f48a4d3d fixed some inappropriate names
paulson
parents: 33533
diff changeset
   350
                    borel_measurable_add_borel_measurable f g) 
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   351
  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   352
        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   353
    by (simp add: minus_divide_right)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   354
  also have "... \<in> borel_measurable M" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   355
    by (fast intro: affine_borel_measurable borel_measurable_square 
33535
b233f48a4d3d fixed some inappropriate names
paulson
parents: 33533
diff changeset
   356
                    borel_measurable_add_borel_measurable 
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   357
                    borel_measurable_uminus_borel_measurable f g)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   358
  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   359
  show ?thesis
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   360
    apply (simp add: times_eq_sum_squares real_diff_def) 
33535
b233f48a4d3d fixed some inappropriate names
paulson
parents: 33533
diff changeset
   361
    using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   362
    done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   363
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   364
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   365
lemma (in measure_space) borel_measurable_diff_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   366
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   367
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   368
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   369
unfolding real_diff_def
33535
b233f48a4d3d fixed some inappropriate names
paulson
parents: 33533
diff changeset
   370
  by (fast intro: borel_measurable_add_borel_measurable 
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   371
                  borel_measurable_uminus_borel_measurable f g)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   372
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   373
lemma (in measure_space) borel_measurable_setsum_borel_measurable:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   374
  assumes s: "finite s"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   375
  shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   376
proof (induct s)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   377
  case empty
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   378
  thus ?case
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   379
    by (simp add: borel_measurable_const)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   380
next
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   381
  case (insert x s)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   382
  thus ?case
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   383
    by (auto simp add: borel_measurable_add_borel_measurable) 
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   384
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   385
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   386
lemma (in measure_space) borel_measurable_cong:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   387
  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   388
  shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   389
using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   390
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   391
lemma (in measure_space) borel_measurable_inverse:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   392
  assumes "f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   393
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   394
  unfolding borel_measurable_ge_iff
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   395
proof (safe, rule linorder_cases)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   396
  fix a :: real assume "0 < a"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   397
  { fix w
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   398
    from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   399
      by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   400
                linorder_not_le real_le_refl real_le_trans real_less_def
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   401
                xt1(7) zero_less_divide_1_iff) }
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   402
  hence "{w \<in> space M. a \<le> inverse (f w)} =
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   403
    {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   404
  with Int assms[unfolded borel_measurable_gr_iff]
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   405
    assms[unfolded borel_measurable_le_iff]
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   406
  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   407
next
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   408
  fix a :: real assume "0 = a"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   409
  { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   410
      unfolding `0 = a`[symmetric] by auto }
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   411
  thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   412
    using assms[unfolded borel_measurable_ge_iff] by simp
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   413
next
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   414
  fix a :: real assume "a < 0"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   415
  { fix w
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   416
    from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   417
      apply (cases "0 \<le> f w")
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   418
      apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   419
                   zero_le_divide_1_iff)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   420
      apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   421
                   linorder_not_le real_le_refl real_le_trans)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   422
      done }
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   423
  hence "{w \<in> space M. a \<le> inverse (f w)} =
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   424
    {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   425
  with Un assms[unfolded borel_measurable_ge_iff]
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   426
    assms[unfolded borel_measurable_le_iff]
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   427
  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   428
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   429
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   430
lemma (in measure_space) borel_measurable_divide:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   431
  assumes "f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   432
  and "g \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   433
  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   434
  unfolding field_divide_inverse
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   435
  by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   436
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   437
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   438
section "Monotone convergence"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   439
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   440
definition mono_convergent where
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   441
  "mono_convergent u f s \<equiv>
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   442
        (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   443
        (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   444
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   445
definition "upclose f g x = max (f x) (g x)"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   446
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   447
primrec mon_upclose where
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   448
"mon_upclose 0 u = u 0" |
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   449
"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   450
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   451
lemma mono_convergentD:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   452
  assumes "mono_convergent u f s" and "x \<in> s"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   453
  shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   454
  using assms unfolding mono_convergent_def by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   455
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   456
lemma mono_convergentI:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   457
  assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   458
  assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   459
  shows "mono_convergent u f s"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   460
  using assms unfolding mono_convergent_def by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   461
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   462
lemma (in measure_space) mono_convergent_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   463
  assumes u: "!!n. u n \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   464
  assumes mc: "mono_convergent u f (space M)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   465
  shows "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   466
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   467
  {
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   468
    fix a
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   469
    have 1: "!!w. w \<in> space M & f w <= a \<longleftrightarrow> w \<in> space M & (\<forall>i. u i w <= a)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   470
      proof safe
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   471
        fix w i
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   472
        assume w: "w \<in> space M" and f: "f w \<le> a"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   473
        hence "u i w \<le> f w"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   474
          by (auto intro: SEQ.incseq_le
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   475
                   simp add: mc [unfolded mono_convergent_def])
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   476
        thus "u i w \<le> a" using f
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   477
          by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   478
      next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   479
        fix w 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   480
        assume w: "w \<in> space M" and u: "\<forall>i. u i w \<le> a"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   481
        thus "f w \<le> a"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   482
          by (metis LIMSEQ_le_const2 mc [unfolded mono_convergent_def])
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   483
      qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   484
    have "{w \<in> space M. f w \<le> a} = {w \<in> space M. (\<forall>i. u i w <= a)}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   485
      by (simp add: 1)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   486
    also have "... = (\<Inter>i. {w \<in> space M. u i w \<le> a})" 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   487
      by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   488
    also have "...  \<in> sets M" using u
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   489
      by (auto simp add: borel_measurable_le_iff intro: countable_INT) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   490
    finally have "{w \<in> space M. f w \<le> a} \<in> sets M" .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   491
  }
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   492
  thus ?thesis 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   493
    by (auto simp add: borel_measurable_le_iff) 
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   494
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   495
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   496
lemma mono_convergent_le:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   497
  assumes "mono_convergent u f s" and "t \<in> s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   498
  shows "u n t \<le> f t"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   499
using mono_convergentD[OF assms] by (auto intro!: incseq_le)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   500
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   501
lemma mon_upclose_ex:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   502
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   503
  shows "\<exists>n \<le> m. mon_upclose m u x = u n x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   504
proof (induct m)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   505
  case (Suc m)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   506
  then obtain n where "n \<le> m" and *: "mon_upclose m u x = u n x" by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   507
  thus ?case
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   508
  proof (cases "u n x \<le> u (Suc m) x")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   509
    case True with min_max.sup_absorb1 show ?thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   510
      by (auto simp: * upclose_def intro!: exI[of _ "Suc m"])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   511
  next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   512
    case False
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   513
     with min_max.sup_absorb2 `n \<le> m` show ?thesis
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   514
       by (auto simp: * upclose_def intro!: exI[of _ n] min_max.sup_absorb2)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   515
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   516
qed simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   517
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   518
lemma mon_upclose_all:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   519
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   520
  assumes "m \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   521
  shows "u m x \<le> mon_upclose n u x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   522
using assms proof (induct n)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   523
  case 0 thus ?case by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   524
next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   525
  case (Suc n)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   526
  show ?case
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   527
  proof (cases "m = Suc n")
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   528
    case True thus ?thesis by (simp add: upclose_def)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   529
  next
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   530
    case False
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   531
    hence "m \<le> n" using `m \<le> Suc n` by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   532
    from Suc.hyps[OF this]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   533
    show ?thesis by (auto simp: upclose_def intro!: min_max.le_supI2)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   534
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   535
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   536
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   537
lemma mono_convergent_limit:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   538
  fixes f :: "'a \<Rightarrow> real"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   539
  assumes "mono_convergent u f s" and "x \<in> s" and "0 < r"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   540
  shows "\<exists>N. \<forall>n\<ge>N. f x - u n x < r"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   541
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   542
  from LIMSEQ_D[OF mono_convergentD(2)[OF assms(1,2)] `0 < r`]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   543
  obtain N where "\<And>n. N \<le> n \<Longrightarrow> \<bar> u n x - f x \<bar> < r" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   544
  with mono_convergent_le[OF assms(1,2)] `0 < r`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   545
  show ?thesis by (auto intro!: exI[of _ N])
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   546
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   547
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   548
lemma mon_upclose_le_mono_convergent:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   549
  assumes mc: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s" and "x \<in> s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   550
  and "incseq (\<lambda>n. f n x)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   551
  shows "mon_upclose n (u n) x <= f n x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   552
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   553
  obtain m where *: "mon_upclose n (u n) x = u n m x" and "m \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   554
    using mon_upclose_ex[of n "u n" x] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   555
  note this(1)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   556
  also have "u n m x \<le> f m x" using mono_convergent_le[OF assms(1,2)] .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   557
  also have "... \<le> f n x" using assms(3) `m \<le> n` unfolding incseq_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   558
  finally show ?thesis .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   559
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   560
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   561
lemma mon_upclose_mono_convergent:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   562
  assumes mc_u: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   563
  and mc_f: "mono_convergent f h s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   564
  shows "mono_convergent (\<lambda>n. mon_upclose n (u n)) h s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   565
proof (rule mono_convergentI)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   566
  fix x assume "x \<in> s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   567
  show "incseq (\<lambda>n. mon_upclose n (u n) x)" unfolding incseq_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   568
  proof safe
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   569
    fix m n :: nat assume "m \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   570
    obtain i where mon: "mon_upclose m (u m) x = u m i x" and "i \<le> m"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   571
      using mon_upclose_ex[of m "u m" x] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   572
    hence "i \<le> n" using `m \<le> n` by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   573
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   574
    note mon
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   575
    also have "u m i x \<le> u n i x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   576
      using mono_convergentD(1)[OF mc_u `x \<in> s`] `m \<le> n`
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   577
      unfolding incseq_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   578
    also have "u n i x \<le> mon_upclose n (u n) x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   579
      using mon_upclose_all[OF `i \<le> n`, of "u n" x] .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   580
    finally show "mon_upclose m (u m) x \<le> mon_upclose n (u n) x" .
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   581
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   583
  show "(\<lambda>i. mon_upclose i (u i) x) ----> h x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   584
  proof (rule LIMSEQ_I)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   585
    fix r :: real assume "0 < r"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   586
    hence "0 < r / 2" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   587
    from mono_convergent_limit[OF mc_f `x \<in> s` this]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   588
    obtain N where f_h: "\<And>n. N \<le> n \<Longrightarrow> h x - f n x < r / 2" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   589
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   590
    from mono_convergent_limit[OF mc_u `x \<in> s` `0 < r / 2`]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   591
    obtain N' where u_f: "\<And>n. N' \<le> n \<Longrightarrow> f N x - u n N x < r / 2" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   592
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   593
    show "\<exists>N. \<forall>n\<ge>N. norm (mon_upclose n (u n) x - h x) < r"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   594
    proof (rule exI[of _ "max N N'"], safe)
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   595
      fix n assume "max N N' \<le> n"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   596
      hence "N \<le> n" and "N' \<le> n" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   597
      hence "u n N x \<le> mon_upclose n (u n) x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   598
        using mon_upclose_all[of N n "u n" x] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   599
      moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   600
      from add_strict_mono[OF u_f[OF `N' \<le> n`] f_h[OF order_refl]]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   601
      have "h x - u n N x < r" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   602
      ultimately have "h x - mon_upclose n (u n) x < r" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   603
      moreover
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   604
      obtain i where "mon_upclose n (u n) x = u n i x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   605
        using mon_upclose_ex[of n "u n"] by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   606
      with mono_convergent_le[OF mc_u `x \<in> s`, of n i]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   607
           mono_convergent_le[OF mc_f `x \<in> s`, of i]
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   608
      have "mon_upclose n (u n) x \<le> h x" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   609
      ultimately
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   610
      show "norm (mon_upclose n (u n) x - h x) < r" by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   611
     qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   612
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   613
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   614
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   615
lemma mono_conv_outgrow:
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   616
  assumes "incseq x" "x ----> y" "z < y"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   617
  shows "\<exists>b. \<forall> a \<ge> b. z < x a"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   618
using assms
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   619
proof -
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   620
  from assms have "y - z > 0" by simp
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   621
  hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   622
    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   623
    by simp
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   624
  have "\<forall>m. x m \<le> y" using incseq_le assms by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   625
  hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   626
    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   627
  from A B show ?thesis by auto
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   628
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   629
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   630
end