38656

1 


2 
header {* Lebsegue measure *}


3 
(* Author: Robert Himmelmann, TU Muenchen *)


4 


5 
theory Lebesgue_Measure


6 
imports Gauge_Measure Measure Lebesgue_Integration


7 
begin


8 


9 
subsection {* Various *}


10 


11 
lemma seq_offset_iff:"f > l \<longleftrightarrow> (\<lambda>i. f (i + k)) > l"


12 
using seq_offset_rev seq_offset[of f l k] by auto


13 


14 
lemma has_integral_disjoint_union: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"


15 
assumes "(f has_integral i) s" "(f has_integral j) t" "s \<inter> t = {}"


16 
shows "(f has_integral (i + j)) (s \<union> t)"


17 
apply(rule has_integral_union[OF assms(12)]) unfolding assms by auto


18 


19 
lemma lim_eq: assumes "\<forall>n>N. f n = g n" shows "(f > l) \<longleftrightarrow> (g > l)" using assms


20 
proof(induct N arbitrary: f g) case 0


21 
hence *:"\<And>n. f (Suc n) = g (Suc n)" by auto


22 
show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym])


23 
unfolding * ..


24 
next case (Suc n)


25 
show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym])


26 
apply(rule Suc(1)) using Suc(2) by auto


27 
qed


28 


29 
subsection {* Standard Cubes *}


30 


31 
definition cube where


32 
"cube (n::nat) \<equiv> {\<chi>\<chi> i.  real n .. (\<chi>\<chi> i. real n)::_::ordered_euclidean_space}"


33 


34 
lemma cube_subset[intro]:"n\<le>N \<Longrightarrow> cube n \<subseteq> (cube N::'a::ordered_euclidean_space set)"


35 
apply(auto simp: eucl_le[where 'a='a] cube_def) apply(erule_tac[!] x=i in allE)+ by auto


36 


37 
lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n"


38 
unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta'


39 
proof fix x::'a and i assume as:"x\<in>ball 0 (real n)" "i<DIM('a)"


40 
thus " real n \<le> x $$ i" "real n \<ge> x $$ i"


41 
using component_le_norm[of x i] by(auto simp: dist_norm)


42 
qed


43 


44 
lemma mem_big_cube: obtains n where "x \<in> cube n"


45 
proof from real_arch_lt[of "norm x"] guess n ..


46 
thus ?thesis applyapply(rule that[where n=n])


47 
apply(rule ball_subset_cube[unfolded subset_eq,rule_format])


48 
by (auto simp add:dist_norm)


49 
qed


50 


51 
lemma Union_inter_cube:"\<Union>{s \<inter> cube n n. n \<in> UNIV} = s"


52 
proof safe case goal1


53 
from mem_big_cube[of x] guess n . note n=this


54 
show ?case unfolding Union_iff apply(rule_tac x="s \<inter> cube n" in bexI)


55 
using n goal1 by auto


56 
qed


57 


58 
lemma gmeasurable_cube[intro]:"gmeasurable (cube n)"


59 
unfolding cube_def by auto


60 


61 
lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set"


62 
assumes "gmeasurable (s \<inter> cube n)" shows "gmeasure (s \<inter> cube n) \<le> gmeasure (cube n::'a set)"


63 
apply(rule has_gmeasure_subset[of "s\<inter>cube n" _ "cube n"])


64 
unfolding has_gmeasure_measure[THEN sym] using assms by auto


65 


66 


67 
subsection {* Measurability *}


68 


69 
definition lmeasurable :: "('a::ordered_euclidean_space) set => bool" where


70 
"lmeasurable s \<equiv> (\<forall>n::nat. gmeasurable (s \<inter> cube n))"


71 


72 
lemma lmeasurableD[dest]:assumes "lmeasurable s"


73 
shows "\<And>n. gmeasurable (s \<inter> cube n)"


74 
using assms unfolding lmeasurable_def by auto


75 


76 
lemma measurable_imp_lmeasurable: assumes"gmeasurable s"


77 
shows "lmeasurable s" unfolding lmeasurable_def cube_def


78 
using assms gmeasurable_interval by auto


79 


80 
lemma lmeasurable_empty[intro]: "lmeasurable {}"


81 
using gmeasurable_empty apply apply(drule_tac measurable_imp_lmeasurable) .


82 


83 
lemma lmeasurable_union[intro]: assumes "lmeasurable s" "lmeasurable t"


84 
shows "lmeasurable (s \<union> t)"


85 
using assms unfolding lmeasurable_def Int_Un_distrib2


86 
by(auto intro:gmeasurable_union)


87 


88 
lemma lmeasurable_countable_unions_strong:


