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