src/HOL/Probability/Lebesgue_Measure.thy
changeset 38656 d5d342611edb
child 40859 de0b30e6c2d2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Aug 23 19:35:57 2010 +0200
     1.3 @@ -0,0 +1,576 @@
     1.4 +
     1.5 +header {* Lebsegue measure *}
     1.6 +(*  Author:                     Robert Himmelmann, TU Muenchen *)
     1.7 +
     1.8 +theory Lebesgue_Measure
     1.9 +  imports Gauge_Measure Measure Lebesgue_Integration
    1.10 +begin
    1.11 +
    1.12 +subsection {* Various *}
    1.13 +
    1.14 +lemma seq_offset_iff:"f ----> l \<longleftrightarrow> (\<lambda>i. f (i + k)) ----> l"
    1.15 +  using seq_offset_rev seq_offset[of f l k] by auto
    1.16 +
    1.17 +lemma has_integral_disjoint_union: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
    1.18 +  assumes "(f has_integral i) s" "(f has_integral j) t" "s \<inter> t = {}"
    1.19 +  shows "(f has_integral (i + j)) (s \<union> t)"
    1.20 +  apply(rule has_integral_union[OF assms(1-2)]) unfolding assms by auto
    1.21 +
    1.22 +lemma lim_eq: assumes "\<forall>n>N. f n = g n" shows "(f ----> l) \<longleftrightarrow> (g ----> l)" using assms 
    1.23 +proof(induct N arbitrary: f g) case 0
    1.24 +  hence *:"\<And>n. f (Suc n) = g (Suc n)" by auto
    1.25 +  show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym])
    1.26 +    unfolding * ..
    1.27 +next case (Suc n)
    1.28 +  show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym])
    1.29 +    apply(rule Suc(1)) using Suc(2) by auto
    1.30 +qed
    1.31 +
    1.32 +subsection {* Standard Cubes *}
    1.33 +
    1.34 +definition cube where
    1.35 +  "cube (n::nat) \<equiv> {\<chi>\<chi> i. - real n .. (\<chi>\<chi> i. real n)::_::ordered_euclidean_space}"
    1.36 +
    1.37 +lemma cube_subset[intro]:"n\<le>N \<Longrightarrow> cube n \<subseteq> (cube N::'a::ordered_euclidean_space set)"
    1.38 +  apply(auto simp: eucl_le[where 'a='a] cube_def) apply(erule_tac[!] x=i in allE)+ by auto
    1.39 +
    1.40 +lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n"
    1.41 +  unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta'
    1.42 +proof- fix x::'a and i assume as:"x\<in>ball 0 (real n)" "i<DIM('a)"
    1.43 +  thus "- real n \<le> x $$ i" "real n \<ge> x $$ i"
    1.44 +    using component_le_norm[of x i] by(auto simp: dist_norm)
    1.45 +qed
    1.46 +
    1.47 +lemma mem_big_cube: obtains n where "x \<in> cube n"
    1.48 +proof- from real_arch_lt[of "norm x"] guess n ..
    1.49 +  thus ?thesis apply-apply(rule that[where n=n])
    1.50 +    apply(rule ball_subset_cube[unfolded subset_eq,rule_format])
    1.51 +    by (auto simp add:dist_norm)
    1.52 +qed
    1.53 +
    1.54 +lemma Union_inter_cube:"\<Union>{s \<inter> cube n |n. n \<in> UNIV} = s"
    1.55 +proof safe case goal1
    1.56 +  from mem_big_cube[of x] guess n . note n=this
    1.57 +  show ?case unfolding Union_iff apply(rule_tac x="s \<inter> cube n" in bexI)
    1.58 +    using n goal1 by auto
    1.59 +qed
    1.60 +
    1.61 +lemma gmeasurable_cube[intro]:"gmeasurable (cube n)"
    1.62 +  unfolding cube_def by auto
    1.63 +
    1.64 +lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set"
    1.65 +  assumes "gmeasurable (s \<inter> cube n)" shows "gmeasure (s \<inter> cube n) \<le> gmeasure (cube n::'a set)"
    1.66 +  apply(rule has_gmeasure_subset[of "s\<inter>cube n" _ "cube n"])
    1.67 +  unfolding has_gmeasure_measure[THEN sym] using assms by auto
    1.68 +
    1.69 +
    1.70 +subsection {* Measurability *}
    1.71 +
    1.72 +definition lmeasurable :: "('a::ordered_euclidean_space) set => bool" where
    1.73 +  "lmeasurable s \<equiv> (\<forall>n::nat. gmeasurable (s \<inter> cube n))"
    1.74 +
    1.75 +lemma lmeasurableD[dest]:assumes "lmeasurable s"
    1.76 +  shows "\<And>n. gmeasurable (s \<inter> cube n)"
    1.77 +  using assms unfolding lmeasurable_def by auto
    1.78 +
    1.79 +lemma measurable_imp_lmeasurable: assumes"gmeasurable s"
    1.80 +  shows "lmeasurable s" unfolding lmeasurable_def cube_def 
    1.81 +  using assms gmeasurable_interval by auto
    1.82 +
    1.83 +lemma lmeasurable_empty[intro]: "lmeasurable {}"
    1.84 +  using gmeasurable_empty apply- apply(drule_tac measurable_imp_lmeasurable) .
    1.85 +
    1.86 +lemma lmeasurable_union[intro]: assumes "lmeasurable s" "lmeasurable t"
    1.87 +  shows "lmeasurable (s \<union> t)"
    1.88 +  using assms unfolding lmeasurable_def Int_Un_distrib2 
    1.89 +  by(auto intro:gmeasurable_union)
    1.90 +
    1.91 +lemma lmeasurable_countable_unions_strong:
    1.92 +  fixes s::"nat => 'a::ordered_euclidean_space set"
    1.93 +  assumes "\<And>n::nat. lmeasurable(s n)"
    1.94 +  shows "lmeasurable(\<Union>{ s(n) |n. n \<in> UNIV })"
    1.95 +  unfolding lmeasurable_def
    1.96 +proof fix n::nat
    1.97 +  have *:"\<Union>{s n |n. n \<in> UNIV} \<inter> cube n = \<Union>{s k \<inter> cube n |k. k \<in> UNIV}" by auto
    1.98 +  show "gmeasurable (\<Union>{s n |n. n \<in> UNIV} \<inter> cube n)" unfolding *
    1.99 +    apply(rule gmeasurable_countable_unions_strong)
   1.100 +    apply(rule assms[unfolded lmeasurable_def,rule_format])
   1.101 +  proof- fix k::nat
   1.102 +    show "gmeasure (\<Union>{s ka \<inter> cube n |ka. ka \<le> k}) \<le> gmeasure (cube n::'a set)"
   1.103 +      apply(rule measure_subset) apply(rule gmeasurable_finite_unions)
   1.104 +      using assms(1)[unfolded lmeasurable_def] by auto
   1.105 +  qed
   1.106 +qed
   1.107 +
   1.108 +lemma lmeasurable_inter[intro]: fixes s::"'a :: ordered_euclidean_space set"
   1.109 +  assumes "lmeasurable s" "lmeasurable t" shows "lmeasurable (s \<inter> t)"
   1.110 +  unfolding lmeasurable_def
   1.111 +proof fix n::nat
   1.112 +  have *:"s \<inter> t \<inter> cube n = (s \<inter> cube n) \<inter> (t \<inter> cube n)" by auto
   1.113 +  show "gmeasurable (s \<inter> t \<inter> cube n)"
   1.114 +    using assms unfolding lmeasurable_def *
   1.115 +    using gmeasurable_inter[of "s \<inter> cube n" "t \<inter> cube n"] by auto
   1.116 +qed
   1.117 +
   1.118 +lemma lmeasurable_complement[intro]: assumes "lmeasurable s"
   1.119 +  shows "lmeasurable (UNIV - s)"
   1.120 +  unfolding lmeasurable_def
   1.121 +proof fix n::nat
   1.122 +  have *:"(UNIV - s) \<inter> cube n = cube n - (s \<inter> cube n)" by auto
   1.123 +  show "gmeasurable ((UNIV - s) \<inter> cube n)" unfolding * 
   1.124 +    apply(rule gmeasurable_diff) using assms unfolding lmeasurable_def by auto
   1.125 +qed
   1.126 +
   1.127 +lemma lmeasurable_finite_unions:
   1.128 +  assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> lmeasurable s"
   1.129 +  shows "lmeasurable (\<Union> f)" unfolding lmeasurable_def
   1.130 +proof fix n::nat have *:"(\<Union>f \<inter> cube n) = \<Union>{x \<inter> cube n | x . x\<in>f}" by auto
   1.131 +  show "gmeasurable (\<Union>f \<inter> cube n)" unfolding *
   1.132 +    apply(rule gmeasurable_finite_unions) unfolding simple_image 
   1.133 +    using assms unfolding lmeasurable_def by auto
   1.134 +qed
   1.135 +
   1.136 +lemma negligible_imp_lmeasurable[dest]: fixes s::"'a::ordered_euclidean_space set"
   1.137 +  assumes "negligible s" shows "lmeasurable s"
   1.138 +  unfolding lmeasurable_def
   1.139 +proof case goal1
   1.140 +  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)"
   1.141 +    unfolding indicator_def_raw by auto
   1.142 +  note assms[unfolded negligible_def,rule_format,of "(\<chi>\<chi> i. - real n)::'a" "\<chi>\<chi> i. real n"]
   1.143 +  thus ?case apply-apply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def
   1.144 +    apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric]
   1.145 +    apply(subst has_integral_restrict_univ[THEN sym]) unfolding * .
   1.146 +qed
   1.147 +
   1.148 +
   1.149 +section {* The Lebesgue Measure *}
   1.150 +
   1.151 +definition has_lmeasure (infixr "has'_lmeasure" 80) where
   1.152 +  "s has_lmeasure m \<equiv> lmeasurable s \<and> ((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially"
   1.153 +
   1.154 +lemma has_lmeasureD: assumes "s has_lmeasure m"
   1.155 +  shows "lmeasurable s" "gmeasurable (s \<inter> cube n)"
   1.156 +  "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially"
   1.157 +  using assms unfolding has_lmeasure_def lmeasurable_def by auto
   1.158 +
   1.159 +lemma has_lmeasureI: assumes "lmeasurable s" "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially"
   1.160 +  shows "s has_lmeasure m" using assms unfolding has_lmeasure_def by auto
   1.161 +
   1.162 +definition lmeasure where
   1.163 +  "lmeasure s \<equiv> SOME m. s has_lmeasure m"
   1.164 +
   1.165 +lemma has_lmeasure_has_gmeasure: assumes "s has_lmeasure (Real m)" "m\<ge>0"
   1.166 +  shows "s has_gmeasure m"
   1.167 +proof- note s = has_lmeasureD[OF assms(1)]
   1.168 +  have *:"(\<lambda>n. (gmeasure (s \<inter> cube n))) ----> m"
   1.169 +    using s(3) apply(subst (asm) lim_Real) using s(2) assms(2) by auto
   1.170 +
   1.171 +  have "(\<lambda>x. if x \<in> s then 1 else (0::real)) integrable_on UNIV \<and>
   1.172 +    (\<lambda>k. integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)))
   1.173 +    ----> integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)"
   1.174 +  proof(rule monotone_convergence_increasing)
   1.175 +    have "\<forall>n. gmeasure (s \<inter> cube n) \<le> m" apply(rule ccontr) unfolding not_all not_le
   1.176 +    proof(erule exE) fix k assume k:"m < gmeasure (s \<inter> cube k)"
   1.177 +      hence "gmeasure (s \<inter> cube k) - m > 0" by auto
   1.178 +      from *[unfolded Lim_sequentially,rule_format,OF this] guess N ..
   1.179 +      note this[unfolded dist_real_def,rule_format,of "N + k"]
   1.180 +      moreover have "gmeasure (s \<inter> cube (N + k)) \<ge> gmeasure (s \<inter> cube k)" apply-
   1.181 +        apply(rule measure_subset) prefer 3 using s(2) 
   1.182 +        using cube_subset[of k "N + k"] by auto
   1.183 +      ultimately show False by auto
   1.184 +    qed
   1.185 +    thus *:"bounded {integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)) |k. True}" 
   1.186 +      unfolding integral_measure_univ[OF s(2)] bounded_def apply-
   1.187 +      apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def
   1.188 +      by (auto simp: measure_pos_le)
   1.189 +
   1.190 +    show "\<forall>k. (\<lambda>x. if x \<in> s \<inter> cube k then (1::real) else 0) integrable_on UNIV"
   1.191 +      unfolding integrable_restrict_univ
   1.192 +      using s(2) unfolding gmeasurable_def has_gmeasure_def by auto
   1.193 +    have *:"\<And>n. n \<le> Suc n" by auto
   1.194 +    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))"
   1.195 +      using cube_subset[OF *] by fastsimp
   1.196 +    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))"
   1.197 +      unfolding Lim_sequentially 
   1.198 +    proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this
   1.199 +      show ?case apply(rule_tac x=N in exI)
   1.200 +      proof safe case goal1
   1.201 +        have "x \<in> cube n" using cube_subset[OF goal1] N
   1.202 +          using ball_subset_cube[of N] by(auto simp: dist_norm) 
   1.203 +        thus ?case using `e>0` by auto
   1.204 +      qed
   1.205 +    qed
   1.206 +  qed note ** = conjunctD2[OF this]
   1.207 +  hence *:"m = integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" apply-
   1.208 +    apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s(2)] using * .
   1.209 +  show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto
   1.210 +qed
   1.211 +
   1.212 +lemma has_lmeasure_unique: "s has_lmeasure m1 \<Longrightarrow> s has_lmeasure m2 \<Longrightarrow> m1 = m2"
   1.213 +  unfolding has_lmeasure_def apply(rule Lim_unique) using trivial_limit_sequentially by auto
   1.214 +
   1.215 +lemma lmeasure_unique[intro]: assumes "A has_lmeasure m" shows "lmeasure A = m"
   1.216 +  using assms unfolding lmeasure_def lmeasurable_def apply-
   1.217 +  apply(rule some_equality) defer apply(rule has_lmeasure_unique) by auto
   1.218 +
   1.219 +lemma glmeasurable_finite: assumes "lmeasurable s" "lmeasure s \<noteq> \<omega>" 
   1.220 +  shows "gmeasurable s"
   1.221 +proof-  have "\<exists>B. \<forall>n. gmeasure (s \<inter> cube n) \<le> B"
   1.222 +  proof(rule ccontr) case goal1
   1.223 +    note as = this[unfolded not_ex not_all not_le]
   1.224 +    have "s has_lmeasure \<omega>" apply- apply(rule has_lmeasureI[OF assms(1)])
   1.225 +      unfolding Lim_omega
   1.226 +    proof fix B::real
   1.227 +      from as[rule_format,of B] guess N .. note N = this
   1.228 +      have "\<And>n. N \<le> n \<Longrightarrow> B \<le> gmeasure (s \<inter> cube n)"
   1.229 +        apply(rule order_trans[where y="gmeasure (s \<inter> cube N)"]) defer
   1.230 +        apply(rule measure_subset) prefer 3
   1.231 +        using cube_subset N assms(1)[unfolded lmeasurable_def] by auto
   1.232 +      thus "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (s \<inter> cube n))" apply-
   1.233 +        apply(subst Real_max') apply(rule_tac x=N in exI,safe)
   1.234 +        unfolding pinfreal_less_eq apply(subst if_P) by auto
   1.235 +    qed note lmeasure_unique[OF this]
   1.236 +    thus False using assms(2) by auto
   1.237 +  qed then guess B .. note B=this
   1.238 +
   1.239 +  show ?thesis apply(rule gmeasurable_nested_unions[of "\<lambda>n. s \<inter> cube n",
   1.240 +    unfolded Union_inter_cube,THEN conjunct1, where B1=B])
   1.241 +  proof- fix n::nat
   1.242 +    show " gmeasurable (s \<inter> cube n)" using assms by auto
   1.243 +    show "gmeasure (s \<inter> cube n) \<le> B" using B by auto
   1.244 +    show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)"
   1.245 +      by (rule Int_mono) (simp_all add: cube_subset)
   1.246 +  qed
   1.247 +qed
   1.248 +
   1.249 +lemma lmeasure_empty[intro]:"lmeasure {} = 0"
   1.250 +  apply(rule lmeasure_unique)
   1.251 +  unfolding has_lmeasure_def by auto
   1.252 +
   1.253 +lemma lmeasurableI[dest]:"s has_lmeasure m \<Longrightarrow> lmeasurable s"
   1.254 +  unfolding has_lmeasure_def by auto
   1.255 +
   1.256 +lemma has_gmeasure_has_lmeasure: assumes "s has_gmeasure m"
   1.257 +  shows "s has_lmeasure (Real m)"
   1.258 +proof- have gmea:"gmeasurable s" using assms by auto
   1.259 +  have m:"m \<ge> 0" using assms by auto
   1.260 +  have *:"m = gmeasure (\<Union>{s \<inter> cube n |n. n \<in> UNIV})" unfolding Union_inter_cube
   1.261 +    using assms by(rule measure_unique[THEN sym])
   1.262 +  show ?thesis unfolding has_lmeasure_def
   1.263 +    apply(rule,rule measurable_imp_lmeasurable[OF gmea])
   1.264 +    apply(subst lim_Real) apply(rule,rule,rule m) unfolding *
   1.265 +    apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"])
   1.266 +  proof- fix n::nat show *:"gmeasurable (s \<inter> cube n)"
   1.267 +      using gmeasurable_inter[OF gmea gmeasurable_cube] .
   1.268 +    show "gmeasure (s \<inter> cube n) \<le> gmeasure s" apply(rule measure_subset)
   1.269 +      apply(rule * gmea)+ by auto
   1.270 +    show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" using cube_subset[of n "Suc n"] by auto
   1.271 +  qed
   1.272 +qed    
   1.273 +    
   1.274 +lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)"
   1.275 +proof- note has_gmeasure_measureI[OF assms]
   1.276 +  note has_gmeasure_has_lmeasure[OF this]
   1.277 +  thus ?thesis by(rule lmeasure_unique)
   1.278 +qed
   1.279 +
   1.280 +lemma has_lmeasure_lmeasure: "lmeasurable s \<longleftrightarrow> s has_lmeasure (lmeasure s)" (is "?l = ?r")
   1.281 +proof assume ?l let ?f = "\<lambda>n. Real (gmeasure (s \<inter> cube n))"
   1.282 +  have "\<forall>n m. n\<ge>m \<longrightarrow> ?f n \<ge> ?f m" unfolding pinfreal_less_eq apply safe
   1.283 +    apply(subst if_P) defer apply(rule measure_subset) prefer 3
   1.284 +    apply(drule cube_subset) using `?l` by auto
   1.285 +  from lim_pinfreal_increasing[OF this] guess l . note l=this
   1.286 +  hence "s has_lmeasure l" using `?l` apply-apply(rule has_lmeasureI) by auto
   1.287 +  thus ?r using lmeasure_unique by auto
   1.288 +next assume ?r thus ?l unfolding has_lmeasure_def by auto
   1.289 +qed
   1.290 +
   1.291 +lemma lmeasure_subset[dest]: assumes "lmeasurable s" "lmeasurable t" "s \<subseteq> t"
   1.292 +  shows "lmeasure s \<le> lmeasure t"
   1.293 +proof(cases "lmeasure t = \<omega>")
   1.294 +  case False have som:"lmeasure s \<noteq> \<omega>"
   1.295 +  proof(rule ccontr,unfold not_not) assume as:"lmeasure s = \<omega>"
   1.296 +    have "t has_lmeasure \<omega>" using assms(2) apply(rule has_lmeasureI)
   1.297 +      unfolding Lim_omega
   1.298 +    proof case goal1
   1.299 +      note assms(1)[unfolded has_lmeasure_lmeasure]
   1.300 +      note has_lmeasureD(3)[OF this,unfolded as Lim_omega,rule_format,of B]
   1.301 +      then guess N .. note N = this
   1.302 +      show ?case apply(rule_tac x=N in exI) apply safe
   1.303 +        apply(rule order_trans) apply(rule N[rule_format],assumption)
   1.304 +        unfolding pinfreal_less_eq apply(subst if_P)defer
   1.305 +        apply(rule measure_subset) using assms by auto
   1.306 +    qed
   1.307 +    thus False using lmeasure_unique False by auto
   1.308 +  qed
   1.309 +
   1.310 +  note assms(1)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this]
   1.311 +  hence "(\<lambda>n. Real (gmeasure (s \<inter> cube n))) ----> Real (real (lmeasure s))"
   1.312 +    unfolding Real_real'[OF som] .
   1.313 +  hence l1:"(\<lambda>n. gmeasure (s \<inter> cube n)) ----> real (lmeasure s)"
   1.314 +    apply-apply(subst(asm) lim_Real) by auto
   1.315 +
   1.316 +  note assms(2)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this]
   1.317 +  hence "(\<lambda>n. Real (gmeasure (t \<inter> cube n))) ----> Real (real (lmeasure t))"
   1.318 +    unfolding Real_real'[OF False] .
   1.319 +  hence l2:"(\<lambda>n. gmeasure (t \<inter> cube n)) ----> real (lmeasure t)"
   1.320 +    apply-apply(subst(asm) lim_Real) by auto
   1.321 +
   1.322 +  have "real (lmeasure s) \<le> real (lmeasure t)" apply(rule LIMSEQ_le[OF l1 l2])
   1.323 +    apply(rule_tac x=0 in exI,safe) apply(rule measure_subset) using assms by auto
   1.324 +  hence "Real (real (lmeasure s)) \<le> Real (real (lmeasure t))"
   1.325 +    unfolding pinfreal_less_eq by auto
   1.326 +  thus ?thesis unfolding Real_real'[OF som] Real_real'[OF False] .
   1.327 +qed auto
   1.328 +
   1.329 +lemma has_lmeasure_negligible_unions_image:
   1.330 +  assumes "finite s" "\<And>x. x \<in> s ==> lmeasurable(f x)"
   1.331 +  "\<And>x y. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x \<noteq> y \<Longrightarrow> negligible((f x) \<inter> (f y))"
   1.332 +  shows "(\<Union> (f ` s)) has_lmeasure (setsum (\<lambda>x. lmeasure(f x)) s)"
   1.333 +  unfolding has_lmeasure_def
   1.334 +proof show lmeaf:"lmeasurable (\<Union>f ` s)" apply(rule lmeasurable_finite_unions)
   1.335 +    using assms(1-2) by auto
   1.336 +  show "(\<lambda>n. Real (gmeasure (\<Union>f ` s \<inter> cube n))) ----> (\<Sum>x\<in>s. lmeasure (f x))" (is ?l)
   1.337 +  proof(cases "\<exists>x\<in>s. lmeasure (f x) = \<omega>")
   1.338 +    case False hence *:"(\<Sum>x\<in>s. lmeasure (f x)) \<noteq> \<omega>" apply-
   1.339 +      apply(rule setsum_neq_omega) using assms(1) by auto
   1.340 +    have gmea:"\<And>x. x\<in>s \<Longrightarrow> gmeasurable (f x)" apply(rule glmeasurable_finite) using False assms(2) by auto
   1.341 +    have "(\<Sum>x\<in>s. lmeasure (f x)) = (\<Sum>x\<in>s. Real (gmeasure (f x)))" apply(rule setsum_cong2)
   1.342 +      apply(rule gmeasure_lmeasure) using False assms(2) gmea by auto
   1.343 +    also have "... = Real (\<Sum>x\<in>s. (gmeasure (f x)))" apply(rule setsum_Real) by auto
   1.344 +    finally have sum:"(\<Sum>x\<in>s. lmeasure (f x)) = Real (\<Sum>x\<in>s. gmeasure (f x))" .
   1.345 +    have sum_0:"(\<Sum>x\<in>s. gmeasure (f x)) \<ge> 0" apply(rule setsum_nonneg) by auto
   1.346 +    have int_un:"\<Union>f ` s has_gmeasure (\<Sum>x\<in>s. gmeasure (f x))"
   1.347 +      apply(rule has_gmeasure_negligible_unions_image) using assms gmea by auto
   1.348 +
   1.349 +    have unun:"\<Union>{\<Union>f ` s \<inter> cube n |n. n \<in> UNIV} = \<Union>f ` s" unfolding simple_image 
   1.350 +    proof safe fix x y assume as:"x \<in> f y" "y \<in> s"
   1.351 +      from mem_big_cube[of x] guess n . note n=this
   1.352 +      thus "x \<in> \<Union>range (\<lambda>n. \<Union>f ` s \<inter> cube n)" unfolding Union_iff
   1.353 +        apply-apply(rule_tac x="\<Union>f ` s \<inter> cube n" in bexI) using as by auto
   1.354 +    qed
   1.355 +    show ?l apply(subst Real_real'[OF *,THEN sym])apply(subst lim_Real) 
   1.356 +      apply rule apply rule unfolding sum real_Real if_P[OF sum_0] apply(rule sum_0)
   1.357 +      unfolding measure_unique[OF int_un,THEN sym] apply(subst(2) unun[THEN sym])
   1.358 +      apply(rule has_gmeasure_nested_unions[THEN conjunct2])
   1.359 +    proof- fix n::nat
   1.360 +      show *:"gmeasurable (\<Union>f ` s \<inter> cube n)" using lmeaf unfolding lmeasurable_def by auto
   1.361 +      thus "gmeasure (\<Union>f ` s \<inter> cube n) \<le> gmeasure (\<Union>f ` s)"
   1.362 +        apply(rule measure_subset) using int_un by auto
   1.363 +      show "\<Union>f ` s \<inter> cube n \<subseteq> \<Union>f ` s \<inter> cube (Suc n)"
   1.364 +        using cube_subset[of n "Suc n"] by auto
   1.365 +    qed
   1.366 +
   1.367 +  next case True then guess X .. note X=this
   1.368 +    hence sum:"(\<Sum>x\<in>s. lmeasure (f x)) = \<omega>" using setsum_\<omega>[THEN iffD2, of s] assms by fastsimp
   1.369 +    show ?l unfolding sum Lim_omega
   1.370 +    proof fix B::real
   1.371 +      have Xm:"(f X) has_lmeasure \<omega>" using X by (metis assms(2) has_lmeasure_lmeasure)
   1.372 +      note this[unfolded has_lmeasure_def,THEN conjunct2, unfolded Lim_omega]
   1.373 +      from this[rule_format,of B] guess N .. note N=this[rule_format]
   1.374 +      show "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (\<Union>f ` s \<inter> cube n))"
   1.375 +        apply(rule_tac x=N in exI)
   1.376 +      proof safe case goal1 show ?case apply(rule order_trans[OF N[OF goal1]])
   1.377 +          unfolding pinfreal_less_eq apply(subst if_P) defer
   1.378 +          apply(rule measure_subset) using has_lmeasureD(2)[OF Xm]
   1.379 +          using lmeaf unfolding lmeasurable_def using X(1) by auto
   1.380 +      qed qed qed qed
   1.381 +
   1.382 +lemma has_lmeasure_negligible_unions:
   1.383 +  assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)"
   1.384 +  "\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> negligible (s\<inter>t)"
   1.385 +  shows "(\<Union> f) has_lmeasure (setsum m f)"
   1.386 +proof- have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2)
   1.387 +    apply(subst lmeasure_unique[OF assms(2)]) by auto
   1.388 +  show ?thesis unfolding *
   1.389 +    apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply])
   1.390 +    using assms by auto
   1.391 +qed
   1.392 +
   1.393 +lemma has_lmeasure_disjoint_unions:
   1.394 +  assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)"
   1.395 +  "\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> s \<inter> t = {}"
   1.396 +  shows "(\<Union> f) has_lmeasure (setsum m f)"
   1.397 +proof- have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2)
   1.398 +    apply(subst lmeasure_unique[OF assms(2)]) by auto
   1.399 +  show ?thesis unfolding *
   1.400 +    apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply])
   1.401 +    using assms by auto
   1.402 +qed
   1.403 +
   1.404 +lemma has_lmeasure_nested_unions:
   1.405 +  assumes "\<And>n. lmeasurable(s n)" "\<And>n. s(n) \<subseteq> s(Suc n)"
   1.406 +  shows "lmeasurable(\<Union> { s n | n. n \<in> UNIV }) \<and>
   1.407 +  (\<lambda>n. lmeasure(s n)) ----> lmeasure(\<Union> { s(n) | n. n \<in> UNIV })" (is "?mea \<and> ?lim")
   1.408 +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
   1.409 +  have 3:"\<And>n. \<forall>m\<ge>n. s n \<subseteq> s m" apply(rule transitive_stepwise_le) using assms(2) by auto
   1.410 +  have mea:"?mea" unfolding lmeasurable_def cube apply rule 
   1.411 +    apply(rule_tac B1="gmeasure (cube n)" in has_gmeasure_nested_unions[THEN conjunct1])
   1.412 +    prefer 3 apply rule using assms(1) unfolding lmeasurable_def
   1.413 +    by(auto intro!:assms(2)[unfolded subset_eq,rule_format])
   1.414 +  show ?thesis apply(rule,rule mea)
   1.415 +  proof(cases "lmeasure(\<Union> { s(n) | n. n \<in> UNIV }) = \<omega>")
   1.416 +    case True show ?lim unfolding True Lim_omega
   1.417 +    proof(rule ccontr) case goal1 note this[unfolded not_all not_ex]
   1.418 +      hence "\<exists>B. \<forall>n. \<exists>m\<ge>n. Real B > lmeasure (s m)" by(auto simp add:not_le)
   1.419 +      from this guess B .. note B=this[rule_format]
   1.420 +
   1.421 +      have "\<forall>n. gmeasurable (s n) \<and> gmeasure (s n) \<le> max B 0" 
   1.422 +      proof safe fix n::nat from B[of n] guess m .. note m=this
   1.423 +        hence *:"lmeasure (s n) < Real B" apply-apply(rule le_less_trans)
   1.424 +          apply(rule lmeasure_subset[OF assms(1,1)]) apply(rule 3[rule_format]) by auto
   1.425 +        thus **:"gmeasurable (s n)" apply-apply(rule glmeasurable_finite[OF assms(1)]) by auto
   1.426 +        thus "gmeasure (s n) \<le> max B 0"  using * unfolding gmeasure_lmeasure[OF **] Real_max'[of B]
   1.427 +          unfolding pinfreal_less apply- apply(subst(asm) if_P) by auto
   1.428 +      qed
   1.429 +      hence "\<And>n. gmeasurable (s n)" "\<And>n. gmeasure (s n) \<le> max B 0" by auto
   1.430 +      note g = conjunctD2[OF has_gmeasure_nested_unions[of s, OF this assms(2)]]
   1.431 +      show False using True unfolding gmeasure_lmeasure[OF g(1)] by auto
   1.432 +    qed
   1.433 +  next let ?B = "lmeasure (\<Union>{s n |n. n \<in> UNIV})"
   1.434 +    case False note gmea_lim = glmeasurable_finite[OF mea this]
   1.435 +    have ls:"\<And>n. lmeasure (s n) \<le> lmeasure (\<Union>{s n |n. n \<in> UNIV})"
   1.436 +      apply(rule lmeasure_subset) using assms(1) mea by auto
   1.437 +    have "\<And>n. lmeasure (s n) \<noteq> \<omega>"
   1.438 +    proof(rule ccontr,safe) case goal1
   1.439 +      show False using False ls[of n] unfolding goal1 by auto
   1.440 +    qed
   1.441 +    note gmea = glmeasurable_finite[OF assms(1) this]
   1.442 +
   1.443 +    have "\<And>n. gmeasure (s n) \<le> real ?B"  unfolding gmeasure_lmeasure[OF gmea_lim]
   1.444 +      unfolding real_Real apply(subst if_P,rule) apply(rule measure_subset)
   1.445 +      using gmea gmea_lim by auto
   1.446 +    note has_gmeasure_nested_unions[of s, OF gmea this assms(2)]
   1.447 +    thus ?lim unfolding gmeasure_lmeasure[OF gmea] gmeasure_lmeasure[OF gmea_lim]
   1.448 +      apply-apply(subst lim_Real) by auto
   1.449 +  qed
   1.450 +qed
   1.451 +
   1.452 +lemma has_lmeasure_countable_negligible_unions: 
   1.453 +  assumes "\<And>n. lmeasurable(s n)" "\<And>m n. m \<noteq> n \<Longrightarrow> negligible(s m \<inter> s n)"
   1.454 +  shows "(\<lambda>m. setsum (\<lambda>n. lmeasure(s n)) {..m}) ----> (lmeasure(\<Union> { s(n) |n. n \<in> UNIV }))"
   1.455 +proof- have *:"\<And>n. (\<Union> (s ` {0..n})) has_lmeasure (setsum (\<lambda>k. lmeasure(s k)) {0..n})"
   1.456 +    apply(rule has_lmeasure_negligible_unions_image) using assms by auto
   1.457 +  have **:"(\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV}) = (\<Union>{s n |n. n \<in> UNIV})" unfolding simple_image by fastsimp
   1.458 +  have "lmeasurable (\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV}) \<and>
   1.459 +    (\<lambda>n. lmeasure (\<Union>(s ` {0..n}))) ----> lmeasure (\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV})"
   1.460 +    apply(rule has_lmeasure_nested_unions) apply(rule has_lmeasureD(1)[OF *])
   1.461 +    apply(rule Union_mono,rule image_mono) by auto
   1.462 +  note lem = conjunctD2[OF this,unfolded **] 
   1.463 +  show ?thesis using lem(2) unfolding lmeasure_unique[OF *] unfolding atLeast0AtMost .
   1.464 +qed
   1.465 +
   1.466 +lemma lmeasure_eq_0: assumes "negligible s" shows "lmeasure s = 0"
   1.467 +proof- note mea=negligible_imp_lmeasurable[OF assms]
   1.468 +  have *:"\<And>n. (gmeasure (s \<inter> cube n)) = 0" 
   1.469 +    unfolding gmeasurable_measure_eq_0[OF mea[unfolded lmeasurable_def,rule_format]]
   1.470 +    using assms by auto
   1.471 +  show ?thesis
   1.472 +    apply(rule lmeasure_unique) unfolding has_lmeasure_def
   1.473 +    apply(rule,rule mea) unfolding * by auto
   1.474 +qed
   1.475 +
   1.476 +lemma negligible_img_gmeasurable: fixes s::"'a::ordered_euclidean_space set"
   1.477 +  assumes "negligible s" shows "gmeasurable s"
   1.478 +  apply(rule glmeasurable_finite)
   1.479 +  using lmeasure_eq_0[OF assms] negligible_imp_lmeasurable[OF assms] by auto
   1.480 +
   1.481 +
   1.482 +
   1.483 +
   1.484 +section {* Instantiation of _::euclidean_space as measure_space *}
   1.485 +
   1.486 +definition lebesgue_space :: "'a::ordered_euclidean_space algebra" where
   1.487 +  "lebesgue_space = \<lparr> space = UNIV, sets = lmeasurable \<rparr>"
   1.488 +
   1.489 +lemma lebesgue_measurable[simp]:"A \<in> sets lebesgue_space \<longleftrightarrow> lmeasurable A"
   1.490 +  unfolding lebesgue_space_def by(auto simp: mem_def)
   1.491 +
   1.492 +lemma mem_gmeasurable[simp]: "A \<in> gmeasurable \<longleftrightarrow> gmeasurable A"
   1.493 +  unfolding mem_def ..
   1.494 +
   1.495 +interpretation lebesgue: measure_space lebesgue_space lmeasure
   1.496 +  apply(intro_locales) unfolding measure_space_axioms_def countably_additive_def
   1.497 +  unfolding sigma_algebra_axioms_def algebra_def
   1.498 +  unfolding lebesgue_measurable
   1.499 +proof safe
   1.500 +  fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space" "disjoint_family A"
   1.501 +    "lmeasurable (UNION UNIV A)"
   1.502 +  have *:"UNION UNIV A = \<Union>range A" by auto
   1.503 +  show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (UNION UNIV A)" 
   1.504 +    unfolding psuminf_def apply(rule SUP_Lim_pinfreal)
   1.505 +  proof- fix n m::nat assume mn:"m\<le>n"
   1.506 +    have *:"\<And>m. (\<Sum>n<m. lmeasure (A n)) = lmeasure (\<Union>A ` {..<m})"
   1.507 +      apply(subst lmeasure_unique[OF has_lmeasure_negligible_unions[where m=lmeasure]])
   1.508 +      apply(rule finite_imageI) apply rule apply(subst has_lmeasure_lmeasure[THEN sym])
   1.509 +    proof- fix m::nat
   1.510 +      show "(\<Sum>n<m. lmeasure (A n)) = setsum lmeasure (A ` {..<m})"
   1.511 +        apply(subst setsum_reindex_nonzero) unfolding o_def apply rule
   1.512 +        apply(rule lmeasure_eq_0) using as(2) unfolding disjoint_family_on_def
   1.513 +        apply(erule_tac x=x in ballE,safe,erule_tac x=y in ballE) by auto
   1.514 +    next fix m s assume "s \<in> A ` {..<m}"
   1.515 +      hence "s \<in> range A" by auto thus "lmeasurable s" using as(1) by fastsimp
   1.516 +    next fix m s t assume st:"s  \<in> A ` {..<m}" "t \<in> A ` {..<m}" "s \<noteq> t"
   1.517 +      from st(1-2) guess sa ta unfolding image_iff apply-by(erule bexE)+ note a=this
   1.518 +      from st(3) have "sa \<noteq> ta" unfolding a by auto
   1.519 +      thus "negligible (s \<inter> t)" 
   1.520 +        using as(2) unfolding disjoint_family_on_def a
   1.521 +        apply(erule_tac x=sa in ballE,erule_tac x=ta in ballE) by auto
   1.522 +    qed
   1.523 +
   1.524 +    have "\<And>m. lmeasurable (\<Union>A ` {..<m})"  apply(rule lmeasurable_finite_unions)
   1.525 +      apply(rule finite_imageI,rule) using as(1) by fastsimp
   1.526 +    from this this show "(\<Sum>n<m. lmeasure (A n)) \<le> (\<Sum>n<n. lmeasure (A n))" unfolding *
   1.527 +      apply(rule lmeasure_subset) apply(rule Union_mono) apply(rule image_mono) using mn by auto
   1.528 +    
   1.529 +  next have *:"UNION UNIV A = \<Union>{A n |n. n \<in> UNIV}" by auto
   1.530 +    show "(\<lambda>n. \<Sum>n<n. lmeasure (A n)) ----> lmeasure (UNION UNIV A)"
   1.531 +      apply(rule LIMSEQ_imp_Suc) unfolding lessThan_Suc_atMost *
   1.532 +      apply(rule has_lmeasure_countable_negligible_unions)
   1.533 +      using as unfolding disjoint_family_on_def subset_eq by auto
   1.534 +  qed
   1.535 +
   1.536 +next show "lmeasure {} = 0" by auto
   1.537 +next fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space"
   1.538 +  have *:"UNION UNIV A = (\<Union>{A n |n. n \<in> UNIV})" unfolding simple_image by auto
   1.539 +  show "lmeasurable (UNION UNIV A)" unfolding * using as unfolding subset_eq
   1.540 +    using lmeasurable_countable_unions_strong[of A] by auto
   1.541 +qed(auto simp: lebesgue_space_def mem_def)
   1.542 +
   1.543 +
   1.544 +
   1.545 +lemma lmeasurbale_closed_interval[intro]:
   1.546 +  "lmeasurable {a..b::'a::ordered_euclidean_space}"
   1.547 +  unfolding lmeasurable_def cube_def inter_interval by auto
   1.548 +
   1.549 +lemma space_lebesgue_space[simp]:"space lebesgue_space = UNIV"
   1.550 +  unfolding lebesgue_space_def by auto
   1.551 +
   1.552 +abbreviation "gintegral \<equiv> Integration.integral"
   1.553 +
   1.554 +lemma lebesgue_simple_function_indicator:
   1.555 +  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
   1.556 +  assumes f:"lebesgue.simple_function f"
   1.557 +  shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
   1.558 +  apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto
   1.559 +
   1.560 +lemma lmeasure_gmeasure:
   1.561 +  "gmeasurable s \<Longrightarrow> gmeasure s = real (lmeasure s)"
   1.562 +  apply(subst gmeasure_lmeasure) by auto
   1.563 +
   1.564 +lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \<noteq> \<omega>"
   1.565 +  using gmeasure_lmeasure[OF assms] by auto
   1.566 +
   1.567 +lemma negligible_lmeasure: assumes "lmeasurable s"
   1.568 +  shows "lmeasure s = 0 \<longleftrightarrow> negligible s" (is "?l = ?r")
   1.569 +proof assume ?l
   1.570 +  hence *:"gmeasurable s" using glmeasurable_finite[of s] assms by auto
   1.571 +  show ?r unfolding gmeasurable_measure_eq_0[THEN sym,OF *]
   1.572 +    unfolding lmeasure_gmeasure[OF *] using `?l` by auto
   1.573 +next assume ?r
   1.574 +  note g=negligible_img_gmeasurable[OF this] and measure_eq_0[OF this]
   1.575 +  hence "real (lmeasure s) = 0" using lmeasure_gmeasure[of s] by auto
   1.576 +  thus ?l using lmeasure_finite[OF g] apply- apply(rule real_0_imp_eq_0) by auto
   1.577 +qed
   1.578 +
   1.579 +end