89 
fixes s::"nat => 'a::ordered_euclidean_space set"


90 
assumes "\<And>n::nat. lmeasurable(s n)"


91 
shows "lmeasurable(\<Union>{ s(n) n. n \<in> UNIV })"


92 
unfolding lmeasurable_def


93 
proof fix n::nat


94 
have *:"\<Union>{s n n. n \<in> UNIV} \<inter> cube n = \<Union>{s k \<inter> cube n k. k \<in> UNIV}" by auto


95 
show "gmeasurable (\<Union>{s n n. n \<in> UNIV} \<inter> cube n)" unfolding *


96 
apply(rule gmeasurable_countable_unions_strong)


97 
apply(rule assms[unfolded lmeasurable_def,rule_format])


98 
proof fix k::nat


99 
show "gmeasure (\<Union>{s ka \<inter> cube n ka. ka \<le> k}) \<le> gmeasure (cube n::'a set)"


100 
apply(rule measure_subset) apply(rule gmeasurable_finite_unions)


101 
using assms(1)[unfolded lmeasurable_def] by auto


102 
qed


103 
qed


104 


105 
lemma lmeasurable_inter[intro]: fixes s::"'a :: ordered_euclidean_space set"


106 
assumes "lmeasurable s" "lmeasurable t" shows "lmeasurable (s \<inter> t)"


107 
unfolding lmeasurable_def


108 
proof fix n::nat


109 
have *:"s \<inter> t \<inter> cube n = (s \<inter> cube n) \<inter> (t \<inter> cube n)" by auto


110 
show "gmeasurable (s \<inter> t \<inter> cube n)"


111 
using assms unfolding lmeasurable_def *


112 
using gmeasurable_inter[of "s \<inter> cube n" "t \<inter> cube n"] by auto


113 
qed


114 


115 
lemma lmeasurable_complement[intro]: assumes "lmeasurable s"


116 
shows "lmeasurable (UNIV  s)"


117 
unfolding lmeasurable_def


118 
proof fix n::nat


119 
have *:"(UNIV  s) \<inter> cube n = cube n  (s \<inter> cube n)" by auto


120 
show "gmeasurable ((UNIV  s) \<inter> cube n)" unfolding *


121 
apply(rule gmeasurable_diff) using assms unfolding lmeasurable_def by auto


122 
qed


123 


124 
lemma lmeasurable_finite_unions:


125 
assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> lmeasurable s"


126 
shows "lmeasurable (\<Union> f)" unfolding lmeasurable_def


127 
proof fix n::nat have *:"(\<Union>f \<inter> cube n) = \<Union>{x \<inter> cube n  x . x\<in>f}" by auto


128 
show "gmeasurable (\<Union>f \<inter> cube n)" unfolding *


129 
apply(rule gmeasurable_finite_unions) unfolding simple_image


130 
using assms unfolding lmeasurable_def by auto


131 
qed


132 


133 
lemma negligible_imp_lmeasurable[dest]: fixes s::"'a::ordered_euclidean_space set"


134 
assumes "negligible s" shows "lmeasurable s"


135 
unfolding lmeasurable_def


136 
proof case goal1


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)"


138 
unfolding indicator_def_raw by auto


139 
note assms[unfolded negligible_def,rule_format,of "(\<chi>\<chi> i.  real n)::'a" "\<chi>\<chi> i. real n"]


140 
thus ?case applyapply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def


141 
apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric]


142 
apply(subst has_integral_restrict_univ[THEN sym]) unfolding * .


143 
qed


144 


145 


146 
section {* The Lebesgue Measure *}


147 


148 
definition has_lmeasure (infixr "has'_lmeasure" 80) where


149 
"s has_lmeasure m \<equiv> lmeasurable s \<and> ((\<lambda>n. Real (gmeasure (s \<inter> cube n))) > m) sequentially"


150 


151 
lemma has_lmeasureD: assumes "s has_lmeasure m"


152 
shows "lmeasurable s" "gmeasurable (s \<inter> cube n)"


153 
"((\<lambda>n. Real (gmeasure (s \<inter> cube n))) > m) sequentially"


154 
using assms unfolding has_lmeasure_def lmeasurable_def by auto


155 


156 
lemma has_lmeasureI: assumes "lmeasurable s" "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) > m) sequentially"


157 
shows "s has_lmeasure m" using assms unfolding has_lmeasure_def by auto


158 


159 
definition lmeasure where


160 
"lmeasure s \<equiv> SOME m. s has_lmeasure m"


161 


162 
lemma has_lmeasure_has_gmeasure: assumes "s has_lmeasure (Real m)" "m\<ge>0"


163 
shows "s has_gmeasure m"


