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 \ (\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 \ 'a::banach" ``` hoelzl@38656 ` 15` ``` assumes "(f has_integral i) s" "(f has_integral j) t" "s \ t = {}" ``` hoelzl@38656 ` 16` ``` shows "(f has_integral (i + j)) (s \ 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 "\n>N. f n = g n" shows "(f ----> l) \ (g ----> l)" using assms ``` hoelzl@38656 ` 20` ```proof(induct N arbitrary: f g) case 0 ``` hoelzl@38656 ` 21` ``` hence *:"\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) \ {\\ i. - real n .. (\\ i. real n)::_::ordered_euclidean_space}" ``` hoelzl@38656 ` 33` hoelzl@38656 ` 34` ```lemma cube_subset[intro]:"n\N \ cube n \ (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) \ 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\ball 0 (real n)" "i x \$\$ i" "real n \ 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 \ 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:"\{s \ cube n |n. n \ 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 \ 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 \ cube n)" shows "gmeasure (s \ cube n) \ gmeasure (cube n::'a set)" ``` hoelzl@38656 ` 63` ``` apply(rule has_gmeasure_subset[of "s\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 \ (\n::nat. gmeasurable (s \ cube n))" ``` hoelzl@38656 ` 71` hoelzl@38656 ` 72` ```lemma lmeasurableD[dest]:assumes "lmeasurable s" ``` hoelzl@38656 ` 73` ``` shows "\n. gmeasurable (s \ 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 \ 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 "\n::nat. lmeasurable(s n)" ``` hoelzl@38656 ` 91` ``` shows "lmeasurable(\{ s(n) |n. n \ UNIV })" ``` hoelzl@38656 ` 92` ``` unfolding lmeasurable_def ``` hoelzl@38656 ` 93` ```proof fix n::nat ``` hoelzl@38656 ` 94` ``` have *:"\{s n |n. n \ UNIV} \ cube n = \{s k \ cube n |k. k \ UNIV}" by auto ``` hoelzl@38656 ` 95` ``` show "gmeasurable (\{s n |n. n \ UNIV} \ 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 (\{s ka \ cube n |ka. ka \ k}) \ 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 \ t)" ``` hoelzl@38656 ` 107` ``` unfolding lmeasurable_def ``` hoelzl@38656 ` 108` ```proof fix n::nat ``` hoelzl@38656 ` 109` ``` have *:"s \ t \ cube n = (s \ cube n) \ (t \ cube n)" by auto ``` hoelzl@38656 ` 110` ``` show "gmeasurable (s \ t \ cube n)" ``` hoelzl@38656 ` 111` ``` using assms unfolding lmeasurable_def * ``` hoelzl@38656 ` 112` ``` using gmeasurable_inter[of "s \ cube n" "t \ 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) \ cube n = cube n - (s \ cube n)" by auto ``` hoelzl@38656 ` 120` ``` show "gmeasurable ((UNIV - s) \ 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" "\s. s \ f \ lmeasurable s" ``` hoelzl@38656 ` 126` ``` shows "lmeasurable (\ f)" unfolding lmeasurable_def ``` hoelzl@38656 ` 127` ```proof fix n::nat have *:"(\f \ cube n) = \{x \ cube n | x . x\f}" by auto ``` hoelzl@38656 ` 128` ``` show "gmeasurable (\f \ 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 *:"\x. (if x \ cube n then indicator s x else 0) = (if x \ s \ 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 "(\\ i. - real n)::'a" "\\ 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 \ lmeasurable s \ ((\n. Real (gmeasure (s \ 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 \ cube n)" ``` hoelzl@38656 ` 153` ``` "((\n. Real (gmeasure (s \ 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" "((\n. Real (gmeasure (s \ 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 \ SOME m. s has_lmeasure m" ``` hoelzl@38656 ` 161` hoelzl@38656 ` 162` ```lemma has_lmeasure_has_gmeasure: assumes "s has_lmeasure (Real m)" "m\0" ``` hoelzl@38656 ` 163` ``` shows "s has_gmeasure m" ``` hoelzl@38656 ` 164` ```proof- note s = has_lmeasureD[OF assms(1)] ``` hoelzl@38656 ` 165` ``` have *:"(\n. (gmeasure (s \ 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 "(\x. if x \ s then 1 else (0::real)) integrable_on UNIV \ ``` hoelzl@38656 ` 169` ``` (\k. integral UNIV (\x. if x \ s \ cube k then 1 else (0::real))) ``` hoelzl@38656 ` 170` ``` ----> integral UNIV (\x. if x \ s then 1 else 0)" ``` hoelzl@38656 ` 171` ``` proof(rule monotone_convergence_increasing) ``` hoelzl@38656 ` 172` ``` have "\n. gmeasure (s \ cube n) \ m" apply(rule ccontr) unfolding not_all not_le ``` hoelzl@38656 ` 173` ``` proof(erule exE) fix k assume k:"m < gmeasure (s \ cube k)" ``` hoelzl@38656 ` 174` ``` hence "gmeasure (s \ 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 \ cube (N + k)) \ gmeasure (s \ 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 (\x. if x \ s \ 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 "\k. (\x. if x \ s \ 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 *:"\n. n \ Suc n" by auto ``` hoelzl@38656 ` 191` ``` show "\k. \x\UNIV. (if x \ s \ cube k then 1 else 0) \ (if x \ s \ cube (Suc k) then 1 else (0::real))" ``` hoelzl@38656 ` 192` ``` using cube_subset[OF *] by fastsimp ``` hoelzl@38656 ` 193` ``` show "\x\UNIV. (\k. if x \ s \ cube k then 1 else 0) ----> (if x \ 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 \ 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 (\x. if x \ 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 \ s has_lmeasure m2 \ 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 \ \" ``` hoelzl@38656 ` 217` ``` shows "gmeasurable s" ``` hoelzl@38656 ` 218` ```proof- have "\B. \n. gmeasure (s \ cube n) \ 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 \" 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 "\n. N \ n \ B \ gmeasure (s \ cube n)" ``` hoelzl@38656 ` 226` ``` apply(rule order_trans[where y="gmeasure (s \ 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 "\N. \n\N. Real B \ Real (gmeasure (s \ 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 "\n. s \ 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 \ cube n)" using assms by auto ``` hoelzl@38656 ` 240` ``` show "gmeasure (s \ cube n) \ B" using B by auto ``` hoelzl@38656 ` 241` ``` show "s \ cube n \ s \ 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 \ 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 \ 0" using assms by auto ``` hoelzl@38656 ` 257` ``` have *:"m = gmeasure (\{s \ cube n |n. n \ 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 \ cube n)" ``` hoelzl@38656 ` 264` ``` using gmeasurable_inter[OF gmea gmeasurable_cube] . ``` hoelzl@38656 ` 265` ``` show "gmeasure (s \ cube n) \ gmeasure s" apply(rule measure_subset) ``` hoelzl@38656 ` 266` ``` apply(rule * gmea)+ by auto ``` hoelzl@38656 ` 267` ``` show "s \ cube n \ s \ 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 \ s has_lmeasure (lmeasure s)" (is "?l = ?r") ``` hoelzl@38656 ` 278` ```proof assume ?l let ?f = "\n. Real (gmeasure (s \ cube n))" ``` hoelzl@38656 ` 279` ``` have "\n m. n\m \ ?f n \ ?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 \ t" ``` hoelzl@38656 ` 289` ``` shows "lmeasure s \ lmeasure t" ``` hoelzl@38656 ` 290` ```proof(cases "lmeasure t = \") ``` hoelzl@38656 ` 291` ``` case False have som:"lmeasure s \ \" ``` hoelzl@38656 ` 292` ``` proof(rule ccontr,unfold not_not) assume as:"lmeasure s = \" ``` hoelzl@38656 ` 293` ``` have "t has_lmeasure \" 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 "(\n. Real (gmeasure (s \ cube n))) ----> Real (real (lmeasure s))" ``` hoelzl@38656 ` 309` ``` unfolding Real_real'[OF som] . ``` hoelzl@38656 ` 310` ``` hence l1:"(\n. gmeasure (s \ 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 "(\n. Real (gmeasure (t \ cube n))) ----> Real (real (lmeasure t))" ``` hoelzl@38656 ` 315` ``` unfolding Real_real'[OF False] . ``` hoelzl@38656 ` 316` ``` hence l2:"(\n. gmeasure (t \ 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) \ 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)) \ 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" "\x. x \ s ==> lmeasurable(f x)" ``` hoelzl@38656 ` 328` ``` "\x y. x \ s \ y \ s \ x \ y \ negligible((f x) \ (f y))" ``` hoelzl@38656 ` 329` ``` shows "(\ (f ` s)) has_lmeasure (setsum (\x. lmeasure(f x)) s)" ``` hoelzl@38656 ` 330` ``` unfolding has_lmeasure_def ``` hoelzl@38656 ` 331` ```proof show lmeaf:"lmeasurable (\f ` s)" apply(rule lmeasurable_finite_unions) ``` hoelzl@38656 ` 332` ``` using assms(1-2) by auto ``` hoelzl@38656 ` 333` ``` show "(\n. Real (gmeasure (\f ` s \ cube n))) ----> (\x\s. lmeasure (f x))" (is ?l) ``` hoelzl@38656 ` 334` ``` proof(cases "\x\s. lmeasure (f x) = \") ``` hoelzl@38656 ` 335` ``` case False hence *:"(\x\s. lmeasure (f x)) \ \" apply- ``` hoelzl@38656 ` 336` ``` apply(rule setsum_neq_omega) using assms(1) by auto ``` hoelzl@38656 ` 337` ``` have gmea:"\x. x\s \ gmeasurable (f x)" apply(rule glmeasurable_finite) using False assms(2) by auto ``` hoelzl@38656 ` 338` ``` have "(\x\s. lmeasure (f x)) = (\x\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 (\x\s. (gmeasure (f x)))" apply(rule setsum_Real) by auto ``` hoelzl@38656 ` 341` ``` finally have sum:"(\x\s. lmeasure (f x)) = Real (\x\s. gmeasure (f x))" . ``` hoelzl@38656 ` 342` ``` have sum_0:"(\x\s. gmeasure (f x)) \ 0" apply(rule setsum_nonneg) by auto ``` hoelzl@38656 ` 343` ``` have int_un:"\f ` s has_gmeasure (\x\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:"\{\f ` s \ cube n |n. n \ UNIV} = \f ` s" unfolding simple_image ``` hoelzl@38656 ` 347` ``` proof safe fix x y assume as:"x \ f y" "y \ s" ``` hoelzl@38656 ` 348` ``` from mem_big_cube[of x] guess n . note n=this ``` hoelzl@38656 ` 349` ``` thus "x \ \range (\n. \f ` s \ cube n)" unfolding Union_iff ``` hoelzl@38656 ` 350` ``` apply-apply(rule_tac x="\f ` s \ 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 (\f ` s \ cube n)" using lmeaf unfolding lmeasurable_def by auto ``` hoelzl@38656 ` 358` ``` thus "gmeasure (\f ` s \ cube n) \ gmeasure (\f ` s)" ``` hoelzl@38656 ` 359` ``` apply(rule measure_subset) using int_un by auto ``` hoelzl@38656 ` 360` ``` show "\f ` s \ cube n \ \f ` s \ 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:"(\x\s. lmeasure (f x)) = \" using setsum_\[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 \" 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 "\N. \n\N. Real B \ Real (gmeasure (\f ` s \ 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" "\s. s \ f ==> s has_lmeasure (m s)" ``` hoelzl@38656 ` 381` ``` "\s t. s \ f \ t \ f \ s \ t ==> negligible (s\t)" ``` hoelzl@38656 ` 382` ``` shows "(\ 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" "\s. s \ f ==> s has_lmeasure (m s)" ``` hoelzl@38656 ` 392` ``` "\s t. s \ f \ t \ f \ s \ t ==> s \ t = {}" ``` hoelzl@38656 ` 393` ``` shows "(\ 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 "\n. lmeasurable(s n)" "\n. s(n) \ s(Suc n)" ``` hoelzl@38656 ` 403` ``` shows "lmeasurable(\ { s n | n. n \ UNIV }) \ ``` hoelzl@38656 ` 404` ``` (\n. lmeasure(s n)) ----> lmeasure(\ { s(n) | n. n \ UNIV })" (is "?mea \ ?lim") ``` hoelzl@38656 ` 405` ```proof- have cube:"\m. \ { s(n) | n. n \ UNIV } \ cube m = \ { s(n) \ cube m | n. n \ UNIV }" by blast ``` hoelzl@38656 ` 406` ``` have 3:"\n. \m\n. s n \ 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(\ { s(n) | n. n \ UNIV }) = \") ``` 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 "\B. \n. \m\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 "\n. gmeasurable (s n) \ gmeasure (s n) \ 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) \ 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 "\n. gmeasurable (s n)" "\n. gmeasure (s n) \ 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 (\{s n |n. n \ UNIV})" ``` hoelzl@38656 ` 431` ``` case False note gmea_lim = glmeasurable_finite[OF mea this] ``` hoelzl@38656 ` 432` ``` have ls:"\n. lmeasure (s n) \ lmeasure (\{s n |n. n \ UNIV})" ``` hoelzl@38656 ` 433` ``` apply(rule lmeasure_subset) using assms(1) mea by auto ``` hoelzl@38656 ` 434` ``` have "\n. lmeasure (s n) \ \" ``` 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 "\n. gmeasure (s n) \ 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 "\n. lmeasurable(s n)" "\m n. m \ n \ negligible(s m \ s n)" ``` hoelzl@38656 ` 451` ``` shows "(\m. setsum (\n. lmeasure(s n)) {..m}) ----> (lmeasure(\ { s(n) |n. n \ UNIV }))" ``` hoelzl@38656 ` 452` ```proof- have *:"\n. (\ (s ` {0..n})) has_lmeasure (setsum (\k. lmeasure(s k)) {0..n})" ``` hoelzl@38656 ` 453` ``` apply(rule has_lmeasure_negligible_unions_image) using assms by auto ``` hoelzl@38656 ` 454` ``` have **:"(\{\s ` {0..n} |n. n \ UNIV}) = (\{s n |n. n \ UNIV})" unfolding simple_image by fastsimp ``` hoelzl@38656 ` 455` ``` have "lmeasurable (\{\s ` {0..n} |n. n \ UNIV}) \ ``` hoelzl@38656 ` 456` ``` (\n. lmeasure (\(s ` {0..n}))) ----> lmeasure (\{\s ` {0..n} |n. n \ 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 *:"\n. (gmeasure (s \ 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 = \ space = UNIV, sets = lmeasurable \" ``` hoelzl@38656 ` 485` hoelzl@38656 ` 486` ```lemma lebesgue_measurable[simp]:"A \ sets lebesgue_space \ 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 \ gmeasurable \ 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 \ sets lebesgue_space" "disjoint_family A" ``` hoelzl@38656 ` 498` ``` "lmeasurable (UNION UNIV A)" ``` hoelzl@38656 ` 499` ``` have *:"UNION UNIV A = \range A" by auto ``` hoelzl@38656 ` 500` ``` show "(\\<^isub>\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\n" ``` hoelzl@38656 ` 503` ``` have *:"\m. (\nA ` {..n A ` {.. range A" by auto thus "lmeasurable s" using as(1) by fastsimp ``` hoelzl@38656 ` 513` ``` next fix m s t assume st:"s \ A ` {.. A ` {.. 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 \ ta" unfolding a by auto ``` hoelzl@38656 ` 516` ``` thus "negligible (s \ 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 "\m. lmeasurable (\A ` {..n (\n{A n |n. n \ UNIV}" by auto ``` hoelzl@38656 ` 527` ``` show "(\n. \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 \ sets lebesgue_space" ``` hoelzl@38656 ` 535` ``` have *:"UNION UNIV A = (\{A n |n. n \ 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 \ Integration.integral" ``` hoelzl@38656 ` 550` hoelzl@38656 ` 551` ```lemma lebesgue_simple_function_indicator: ``` hoelzl@38656 ` 552` ``` fixes f::"'a::ordered_euclidean_space \ pinfreal" ``` hoelzl@38656 ` 553` ``` assumes f:"lebesgue.simple_function f" ``` hoelzl@38656 ` 554` ``` shows "f = (\x. (\y \ 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 \ 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 \ \" ``` 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 \ 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 ```