src/HOL/Probability/Lebesgue_Measure.thy
author hoelzl
Mon, 23 Aug 2010 19:35:57 +0200
changeset 38656 d5d342611edb
child 40859 de0b30e6c2d2
permissions -rw-r--r--
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     2
header {* Lebsegue measure *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     3
(*  Author:                     Robert Himmelmann, TU Muenchen *)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     4
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     5
theory Lebesgue_Measure
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     6
  imports Gauge_Measure Measure Lebesgue_Integration
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     7
begin
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     8
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     9
subsection {* Various *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    10
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    11
lemma seq_offset_iff:"f ----> l \<longleftrightarrow> (\<lambda>i. f (i + k)) ----> l"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    12
  using seq_offset_rev seq_offset[of f l k] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    13
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    14
lemma has_integral_disjoint_union: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    15
  assumes "(f has_integral i) s" "(f has_integral j) t" "s \<inter> t = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    16
  shows "(f has_integral (i + j)) (s \<union> t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    17
  apply(rule has_integral_union[OF assms(1-2)]) unfolding assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    18
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    19
lemma lim_eq: assumes "\<forall>n>N. f n = g n" shows "(f ----> l) \<longleftrightarrow> (g ----> l)" using assms 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    20
proof(induct N arbitrary: f g) case 0
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    21
  hence *:"\<And>n. f (Suc n) = g (Suc n)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    22
  show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    23
    unfolding * ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    24
next case (Suc n)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    25
  show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    26
    apply(rule Suc(1)) using Suc(2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    27
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    28
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    29
subsection {* Standard Cubes *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    30
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    31
definition cube where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    32
  "cube (n::nat) \<equiv> {\<chi>\<chi> i. - real n .. (\<chi>\<chi> i. real n)::_::ordered_euclidean_space}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    33
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    34
lemma cube_subset[intro]:"n\<le>N \<Longrightarrow> cube n \<subseteq> (cube N::'a::ordered_euclidean_space set)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    35
  apply(auto simp: eucl_le[where 'a='a] cube_def) apply(erule_tac[!] x=i in allE)+ by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    36
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    37
lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    38
  unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta'
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    39
proof- fix x::'a and i assume as:"x\<in>ball 0 (real n)" "i<DIM('a)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    40
  thus "- real n \<le> x $$ i" "real n \<ge> x $$ i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    41
    using component_le_norm[of x i] by(auto simp: dist_norm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    42
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    43
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    44
lemma mem_big_cube: obtains n where "x \<in> cube n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    45
proof- from real_arch_lt[of "norm x"] guess n ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    46
  thus ?thesis apply-apply(rule that[where n=n])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    47
    apply(rule ball_subset_cube[unfolded subset_eq,rule_format])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    48
    by (auto simp add:dist_norm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    49
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    50
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    51
lemma Union_inter_cube:"\<Union>{s \<inter> cube n |n. n \<in> UNIV} = s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    52
proof safe case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    53
  from mem_big_cube[of x] guess n . note n=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    54
  show ?case unfolding Union_iff apply(rule_tac x="s \<inter> cube n" in bexI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    55
    using n goal1 by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    56
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    57
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    58
lemma gmeasurable_cube[intro]:"gmeasurable (cube n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    59
  unfolding cube_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    60
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    61
lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    62
  assumes "gmeasurable (s \<inter> cube n)" shows "gmeasure (s \<inter> cube n) \<le> gmeasure (cube n::'a set)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    63
  apply(rule has_gmeasure_subset[of "s\<inter>cube n" _ "cube n"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    64
  unfolding has_gmeasure_measure[THEN sym] using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    65
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    66
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    67
subsection {* Measurability *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    68
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    69
definition lmeasurable :: "('a::ordered_euclidean_space) set => bool" where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    70
  "lmeasurable s \<equiv> (\<forall>n::nat. gmeasurable (s \<inter> cube n))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    71
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    72
lemma lmeasurableD[dest]:assumes "lmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    73
  shows "\<And>n. gmeasurable (s \<inter> cube n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    74
  using assms unfolding lmeasurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    75
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    76
lemma measurable_imp_lmeasurable: assumes"gmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    77
  shows "lmeasurable s" unfolding lmeasurable_def cube_def 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    78
  using assms gmeasurable_interval by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    79
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    80
lemma lmeasurable_empty[intro]: "lmeasurable {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    81
  using gmeasurable_empty apply- apply(drule_tac measurable_imp_lmeasurable) .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    82
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    83
lemma lmeasurable_union[intro]: assumes "lmeasurable s" "lmeasurable t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    84
  shows "lmeasurable (s \<union> t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    85
  using assms unfolding lmeasurable_def Int_Un_distrib2 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    86
  by(auto intro:gmeasurable_union)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    87
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    88
lemma lmeasurable_countable_unions_strong:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    89
  fixes s::"nat => 'a::ordered_euclidean_space set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    90
  assumes "\<And>n::nat. lmeasurable(s n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    91
  shows "lmeasurable(\<Union>{ s(n) |n. n \<in> UNIV })"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    92
  unfolding lmeasurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    93
proof fix n::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    94
  have *:"\<Union>{s n |n. n \<in> UNIV} \<inter> cube n = \<Union>{s k \<inter> cube n |k. k \<in> UNIV}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    95
  show "gmeasurable (\<Union>{s n |n. n \<in> UNIV} \<inter> cube n)" unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    96
    apply(rule gmeasurable_countable_unions_strong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    97
    apply(rule assms[unfolded lmeasurable_def,rule_format])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    98
  proof- fix k::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    99
    show "gmeasure (\<Union>{s ka \<inter> cube n |ka. ka \<le> k}) \<le> gmeasure (cube n::'a set)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   100
      apply(rule measure_subset) apply(rule gmeasurable_finite_unions)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   101
      using assms(1)[unfolded lmeasurable_def] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   102
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   103
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   104
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   105
lemma lmeasurable_inter[intro]: fixes s::"'a :: ordered_euclidean_space set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   106
  assumes "lmeasurable s" "lmeasurable t" shows "lmeasurable (s \<inter> t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   107
  unfolding lmeasurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   108
proof fix n::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   109
  have *:"s \<inter> t \<inter> cube n = (s \<inter> cube n) \<inter> (t \<inter> cube n)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   110
  show "gmeasurable (s \<inter> t \<inter> cube n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   111
    using assms unfolding lmeasurable_def *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   112
    using gmeasurable_inter[of "s \<inter> cube n" "t \<inter> cube n"] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   113
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   114
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   115
lemma lmeasurable_complement[intro]: assumes "lmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   116
  shows "lmeasurable (UNIV - s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   117
  unfolding lmeasurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   118
proof fix n::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   119
  have *:"(UNIV - s) \<inter> cube n = cube n - (s \<inter> cube n)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   120
  show "gmeasurable ((UNIV - s) \<inter> cube n)" unfolding * 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   121
    apply(rule gmeasurable_diff) using assms unfolding lmeasurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   122
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   123
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   124
lemma lmeasurable_finite_unions:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   125
  assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> lmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   126
  shows "lmeasurable (\<Union> f)" unfolding lmeasurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   127
proof fix n::nat have *:"(\<Union>f \<inter> cube n) = \<Union>{x \<inter> cube n | x . x\<in>f}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   128
  show "gmeasurable (\<Union>f \<inter> cube n)" unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   129
    apply(rule gmeasurable_finite_unions) unfolding simple_image 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   130
    using assms unfolding lmeasurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   131
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   132
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   133
lemma negligible_imp_lmeasurable[dest]: fixes s::"'a::ordered_euclidean_space set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   134
  assumes "negligible s" shows "lmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   135
  unfolding lmeasurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   136
proof case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   137
  have *:"\<And>x. (if x \<in> cube n then indicator s x else 0) = (if x \<in> s \<inter> cube n then 1 else 0)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   138
    unfolding indicator_def_raw by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   139
  note assms[unfolded negligible_def,rule_format,of "(\<chi>\<chi> i. - real n)::'a" "\<chi>\<chi> i. real n"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   140
  thus ?case apply-apply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   141
    apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   142
    apply(subst has_integral_restrict_univ[THEN sym]) unfolding * .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   143
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   144
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   145
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   146
section {* The Lebesgue Measure *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   147
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   148
definition has_lmeasure (infixr "has'_lmeasure" 80) where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   149
  "s has_lmeasure m \<equiv> lmeasurable s \<and> ((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   150
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   151
lemma has_lmeasureD: assumes "s has_lmeasure m"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   152
  shows "lmeasurable s" "gmeasurable (s \<inter> cube n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   153
  "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   154
  using assms unfolding has_lmeasure_def lmeasurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   155
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   156
lemma has_lmeasureI: assumes "lmeasurable s" "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   157
  shows "s has_lmeasure m" using assms unfolding has_lmeasure_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   158
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   159
definition lmeasure where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   160
  "lmeasure s \<equiv> SOME m. s has_lmeasure m"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   161
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   162
lemma has_lmeasure_has_gmeasure: assumes "s has_lmeasure (Real m)" "m\<ge>0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   163
  shows "s has_gmeasure m"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   164
proof- note s = has_lmeasureD[OF assms(1)]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   165
  have *:"(\<lambda>n. (gmeasure (s \<inter> cube n))) ----> m"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   166
    using s(3) apply(subst (asm) lim_Real) using s(2) assms(2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   167
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   168
  have "(\<lambda>x. if x \<in> s then 1 else (0::real)) integrable_on UNIV \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   169
    (\<lambda>k. integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)))
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   170
    ----> integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   171
  proof(rule monotone_convergence_increasing)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   172
    have "\<forall>n. gmeasure (s \<inter> cube n) \<le> m" apply(rule ccontr) unfolding not_all not_le
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   173
    proof(erule exE) fix k assume k:"m < gmeasure (s \<inter> cube k)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   174
      hence "gmeasure (s \<inter> cube k) - m > 0" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   175
      from *[unfolded Lim_sequentially,rule_format,OF this] guess N ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   176
      note this[unfolded dist_real_def,rule_format,of "N + k"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   177
      moreover have "gmeasure (s \<inter> cube (N + k)) \<ge> gmeasure (s \<inter> cube k)" apply-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   178
        apply(rule measure_subset) prefer 3 using s(2) 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   179
        using cube_subset[of k "N + k"] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   180
      ultimately show False by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   181
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   182
    thus *:"bounded {integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)) |k. True}" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   183
      unfolding integral_measure_univ[OF s(2)] bounded_def apply-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   184
      apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   185
      by (auto simp: measure_pos_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   186
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   187
    show "\<forall>k. (\<lambda>x. if x \<in> s \<inter> cube k then (1::real) else 0) integrable_on UNIV"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   188
      unfolding integrable_restrict_univ
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   189
      using s(2) unfolding gmeasurable_def has_gmeasure_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   190
    have *:"\<And>n. n \<le> Suc n" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   191
    show "\<forall>k. \<forall>x\<in>UNIV. (if x \<in> s \<inter> cube k then 1 else 0) \<le> (if x \<in> s \<inter> cube (Suc k) then 1 else (0::real))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   192
      using cube_subset[OF *] by fastsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   193
    show "\<forall>x\<in>UNIV. (\<lambda>k. if x \<in> s \<inter> cube k then 1 else 0) ----> (if x \<in> s then 1 else (0::real))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   194
      unfolding Lim_sequentially 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   195
    proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   196
      show ?case apply(rule_tac x=N in exI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   197
      proof safe case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   198
        have "x \<in> cube n" using cube_subset[OF goal1] N
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   199
          using ball_subset_cube[of N] by(auto simp: dist_norm) 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   200
        thus ?case using `e>0` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   201
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   202
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   203
  qed note ** = conjunctD2[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   204
  hence *:"m = integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" apply-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   205
    apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s(2)] using * .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   206
  show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   207
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   208
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   209
lemma has_lmeasure_unique: "s has_lmeasure m1 \<Longrightarrow> s has_lmeasure m2 \<Longrightarrow> m1 = m2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   210
  unfolding has_lmeasure_def apply(rule Lim_unique) using trivial_limit_sequentially by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   211
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   212
lemma lmeasure_unique[intro]: assumes "A has_lmeasure m" shows "lmeasure A = m"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   213
  using assms unfolding lmeasure_def lmeasurable_def apply-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   214
  apply(rule some_equality) defer apply(rule has_lmeasure_unique) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   215
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   216
lemma glmeasurable_finite: assumes "lmeasurable s" "lmeasure s \<noteq> \<omega>" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   217
  shows "gmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   218
proof-  have "\<exists>B. \<forall>n. gmeasure (s \<inter> cube n) \<le> B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   219
  proof(rule ccontr) case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   220
    note as = this[unfolded not_ex not_all not_le]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   221
    have "s has_lmeasure \<omega>" apply- apply(rule has_lmeasureI[OF assms(1)])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   222
      unfolding Lim_omega
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   223
    proof fix B::real
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   224
      from as[rule_format,of B] guess N .. note N = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   225
      have "\<And>n. N \<le> n \<Longrightarrow> B \<le> gmeasure (s \<inter> cube n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   226
        apply(rule order_trans[where y="gmeasure (s \<inter> cube N)"]) defer
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   227
        apply(rule measure_subset) prefer 3
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   228
        using cube_subset N assms(1)[unfolded lmeasurable_def] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   229
      thus "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (s \<inter> cube n))" apply-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   230
        apply(subst Real_max') apply(rule_tac x=N in exI,safe)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   231
        unfolding pinfreal_less_eq apply(subst if_P) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   232
    qed note lmeasure_unique[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   233
    thus False using assms(2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   234
  qed then guess B .. note B=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   235
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   236
  show ?thesis apply(rule gmeasurable_nested_unions[of "\<lambda>n. s \<inter> cube n",
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   237
    unfolded Union_inter_cube,THEN conjunct1, where B1=B])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   238
  proof- fix n::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   239
    show " gmeasurable (s \<inter> cube n)" using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   240
    show "gmeasure (s \<inter> cube n) \<le> B" using B by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   241
    show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   242
      by (rule Int_mono) (simp_all add: cube_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   243
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   244
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   245
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   246
lemma lmeasure_empty[intro]:"lmeasure {} = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   247
  apply(rule lmeasure_unique)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   248
  unfolding has_lmeasure_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   249
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   250
lemma lmeasurableI[dest]:"s has_lmeasure m \<Longrightarrow> lmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   251
  unfolding has_lmeasure_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   252
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   253
lemma has_gmeasure_has_lmeasure: assumes "s has_gmeasure m"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   254
  shows "s has_lmeasure (Real m)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   255
proof- have gmea:"gmeasurable s" using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   256
  have m:"m \<ge> 0" using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   257
  have *:"m = gmeasure (\<Union>{s \<inter> cube n |n. n \<in> UNIV})" unfolding Union_inter_cube
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   258
    using assms by(rule measure_unique[THEN sym])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   259
  show ?thesis unfolding has_lmeasure_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   260
    apply(rule,rule measurable_imp_lmeasurable[OF gmea])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   261
    apply(subst lim_Real) apply(rule,rule,rule m) unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   262
    apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   263
  proof- fix n::nat show *:"gmeasurable (s \<inter> cube n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   264
      using gmeasurable_inter[OF gmea gmeasurable_cube] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   265
    show "gmeasure (s \<inter> cube n) \<le> gmeasure s" apply(rule measure_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   266
      apply(rule * gmea)+ by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   267
    show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" using cube_subset[of n "Suc n"] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   268
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   269
qed    
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   270
    
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   271
lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   272
proof- note has_gmeasure_measureI[OF assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   273
  note has_gmeasure_has_lmeasure[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   274
  thus ?thesis by(rule lmeasure_unique)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   275
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   276
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   277
lemma has_lmeasure_lmeasure: "lmeasurable s \<longleftrightarrow> s has_lmeasure (lmeasure s)" (is "?l = ?r")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   278
proof assume ?l let ?f = "\<lambda>n. Real (gmeasure (s \<inter> cube n))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   279
  have "\<forall>n m. n\<ge>m \<longrightarrow> ?f n \<ge> ?f m" unfolding pinfreal_less_eq apply safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   280
    apply(subst if_P) defer apply(rule measure_subset) prefer 3
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   281
    apply(drule cube_subset) using `?l` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   282
  from lim_pinfreal_increasing[OF this] guess l . note l=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   283
  hence "s has_lmeasure l" using `?l` apply-apply(rule has_lmeasureI) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   284
  thus ?r using lmeasure_unique by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   285
next assume ?r thus ?l unfolding has_lmeasure_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   286
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   287
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   288
lemma lmeasure_subset[dest]: assumes "lmeasurable s" "lmeasurable t" "s \<subseteq> t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   289
  shows "lmeasure s \<le> lmeasure t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   290
proof(cases "lmeasure t = \<omega>")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   291
  case False have som:"lmeasure s \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   292
  proof(rule ccontr,unfold not_not) assume as:"lmeasure s = \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   293
    have "t has_lmeasure \<omega>" using assms(2) apply(rule has_lmeasureI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   294
      unfolding Lim_omega
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   295
    proof case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   296
      note assms(1)[unfolded has_lmeasure_lmeasure]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   297
      note has_lmeasureD(3)[OF this,unfolded as Lim_omega,rule_format,of B]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   298
      then guess N .. note N = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   299
      show ?case apply(rule_tac x=N in exI) apply safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   300
        apply(rule order_trans) apply(rule N[rule_format],assumption)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   301
        unfolding pinfreal_less_eq apply(subst if_P)defer
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   302
        apply(rule measure_subset) using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   303
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   304
    thus False using lmeasure_unique False by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   305
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   306
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   307
  note assms(1)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   308
  hence "(\<lambda>n. Real (gmeasure (s \<inter> cube n))) ----> Real (real (lmeasure s))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   309
    unfolding Real_real'[OF som] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   310
  hence l1:"(\<lambda>n. gmeasure (s \<inter> cube n)) ----> real (lmeasure s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   311
    apply-apply(subst(asm) lim_Real) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   312
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   313
  note assms(2)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   314
  hence "(\<lambda>n. Real (gmeasure (t \<inter> cube n))) ----> Real (real (lmeasure t))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   315
    unfolding Real_real'[OF False] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   316
  hence l2:"(\<lambda>n. gmeasure (t \<inter> cube n)) ----> real (lmeasure t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   317
    apply-apply(subst(asm) lim_Real) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   318
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   319
  have "real (lmeasure s) \<le> real (lmeasure t)" apply(rule LIMSEQ_le[OF l1 l2])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   320
    apply(rule_tac x=0 in exI,safe) apply(rule measure_subset) using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   321
  hence "Real (real (lmeasure s)) \<le> Real (real (lmeasure t))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   322
    unfolding pinfreal_less_eq by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   323
  thus ?thesis unfolding Real_real'[OF som] Real_real'[OF False] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   324
qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   325
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   326
lemma has_lmeasure_negligible_unions_image:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   327
  assumes "finite s" "\<And>x. x \<in> s ==> lmeasurable(f x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   328
  "\<And>x y. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x \<noteq> y \<Longrightarrow> negligible((f x) \<inter> (f y))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   329
  shows "(\<Union> (f ` s)) has_lmeasure (setsum (\<lambda>x. lmeasure(f x)) s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   330
  unfolding has_lmeasure_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   331
proof show lmeaf:"lmeasurable (\<Union>f ` s)" apply(rule lmeasurable_finite_unions)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   332
    using assms(1-2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   333
  show "(\<lambda>n. Real (gmeasure (\<Union>f ` s \<inter> cube n))) ----> (\<Sum>x\<in>s. lmeasure (f x))" (is ?l)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   334
  proof(cases "\<exists>x\<in>s. lmeasure (f x) = \<omega>")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   335
    case False hence *:"(\<Sum>x\<in>s. lmeasure (f x)) \<noteq> \<omega>" apply-
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   336
      apply(rule setsum_neq_omega) using assms(1) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   337
    have gmea:"\<And>x. x\<in>s \<Longrightarrow> gmeasurable (f x)" apply(rule glmeasurable_finite) using False assms(2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   338
    have "(\<Sum>x\<in>s. lmeasure (f x)) = (\<Sum>x\<in>s. Real (gmeasure (f x)))" apply(rule setsum_cong2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   339
      apply(rule gmeasure_lmeasure) using False assms(2) gmea by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   340
    also have "... = Real (\<Sum>x\<in>s. (gmeasure (f x)))" apply(rule setsum_Real) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   341
    finally have sum:"(\<Sum>x\<in>s. lmeasure (f x)) = Real (\<Sum>x\<in>s. gmeasure (f x))" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   342
    have sum_0:"(\<Sum>x\<in>s. gmeasure (f x)) \<ge> 0" apply(rule setsum_nonneg) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   343
    have int_un:"\<Union>f ` s has_gmeasure (\<Sum>x\<in>s. gmeasure (f x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   344
      apply(rule has_gmeasure_negligible_unions_image) using assms gmea by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   345
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   346
    have unun:"\<Union>{\<Union>f ` s \<inter> cube n |n. n \<in> UNIV} = \<Union>f ` s" unfolding simple_image 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   347
    proof safe fix x y assume as:"x \<in> f y" "y \<in> s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   348
      from mem_big_cube[of x] guess n . note n=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   349
      thus "x \<in> \<Union>range (\<lambda>n. \<Union>f ` s \<inter> cube n)" unfolding Union_iff
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   350
        apply-apply(rule_tac x="\<Union>f ` s \<inter> cube n" in bexI) using as by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   351
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   352
    show ?l apply(subst Real_real'[OF *,THEN sym])apply(subst lim_Real) 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   353
      apply rule apply rule unfolding sum real_Real if_P[OF sum_0] apply(rule sum_0)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   354
      unfolding measure_unique[OF int_un,THEN sym] apply(subst(2) unun[THEN sym])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   355
      apply(rule has_gmeasure_nested_unions[THEN conjunct2])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   356
    proof- fix n::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   357
      show *:"gmeasurable (\<Union>f ` s \<inter> cube n)" using lmeaf unfolding lmeasurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   358
      thus "gmeasure (\<Union>f ` s \<inter> cube n) \<le> gmeasure (\<Union>f ` s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   359
        apply(rule measure_subset) using int_un by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   360
      show "\<Union>f ` s \<inter> cube n \<subseteq> \<Union>f ` s \<inter> cube (Suc n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   361
        using cube_subset[of n "Suc n"] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   362
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   363
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   364
  next case True then guess X .. note X=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   365
    hence sum:"(\<Sum>x\<in>s. lmeasure (f x)) = \<omega>" using setsum_\<omega>[THEN iffD2, of s] assms by fastsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   366
    show ?l unfolding sum Lim_omega
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   367
    proof fix B::real
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   368
      have Xm:"(f X) has_lmeasure \<omega>" using X by (metis assms(2) has_lmeasure_lmeasure)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   369
      note this[unfolded has_lmeasure_def,THEN conjunct2, unfolded Lim_omega]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   370
      from this[rule_format,of B] guess N .. note N=this[rule_format]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   371
      show "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (\<Union>f ` s \<inter> cube n))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   372
        apply(rule_tac x=N in exI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   373
      proof safe case goal1 show ?case apply(rule order_trans[OF N[OF goal1]])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   374
          unfolding pinfreal_less_eq apply(subst if_P) defer
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   375
          apply(rule measure_subset) using has_lmeasureD(2)[OF Xm]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   376
          using lmeaf unfolding lmeasurable_def using X(1) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   377
      qed qed qed qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   378
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   379
lemma has_lmeasure_negligible_unions:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   380
  assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   381
  "\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> negligible (s\<inter>t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   382
  shows "(\<Union> f) has_lmeasure (setsum m f)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   383
proof- have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   384
    apply(subst lmeasure_unique[OF assms(2)]) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   385
  show ?thesis unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   386
    apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   387
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   388
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   389
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   390
lemma has_lmeasure_disjoint_unions:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   391
  assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   392
  "\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> s \<inter> t = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   393
  shows "(\<Union> f) has_lmeasure (setsum m f)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   394
proof- have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   395
    apply(subst lmeasure_unique[OF assms(2)]) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   396
  show ?thesis unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   397
    apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   398
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   399
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   400
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   401
lemma has_lmeasure_nested_unions:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   402
  assumes "\<And>n. lmeasurable(s n)" "\<And>n. s(n) \<subseteq> s(Suc n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   403
  shows "lmeasurable(\<Union> { s n | n. n \<in> UNIV }) \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   404
  (\<lambda>n. lmeasure(s n)) ----> lmeasure(\<Union> { s(n) | n. n \<in> UNIV })" (is "?mea \<and> ?lim")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   405
proof- have cube:"\<And>m. \<Union> { s(n) | n. n \<in> UNIV } \<inter> cube m = \<Union> { s(n) \<inter> cube m | n. n \<in> UNIV }" by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   406
  have 3:"\<And>n. \<forall>m\<ge>n. s n \<subseteq> s m" apply(rule transitive_stepwise_le) using assms(2) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   407
  have mea:"?mea" unfolding lmeasurable_def cube apply rule 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   408
    apply(rule_tac B1="gmeasure (cube n)" in has_gmeasure_nested_unions[THEN conjunct1])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   409
    prefer 3 apply rule using assms(1) unfolding lmeasurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   410
    by(auto intro!:assms(2)[unfolded subset_eq,rule_format])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   411
  show ?thesis apply(rule,rule mea)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   412
  proof(cases "lmeasure(\<Union> { s(n) | n. n \<in> UNIV }) = \<omega>")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   413
    case True show ?lim unfolding True Lim_omega
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   414
    proof(rule ccontr) case goal1 note this[unfolded not_all not_ex]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   415
      hence "\<exists>B. \<forall>n. \<exists>m\<ge>n. Real B > lmeasure (s m)" by(auto simp add:not_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   416
      from this guess B .. note B=this[rule_format]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   417
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   418
      have "\<forall>n. gmeasurable (s n) \<and> gmeasure (s n) \<le> max B 0" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   419
      proof safe fix n::nat from B[of n] guess m .. note m=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   420
        hence *:"lmeasure (s n) < Real B" apply-apply(rule le_less_trans)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   421
          apply(rule lmeasure_subset[OF assms(1,1)]) apply(rule 3[rule_format]) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   422
        thus **:"gmeasurable (s n)" apply-apply(rule glmeasurable_finite[OF assms(1)]) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   423
        thus "gmeasure (s n) \<le> max B 0"  using * unfolding gmeasure_lmeasure[OF **] Real_max'[of B]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   424
          unfolding pinfreal_less apply- apply(subst(asm) if_P) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   425
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   426
      hence "\<And>n. gmeasurable (s n)" "\<And>n. gmeasure (s n) \<le> max B 0" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   427
      note g = conjunctD2[OF has_gmeasure_nested_unions[of s, OF this assms(2)]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   428
      show False using True unfolding gmeasure_lmeasure[OF g(1)] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   429
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   430
  next let ?B = "lmeasure (\<Union>{s n |n. n \<in> UNIV})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   431
    case False note gmea_lim = glmeasurable_finite[OF mea this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   432
    have ls:"\<And>n. lmeasure (s n) \<le> lmeasure (\<Union>{s n |n. n \<in> UNIV})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   433
      apply(rule lmeasure_subset) using assms(1) mea by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   434
    have "\<And>n. lmeasure (s n) \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   435
    proof(rule ccontr,safe) case goal1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   436
      show False using False ls[of n] unfolding goal1 by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   437
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   438
    note gmea = glmeasurable_finite[OF assms(1) this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   439
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   440
    have "\<And>n. gmeasure (s n) \<le> real ?B"  unfolding gmeasure_lmeasure[OF gmea_lim]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   441
      unfolding real_Real apply(subst if_P,rule) apply(rule measure_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   442
      using gmea gmea_lim by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   443
    note has_gmeasure_nested_unions[of s, OF gmea this assms(2)]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   444
    thus ?lim unfolding gmeasure_lmeasure[OF gmea] gmeasure_lmeasure[OF gmea_lim]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   445
      apply-apply(subst lim_Real) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   446
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   447
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   448
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   449
lemma has_lmeasure_countable_negligible_unions: 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   450
  assumes "\<And>n. lmeasurable(s n)" "\<And>m n. m \<noteq> n \<Longrightarrow> negligible(s m \<inter> s n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   451
  shows "(\<lambda>m. setsum (\<lambda>n. lmeasure(s n)) {..m}) ----> (lmeasure(\<Union> { s(n) |n. n \<in> UNIV }))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   452
proof- have *:"\<And>n. (\<Union> (s ` {0..n})) has_lmeasure (setsum (\<lambda>k. lmeasure(s k)) {0..n})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   453
    apply(rule has_lmeasure_negligible_unions_image) using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   454
  have **:"(\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV}) = (\<Union>{s n |n. n \<in> UNIV})" unfolding simple_image by fastsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   455
  have "lmeasurable (\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV}) \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   456
    (\<lambda>n. lmeasure (\<Union>(s ` {0..n}))) ----> lmeasure (\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   457
    apply(rule has_lmeasure_nested_unions) apply(rule has_lmeasureD(1)[OF *])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   458
    apply(rule Union_mono,rule image_mono) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   459
  note lem = conjunctD2[OF this,unfolded **] 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   460
  show ?thesis using lem(2) unfolding lmeasure_unique[OF *] unfolding atLeast0AtMost .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   461
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   462
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   463
lemma lmeasure_eq_0: assumes "negligible s" shows "lmeasure s = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   464
proof- note mea=negligible_imp_lmeasurable[OF assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   465
  have *:"\<And>n. (gmeasure (s \<inter> cube n)) = 0" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   466
    unfolding gmeasurable_measure_eq_0[OF mea[unfolded lmeasurable_def,rule_format]]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   467
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   468
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   469
    apply(rule lmeasure_unique) unfolding has_lmeasure_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   470
    apply(rule,rule mea) unfolding * by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   471
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   472
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   473
lemma negligible_img_gmeasurable: fixes s::"'a::ordered_euclidean_space set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   474
  assumes "negligible s" shows "gmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   475
  apply(rule glmeasurable_finite)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   476
  using lmeasure_eq_0[OF assms] negligible_imp_lmeasurable[OF assms] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   477
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   478
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   479
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   480
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   481
section {* Instantiation of _::euclidean_space as measure_space *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   482
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   483
definition lebesgue_space :: "'a::ordered_euclidean_space algebra" where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   484
  "lebesgue_space = \<lparr> space = UNIV, sets = lmeasurable \<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   485
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   486
lemma lebesgue_measurable[simp]:"A \<in> sets lebesgue_space \<longleftrightarrow> lmeasurable A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   487
  unfolding lebesgue_space_def by(auto simp: mem_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   488
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   489
lemma mem_gmeasurable[simp]: "A \<in> gmeasurable \<longleftrightarrow> gmeasurable A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   490
  unfolding mem_def ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   491
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   492
interpretation lebesgue: measure_space lebesgue_space lmeasure
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   493
  apply(intro_locales) unfolding measure_space_axioms_def countably_additive_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   494
  unfolding sigma_algebra_axioms_def algebra_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   495
  unfolding lebesgue_measurable
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   496
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   497
  fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space" "disjoint_family A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   498
    "lmeasurable (UNION UNIV A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   499
  have *:"UNION UNIV A = \<Union>range A" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   500
  show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (UNION UNIV A)" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   501
    unfolding psuminf_def apply(rule SUP_Lim_pinfreal)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   502
  proof- fix n m::nat assume mn:"m\<le>n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   503
    have *:"\<And>m. (\<Sum>n<m. lmeasure (A n)) = lmeasure (\<Union>A ` {..<m})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   504
      apply(subst lmeasure_unique[OF has_lmeasure_negligible_unions[where m=lmeasure]])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   505
      apply(rule finite_imageI) apply rule apply(subst has_lmeasure_lmeasure[THEN sym])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   506
    proof- fix m::nat
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   507
      show "(\<Sum>n<m. lmeasure (A n)) = setsum lmeasure (A ` {..<m})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   508
        apply(subst setsum_reindex_nonzero) unfolding o_def apply rule
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   509
        apply(rule lmeasure_eq_0) using as(2) unfolding disjoint_family_on_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   510
        apply(erule_tac x=x in ballE,safe,erule_tac x=y in ballE) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   511
    next fix m s assume "s \<in> A ` {..<m}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   512
      hence "s \<in> range A" by auto thus "lmeasurable s" using as(1) by fastsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   513
    next fix m s t assume st:"s  \<in> A ` {..<m}" "t \<in> A ` {..<m}" "s \<noteq> t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   514
      from st(1-2) guess sa ta unfolding image_iff apply-by(erule bexE)+ note a=this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   515
      from st(3) have "sa \<noteq> ta" unfolding a by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   516
      thus "negligible (s \<inter> t)" 
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   517
        using as(2) unfolding disjoint_family_on_def a
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   518
        apply(erule_tac x=sa in ballE,erule_tac x=ta in ballE) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   519
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   520
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   521
    have "\<And>m. lmeasurable (\<Union>A ` {..<m})"  apply(rule lmeasurable_finite_unions)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   522
      apply(rule finite_imageI,rule) using as(1) by fastsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   523
    from this this show "(\<Sum>n<m. lmeasure (A n)) \<le> (\<Sum>n<n. lmeasure (A n))" unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   524
      apply(rule lmeasure_subset) apply(rule Union_mono) apply(rule image_mono) using mn by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   525
    
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   526
  next have *:"UNION UNIV A = \<Union>{A n |n. n \<in> UNIV}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   527
    show "(\<lambda>n. \<Sum>n<n. lmeasure (A n)) ----> lmeasure (UNION UNIV A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   528
      apply(rule LIMSEQ_imp_Suc) unfolding lessThan_Suc_atMost *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   529
      apply(rule has_lmeasure_countable_negligible_unions)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   530
      using as unfolding disjoint_family_on_def subset_eq by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   531
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   532
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   533
next show "lmeasure {} = 0" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   534
next fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   535
  have *:"UNION UNIV A = (\<Union>{A n |n. n \<in> UNIV})" unfolding simple_image by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   536
  show "lmeasurable (UNION UNIV A)" unfolding * using as unfolding subset_eq
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   537
    using lmeasurable_countable_unions_strong[of A] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   538
qed(auto simp: lebesgue_space_def mem_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   539
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   540
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   541
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   542
lemma lmeasurbale_closed_interval[intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   543
  "lmeasurable {a..b::'a::ordered_euclidean_space}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   544
  unfolding lmeasurable_def cube_def inter_interval by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   545
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   546
lemma space_lebesgue_space[simp]:"space lebesgue_space = UNIV"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   547
  unfolding lebesgue_space_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   548
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   549
abbreviation "gintegral \<equiv> Integration.integral"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   550
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   551
lemma lebesgue_simple_function_indicator:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   552
  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   553
  assumes f:"lebesgue.simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   554
  shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   555
  apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   556
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   557
lemma lmeasure_gmeasure:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   558
  "gmeasurable s \<Longrightarrow> gmeasure s = real (lmeasure s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   559
  apply(subst gmeasure_lmeasure) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   560
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   561
lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   562
  using gmeasure_lmeasure[OF assms] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   563
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   564
lemma negligible_lmeasure: assumes "lmeasurable s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   565
  shows "lmeasure s = 0 \<longleftrightarrow> negligible s" (is "?l = ?r")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   566
proof assume ?l
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   567
  hence *:"gmeasurable s" using glmeasurable_finite[of s] assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   568
  show ?r unfolding gmeasurable_measure_eq_0[THEN sym,OF *]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   569
    unfolding lmeasure_gmeasure[OF *] using `?l` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   570
next assume ?r
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   571
  note g=negligible_img_gmeasurable[OF this] and measure_eq_0[OF this]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   572
  hence "real (lmeasure s) = 0" using lmeasure_gmeasure[of s] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   573
  thus ?l using lmeasure_finite[OF g] apply- apply(rule real_0_imp_eq_0) by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   574
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   575
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
   576
end