164 
proof note s = has_lmeasureD[OF assms(1)]


165 
have *:"(\<lambda>n. (gmeasure (s \<inter> cube n))) > m"


166 
using s(3) apply(subst (asm) lim_Real) using s(2) assms(2) by auto


167 


168 
have "(\<lambda>x. if x \<in> s then 1 else (0::real)) integrable_on UNIV \<and>


169 
(\<lambda>k. integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)))


170 
> integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)"


171 
proof(rule monotone_convergence_increasing)


172 
have "\<forall>n. gmeasure (s \<inter> cube n) \<le> m" apply(rule ccontr) unfolding not_all not_le


173 
proof(erule exE) fix k assume k:"m < gmeasure (s \<inter> cube k)"


174 
hence "gmeasure (s \<inter> cube k)  m > 0" by auto


175 
from *[unfolded Lim_sequentially,rule_format,OF this] guess N ..


176 
note this[unfolded dist_real_def,rule_format,of "N + k"]


177 
moreover have "gmeasure (s \<inter> cube (N + k)) \<ge> gmeasure (s \<inter> cube k)" apply


178 
apply(rule measure_subset) prefer 3 using s(2)


179 
using cube_subset[of k "N + k"] by auto


180 
ultimately show False by auto


181 
qed


182 
thus *:"bounded {integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)) k. True}"


183 
unfolding integral_measure_univ[OF s(2)] bounded_def apply


184 
apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def


185 
by (auto simp: measure_pos_le)


186 


187 
show "\<forall>k. (\<lambda>x. if x \<in> s \<inter> cube k then (1::real) else 0) integrable_on UNIV"


188 
unfolding integrable_restrict_univ


189 
using s(2) unfolding gmeasurable_def has_gmeasure_def by auto


190 
have *:"\<And>n. n \<le> Suc n" by auto


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))"


192 
using cube_subset[OF *] by fastsimp


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))"


194 
unfolding Lim_sequentially


195 
proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this


196 
show ?case apply(rule_tac x=N in exI)


197 
proof safe case goal1


198 
have "x \<in> cube n" using cube_subset[OF goal1] N


199 
using ball_subset_cube[of N] by(auto simp: dist_norm)


200 
thus ?case using `e>0` by auto


201 
qed


202 
qed


203 
qed note ** = conjunctD2[OF this]


204 
hence *:"m = integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" apply


205 
apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s(2)] using * .


206 
show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto


207 
qed


208 


209 
lemma has_lmeasure_unique: "s has_lmeasure m1 \<Longrightarrow> s has_lmeasure m2 \<Longrightarrow> m1 = m2"


210 
unfolding has_lmeasure_def apply(rule Lim_unique) using trivial_limit_sequentially by auto


211 


212 
lemma lmeasure_unique[intro]: assumes "A has_lmeasure m" shows "lmeasure A = m"


213 
using assms unfolding lmeasure_def lmeasurable_def apply


214 
apply(rule some_equality) defer apply(rule has_lmeasure_unique) by auto


215 


216 
lemma glmeasurable_finite: assumes "lmeasurable s" "lmeasure s \<noteq> \<omega>"


217 
shows "gmeasurable s"


218 
proof have "\<exists>B. \<forall>n. gmeasure (s \<inter> cube n) \<le> B"


219 
proof(rule ccontr) case goal1


220 
note as = this[unfolded not_ex not_all not_le]


221 
have "s has_lmeasure \<omega>" apply apply(rule has_lmeasureI[OF assms(1)])


222 
unfolding Lim_omega


223 
proof fix B::real


224 
from as[rule_format,of B] guess N .. note N = this


225 
have "\<And>n. N \<le> n \<Longrightarrow> B \<le> gmeasure (s \<inter> cube n)"


226 
apply(rule order_trans[where y="gmeasure (s \<inter> cube N)"]) defer


227 
apply(rule measure_subset) prefer 3


228 
using cube_subset N assms(1)[unfolded lmeasurable_def] by auto


229 
thus "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (s \<inter> cube n))" apply


230 
apply(subst Real_max') apply(rule_tac x=N in exI,safe)


231 
unfolding pinfreal_less_eq apply(subst if_P) by auto


232 
qed note lmeasure_unique[OF this]


233 
thus False using assms(2) by auto


234 
qed then guess B .. note B=this


235 


236 
show ?thesis apply(rule gmeasurable_nested_unions[of "\<lambda>n. s \<inter> cube n",


237 
unfolded Union_inter_cube,THEN conjunct1, where B1=B])


238 
proof fix n::nat


239 
show " gmeasurable (s \<inter> cube n)" using assms by auto


240 
show "gmeasure (s \<inter> cube n) \<le> B" using B by auto


241 
show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)"


242 
by (rule Int_mono) (simp_all add: cube_subset)


243 
qed


244 
qed


245 


246 
lemma lmeasure_empty[intro]:"lmeasure {} = 0"


247 
apply(rule lmeasure_unique)


248 
unfolding has_lmeasure_def by auto


249 


250 
lemma lmeasurableI[dest]:"s has_lmeasure m \<Longrightarrow> lmeasurable s"


251 
unfolding has_lmeasure_def by auto


252 


253 
lemma has_gmeasure_has_lmeasure: assumes "s has_gmeasure m"


254 
shows "s has_lmeasure (Real m)"


255 
proof have gmea:"gmeasurable s" using assms by auto


256 
have m:"m \<ge> 0" using assms by auto


257 
have *:"m = gmeasure (\<Union>{s \<inter> cube n n. n \<in> UNIV})" unfolding Union_inter_cube


258 
using assms by(rule measure_unique[THEN sym])


259 
show ?thesis unfolding has_lmeasure_def


260 
apply(rule,rule measurable_imp_lmeasurable[OF gmea])


261 
apply(subst lim_Real) apply(rule,rule,rule m) unfolding *


262 
apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"])


263 
proof fix n::nat show *:"gmeasurable (s \<inter> cube n)"


264 
using gmeasurable_inter[OF gmea gmeasurable_cube] .


265 
show "gmeasure (s \<inter> cube n) \<le> gmeasure s" apply(rule measure_subset)


266 
apply(rule * gmea)+ by auto


267 
show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" using cube_subset[of n "Suc n"] by auto


268 
qed


269 
qed


270 


271 
lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)"


272 
proof note has_gmeasure_measureI[OF assms]


273 
note has_gmeasure_has_lmeasure[OF this]


274 
thus ?thesis by(rule lmeasure_unique)


275 
qed


276 


277 
lemma has_lmeasure_lmeasure: "lmeasurable s \<longleftrightarrow> s has_lmeasure (lmeasure s)" (is "?l = ?r")


278 
proof assume ?l let ?f = "\<lambda>n. Real (gmeasure (s \<inter> cube n))"


279 
have "\<forall>n m. n\<ge>m \<longrightarrow> ?f n \<ge> ?f m" unfolding pinfreal_less_eq apply safe


280 
apply(subst if_P) defer apply(rule measure_subset) prefer 3


281 
apply(drule cube_subset) using `?l` by auto


282 
from lim_pinfreal_increasing[OF this] guess l . note l=this


283 
hence "s has_lmeasure l" using `?l` applyapply(rule has_lmeasureI) by auto


284 
thus ?r using lmeasure_unique by auto


285 
next assume ?r thus ?l unfolding has_lmeasure_def by auto


286 
qed


287 


288 
lemma lmeasure_subset[dest]: assumes "lmeasurable s" "lmeasurable t" "s \<subseteq> t"


289 
shows "lmeasure s \<le> lmeasure t"


290 
proof(cases "lmeasure t = \<omega>")


291 
case False have som:"lmeasure s \<noteq> \<omega>"


292 
proof(rule ccontr,unfold not_not) assume as:"lmeasure s = \<omega>"


293 
have "t has_lmeasure \<omega>" using assms(2) apply(rule has_lmeasureI)


294 
unfolding Lim_omega


295 
proof case goal1


296 
note assms(1)[unfolded has_lmeasure_lmeasure]


297 
note has_lmeasureD(3)[OF this,unfolded as Lim_omega,rule_format,of B]


298 
then guess N .. note N = this


299 
show ?case apply(rule_tac x=N in exI) apply safe


300 
apply(rule order_trans) apply(rule N[rule_format],assumption)


301 
unfolding pinfreal_less_eq apply(subst if_P)defer


302 
apply(rule measure_subset) using assms by auto


303 
qed


304 
thus False using lmeasure_unique False by auto


305 
qed


306 


307 
note assms(1)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this]


308 
hence "(\<lambda>n. Real (gmeasure (s \<inter> cube n))) > Real (real (lmeasure s))"


309 
unfolding Real_real'[OF som] .


310 
hence l1:"(\<lambda>n. gmeasure (s \<inter> cube n)) > real (lmeasure s)"


311 
applyapply(subst(asm) lim_Real) by auto


312 


313 
note assms(2)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this]


314 
hence "(\<lambda>n. Real (gmeasure (t \<inter> cube n))) > Real (real (lmeasure t))"


315 
unfolding Real_real'[OF False] .


316 
hence l2:"(\<lambda>n. gmeasure (t \<inter> cube n)) > real (lmeasure t)"


317 
applyapply(subst(asm) lim_Real) by auto


318 


319 
have "real (lmeasure s) \<le> real (lmeasure t)" apply(rule LIMSEQ_le[OF l1 l2])


320 
apply(rule_tac x=0 in exI,safe) apply(rule measure_subset) using assms by auto


321 
hence "Real (real (lmeasure s)) \<le> Real (real (lmeasure t))"


322 
unfolding pinfreal_less_eq by auto


323 
thus ?thesis unfolding Real_real'[OF som] Real_real'[OF False] .


324 
qed auto


325 


326 
lemma has_lmeasure_negligible_unions_image:


327 
assumes "finite s" "\<And>x. x \<in> s ==> lmeasurable(f x)"


328 
"\<And>x y. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x \<noteq> y \<Longrightarrow> negligible((f x) \<inter> (f y))"


329 
shows "(\<Union> (f ` s)) has_lmeasure (setsum (\<lambda>x. lmeasure(f x)) s)"


330 
unfolding has_lmeasure_def


331 
proof show lmeaf:"lmeasurable (\<Union>f ` s)" apply(rule lmeasurable_finite_unions)


332 
using assms(12) by auto


333 
show "(\<lambda>n. Real (gmeasure (\<Union>f ` s \<inter> cube n))) > (\<Sum>x\<in>s. lmeasure (f x))" (is ?l)


334 
proof(cases "\<exists>x\<in>s. lmeasure (f x) = \<omega>")


335 
case False hence *:"(\<Sum>x\<in>s. lmeasure (f x)) \<noteq> \<omega>" apply


336 
apply(rule setsum_neq_omega) using assms(1) by auto


337 
have gmea:"\<And>x. x\<in>s \<Longrightarrow> gmeasurable (f x)" apply(rule glmeasurable_finite) using False assms(2) by auto


338 
have "(\<Sum>x\<in>s. lmeasure (f x)) = (\<Sum>x\<in>s. Real (gmeasure (f x)))" apply(rule setsum_cong2)


339 
apply(rule gmeasure_lmeasure) using False assms(2) gmea by auto


340 
also have "... = Real (\<Sum>x\<in>s. (gmeasure (f x)))" apply(rule setsum_Real) by auto


341 
finally have sum:"(\<Sum>x\<in>s. lmeasure (f x)) = Real (\<Sum>x\<in>s. gmeasure (f x))" .


342 
have sum_0:"(\<Sum>x\<in>s. gmeasure (f x)) \<ge> 0" apply(rule setsum_nonneg) by auto


343 
have int_un:"\<Union>f ` s has_gmeasure (\<Sum>x\<in>s. gmeasure (f x))"


344 
apply(rule has_gmeasure_negligible_unions_image) using assms gmea by auto


345 


346 
have unun:"\<Union>{\<Union>f ` s \<inter> cube n n. n \<in> UNIV} = \<Union>f ` s" unfolding simple_image


347 
proof safe fix x y assume as:"x \<in> f y" "y \<in> s"


348 
from mem_big_cube[of x] guess n . note n=this


349 
thus "x \<in> \<Union>range (\<lambda>n. \<Union>f ` s \<inter> cube n)" unfolding Union_iff


350 
applyapply(rule_tac x="\<Union>f ` s \<inter> cube n" in bexI) using as by auto


351 
qed


352 
show ?l apply(subst Real_real'[OF *,THEN sym])apply(subst lim_Real)


353 
apply rule apply rule unfolding sum real_Real if_P[OF sum_0] apply(rule sum_0)


354 
unfolding measure_unique[OF int_un,THEN sym] apply(subst(2) unun[THEN sym])


355 
apply(rule has_gmeasure_nested_unions[THEN conjunct2])


356 
proof fix n::nat


357 
show *:"gmeasurable (\<Union>f ` s \<inter> cube n)" using lmeaf unfolding lmeasurable_def by auto


358 
thus "gmeasure (\<Union>f ` s \<inter> cube n) \<le> gmeasure (\<Union>f ` s)"


359 
apply(rule measure_subset) using int_un by auto


360 
show "\<Union>f ` s \<inter> cube n \<subseteq> \<Union>f ` s \<inter> cube (Suc n)"


361 
using cube_subset[of n "Suc n"] by auto


362 
qed


363 


364 
next case True then guess X .. note X=this


365 
hence sum:"(\<Sum>x\<in>s. lmeasure (f x)) = \<omega>" using setsum_\<omega>[THEN iffD2, of s] assms by fastsimp


366 
show ?l unfolding sum Lim_omega


367 
proof fix B::real


368 
have Xm:"(f X) has_lmeasure \<omega>" using X by (metis assms(2) has_lmeasure_lmeasure)


369 
note this[unfolded has_lmeasure_def,THEN conjunct2, unfolded Lim_omega]


370 
from this[rule_format,of B] guess N .. note N=this[rule_format]


371 
show "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (\<Union>f ` s \<inter> cube n))"


372 
apply(rule_tac x=N in exI)


373 
proof safe case goal1 show ?case apply(rule order_trans[OF N[OF goal1]])


374 
unfolding pinfreal_less_eq apply(subst if_P) defer


375 
apply(rule measure_subset) using has_lmeasureD(2)[OF Xm]


376 
using lmeaf unfolding lmeasurable_def using X(1) by auto


377 
qed qed qed qed


378 


379 
lemma has_lmeasure_negligible_unions:


380 
assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)"


381 
"\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> negligible (s\<inter>t)"


382 
shows "(\<Union> f) has_lmeasure (setsum m f)"


383 
proof have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2)


384 
apply(subst lmeasure_unique[OF assms(2)]) by auto


385 
show ?thesis unfolding *


386 
apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply])


387 
using assms by auto


388 
qed


389 


390 
lemma has_lmeasure_disjoint_unions:


391 
assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)"


392 
"\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> s \<inter> t = {}"


393 
shows "(\<Union> f) has_lmeasure (setsum m f)"


394 
proof have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2)


395 
apply(subst lmeasure_unique[OF assms(2)]) by auto


396 
show ?thesis unfolding *


397 
apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply])


398 
using assms by auto


399 
qed


400 


401 
lemma has_lmeasure_nested_unions:


402 
assumes "\<And>n. lmeasurable(s n)" "\<And>n. s(n) \<subseteq> s(Suc n)"


403 
shows "lmeasurable(\<Union> { s n  n. n \<in> UNIV }) \<and>


404 
(\<lambda>n. lmeasure(s n)) > lmeasure(\<Union> { s(n)  n. n \<in> UNIV })" (is "?mea \<and> ?lim")


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


406 
have 3:"\<And>n. \<forall>m\<ge>n. s n \<subseteq> s m" apply(rule transitive_stepwise_le) using assms(2) by auto


407 
have mea:"?mea" unfolding lmeasurable_def cube apply rule


408 
apply(rule_tac B1="gmeasure (cube n)" in has_gmeasure_nested_unions[THEN conjunct1])


409 
prefer 3 apply rule using assms(1) unfolding lmeasurable_def


410 
by(auto intro!:assms(2)[unfolded subset_eq,rule_format])


411 
show ?thesis apply(rule,rule mea)


412 
proof(cases "lmeasure(\<Union> { s(n)  n. n \<in> UNIV }) = \<omega>")


413 
case True show ?lim unfolding True Lim_omega


414 
proof(rule ccontr) case goal1 note this[unfolded not_all not_ex]


415 
hence "\<exists>B. \<forall>n. \<exists>m\<ge>n. Real B > lmeasure (s m)" by(auto simp add:not_le)


416 
from this guess B .. note B=this[rule_format]


417 


418 
have "\<forall>n. gmeasurable (s n) \<and> gmeasure (s n) \<le> max B 0"


419 
proof safe fix n::nat from B[of n] guess m .. note m=this


420 
hence *:"lmeasure (s n) < Real B" applyapply(rule le_less_trans)


421 
apply(rule lmeasure_subset[OF assms(1,1)]) apply(rule 3[rule_format]) by auto


422 
thus **:"gmeasurable (s n)" applyapply(rule glmeasurable_finite[OF assms(1)]) by auto


423 
thus "gmeasure (s n) \<le> max B 0" using * unfolding gmeasure_lmeasure[OF **] Real_max'[of B]


424 
unfolding pinfreal_less apply apply(subst(asm) if_P) by auto


425 
qed


426 
hence "\<And>n. gmeasurable (s n)" "\<And>n. gmeasure (s n) \<le> max B 0" by auto


427 
note g = conjunctD2[OF has_gmeasure_nested_unions[of s, OF this assms(2)]]


428 
show False using True unfolding gmeasure_lmeasure[OF g(1)] by auto


429 
qed


430 
next let ?B = "lmeasure (\<Union>{s n n. n \<in> UNIV})"


431 
case False note gmea_lim = glmeasurable_finite[OF mea this]


432 
have ls:"\<And>n. lmeasure (s n) \<le> lmeasure (\<Union>{s n n. n \<in> UNIV})"


433 
apply(rule lmeasure_subset) using assms(1) mea by auto


434 
have "\<And>n. lmeasure (s n) \<noteq> \<omega>"


435 
proof(rule ccontr,safe) case goal1


436 
show False using False ls[of n] unfolding goal1 by auto


437 
qed


438 
note gmea = glmeasurable_finite[OF assms(1) this]


439 


440 
have "\<And>n. gmeasure (s n) \<le> real ?B" unfolding gmeasure_lmeasure[OF gmea_lim]


441 
unfolding real_Real apply(subst if_P,rule) apply(rule measure_subset)


442 
using gmea gmea_lim by auto


443 
note has_gmeasure_nested_unions[of s, OF gmea this assms(2)]


444 
thus ?lim unfolding gmeasure_lmeasure[OF gmea] gmeasure_lmeasure[OF gmea_lim]


445 
applyapply(subst lim_Real) by auto


446 
qed


447 
qed


448 


449 
lemma has_lmeasure_countable_negligible_unions:


450 
assumes "\<And>n. lmeasurable(s n)" "\<And>m n. m \<noteq> n \<Longrightarrow> negligible(s m \<inter> s n)"


451 
shows "(\<lambda>m. setsum (\<lambda>n. lmeasure(s n)) {..m}) > (lmeasure(\<Union> { s(n) n. n \<in> UNIV }))"


452 
proof have *:"\<And>n. (\<Union> (s ` {0..n})) has_lmeasure (setsum (\<lambda>k. lmeasure(s k)) {0..n})"


453 
apply(rule has_lmeasure_negligible_unions_image) using assms by auto


454 
have **:"(\<Union>{\<Union>s ` {0..n} n. n \<in> UNIV}) = (\<Union>{s n n. n \<in> UNIV})" unfolding simple_image by fastsimp


455 
have "lmeasurable (\<Union>{\<Union>s ` {0..n} n. n \<in> UNIV}) \<and>


456 
(\<lambda>n. lmeasure (\<Union>(s ` {0..n}))) > lmeasure (\<Union>{\<Union>s ` {0..n} n. n \<in> UNIV})"


457 
apply(rule has_lmeasure_nested_unions) apply(rule has_lmeasureD(1)[OF *])


458 
apply(rule Union_mono,rule image_mono) by auto


459 
note lem = conjunctD2[OF this,unfolded **]


460 
show ?thesis using lem(2) unfolding lmeasure_unique[OF *] unfolding atLeast0AtMost .


461 
qed


462 


463 
lemma lmeasure_eq_0: assumes "negligible s" shows "lmeasure s = 0"


464 
proof note mea=negligible_imp_lmeasurable[OF assms]


465 
have *:"\<And>n. (gmeasure (s \<inter> cube n)) = 0"


466 
unfolding gmeasurable_measure_eq_0[OF mea[unfolded lmeasurable_def,rule_format]]


467 
using assms by auto


468 
show ?thesis


469 
apply(rule lmeasure_unique) unfolding has_lmeasure_def


470 
apply(rule,rule mea) unfolding * by auto


471 
qed


472 


473 
lemma negligible_img_gmeasurable: fixes s::"'a::ordered_euclidean_space set"


474 
assumes "negligible s" shows "gmeasurable s"


475 
apply(rule glmeasurable_finite)


476 
using lmeasure_eq_0[OF assms] negligible_imp_lmeasurable[OF assms] by auto


477 


478 


479 


480 


481 
section {* Instantiation of _::euclidean_space as measure_space *}


482 


483 
definition lebesgue_space :: "'a::ordered_euclidean_space algebra" where


484 
"lebesgue_space = \<lparr> space = UNIV, sets = lmeasurable \<rparr>"


485 


486 
lemma lebesgue_measurable[simp]:"A \<in> sets lebesgue_space \<longleftrightarrow> lmeasurable A"


487 
unfolding lebesgue_space_def by(auto simp: mem_def)


488 


489 
lemma mem_gmeasurable[simp]: "A \<in> gmeasurable \<longleftrightarrow> gmeasurable A"


490 
unfolding mem_def ..


491 


492 
interpretation lebesgue: measure_space lebesgue_space lmeasure


493 
apply(intro_locales) unfolding measure_space_axioms_def countably_additive_def


494 
unfolding sigma_algebra_axioms_def algebra_def


495 
unfolding lebesgue_measurable


496 
proof safe


497 
fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space" "disjoint_family A"


498 
"lmeasurable (UNION UNIV A)"


499 
have *:"UNION UNIV A = \<Union>range A" by auto


500 
show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (UNION UNIV A)"


501 
unfolding psuminf_def apply(rule SUP_Lim_pinfreal)


502 
proof fix n m::nat assume mn:"m\<le>n"


503 
have *:"\<And>m. (\<Sum>n<m. lmeasure (A n)) = lmeasure (\<Union>A ` {..<m})"


504 
apply(subst lmeasure_unique[OF has_lmeasure_negligible_unions[where m=lmeasure]])


505 
apply(rule finite_imageI) apply rule apply(subst has_lmeasure_lmeasure[THEN sym])


506 
proof fix m::nat


507 
show "(\<Sum>n<m. lmeasure (A n)) = setsum lmeasure (A ` {..<m})"


508 
apply(subst setsum_reindex_nonzero) unfolding o_def apply rule


509 
apply(rule lmeasure_eq_0) using as(2) unfolding disjoint_family_on_def


510 
apply(erule_tac x=x in ballE,safe,erule_tac x=y in ballE) by auto


511 
next fix m s assume "s \<in> A ` {..<m}"


512 
hence "s \<in> range A" by auto thus "lmeasurable s" using as(1) by fastsimp


513 
next fix m s t assume st:"s \<in> A ` {..<m}" "t \<in> A ` {..<m}" "s \<noteq> t"


514 
from st(12) guess sa ta unfolding image_iff applyby(erule bexE)+ note a=this


515 
from st(3) have "sa \<noteq> ta" unfolding a by auto


516 
thus "negligible (s \<inter> t)"


517 
using as(2) unfolding disjoint_family_on_def a


518 
apply(erule_tac x=sa in ballE,erule_tac x=ta in ballE) by auto


519 
qed


520 


521 
have "\<And>m. lmeasurable (\<Union>A ` {..<m})" apply(rule lmeasurable_finite_unions)


522 
apply(rule finite_imageI,rule) using as(1) by fastsimp


523 
from this this show "(\<Sum>n<m. lmeasure (A n)) \<le> (\<Sum>n<n. lmeasure (A n))" unfolding *


524 
apply(rule lmeasure_subset) apply(rule Union_mono) apply(rule image_mono) using mn by auto


525 


526 
next have *:"UNION UNIV A = \<Union>{A n n. n \<in> UNIV}" by auto


527 
show "(\<lambda>n. \<Sum>n<n. lmeasure (A n)) > lmeasure (UNION UNIV A)"


528 
apply(rule LIMSEQ_imp_Suc) unfolding lessThan_Suc_atMost *


529 
apply(rule has_lmeasure_countable_negligible_unions)


530 
using as unfolding disjoint_family_on_def subset_eq by auto


531 
qed


532 


533 
next show "lmeasure {} = 0" by auto


534 
next fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space"


535 
have *:"UNION UNIV A = (\<Union>{A n n. n \<in> UNIV})" unfolding simple_image by auto


536 
show "lmeasurable (UNION UNIV A)" unfolding * using as unfolding subset_eq


537 
using lmeasurable_countable_unions_strong[of A] by auto


538 
qed(auto simp: lebesgue_space_def mem_def)


539 


540 


541 


542 
lemma lmeasurbale_closed_interval[intro]:


543 
"lmeasurable {a..b::'a::ordered_euclidean_space}"


544 
unfolding lmeasurable_def cube_def inter_interval by auto


545 


546 
lemma space_lebesgue_space[simp]:"space lebesgue_space = UNIV"


547 
unfolding lebesgue_space_def by auto


548 


549 
abbreviation "gintegral \<equiv> Integration.integral"


550 


551 
lemma lebesgue_simple_function_indicator:


552 
fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"


553 
assumes f:"lebesgue.simple_function f"


554 
shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f ` {y}) x))"


555 
apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto


556 


557 
lemma lmeasure_gmeasure:


558 
"gmeasurable s \<Longrightarrow> gmeasure s = real (lmeasure s)"


559 
apply(subst gmeasure_lmeasure) by auto


560 


561 
lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \<noteq> \<omega>"


562 
using gmeasure_lmeasure[OF assms] by auto


563 


564 
lemma negligible_lmeasure: assumes "lmeasurable s"


565 
shows "lmeasure s = 0 \<longleftrightarrow> negligible s" (is "?l = ?r")


566 
proof assume ?l


567 
hence *:"gmeasurable s" using glmeasurable_finite[of s] assms by auto


568 
show ?r unfolding gmeasurable_measure_eq_0[THEN sym,OF *]


569 
unfolding lmeasure_gmeasure[OF *] using `?l` by auto


570 
next assume ?r


571 
note g=negligible_img_gmeasurable[OF this] and measure_eq_0[OF this]


572 
hence "real (lmeasure s) = 0" using lmeasure_gmeasure[of s] by auto


573 
thus ?l using lmeasure_finite[OF g] apply apply(rule real_0_imp_eq_0) by auto


574 
qed


575 


576 
end
