# HG changeset patch # User paulson # Date 1256730186 0 # Node ID 73a0c804840fbe5ebbbf12a35d4cc7e5fc005636 # Parent 02de0317f66fb7509c0e48b5c99f4175a3ed9df6# Parent 7be66dee1a5ae6c9dfa8058060d6e02b13298498 merged diff -r 02de0317f66f -r 73a0c804840f NEWS --- a/NEWS Wed Oct 28 00:24:38 2009 +0100 +++ b/NEWS Wed Oct 28 11:43:06 2009 +0000 @@ -65,6 +65,10 @@ of finite and infinite sets. It is shown that they form a complete lattice. +* New theory SupInf of the supremum and infimum operators for sets of reals. + +* New theory Probability containing a development of measure theory, eventually leading to Lebesgue integration and probability. + * Split off prime number ingredients from theory GCD to theory Number_Theory/Primes; diff -r 02de0317f66f -r 73a0c804840f src/HOL/Complex_Main.thy --- a/src/HOL/Complex_Main.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Complex_Main.thy Wed Oct 28 11:43:06 2009 +0000 @@ -4,6 +4,7 @@ imports Main Real + SupInf Complex Log Ln diff -r 02de0317f66f -r 73a0c804840f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Oct 28 11:43:06 2009 +0000 @@ -51,6 +51,7 @@ HOL-Nominal-Examples \ HOL-Number_Theory \ HOL-Old_Number_Theory \ + HOL-Probability \ HOL-Prolog \ HOL-SET_Protocol \ HOL-SMT-Examples \ @@ -345,6 +346,7 @@ RealVector.thy \ SEQ.thy \ Series.thy \ + SupInf.thy \ Taylor.thy \ Transcendental.thy \ Tools/float_syntax.ML \ @@ -1067,6 +1069,18 @@ Multivariate_Analysis/Convex_Euclidean_Space.thy @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis +## HOL-Probability + +HOL-Probability: HOL $(LOG)/HOL-Probability.gz + +$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \ + Probability/Probability.thy \ + Probability/Sigma_Algebra.thy \ + Probability/SeriesPlus.thy \ + Probability/Caratheodory.thy \ + Probability/Measure.thy + $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability + ## HOL-Nominal HOL-Nominal: HOL $(OUT)/HOL-Nominal diff -r 02de0317f66f -r 73a0c804840f src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Library/FuncSet.thy Wed Oct 28 11:43:06 2009 +0000 @@ -101,6 +101,19 @@ lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" by auto +lemma prod_final: + assumes 1: "fst \ f \ Pi A B" and 2: "snd \ f \ Pi A C" + shows "f \ (\ z \ A. B z \ C z)" +proof (rule Pi_I) + fix z + assume z: "z \ A" + have "f z = (fst (f z), snd (f z))" + by simp + also have "... \ B z \ C z" + by (metis SigmaI PiE o_apply 1 2 z) + finally show "f z \ B z \ C z" . +qed + subsection{*Composition With a Restricted Domain: @{term compose}*} diff -r 02de0317f66f -r 73a0c804840f src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Oct 28 11:43:06 2009 +0000 @@ -1133,7 +1133,7 @@ hence "x + y \ s" using `?lhs`[unfolded convex_def, THEN conjunct1] apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE) apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto } - thus ?thesis unfolding convex_def cone_def by blast + thus ?thesis unfolding convex_def cone_def by auto qed lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set" @@ -1742,17 +1742,16 @@ using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0] using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast) hence ab:"\x\s. \y\t. b + inner a y < inner a x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff) - def k \ "rsup ((\x. inner a x) ` t)" + def k \ "Sup ((\x. inner a x) ` t)" show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI) apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof- from ab have "((\x. inner a x) ` t) *<= (inner a y - b)" apply(erule_tac x=y in ballE) apply(rule setleI) using `y\s` by auto - hence k:"isLub UNIV ((\x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto + hence k:"isLub UNIV ((\x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto fix x assume "x\t" thus "inner a x < (k + b / 2)" using `0s" - hence "k \ inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5) - unfolding setle_def + hence "k \ inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5) using ab[THEN bspec[where x=x]] by auto thus "k + b / 2 < inner a x" using `0 < b` by auto qed @@ -1794,11 +1793,20 @@ assumes "convex s" "convex (t::(real^'n::finite) set)" "s \ {}" "t \ {}" "s \ t = {}" shows "\a b. a \ 0 \ (\x\s. inner a x \ b) \ (\x\t. inner a x \ b)" proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] - obtain a where "a\0" "\x\{x - y |x y. x \ t \ y \ s}. 0 \ inner a x" using assms(3-5) by auto - hence "\x\t. \y\s. inner a y \ inner a x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff) - thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\x. inner a x) ` s)" in exI) using `a\0` - apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def - prefer 4 using assms(3-5) by blast+ qed + obtain a where "a\0" "\x\{x - y |x y. x \ t \ y \ s}. 0 \ inner a x" + using assms(3-5) by auto + hence "\x\t. \y\s. inner a y \ inner a x" + by (force simp add: inner_diff) + thus ?thesis + apply(rule_tac x=a in exI, rule_tac x="Sup ((\x. inner a x) ` s)" in exI) using `a\0` + apply auto + apply (rule Sup[THEN isLubD2]) + prefer 4 + apply (rule Sup_least) + using assms(3-5) apply (auto simp add: setle_def) + apply (metis COMBC_def Collect_def Collect_mem_eq) + done +qed subsection {* More convexity generalities. *} @@ -2571,12 +2579,17 @@ thus "f y \ k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm by(auto simp add: vector_component_simps) qed hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous) - apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto - thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed - -subsection {* Line segments, starlike sets etc. *) -(* Use the same overloading tricks as for intervals, so that *) -(* segment[a,b] is closed and segment(a,b) is open relative to affine hull. *} + apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) + apply force + done + thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] + using `d>0` by auto +qed + +subsection {* Line segments, Starlike Sets, etc.*} + +(* Use the same overloading tricks as for intervals, so that + segment[a,b] is closed and segment(a,b) is open relative to affine hull. *) definition midpoint :: "real ^ 'n::finite \ real ^ 'n \ real ^ 'n" where diff -r 02de0317f66f -r 73a0c804840f src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Oct 28 11:43:06 2009 +0000 @@ -2297,242 +2297,9 @@ ultimately show ?thesis by metis qed -(* Supremum and infimum of real sets *) - - -definition rsup:: "real set \ real" where - "rsup S = (SOME a. isLub UNIV S a)" - -lemma rsup_alt: "rsup S = (SOME a. (\x \ S. x \ a) \ (\b. (\x \ S. x \ b) \ a \ b))" by (auto simp add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def) - -lemma rsup: assumes Se: "S \ {}" and b: "\b. S *<= b" - shows "isLub UNIV S (rsup S)" -using Se b -unfolding rsup_def -apply clarify -apply (rule someI_ex) -apply (rule reals_complete) -by (auto simp add: isUb_def setle_def) - -lemma rsup_le: assumes Se: "S \ {}" and Sb: "S *<= b" shows "rsup S \ b" -proof- - from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def) - from rsup[OF Se] Sb have "isLub UNIV S (rsup S)" by blast - then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def) -qed - -lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \ {}" - shows "rsup S = Max S" -using fS Se -proof- - let ?m = "Max S" - from Max_ge[OF fS] have Sm: "\ x\ S. x \ ?m" by metis - with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def) - from Max_in[OF fS Se] lub have mrS: "?m \ rsup S" - by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) - moreover - have "rsup S \ ?m" using Sm lub - by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - ultimately show ?thesis by arith -qed - -lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \ {}" - shows "rsup S \ S" - using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis - -lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \ {}" - shows "isUb S S (rsup S)" - using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS] - unfolding isUb_def setle_def by metis - -lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a \ rsup S \ (\ x \ S. a \ x)" -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) - -lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a \ rsup S \ (\ x \ S. a \ x)" -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) - -lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a < rsup S \ (\ x \ S. a < x)" -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) - -lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a > rsup S \ (\ x \ S. a > x)" -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) - -lemma rsup_unique: assumes b: "S *<= b" and S: "\b' < b. \x \ S. b' < x" - shows "rsup S = b" -using b S -unfolding setle_def rsup_alt -apply - -apply (rule some_equality) -apply (metis linorder_not_le order_eq_iff[symmetric])+ -done - -lemma rsup_le_subset: "S\{} \ S \ T \ (\b. T *<= b) \ rsup S \ rsup T" - apply (rule rsup_le) - apply simp - using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def) - -lemma isUb_def': "isUb R S = (\x. S *<= x \ x \ R)" - apply (rule ext) - by (metis isUb_def) - -lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def) -lemma rsup_bounds: assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" - shows "a \ rsup S \ rsup S \ b" -proof- - from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast - hence b: "rsup S \ b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def') - from Se obtain y where y: "y \ S" by blast - from lub l have "a \ rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def') - apply (erule ballE[where x=y]) - apply (erule ballE[where x=y]) - apply arith - using y apply auto - done - with b show ?thesis by blast -qed - -lemma rsup_abs_le: "S \ {} \ (\x\S. \x\ \ a) \ \rsup S\ \ a" - unfolding abs_le_interval_iff using rsup_bounds[of S "-a" a] - by (auto simp add: setge_def setle_def) - -lemma rsup_asclose: assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\rsup S - l\ \ e" -proof- - have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" by arith - show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th - by (auto simp add: setge_def setle_def) -qed - -definition rinf:: "real set \ real" where - "rinf S = (SOME a. isGlb UNIV S a)" - -lemma rinf_alt: "rinf S = (SOME a. (\x \ S. x \ a) \ (\b. (\x \ S. x \ b) \ a \ b))" by (auto simp add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def) - -lemma reals_complete_Glb: assumes Se: "\x. x \ S" and lb: "\ y. isLb UNIV S y" - shows "\(t::real). isGlb UNIV S t" -proof- - let ?M = "uminus ` S" - from lb have th: "\y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def) - by (rule_tac x="-y" in exI, auto) - from Se have Me: "\x. x \ ?M" by blast - from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast - have "isGlb UNIV S (- t)" using t - apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def) - apply (erule_tac x="-y" in allE) - apply auto - done - then show ?thesis by metis -qed - -lemma rinf: assumes Se: "S \ {}" and b: "\b. b <=* S" - shows "isGlb UNIV S (rinf S)" -using Se b -unfolding rinf_def -apply clarify -apply (rule someI_ex) -apply (rule reals_complete_Glb) -apply (auto simp add: isLb_def setle_def setge_def) -done - -lemma rinf_ge: assumes Se: "S \ {}" and Sb: "b <=* S" shows "rinf S \ b" -proof- - from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def) - from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)" by blast - then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def) -qed - -lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \ {}" - shows "rinf S = Min S" -using fS Se -proof- - let ?m = "Min S" - from Min_le[OF fS] have Sm: "\ x\ S. x \ ?m" by metis - with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def) - from Min_in[OF fS Se] glb have mrS: "?m \ rinf S" - by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def) - moreover - have "rinf S \ ?m" using Sm glb - by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def) - ultimately show ?thesis by arith -qed - -lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \ {}" - shows "rinf S \ S" - using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis - -lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \ {}" - shows "isLb S S (rinf S)" - using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS] - unfolding isLb_def setge_def by metis - -lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a \ rinf S \ (\ x \ S. a \ x)" -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) - -lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a \ rinf S \ (\ x \ S. a \ x)" -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) - -lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a < rinf S \ (\ x \ S. a < x)" -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) - -lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \ {}" - shows "a > rinf S \ (\ x \ S. a > x)" -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) - -lemma rinf_unique: assumes b: "b <=* S" and S: "\b' > b. \x \ S. b' > x" - shows "rinf S = b" -using b S -unfolding setge_def rinf_alt -apply - -apply (rule some_equality) -apply (metis linorder_not_le order_eq_iff[symmetric])+ -done - -lemma rinf_ge_subset: "S\{} \ S \ T \ (\b. b <=* T) \ rinf S >= rinf T" - apply (rule rinf_ge) - apply simp - using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def) - -lemma isLb_def': "isLb R S = (\x. x <=* S \ x \ R)" - apply (rule ext) - by (metis isLb_def) - -lemma rinf_bounds: assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" - shows "a \ rinf S \ rinf S \ b" -proof- - from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast - hence b: "a \ rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def') - from Se obtain y where y: "y \ S" by blast - from lub u have "b \ rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def') - apply (erule ballE[where x=y]) - apply (erule ballE[where x=y]) - apply arith - using y apply auto - done - with b show ?thesis by blast -qed - -lemma rinf_abs_ge: "S \ {} \ (\x\S. \x\ \ a) \ \rinf S\ \ a" - unfolding abs_le_interval_iff using rinf_bounds[of S "-a" a] - by (auto simp add: setge_def setle_def) - -lemma rinf_asclose: assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\rinf S - l\ \ e" -proof- - have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" by arith - show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th - by (auto simp add: setge_def setle_def) -qed - - - subsection{* Operator norm. *} -definition "onorm f = rsup {norm (f x)| x. norm x = 1}" +definition "onorm f = Sup {norm (f x)| x. norm x = 1}" lemma norm_bound_generalize: fixes f:: "real ^'n::finite \ real^'m::finite" @@ -2578,7 +2345,7 @@ have Se: "?S \ {}" using norm_basis by auto from linear_bounded[OF lf] have b: "\ b. ?S *<= b" unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) - {from rsup[OF Se b, unfolded onorm_def[symmetric]] + {from Sup[OF Se b, unfolded onorm_def[symmetric]] show "norm (f x) <= onorm f * norm x" apply - apply (rule spec[where x = x]) @@ -2586,7 +2353,7 @@ by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} { show "\x. norm (f x) <= b * norm x \ onorm f <= b" - using rsup[OF Se b, unfolded onorm_def[symmetric]] + using Sup[OF Se b, unfolded onorm_def[symmetric]] unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} } @@ -2612,7 +2379,7 @@ by(auto intro: vector_choose_size set_ext) show ?thesis unfolding onorm_def th - apply (rule rsup_unique) by (simp_all add: setle_def) + apply (rule Sup_unique) by (simp_all add: setle_def) qed lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \ real ^'m::finite)" @@ -3055,31 +2822,6 @@ qed (* ------------------------------------------------------------------------- *) -(* Relate max and min to sup and inf. *) -(* ------------------------------------------------------------------------- *) - -lemma real_max_rsup: "max x y = rsup {x,y}" -proof- - have f: "finite {x, y}" "{x,y} \ {}" by simp_all - from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \ max x y" by simp - moreover - have "max x y \ rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"] - by (simp add: linorder_linear) - ultimately show ?thesis by arith -qed - -lemma real_min_rinf: "min x y = rinf {x,y}" -proof- - have f: "finite {x, y}" "{x,y} \ {}" by simp_all - from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \ min x y" - by (simp add: linorder_linear) - moreover - have "min x y \ rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"] - by simp - ultimately show ?thesis by arith -qed - -(* ------------------------------------------------------------------------- *) (* Geometric progression. *) (* ------------------------------------------------------------------------- *) @@ -5048,7 +4790,7 @@ (* Infinity norm. *) -definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\ (UNIV :: 'n set)}" +definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\ (UNIV :: 'n set)}" lemma numseg_dimindex_nonempty: "\i. i \ (UNIV :: 'n set)" by auto @@ -5065,7 +4807,7 @@ lemma infnorm_pos_le: "0 \ infnorm (x::real^'n::finite)" unfolding infnorm_def - unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma] + unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma] unfolding infnorm_set_image by auto @@ -5076,13 +4818,13 @@ have th2: "\x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith show ?thesis unfolding infnorm_def - unfolding rsup_finite_le_iff[ OF infnorm_set_lemma] + unfolding Sup_finite_le_iff[ OF infnorm_set_lemma] apply (subst diff_le_eq[symmetric]) - unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma] + unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma] unfolding infnorm_set_image bex_simps apply (subst th) unfolding th1 - unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma] + unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps bex_simps apply simp @@ -5094,7 +4836,7 @@ proof- have "infnorm x <= 0 \ x = 0" unfolding infnorm_def - unfolding rsup_finite_le_iff[OF infnorm_set_lemma] + unfolding Sup_finite_le_iff[OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps by vector then show ?thesis using infnorm_pos_le[of x] by simp @@ -5105,7 +4847,7 @@ lemma infnorm_neg: "infnorm (- x) = infnorm x" unfolding infnorm_def - apply (rule cong[of "rsup" "rsup"]) + apply (rule cong[of "Sup" "Sup"]) apply blast apply (rule set_ext) apply auto @@ -5140,14 +4882,15 @@ apply (rule finite_imageI) unfolding Collect_def mem_def by simp have S0: "?S \ {}" by blast have th1: "\S f. f ` S = { f i| i. i \ S}" by blast - from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0] - show ?thesis unfolding infnorm_def isUb_def setle_def - unfolding infnorm_set_image ball_simps by auto + from Sup_finite_in[OF fS S0] + show ?thesis unfolding infnorm_def infnorm_set_image + by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty + rangeI real_le_refl) qed lemma infnorm_mul_lemma: "infnorm(a *s x) <= \a\ * infnorm x" apply (subst infnorm_def) - unfolding rsup_finite_le_iff[OF infnorm_set_lemma] + unfolding Sup_finite_le_iff[OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps apply (simp add: abs_mult) apply (rule allI) @@ -5180,7 +4923,7 @@ (* Prove that it differs only up to a bound from Euclidean norm. *) lemma infnorm_le_norm: "infnorm x \ norm x" - unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma] + unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps by (metis component_le_norm) lemma card_enum: "card {1 .. n} = n" by auto @@ -5200,7 +4943,7 @@ apply (rule setsum_bounded) apply (rule power_mono) unfolding abs_of_nonneg[OF infnorm_pos_le] - unfolding infnorm_def rsup_finite_ge_iff[OF infnorm_set_lemma] + unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma] unfolding infnorm_set_image bex_simps apply blast by (rule abs_ge_zero) diff -r 02de0317f66f -r 73a0c804840f src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Oct 28 11:43:06 2009 +0000 @@ -2100,59 +2100,54 @@ shows "bounded S \ (\a. \x\S. abs x <= a)" by (simp add: bounded_iff) -lemma bounded_has_rsup: assumes "bounded S" "S \ {}" - shows "\x\S. x <= rsup S" and "\b. (\x\S. x <= b) \ rsup S <= b" +lemma bounded_has_Sup: + fixes S :: "real set" + assumes "bounded S" "S \ {}" + shows "\x\S. x <= Sup S" and "\b. (\x\S. x <= b) \ Sup S <= b" +proof + fix x assume "x\S" + thus "x \ Sup S" + by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real) +next + show "\b. (\x\S. x \ b) \ Sup S \ b" using assms + by (metis SupInf.Sup_least) +qed + +lemma Sup_insert: + fixes S :: "real set" + shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" +by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal) + +lemma Sup_insert_finite: + fixes S :: "real set" + shows "finite S \ Sup(insert x S) = (if S = {} then x else max x (Sup S))" + apply (rule Sup_insert) + apply (rule finite_imp_bounded) + by simp + +lemma bounded_has_Inf: + fixes S :: "real set" + assumes "bounded S" "S \ {}" + shows "\x\S. x >= Inf S" and "\b. (\x\S. x >= b) \ Inf S >= b" proof fix x assume "x\S" from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto - hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def) - thus "x \ rsup S" using rsup[OF `S\{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\S` by auto -next - show "\b. (\x\S. x \ b) \ rsup S \ b" using assms - using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def] - apply (auto simp add: bounded_real) - by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def) -qed - -lemma rsup_insert: assumes "bounded S" - shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))" -proof(cases "S={}") - case True thus ?thesis using rsup_finite_in[of "{x}"] by auto + thus "x \ Inf S" using `x\S` + by (metis Inf_lower_EX abs_le_D2 minus_le_iff) next - let ?S = "insert x S" - case False - hence *:"\x\S. x \ rsup S" using bounded_has_rsup(1)[of S] using assms by auto - hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto - hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto - moreover - have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto - { fix y assume as:"isUb UNIV (insert x S) y" - hence "max x (rsup S) \ y" unfolding isUb_def using rsup_le[OF `S\{}`] - unfolding setle_def by auto } - hence "max x (rsup S) <=* isUb UNIV (insert x S)" unfolding setge_def Ball_def mem_def by auto - hence "isLub UNIV ?S (max x (rsup S))" using ** isLubI2[of UNIV ?S "max x (rsup S)"] unfolding Collect_def by auto - ultimately show ?thesis using real_isLub_unique[of UNIV ?S] using `S\{}` by auto -qed - -lemma sup_insert_finite: "finite S \ rsup(insert x S) = (if S = {} then x else max x (rsup S))" - apply (rule rsup_insert) - apply (rule finite_imp_bounded) - by simp - -lemma bounded_has_rinf: - assumes "bounded S" "S \ {}" - shows "\x\S. x >= rinf S" and "\b. (\x\S. x >= b) \ rinf S >= b" -proof - fix x assume "x\S" - from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto - hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto - thus "x \ rinf S" using rinf[OF `S\{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\S` by auto -next - show "\b. (\x\S. x >= b) \ rinf S \ b" using assms - using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def] - apply (auto simp add: bounded_real) - by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def) -qed + show "\b. (\x\S. x >= b) \ Inf S \ b" using assms + by (metis SupInf.Inf_greatest) +qed + +lemma Inf_insert: + fixes S :: "real set" + shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" +by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) +lemma Inf_insert_finite: + fixes S :: "real set" + shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" + by (rule Inf_insert, rule finite_imp_bounded, simp) + (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *) lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)" @@ -2161,29 +2156,6 @@ apply (blast intro!: order_antisym dest!: isGlb_le_isLb) done -lemma rinf_insert: assumes "bounded S" - shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs") -proof(cases "S={}") - case True thus ?thesis using rinf_finite_in[of "{x}"] by auto -next - let ?S = "insert x S" - case False - hence *:"\x\S. x \ rinf S" using bounded_has_rinf(1)[of S] using assms by auto - hence "min x (rinf S) <=* insert x S" unfolding setge_def by auto - hence "isGlb UNIV ?S (rinf ?S)" using rinf[of ?S] by auto - moreover - have **:"isLb UNIV ?S (min x (rinf S))" unfolding isLb_def setge_def using * by auto - { fix y assume as:"isLb UNIV (insert x S) y" - hence "min x (rinf S) \ y" unfolding isLb_def using rinf_ge[OF `S\{}`] - unfolding setge_def by auto } - hence "isLb UNIV (insert x S) *<= min x (rinf S)" unfolding setle_def Ball_def mem_def by auto - hence "isGlb UNIV ?S (min x (rinf S))" using ** isGlbI2[of UNIV ?S "min x (rinf S)"] unfolding Collect_def by auto - ultimately show ?thesis using real_isGlb_unique[of UNIV ?S] using `S\{}` by auto -qed - -lemma inf_insert_finite: "finite S ==> rinf(insert x S) = (if S = {} then x else min x (rinf S))" - by (rule rinf_insert, rule finite_imp_bounded, simp) - subsection{* Compactness (the definition is the one based on convegent subsequences). *} definition @@ -4120,30 +4092,35 @@ shows "\x \ s. \y \ s. y \ x" proof- from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto - { fix e::real assume as: "\x\s. x \ rsup s" "rsup s \ s" "0 < e" "\x'\s. x' = rsup s \ \ rsup s - x' < e" - have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto - moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto - ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto } - thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]] - apply(rule_tac x="rsup s" in bexI) by auto -qed + { fix e::real assume as: "\x\s. x \ Sup s" "Sup s \ s" "0 < e" "\x'\s. x' = Sup s \ \ Sup s - x' < e" + have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto + moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto + ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto } + thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]] + apply(rule_tac x="Sup s" in bexI) by auto +qed + +lemma Inf: + fixes S :: "real set" + shows "S \ {} ==> (\b. b <=* S) ==> isGlb UNIV S (Inf S)" +by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) lemma compact_attains_inf: fixes s :: "real set" assumes "compact s" "s \ {}" shows "\x \ s. \y \ s. x \ y" proof- from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto - { fix e::real assume as: "\x\s. x \ rinf s" "rinf s \ s" "0 < e" - "\x'\s. x' = rinf s \ \ abs (x' - rinf s) < e" - have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto + { fix e::real assume as: "\x\s. x \ Inf s" "Inf s \ s" "0 < e" + "\x'\s. x' = Inf s \ \ abs (x' - Inf s) < e" + have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto moreover { fix x assume "x \ s" - hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto - have "rinf s + e \ x" using as(4)[THEN bspec[where x=x]] using as(2) `x\s` unfolding * by auto } - hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto - ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto } - thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]] - apply(rule_tac x="rinf s" in bexI) by auto + hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto + have "Inf s + e \ x" using as(4)[THEN bspec[where x=x]] using as(2) `x\s` unfolding * by auto } + hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto + ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto } + thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]] + apply(rule_tac x="Inf s" in bexI) by auto qed lemma continuous_attains_sup: @@ -4413,7 +4390,7 @@ text{* We can state this in terms of diameter of a set. *} -definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \ s \ y \ s})" +definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \ s \ y \ s})" (* TODO: generalize to class metric_space *) lemma diameter_bounded: @@ -4427,12 +4404,22 @@ hence "norm (x - y) \ 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps) } note * = this { fix x y assume "x\s" "y\s" hence "s \ {}" by auto - have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\{}` unfolding setle_def by auto + have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\{}` unfolding setle_def + apply auto (*FIXME: something horrible has happened here!*) + apply atomize + apply safe + apply metis + + done have "norm(x - y) \ diameter s" unfolding diameter_def using `s\{}` *[OF `x\s` `y\s`] `x\s` `y\s` isLubD1[OF lub] unfolding setle_def by auto } moreover { fix d::real assume "d>0" "d < diameter s" hence "s\{}" unfolding diameter_def by auto - hence lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] unfolding setle_def by auto + hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def + apply auto (*FIXME: something horrible has happened here!*) + apply atomize + apply safe + apply metis + + done have "\d' \ ?D. d' > d" proof(rule ccontr) assume "\ (\d'\{norm (x - y) |x y. x \ s \ y \ s}. d < d')" @@ -4456,8 +4443,8 @@ proof- have b:"bounded s" using assms(1) by (rule compact_imp_bounded) then obtain x y where xys:"x\s" "y\s" and xy:"\u\s. \v\s. norm (u - v) \ norm (x - y)" using compact_sup_maxdistance[OF assms] by auto - hence "diameter s \ norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \ s \ y \ s}" "norm (x - y)"] - unfolding setle_def and diameter_def by auto + hence "diameter s \ norm (x - y)" + by (force simp add: diameter_def intro!: Sup_least) thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto qed diff -r 02de0317f66f -r 73a0c804840f src/HOL/Probability/Caratheodory.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Caratheodory.thy Wed Oct 28 11:43:06 2009 +0000 @@ -0,0 +1,993 @@ +header {*Caratheodory Extension Theorem*} + +theory Caratheodory + imports Sigma_Algebra SupInf SeriesPlus + +begin + +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} + +subsection {* Measure Spaces *} + +text {*A measure assigns a nonnegative real to every measurable set. + It is countably additive for disjoint sets.*} + +record 'a measure_space = "'a algebra" + + measure:: "'a set \ real" + +definition + disjoint_family where + "disjoint_family A \ (\m n. m \ n \ A m \ A n = {})" + +definition + positive where + "positive M f \ f {} = (0::real) & (\x \ sets M. 0 \ f x)" + +definition + additive where + "additive M f \ + (\x \ sets M. \y \ sets M. x \ y = {} + \ f (x \ y) = f x + f y)" + +definition + countably_additive where + "countably_additive M f \ + (\A. range A \ sets M \ + disjoint_family A \ + (\i. A i) \ sets M \ + (\n. f (A n)) sums f (\i. A i))" + +definition + increasing where + "increasing M f \ (\x \ sets M. \y \ sets M. x \ y \ f x \ f y)" + +definition + subadditive where + "subadditive M f \ + (\x \ sets M. \y \ sets M. x \ y = {} + \ f (x \ y) \ f x + f y)" + +definition + countably_subadditive where + "countably_subadditive M f \ + (\A. range A \ sets M \ + disjoint_family A \ + (\i. A i) \ sets M \ + summable (f o A) \ + f (\i. A i) \ suminf (\n. f (A n)))" + +definition + lambda_system where + "lambda_system M f = + {l. l \ sets M & (\x \ sets M. f (l \ x) + f ((space M - l) \ x) = f x)}" + +definition + outer_measure_space where + "outer_measure_space M f \ + positive M f & increasing M f & countably_subadditive M f" + +definition + measure_set where + "measure_set M f X = + {r . \A. range A \ sets M & disjoint_family A & X \ (\i. A i) & (f \ A) sums r}" + + +locale measure_space = sigma_algebra + + assumes positive: "!!a. a \ sets M \ 0 \ measure M a" + and empty_measure [simp]: "measure M {} = (0::real)" + and ca: "countably_additive M (measure M)" + +subsection {* Basic Lemmas *} + +lemma positive_imp_0: "positive M f \ f {} = 0" + by (simp add: positive_def) + +lemma positive_imp_pos: "positive M f \ x \ sets M \ 0 \ f x" + by (simp add: positive_def) + +lemma increasingD: + "increasing M f \ x \ y \ x\sets M \ y\sets M \ f x \ f y" + by (auto simp add: increasing_def) + +lemma subadditiveD: + "subadditive M f \ x \ y = {} \ x\sets M \ y\sets M + \ f (x \ y) \ f x + f y" + by (auto simp add: subadditive_def) + +lemma additiveD: + "additive M f \ x \ y = {} \ x\sets M \ y\sets M + \ f (x \ y) = f x + f y" + by (auto simp add: additive_def) + +lemma countably_additiveD: + "countably_additive M f \ range A \ sets M \ disjoint_family A + \ (\i. A i) \ sets M \ (\n. f (A n)) sums f (\i. A i)" + by (simp add: countably_additive_def) + +lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" + by blast + +lemma Int_Diff_Un: "A \ B \ (A - B) = A" + by blast + +lemma disjoint_family_subset: + "disjoint_family A \ (!!x. B x \ A x) \ disjoint_family B" + by (force simp add: disjoint_family_def) + +subsection {* A Two-Element Series *} + +definition binaryset :: "'a set \ 'a set \ nat \ 'a set " + where "binaryset A B = (\\<^isup>x. {})(0 := A, Suc 0 := B)" + +lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" + apply (simp add: binaryset_def) + apply (rule set_ext) + apply (auto simp add: image_iff) + done + +lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B" + by (simp add: UNION_eq_Union_image range_binaryset_eq) + +lemma LIMSEQ_binaryset: + assumes f: "f {} = 0" + shows "(\n. \i = 0.. f A + f B" +proof - + have "(\n. \i = 0..< Suc (Suc n). f (binaryset A B i)) = (\n. f A + f B)" + proof + fix n + show "(\i\nat = 0\nat.. f A + f B" by (rule LIMSEQ_const) + ultimately + have "(\n. \i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" + by metis + hence "(\n. \i = 0..< n+2. f (binaryset A B i)) ----> f A + f B" + by simp + thus ?thesis by (rule LIMSEQ_offset [where k=2]) +qed + +lemma binaryset_sums: + assumes f: "f {} = 0" + shows "(\n. f (binaryset A B n)) sums (f A + f B)" + by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) + +lemma suminf_binaryset_eq: + "f {} = 0 \ suminf (\n. f (binaryset A B n)) = f A + f B" + by (metis binaryset_sums sums_unique) + + +subsection {* Lambda Systems *} + +lemma (in algebra) lambda_system_eq: + "lambda_system M f = + {l. l \ sets M & (\x \ sets M. f (x \ l) + f (x - l) = f x)}" +proof - + have [simp]: "!!l x. l \ sets M \ x \ sets M \ (space M - l) \ x = x - l" + by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space) + show ?thesis + by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+ +qed + +lemma (in algebra) lambda_system_empty: + "positive M f \ {} \ lambda_system M f" + by (auto simp add: positive_def lambda_system_eq) + +lemma lambda_system_sets: + "x \ lambda_system M f \ x \ sets M" + by (simp add: lambda_system_def) + +lemma (in algebra) lambda_system_Compl: + fixes f:: "'a set \ real" + assumes x: "x \ lambda_system M f" + shows "space M - x \ lambda_system M f" + proof - + have "x \ space M" + by (metis sets_into_space lambda_system_sets x) + hence "space M - (space M - x) = x" + by (metis double_diff equalityE) + with x show ?thesis + by (force simp add: lambda_system_def) + qed + +lemma (in algebra) lambda_system_Int: + fixes f:: "'a set \ real" + assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" + shows "x \ y \ lambda_system M f" + proof - + from xl yl show ?thesis + proof (auto simp add: positive_def lambda_system_eq Int) + fix u + assume x: "x \ sets M" and y: "y \ sets M" and u: "u \ sets M" + and fx: "\z\sets M. f (z \ x) + f (z - x) = f z" + and fy: "\z\sets M. f (z \ y) + f (z - y) = f z" + have "u - x \ y \ sets M" + by (metis Diff Diff_Int Un u x y) + moreover + have "(u - (x \ y)) \ y = u \ y - x" by blast + moreover + have "u - x \ y - y = u - y" by blast + ultimately + have ey: "f (u - x \ y) = f (u \ y - x) + f (u - y)" using fy + by force + have "f (u \ (x \ y)) + f (u - x \ y) + = (f (u \ (x \ y)) + f (u \ y - x)) + f (u - y)" + by (simp add: ey) + also have "... = (f ((u \ y) \ x) + f (u \ y - x)) + f (u - y)" + by (simp add: Int_ac) + also have "... = f (u \ y) + f (u - y)" + using fx [THEN bspec, of "u \ y"] Int y u + by force + also have "... = f u" + by (metis fy u) + finally show "f (u \ (x \ y)) + f (u - x \ y) = f u" . + qed + qed + + +lemma (in algebra) lambda_system_Un: + fixes f:: "'a set \ real" + assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" + shows "x \ y \ lambda_system M f" +proof - + have "(space M - x) \ (space M - y) \ sets M" + by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) + moreover + have "x \ y = space M - ((space M - x) \ (space M - y))" + by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ + ultimately show ?thesis + by (metis lambda_system_Compl lambda_system_Int xl yl) +qed + +lemma (in algebra) lambda_system_algebra: + "positive M f \ algebra (M (|sets := lambda_system M f|))" + apply (auto simp add: algebra_def) + apply (metis lambda_system_sets set_mp sets_into_space) + apply (metis lambda_system_empty) + apply (metis lambda_system_Compl) + apply (metis lambda_system_Un) + done + +lemma (in algebra) lambda_system_strong_additive: + assumes z: "z \ sets M" and disj: "x \ y = {}" + and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" + shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)" + proof - + have "z \ x = (z \ (x \ y)) \ x" using disj by blast + moreover + have "z \ y = (z \ (x \ y)) - x" using disj by blast + moreover + have "(z \ (x \ y)) \ sets M" + by (metis Int Un lambda_system_sets xl yl z) + ultimately show ?thesis using xl yl + by (simp add: lambda_system_eq) + qed + +lemma (in algebra) Int_space_eq1 [simp]: "x \ sets M \ space M \ x = x" + by (metis Int_absorb1 sets_into_space) + +lemma (in algebra) Int_space_eq2 [simp]: "x \ sets M \ x \ space M = x" + by (metis Int_absorb2 sets_into_space) + +lemma (in algebra) lambda_system_additive: + "additive (M (|sets := lambda_system M f|)) f" + proof (auto simp add: additive_def) + fix x and y + assume disj: "x \ y = {}" + and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" + hence "x \ sets M" "y \ sets M" by (blast intro: lambda_system_sets)+ + thus "f (x \ y) = f x + f y" + using lambda_system_strong_additive [OF top disj xl yl] + by (simp add: Un) + qed + + +lemma (in algebra) countably_subadditive_subadditive: + assumes f: "positive M f" and cs: "countably_subadditive M f" + shows "subadditive M f" +proof (auto simp add: subadditive_def) + fix x y + assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" + hence "disjoint_family (binaryset x y)" + by (auto simp add: disjoint_family_def binaryset_def) + hence "range (binaryset x y) \ sets M \ + (\i. binaryset x y i) \ sets M \ + summable (f o (binaryset x y)) \ + f (\i. binaryset x y i) \ suminf (\n. f (binaryset x y n))" + using cs by (simp add: countably_subadditive_def) + hence "{x,y,{}} \ sets M \ x \ y \ sets M \ + summable (f o (binaryset x y)) \ + f (x \ y) \ suminf (\n. f (binaryset x y n))" + by (simp add: range_binaryset_eq UN_binaryset_eq) + thus "f (x \ y) \ f x + f y" using f x y binaryset_sums + by (auto simp add: Un sums_iff positive_def o_def) +qed + + +definition disjointed :: "(nat \ 'a set) \ nat \ 'a set " + where "disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)" + apply (rule UN_finite2_eq [where k=0]) + apply (simp add: finite_UN_disjointed_eq) + done + +lemma less_disjoint_disjointed: "m disjointed A m \ disjointed A n = {}" + by (auto simp add: disjointed_def) + +lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" + by (simp add: disjoint_family_def) + (metis neq_iff Int_commute less_disjoint_disjointed) + +lemma disjointed_subset: "disjointed A n \ A n" + by (auto simp add: disjointed_def) + + +lemma (in algebra) UNION_in_sets: + fixes A:: "nat \ 'a set" + assumes A: "range A \ sets M " + shows "(\i\{0.. sets M" +proof (induct n) + case 0 show ?case by simp +next + case (Suc n) + thus ?case + by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) +qed + +lemma (in algebra) range_disjointed_sets: + assumes A: "range A \ sets M " + shows "range (disjointed A) \ sets M" +proof (auto simp add: disjointed_def) + fix n + show "A n - (\i\{0.. sets M" using UNION_in_sets + by (metis A Diff UNIV_I disjointed_def image_subset_iff) +qed + +lemma sigma_algebra_disjoint_iff: + "sigma_algebra M \ + algebra M & + (\A. range A \ sets M \ disjoint_family A \ + (\i::nat. A i) \ sets M)" +proof (auto simp add: sigma_algebra_iff) + fix A :: "nat \ 'a set" + assume M: "algebra M" + and A: "range A \ sets M" + and UnA: "\A. range A \ sets M \ + disjoint_family A \ (\i::nat. A i) \ sets M" + hence "range (disjointed A) \ sets M \ + disjoint_family (disjointed A) \ + (\i. disjointed A i) \ sets M" by blast + hence "(\i. disjointed A i) \ sets M" + by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) + thus "(\i::nat. A i) \ sets M" by (simp add: UN_disjointed_eq) +qed + + +lemma (in algebra) additive_sum: + fixes A:: "nat \ 'a set" + assumes f: "positive M f" and ad: "additive M f" + and A: "range A \ sets M" + and disj: "disjoint_family A" + shows "setsum (f o A) {0..i\{0.. (\i\{0.. sets M" using A by blast + moreover have "(\i\{0.. sets M" + by (metis A UNION_in_sets atLeast0LessThan) + moreover + ultimately have "f (A n \ (\i\{0..i\{0.. range A \ sets M \ disjoint_family A \ + (\i. A i) \ sets M \ summable (f o A) \ f (\i. A i) \ suminf (f o A)" + by (auto simp add: countably_subadditive_def o_def) + +lemma (in algebra) increasing_additive_summable: + fixes A:: "nat \ 'a set" + assumes f: "positive M f" and ad: "additive M f" + and inc: "increasing M f" + and A: "range A \ sets M" + and disj: "disjoint_family A" + shows "summable (f o A)" +proof (rule pos_summable) + fix n + show "0 \ (f \ A) n" using f A + by (force simp add: positive_def) + next + fix n + have "setsum (f \ A) {0..i\{0.. f (space M)" using space_closed A + by (blast intro: increasingD [OF inc] UNION_in_sets top) + finally show "setsum (f \ A) {0.. f (space M)" . +qed + +lemma lambda_system_positive: + "positive M f \ positive (M (|sets := lambda_system M f|)) f" + by (simp add: positive_def lambda_system_def) + +lemma lambda_system_increasing: + "increasing M f \ increasing (M (|sets := lambda_system M f|)) f" + by (simp add: increasing_def lambda_system_def) + +lemma (in algebra) lambda_system_strong_sum: + fixes A:: "nat \ 'a set" + assumes f: "positive M f" and a: "a \ sets M" + and A: "range A \ lambda_system M f" + and disj: "disjoint_family A" + shows "(\i = 0..A i)) = f (a \ (\i\{0.. UNION {0.. lambda_system M f" using A + by blast + have 4: "UNION {0.. lambda_system M f" + using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] + by simp + from Suc.hyps show ?case + by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) +qed + + +lemma (in sigma_algebra) lambda_system_caratheodory: + assumes oms: "outer_measure_space M f" + and A: "range A \ lambda_system M f" + and disj: "disjoint_family A" + shows "(\i. A i) \ lambda_system M f & (f \ A) sums f (\i. A i)" +proof - + have pos: "positive M f" and inc: "increasing M f" + and csa: "countably_subadditive M f" + by (metis oms outer_measure_space_def)+ + have sa: "subadditive M f" + by (metis countably_subadditive_subadditive csa pos) + have A': "range A \ sets (M(|sets := lambda_system M f|))" using A + by simp + have alg_ls: "algebra (M(|sets := lambda_system M f|))" + by (rule lambda_system_algebra [OF pos]) + have A'': "range A \ sets M" + by (metis A image_subset_iff lambda_system_sets) + have sumfA: "summable (f \ A)" + by (metis algebra.increasing_additive_summable [OF alg_ls] + lambda_system_positive lambda_system_additive lambda_system_increasing + A' oms outer_measure_space_def disj) + have U_in: "(\i. A i) \ sets M" + by (metis A countable_UN image_subset_iff lambda_system_sets) + have U_eq: "f (\i. A i) = suminf (f o A)" + proof (rule antisym) + show "f (\i. A i) \ suminf (f \ A)" + by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) + show "suminf (f \ A) \ f (\i. A i)" + by (rule suminf_le [OF sumfA]) + (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right + lambda_system_positive lambda_system_additive + subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) + qed + { + fix a + assume a [iff]: "a \ sets M" + have "f (a \ (\i. A i)) + f (a - (\i. A i)) = f a" + proof - + have summ: "summable (f \ (\i. a \ i) \ A)" using pos A'' + apply - + apply (rule summable_comparison_test [OF _ sumfA]) + apply (rule_tac x="0" in exI) + apply (simp add: positive_def) + apply (auto simp add: ) + apply (subst abs_of_nonneg) + apply (metis A'' Int UNIV_I a image_subset_iff) + apply (blast intro: increasingD [OF inc] a) + done + show ?thesis + proof (rule antisym) + have "range (\i. a \ A i) \ sets M" using A'' + by blast + moreover + have "disjoint_family (\i. a \ A i)" using disj + by (auto simp add: disjoint_family_def) + moreover + have "a \ (\i. A i) \ sets M" + by (metis Int U_in a) + ultimately + have "f (a \ (\i. A i)) \ suminf (f \ (\i. a \ i) \ A)" + using countably_subadditiveD [OF csa, of "(\i. a \ A i)"] summ + by (simp add: o_def) + moreover + have "suminf (f \ (\i. a \ i) \ A) \ f a - f (a - (\i. A i))" + proof (rule suminf_le [OF summ]) + fix n + have UNION_in: "(\i\{0.. sets M" + by (metis A'' UNION_in_sets) + have le_fa: "f (UNION {0.. a) \ f a" using A'' + by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) + have ls: "(\i\{0.. lambda_system M f" + using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]] + by (simp add: A) + hence eq_fa: "f (a \ (\i\{0..i\{0..i. A i)) \ f (a - (\i\{0.. (\i. a \ i) \ A) {0.. f a - f (a - (\i. A i))" + using eq_fa + by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos + a A disj) + qed + ultimately show "f (a \ (\i. A i)) + f (a - (\i. A i)) \ f a" + by arith + next + have "f a \ f (a \ (\i. A i) \ (a - (\i. A i)))" + by (blast intro: increasingD [OF inc] a U_in) + also have "... \ f (a \ (\i. A i)) + f (a - (\i. A i))" + by (blast intro: subadditiveD [OF sa] Int Diff U_in) + finally show "f a \ f (a \ (\i. A i)) + f (a - (\i. A i))" . + qed + qed + } + thus ?thesis + by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA) +qed + +lemma (in sigma_algebra) caratheodory_lemma: + assumes oms: "outer_measure_space M f" + shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)" +proof - + have pos: "positive M f" + by (metis oms outer_measure_space_def) + have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)" + using lambda_system_algebra [OF pos] + by (simp add: algebra_def) + then moreover + have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)" + using lambda_system_caratheodory [OF oms] + by (simp add: sigma_algebra_disjoint_iff) + moreover + have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" + using pos lambda_system_caratheodory [OF oms] + by (simp add: measure_space_axioms_def positive_def lambda_system_sets + countably_additive_def o_def) + ultimately + show ?thesis + by intro_locales (auto simp add: sigma_algebra_def) +qed + + +lemma (in algebra) inf_measure_nonempty: + assumes f: "positive M f" and b: "b \ sets M" and a: "a \ b" + shows "f b \ measure_set M f a" +proof - + have "(f \ (\i. {})(0 := b)) sums setsum (f \ (\i. {})(0 := b)) {0..<1::nat}" + by (rule series_zero) (simp add: positive_imp_0 [OF f]) + also have "... = f b" + by simp + finally have "(f \ (\i. {})(0 := b)) sums f b" . + thus ?thesis using a + by (auto intro!: exI [of _ "(\i. {})(0 := b)"] + simp add: measure_set_def disjoint_family_def b split_if_mem2) +qed + +lemma (in algebra) inf_measure_pos0: + "positive M f \ x \ measure_set M f a \ 0 \ x" +apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero) +apply blast +done + +lemma (in algebra) inf_measure_pos: + shows "positive M f \ x \ space M \ 0 \ Inf (measure_set M f x)" +apply (rule Inf_greatest) +apply (metis emptyE inf_measure_nonempty top) +apply (metis inf_measure_pos0) +done + +lemma (in algebra) additive_increasing: + assumes posf: "positive M f" and addf: "additive M f" + shows "increasing M f" +proof (auto simp add: increasing_def) + fix x y + assume xy: "x \ sets M" "y \ sets M" "x \ y" + have "f x \ f x + f (y-x)" using posf + by (simp add: positive_def) (metis Diff xy) + also have "... = f (x \ (y-x))" using addf + by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy) + also have "... = f y" + by (metis Un_Diff_cancel Un_absorb1 xy) + finally show "f x \ f y" . +qed + +lemma (in algebra) countably_additive_additive: + assumes posf: "positive M f" and ca: "countably_additive M f" + shows "additive M f" +proof (auto simp add: additive_def) + fix x y + assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" + hence "disjoint_family (binaryset x y)" + by (auto simp add: disjoint_family_def binaryset_def) + hence "range (binaryset x y) \ sets M \ + (\i. binaryset x y i) \ sets M \ + f (\i. binaryset x y i) = suminf (\n. f (binaryset x y n))" + using ca + by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) + hence "{x,y,{}} \ sets M \ x \ y \ sets M \ + f (x \ y) = suminf (\n. f (binaryset x y n))" + by (simp add: range_binaryset_eq UN_binaryset_eq) + thus "f (x \ y) = f x + f y" using posf x y + by (simp add: Un suminf_binaryset_eq positive_def) +qed + +lemma (in algebra) inf_measure_agrees: + assumes posf: "positive M f" and ca: "countably_additive M f" + and s: "s \ sets M" + shows "Inf (measure_set M f s) = f s" +proof (rule Inf_eq) + fix z + assume z: "z \ measure_set M f s" + from this obtain A where + A: "range A \ sets M" and disj: "disjoint_family A" + and "s \ (\x. A x)" and sm: "summable (f \ A)" + and si: "suminf (f \ A) = z" + by (auto simp add: measure_set_def sums_iff) + hence seq: "s = (\i. A i \ s)" by blast + have inc: "increasing M f" + by (metis additive_increasing ca countably_additive_additive posf) + have sums: "(\i. f (A i \ s)) sums f (\i. A i \ s)" + proof (rule countably_additiveD [OF ca]) + show "range (\n. A n \ s) \ sets M" using A s + by blast + show "disjoint_family (\n. A n \ s)" using disj + by (auto simp add: disjoint_family_def) + show "(\i. A i \ s) \ sets M" using A s + by (metis UN_extend_simps(4) s seq) + qed + hence "f s = suminf (\i. f (A i \ s))" + by (metis Int_commute UN_simps(4) seq sums_iff) + also have "... \ suminf (f \ A)" + proof (rule summable_le [OF _ _ sm]) + show "\n. f (A n \ s) \ (f \ A) n" using A s + by (force intro: increasingD [OF inc]) + show "summable (\i. f (A i \ s))" using sums + by (simp add: sums_iff) + qed + also have "... = z" by (rule si) + finally show "f s \ z" . +next + fix y + assume y: "!!u. u \ measure_set M f s \ y \ u" + thus "y \ f s" + by (blast intro: inf_measure_nonempty [OF posf s subset_refl]) +qed + +lemma (in algebra) inf_measure_empty: + assumes posf: "positive M f" + shows "Inf (measure_set M f {}) = 0" +proof (rule antisym) + show "0 \ Inf (measure_set M f {})" + by (metis empty_subsetI inf_measure_pos posf) + show "Inf (measure_set M f {}) \ 0" + by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf + positive_imp_0 subset_refl) +qed + +lemma (in algebra) inf_measure_positive: + "positive M f \ + positive (| space = space M, sets = Pow (space M) |) + (\x. Inf (measure_set M f x))" + by (simp add: positive_def inf_measure_empty inf_measure_pos) + +lemma (in algebra) inf_measure_increasing: + assumes posf: "positive M f" + shows "increasing (| space = space M, sets = Pow (space M) |) + (\x. Inf (measure_set M f x))" +apply (auto simp add: increasing_def) +apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf) +apply (rule Inf_lower) +apply (clarsimp simp add: measure_set_def, blast) +apply (blast intro: inf_measure_pos0 posf) +done + + +lemma (in algebra) inf_measure_le: + assumes posf: "positive M f" and inc: "increasing M f" + and x: "x \ {r . \A. range A \ sets M & s \ (\i. A i) & (f \ A) sums r}" + shows "Inf (measure_set M f s) \ x" +proof - + from x + obtain A where A: "range A \ sets M" and ss: "s \ (\i. A i)" + and sm: "summable (f \ A)" and xeq: "suminf (f \ A) = x" + by (auto simp add: sums_iff) + have dA: "range (disjointed A) \ sets M" + by (metis A range_disjointed_sets) + have "\n. \(f o disjointed A) n\ \ (f \ A) n" + proof (auto) + fix n + have "\f (disjointed A n)\ = f (disjointed A n)" using posf dA + by (auto simp add: positive_def image_subset_iff) + also have "... \ f (A n)" + by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) + finally show "\f (disjointed A n)\ \ f (A n)" . + qed + from Series.summable_le2 [OF this sm] + have sda: "summable (f o disjointed A)" + "suminf (f o disjointed A) \ suminf (f \ A)" + by blast+ + hence ley: "suminf (f o disjointed A) \ x" + by (metis xeq) + from sda have "(f \ disjointed A) sums suminf (f \ disjointed A)" + by (simp add: sums_iff) + hence y: "suminf (f o disjointed A) \ measure_set M f s" + apply (auto simp add: measure_set_def) + apply (rule_tac x="disjointed A" in exI) + apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA) + done + show ?thesis + by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf) +qed + +lemma (in algebra) inf_measure_close: + assumes posf: "positive M f" and e: "0 < e" and ss: "s \ (space M)" + shows "\A l. range A \ sets M & disjoint_family A & s \ (\i. A i) & + (f \ A) sums l & l \ Inf (measure_set M f s) + e" +proof - + have " measure_set M f s \ {}" + by (metis emptyE ss inf_measure_nonempty [OF posf top]) + hence "\l \ measure_set M f s. l < Inf (measure_set M f s) + e" + by (rule Inf_close [OF _ e]) + thus ?thesis + by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto) +qed + +lemma (in algebra) inf_measure_countably_subadditive: + assumes posf: "positive M f" and inc: "increasing M f" + shows "countably_subadditive (| space = space M, sets = Pow (space M) |) + (\x. Inf (measure_set M f x))" +proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon) + fix A :: "nat \ 'a set" and e :: real + assume A: "range A \ Pow (space M)" + and disj: "disjoint_family A" + and sb: "(\i. A i) \ space M" + and sum1: "summable (\n. Inf (measure_set M f (A n)))" + and e: "0 < e" + have "!!n. \B l. range B \ sets M \ disjoint_family B \ A n \ (\i. B i) \ + (f o B) sums l \ + l \ Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" + apply (rule inf_measure_close [OF posf]) + apply (metis e half mult_pos_pos zero_less_power) + apply (metis UNIV_I UN_subset_iff sb) + done + hence "\BB ll. \n. range (BB n) \ sets M \ disjoint_family (BB n) \ + A n \ (\i. BB n i) \ (f o BB n) sums ll n \ + ll n \ Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" + by (rule choice2) + then obtain BB ll + where BB: "!!n. (range (BB n) \ sets M)" + and disjBB: "!!n. disjoint_family (BB n)" + and sbBB: "!!n. A n \ (\i. BB n i)" + and BBsums: "!!n. (f o BB n) sums ll n" + and ll: "!!n. ll n \ Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" + by auto blast + have llpos: "!!n. 0 \ ll n" + by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero + range_subsetD BB) + have sll: "summable ll & + suminf ll \ suminf (\n. Inf (measure_set M f (A n))) + e" + proof - + have "(\n. e * (1/2)^(Suc n)) sums (e*1)" + by (rule sums_mult [OF power_half_series]) + hence sum0: "summable (\n. e * (1 / 2) ^ Suc n)" + and eqe: "(\n. e * (1 / 2) ^ n / 2) = e" + by (auto simp add: sums_iff) + have 0: "suminf (\n. Inf (measure_set M f (A n))) + + suminf (\n. e * (1/2)^(Suc n)) = + suminf (\n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))" + by (rule suminf_add [OF sum1 sum0]) + have 1: "\n. \ll n\ \ Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n" + by (metis ll llpos abs_of_nonneg) + have 2: "summable (\n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))" + by (rule summable_add [OF sum1 sum0]) + have "suminf ll \ (\n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)" + using Series.summable_le2 [OF 1 2] by auto + also have "... = (\n. Inf (measure_set M f (A n))) + + (\n. e * (1 / 2) ^ Suc n)" + by (metis 0) + also have "... = (\n. Inf (measure_set M f (A n))) + e" + by (simp add: eqe) + finally show ?thesis using Series.summable_le2 [OF 1 2] by auto + qed + def C \ "(split BB) o nat_to_nat2" + have C: "!!n. C n \ sets M" + apply (rule_tac p="nat_to_nat2 n" in PairE) + apply (simp add: C_def) + apply (metis BB subsetD rangeI) + done + have sbC: "(\i. A i) \ (\i. C i)" + proof (auto simp add: C_def) + fix x i + assume x: "x \ A i" + with sbBB [of i] obtain j where "x \ BB i j" + by blast + thus "\i. x \ split BB (nat_to_nat2 i)" + by (metis nat_to_nat2_surj internal_split_def prod.cases + prod_case_split surj_f_inv_f) + qed + have "(f \ C) = (f \ (\(x, y). BB x y)) \ nat_to_nat2" + by (rule ext) (auto simp add: C_def) + also have "... sums suminf ll" + proof (rule suminf_2dimen) + show "\m n. 0 \ (f \ (\(x, y). BB x y)) (m, n)" using posf BB + by (force simp add: positive_def) + show "\m. (\n. (f \ (\(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB + by (force simp add: o_def) + show "summable ll" using sll + by auto + qed + finally have Csums: "(f \ C) sums suminf ll" . + have "Inf (measure_set M f (\i. A i)) \ suminf ll" + apply (rule inf_measure_le [OF posf inc], auto) + apply (rule_tac x="C" in exI) + apply (auto simp add: C sbC Csums) + done + also have "... \ (\n. Inf (measure_set M f (A n))) + e" using sll + by blast + finally show "Inf (measure_set M f (\i. A i)) \ + (\n. Inf (measure_set M f (A n))) + e" . +qed + +lemma (in algebra) inf_measure_outer: + "positive M f \ increasing M f + \ outer_measure_space (| space = space M, sets = Pow (space M) |) + (\x. Inf (measure_set M f x))" + by (simp add: outer_measure_space_def inf_measure_positive + inf_measure_increasing inf_measure_countably_subadditive) + +(*MOVE UP*) + +lemma (in algebra) algebra_subset_lambda_system: + assumes posf: "positive M f" and inc: "increasing M f" + and add: "additive M f" + shows "sets M \ lambda_system (| space = space M, sets = Pow (space M) |) + (\x. Inf (measure_set M f x))" +proof (auto dest: sets_into_space + simp add: algebra.lambda_system_eq [OF algebra_Pow]) + fix x s + assume x: "x \ sets M" + and s: "s \ space M" + have [simp]: "!!x. x \ sets M \ s \ (space M - x) = s-x" using s + by blast + have "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) + \ Inf (measure_set M f s)" + proof (rule field_le_epsilon) + fix e :: real + assume e: "0 < e" + from inf_measure_close [OF posf e s] + obtain A l where A: "range A \ sets M" and disj: "disjoint_family A" + and sUN: "s \ (\i. A i)" and fsums: "(f \ A) sums l" + and l: "l \ Inf (measure_set M f s) + e" + by auto + have [simp]: "!!x. x \ sets M \ + (f o (\z. z \ (space M - x)) o A) = (f o (\z. z - x) o A)" + by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) + have [simp]: "!!n. f (A n \ x) + f (A n - x) = f (A n)" + by (subst additiveD [OF add, symmetric]) + (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) + have fsumb: "summable (f \ A)" + by (metis fsums sums_iff) + { fix u + assume u: "u \ sets M" + have [simp]: "\n. \f (A n \ u)\ \ f (A n)" + by (simp add: positive_imp_pos [OF posf] increasingD [OF inc] + u Int range_subsetD [OF A]) + have 1: "summable (f o (\z. z\u) o A)" + by (rule summable_comparison_test [OF _ fsumb]) simp + have 2: "Inf (measure_set M f (s\u)) \ suminf (f o (\z. z\u) o A)" + proof (rule Inf_lower) + show "suminf (f \ (\z. z \ u) \ A) \ measure_set M f (s \ u)" + apply (simp add: measure_set_def) + apply (rule_tac x="(\z. z \ u) o A" in exI) + apply (auto simp add: disjoint_family_subset [OF disj]) + apply (blast intro: u range_subsetD [OF A]) + apply (blast dest: subsetD [OF sUN]) + apply (metis 1 o_assoc sums_iff) + done + next + show "\x. x \ measure_set M f (s \ u) \ 0 \ x" + by (blast intro: inf_measure_pos0 [OF posf]) + qed + note 1 2 + } note lesum = this + have sum1: "summable (f o (\z. z\x) o A)" + and inf1: "Inf (measure_set M f (s\x)) \ suminf (f o (\z. z\x) o A)" + and sum2: "summable (f o (\z. z \ (space M - x)) o A)" + and inf2: "Inf (measure_set M f (s \ (space M - x))) + \ suminf (f o (\z. z \ (space M - x)) o A)" + by (metis Diff lesum top x)+ + hence "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) + \ suminf (f o (\s. s\x) o A) + suminf (f o (\s. s-x) o A)" + by (simp add: x) + also have "... \ suminf (f o A)" using suminf_add [OF sum1 sum2] + by (simp add: x) (simp add: o_def) + also have "... \ Inf (measure_set M f s) + e" + by (metis fsums l sums_unique) + finally show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) + \ Inf (measure_set M f s) + e" . + qed + moreover + have "Inf (measure_set M f s) + \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" + proof - + have "Inf (measure_set M f s) = Inf (measure_set M f ((s\x) \ (s-x)))" + by (metis Un_Diff_Int Un_commute) + also have "... \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" + apply (rule subadditiveD) + apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow + inf_measure_positive inf_measure_countably_subadditive posf inc) + apply (auto simp add: subsetD [OF s]) + done + finally show ?thesis . + qed + ultimately + show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) + = Inf (measure_set M f s)" + by (rule order_antisym) +qed + +lemma measure_down: + "measure_space N \ sigma_algebra M \ sets M \ sets N \ + (measure M = measure N) \ measure_space M" + by (simp add: measure_space_def measure_space_axioms_def positive_def + countably_additive_def) + blast + +theorem (in algebra) caratheodory: + assumes posf: "positive M f" and ca: "countably_additive M f" + shows "\MS :: 'a measure_space. + (\s \ sets M. measure MS s = f s) \ + ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \ + measure_space MS" + proof - + have inc: "increasing M f" + by (metis additive_increasing ca countably_additive_additive posf) + let ?infm = "(\x. Inf (measure_set M f x))" + def ls \ "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" + have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)" + using sigma_algebra.caratheodory_lemma + [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] + by (simp add: ls_def) + hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)" + by (simp add: measure_space_def) + have "sets M \ ls" + by (simp add: ls_def) + (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) + hence sgs_sb: "sigma_sets (space M) (sets M) \ ls" + using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] + by simp + have "measure_space (|space = space M, + sets = sigma_sets (space M) (sets M), + measure = ?infm|)" + by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) + (simp_all add: sgs_sb space_closed) + thus ?thesis + by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) +qed + +end diff -r 02de0317f66f -r 73a0c804840f src/HOL/Probability/Measure.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Measure.thy Wed Oct 28 11:43:06 2009 +0000 @@ -0,0 +1,916 @@ +header {*Measures*} + +theory Measure + imports Caratheodory FuncSet +begin + +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} + +definition prod_sets where + "prod_sets A B = {z. \x \ A. \y \ B. z = x \ y}" + +lemma prod_setsI: "x \ A \ y \ B \ (x \ y) \ prod_sets A B" + by (auto simp add: prod_sets_def) + +definition + closed_cdi where + "closed_cdi M \ + sets M \ Pow (space M) & + (\s \ sets M. space M - s \ sets M) & + (\A. (range A \ sets M) & (A 0 = {}) & (\n. A n \ A (Suc n)) \ + (\i. A i) \ sets M) & + (\A. (range A \ sets M) & disjoint_family A \ (\i::nat. A i) \ sets M)" + + +inductive_set + smallest_ccdi_sets :: "('a, 'b) algebra_scheme \ 'a set set" + for M + where + Basic [intro]: + "a \ sets M \ a \ smallest_ccdi_sets M" + | Compl [intro]: + "a \ smallest_ccdi_sets M \ space M - a \ smallest_ccdi_sets M" + | Inc: + "range A \ Pow(smallest_ccdi_sets M) \ A 0 = {} \ (\n. A n \ A (Suc n)) + \ (\i. A i) \ smallest_ccdi_sets M" + | Disj: + "range A \ Pow(smallest_ccdi_sets M) \ disjoint_family A + \ (\i::nat. A i) \ smallest_ccdi_sets M" + monos Pow_mono + + +definition + smallest_closed_cdi where + "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)" + +definition + measurable where + "measurable a b = {f . sigma_algebra a & sigma_algebra b & + f \ (space a -> space b) & + (\y \ sets b. (f -` y) \ (space a) \ sets a)}" + +definition + measure_preserving where + "measure_preserving m1 m2 = + measurable m1 m2 \ + {f . measure_space m1 & measure_space m2 & + (\y \ sets m2. measure m1 ((f -` y) \ (space m1)) = measure m2 y)}" + +lemma space_smallest_closed_cdi [simp]: + "space (smallest_closed_cdi M) = space M" + by (simp add: smallest_closed_cdi_def) + + +lemma (in algebra) smallest_closed_cdi1: "sets M \ sets (smallest_closed_cdi M)" + by (auto simp add: smallest_closed_cdi_def) + +lemma (in algebra) smallest_ccdi_sets: + "smallest_ccdi_sets M \ Pow (space M)" + apply (rule subsetI) + apply (erule smallest_ccdi_sets.induct) + apply (auto intro: range_subsetD dest: sets_into_space) + done + +lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)" + apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets) + apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) + + done + +lemma (in algebra) smallest_closed_cdi3: + "sets (smallest_closed_cdi M) \ Pow (space M)" + by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) + +lemma closed_cdi_subset: "closed_cdi M \ sets M \ Pow (space M)" + by (simp add: closed_cdi_def) + +lemma closed_cdi_Compl: "closed_cdi M \ s \ sets M \ space M - s \ sets M" + by (simp add: closed_cdi_def) + +lemma closed_cdi_Inc: + "closed_cdi M \ range A \ sets M \ A 0 = {} \ (!!n. A n \ A (Suc n)) \ + (\i. A i) \ sets M" + by (simp add: closed_cdi_def) + +lemma closed_cdi_Disj: + "closed_cdi M \ range A \ sets M \ disjoint_family A \ (\i::nat. A i) \ sets M" + by (simp add: closed_cdi_def) + +lemma closed_cdi_Un: + assumes cdi: "closed_cdi M" and empty: "{} \ sets M" + and A: "A \ sets M" and B: "B \ sets M" + and disj: "A \ B = {}" + shows "A \ B \ sets M" +proof - + have ra: "range (binaryset A B) \ sets M" + by (simp add: range_binaryset_eq empty A B) + have di: "disjoint_family (binaryset A B)" using disj + by (simp add: disjoint_family_def binaryset_def Int_commute) + from closed_cdi_Disj [OF cdi ra di] + show ?thesis + by (simp add: UN_binaryset_eq) +qed + +lemma (in algebra) smallest_ccdi_sets_Un: + assumes A: "A \ smallest_ccdi_sets M" and B: "B \ smallest_ccdi_sets M" + and disj: "A \ B = {}" + shows "A \ B \ smallest_ccdi_sets M" +proof - + have ra: "range (binaryset A B) \ Pow (smallest_ccdi_sets M)" + by (simp add: range_binaryset_eq A B empty_sets smallest_ccdi_sets.Basic) + have di: "disjoint_family (binaryset A B)" using disj + by (simp add: disjoint_family_def binaryset_def Int_commute) + from Disj [OF ra di] + show ?thesis + by (simp add: UN_binaryset_eq) +qed + + + +lemma (in algebra) smallest_ccdi_sets_Int1: + assumes a: "a \ sets M" + shows "b \ smallest_ccdi_sets M \ a \ b \ smallest_ccdi_sets M" +proof (induct rule: smallest_ccdi_sets.induct) + case (Basic x) + thus ?case + by (metis a Int smallest_ccdi_sets.Basic) +next + case (Compl x) + have "a \ (space M - x) = space M - ((space M - a) \ (a \ x))" + by blast + also have "... \ smallest_ccdi_sets M" + by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2 + Diff_disjoint Int_Diff Int_empty_right Un_commute + smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl + smallest_ccdi_sets_Un) + finally show ?case . +next + case (Inc A) + have 1: "(\i. (\i. a \ A i) i) = a \ (\i. A i)" + by blast + have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets M)" using Inc + by blast + moreover have "(\i. a \ A i) 0 = {}" + by (simp add: Inc) + moreover have "!!n. (\i. a \ A i) n \ (\i. a \ A i) (Suc n)" using Inc + by blast + ultimately have 2: "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets M" + by (rule smallest_ccdi_sets.Inc) + show ?case + by (metis 1 2) +next + case (Disj A) + have 1: "(\i. (\i. a \ A i) i) = a \ (\i. A i)" + by blast + have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets M)" using Disj + by blast + moreover have "disjoint_family (\i. a \ A i)" using Disj + by (auto simp add: disjoint_family_def) + ultimately have 2: "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets M" + by (rule smallest_ccdi_sets.Disj) + show ?case + by (metis 1 2) +qed + + +lemma (in algebra) smallest_ccdi_sets_Int: + assumes b: "b \ smallest_ccdi_sets M" + shows "a \ smallest_ccdi_sets M \ a \ b \ smallest_ccdi_sets M" +proof (induct rule: smallest_ccdi_sets.induct) + case (Basic x) + thus ?case + by (metis b smallest_ccdi_sets_Int1) +next + case (Compl x) + have "(space M - x) \ b = space M - (x \ b \ (space M - b))" + by blast + also have "... \ smallest_ccdi_sets M" + by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b + smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) + finally show ?case . +next + case (Inc A) + have 1: "(\i. (\i. A i \ b) i) = (\i. A i) \ b" + by blast + have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets M)" using Inc + by blast + moreover have "(\i. A i \ b) 0 = {}" + by (simp add: Inc) + moreover have "!!n. (\i. A i \ b) n \ (\i. A i \ b) (Suc n)" using Inc + by blast + ultimately have 2: "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets M" + by (rule smallest_ccdi_sets.Inc) + show ?case + by (metis 1 2) +next + case (Disj A) + have 1: "(\i. (\i. A i \ b) i) = (\i. A i) \ b" + by blast + have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets M)" using Disj + by blast + moreover have "disjoint_family (\i. A i \ b)" using Disj + by (auto simp add: disjoint_family_def) + ultimately have 2: "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets M" + by (rule smallest_ccdi_sets.Disj) + show ?case + by (metis 1 2) +qed + +lemma (in algebra) sets_smallest_closed_cdi_Int: + "a \ sets (smallest_closed_cdi M) \ b \ sets (smallest_closed_cdi M) + \ a \ b \ sets (smallest_closed_cdi M)" + by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) + +lemma algebra_iff_Int: + "algebra M \ + sets M \ Pow (space M) & {} \ sets M & + (\a \ sets M. space M - a \ sets M) & + (\a \ sets M. \ b \ sets M. a \ b \ sets M)" +proof (auto simp add: algebra.Int, auto simp add: algebra_def) + fix a b + assume ab: "sets M \ Pow (space M)" + "\a\sets M. space M - a \ sets M" + "\a\sets M. \b\sets M. a \ b \ sets M" + "a \ sets M" "b \ sets M" + hence "a \ b = space M - ((space M - a) \ (space M - b))" + by blast + also have "... \ sets M" + by (metis ab) + finally show "a \ b \ sets M" . +qed + +lemma (in algebra) sigma_property_disjoint_lemma: + assumes sbC: "sets M \ C" + and ccdi: "closed_cdi (|space = space M, sets = C|)" + shows "sigma_sets (space M) (sets M) \ C" +proof - + have "smallest_ccdi_sets M \ {B . sets M \ B \ sigma_algebra (|space = space M, sets = B|)}" + apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int + smallest_ccdi_sets_Int) + apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) + apply (blast intro: smallest_ccdi_sets.Disj) + done + hence "sigma_sets (space M) (sets M) \ smallest_ccdi_sets M" + by auto + (metis sigma_algebra.sigma_sets_subset algebra.simps(1) + algebra.simps(2) subsetD) + also have "... \ C" + proof + fix x + assume x: "x \ smallest_ccdi_sets M" + thus "x \ C" + proof (induct rule: smallest_ccdi_sets.induct) + case (Basic x) + thus ?case + by (metis Basic subsetD sbC) + next + case (Compl x) + thus ?case + by (blast intro: closed_cdi_Compl [OF ccdi, simplified]) + next + case (Inc A) + thus ?case + by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) + next + case (Disj A) + thus ?case + by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) + qed + qed + finally show ?thesis . +qed + +lemma (in algebra) sigma_property_disjoint: + assumes sbC: "sets M \ C" + and compl: "!!s. s \ C \ sigma_sets (space M) (sets M) \ space M - s \ C" + and inc: "!!A. range A \ C \ sigma_sets (space M) (sets M) + \ A 0 = {} \ (!!n. A n \ A (Suc n)) + \ (\i. A i) \ C" + and disj: "!!A. range A \ C \ sigma_sets (space M) (sets M) + \ disjoint_family A \ (\i::nat. A i) \ C" + shows "sigma_sets (space M) (sets M) \ C" +proof - + have "sigma_sets (space M) (sets M) \ C \ sigma_sets (space M) (sets M)" + proof (rule sigma_property_disjoint_lemma) + show "sets M \ C \ sigma_sets (space M) (sets M)" + by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic) + next + show "closed_cdi \space = space M, sets = C \ sigma_sets (space M) (sets M)\" + by (simp add: closed_cdi_def compl inc disj) + (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed + IntE sigma_sets.Compl range_subsetD sigma_sets.Union) + qed + thus ?thesis + by blast +qed + + +(* or just countably_additiveD [OF measure_space.ca] *) +lemma (in measure_space) measure_countably_additive: + "range A \ sets M + \ disjoint_family A \ (\i. A i) \ sets M + \ (measure M o A) sums measure M (\i. A i)" + by (insert ca) (simp add: countably_additive_def o_def) + +lemma (in measure_space) additive: + "additive M (measure M)" +proof (rule algebra.countably_additive_additive [OF _ _ ca]) + show "algebra M" + by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms) + show "positive M (measure M)" + by (simp add: positive_def empty_measure positive) +qed + +lemma (in measure_space) measure_additive: + "a \ sets M \ b \ sets M \ a \ b = {} + \ measure M a + measure M b = measure M (a \ b)" + by (metis additiveD additive) + +lemma (in measure_space) measure_compl: + assumes s: "s \ sets M" + shows "measure M (space M - s) = measure M (space M) - measure M s" +proof - + have "measure M (space M) = measure M (s \ (space M - s))" using s + by (metis Un_Diff_cancel Un_absorb1 s sets_into_space) + also have "... = measure M s + measure M (space M - s)" + by (rule additiveD [OF additive]) (auto simp add: s) + finally have "measure M (space M) = measure M s + measure M (space M - s)" . + thus ?thesis + by arith +qed + +lemma disjoint_family_Suc: + assumes Suc: "!!n. A n \ A (Suc n)" + shows "disjoint_family (\i. A (Suc i) - A i)" +proof - + { + fix m + have "!!n. A n \ A (m+n)" + proof (induct m) + case 0 show ?case by simp + next + case (Suc m) thus ?case + by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans) + qed + } + hence "!!m n. m < n \ A m \ A n" + by (metis add_commute le_add_diff_inverse nat_less_le) + thus ?thesis + by (auto simp add: disjoint_family_def) + (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) +qed + + +lemma (in measure_space) measure_countable_increasing: + assumes A: "range A \ sets M" + and A0: "A 0 = {}" + and ASuc: "!!n. A n \ A (Suc n)" + shows "(measure M o A) ----> measure M (\i. A i)" +proof - + { + fix n + have "(measure M \ A) n = + setsum (measure M \ (\i. A (Suc i) - A i)) {0.. (A (Suc m) - A m)" + by (metis ASuc Un_Diff_cancel Un_absorb1) + hence "measure M (A (Suc m)) = + measure M (A m) + measure M (A (Suc m) - A m)" + by (subst measure_additive) + (auto simp add: measure_additive range_subsetD [OF A]) + with Suc show ?case + by simp + qed + } + hence Meq: "measure M o A = (\n. setsum (measure M o (\i. A(Suc i) - A i)) {0..i. A (Suc i) - A i) = (\i. A i)" + proof (rule UN_finite2_eq [where k=1], simp) + fix i + show "(\i\{0..i\{0..i. A (Suc i) - A i \ sets M" + by (metis A Diff range_subsetD) + have A2: "(\i. A (Suc i) - A i) \ sets M" + by (blast intro: countable_UN range_subsetD [OF A]) + have "(measure M o (\i. A (Suc i) - A i)) sums measure M (\i. A (Suc i) - A i)" + by (rule measure_countably_additive) + (auto simp add: disjoint_family_Suc ASuc A1 A2) + also have "... = measure M (\i. A i)" + by (simp add: Aeq) + finally have "(measure M o (\i. A (Suc i) - A i)) sums measure M (\i. A i)" . + thus ?thesis + by (auto simp add: sums_iff Meq dest: summable_sumr_LIMSEQ_suminf) +qed + +lemma (in measure_space) monotone_convergence: + assumes A: "range A \ sets M" + and ASuc: "!!n. A n \ A (Suc n)" + shows "(measure M \ A) ----> measure M (\i. A i)" +proof - + have ueq: "(\i. nat_case {} A i) = (\i. A i)" + by (auto simp add: split: nat.splits) + have meq: "measure M \ A = (\n. (measure M \ nat_case {} A) (Suc n))" + by (rule ext) simp + have "(measure M \ nat_case {} A) ----> measure M (\i. nat_case {} A i)" + by (rule measure_countable_increasing) + (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) + also have "... = measure M (\i. A i)" + by (simp add: ueq) + finally have "(measure M \ nat_case {} A) ----> measure M (\i. A i)" . + thus ?thesis using meq + by (metis LIMSEQ_Suc) +qed + +lemma measurable_sigma_preimages: + assumes a: "sigma_algebra a" and b: "sigma_algebra b" + and f: "f \ space a -> space b" + and ba: "!!y. y \ sets b ==> f -` y \ sets a" + shows "sigma_algebra (|space = space a, sets = (vimage f) ` (sets b) |)" +proof (simp add: sigma_algebra_iff2, intro conjI) + show "op -` f ` sets b \ Pow (space a)" + by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI) +next + show "{} \ op -` f ` sets b" + by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty) +next + { fix y + assume y: "y \ sets b" + with a b f + have "space a - f -` y = f -` (space b - y)" + by (auto simp add: sigma_algebra_iff2) (blast intro: ba) + hence "space a - (f -` y) \ (vimage f) ` sets b" + by auto + (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq + sigma_sets.Compl) + } + thus "\s\sets b. space a - f -` s \ (vimage f) ` sets b" + by blast +next + { + fix A:: "nat \ 'a set" + assume A: "range A \ (vimage f) ` (sets b)" + have "(\i. A i) \ (vimage f) ` (sets b)" + proof - + def B \ "\i. @v. v \ sets b \ f -` v = A i" + { + fix i + have "A i \ (vimage f) ` (sets b)" using A + by blast + hence "\v. v \ sets b \ f -` v = A i" + by blast + hence "B i \ sets b \ f -` B i = A i" + by (simp add: B_def) (erule someI_ex) + } note B = this + show ?thesis + proof + show "(\i. A i) = f -` (\i. B i)" + by (simp add: vimage_UN B) + show "(\i. B i) \ sets b" using B + by (auto intro: sigma_algebra.countable_UN [OF b]) + qed + qed + } + thus "\A::nat \ 'a set. + range A \ (vimage f) ` sets b \ (\i. A i) \ (vimage f) ` sets b" + by blast +qed + +lemma (in sigma_algebra) measurable_sigma: + assumes B: "B \ Pow X" + and f: "f \ space M -> X" + and ba: "!!y. y \ B ==> (f -` y) \ space M \ sets M" + shows "f \ measurable M (sigma X B)" +proof - + have "sigma_sets X B \ {y . (f -` y) \ space M \ sets M & y \ X}" + proof clarify + fix x + assume "x \ sigma_sets X B" + thus "f -` x \ space M \ sets M \ x \ X" + proof induct + case (Basic a) + thus ?case + by (auto simp add: ba) (metis B subsetD PowD) + next + case Empty + thus ?case + by auto + next + case (Compl a) + have [simp]: "f -` X \ space M = space M" + by (auto simp add: funcset_mem [OF f]) + thus ?case + by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl) + next + case (Union a) + thus ?case + by (simp add: vimage_UN, simp only: UN_extend_simps(4)) + (blast intro: countable_UN) + qed + qed + thus ?thesis + by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) + (auto simp add: sigma_def) +qed + +lemma measurable_subset: + "measurable a b \ measurable a (sigma (space b) (sets b))" + apply clarify + apply (rule sigma_algebra.measurable_sigma) + apply (auto simp add: measurable_def) + apply (metis algebra.sets_into_space subsetD sigma_algebra_iff) + done + +lemma measurable_eqI: + "space m1 = space m1' \ space m2 = space m2' + \ sets m1 = sets m1' \ sets m2 = sets m2' + \ measurable m1 m2 = measurable m1' m2'" + by (simp add: measurable_def sigma_algebra_iff2) + +lemma measure_preserving_lift: + fixes f :: "'a1 \ 'a2" + and m1 :: "('a1, 'b1) measure_space_scheme" + and m2 :: "('a2, 'b2) measure_space_scheme" + assumes m1: "measure_space m1" and m2: "measure_space m2" + defines "m x \ (|space = space m2, sets = x, measure = measure m2, ... = more m2|)" + assumes setsm2: "sets m2 = sigma_sets (space m2) a" + and fmp: "f \ measure_preserving m1 (m a)" + shows "f \ measure_preserving m1 m2" +proof - + have [simp]: "!!x. space (m x) = space m2 & sets (m x) = x & measure (m x) = measure m2" + by (simp add: m_def) + have sa1: "sigma_algebra m1" using m1 + by (simp add: measure_space_def) + show ?thesis using fmp + proof (clarsimp simp add: measure_preserving_def m1 m2) + assume fm: "f \ measurable m1 (m a)" + and mam: "measure_space (m a)" + and meq: "\y\a. measure m1 (f -` y \ space m1) = measure m2 y" + have "f \ measurable m1 (sigma (space (m a)) (sets (m a)))" + by (rule subsetD [OF measurable_subset fm]) + also have "... = measurable m1 m2" + by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) + finally have f12: "f \ measurable m1 m2" . + hence ffn: "f \ space m1 \ space m2" + by (simp add: measurable_def) + have "space m1 \ f -` (space m2)" + by auto (metis PiE ffn) + hence fveq [simp]: "(f -` (space m2)) \ space m1 = space m1" + by blast + { + fix y + assume y: "y \ sets m2" + have ama: "algebra (m a)" using mam + by (simp add: measure_space_def sigma_algebra_iff) + have spa: "space m2 \ a" using algebra.top [OF ama] + by (simp add: m_def) + have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))" + by (simp add: m_def) + also have "... \ {s . measure m1 ((f -` s) \ space m1) = measure m2 s}" + proof (rule algebra.sigma_property_disjoint, auto simp add: ama) + fix x + assume x: "x \ a" + thus "measure m1 (f -` x \ space m1) = measure m2 x" + by (simp add: meq) + next + fix s + assume eq: "measure m1 (f -` s \ space m1) = measure m2 s" + and s: "s \ sigma_sets (space m2) a" + hence s2: "s \ sets m2" + by (simp add: setsm2) + thus "measure m1 (f -` (space m2 - s) \ space m1) = + measure m2 (space m2 - s)" using f12 + by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2 + measure_space.measure_compl measurable_def) + (metis fveq meq spa) + next + fix A + assume A0: "A 0 = {}" + and ASuc: "!!n. A n \ A (Suc n)" + and rA1: "range A \ + {s. measure m1 (f -` s \ space m1) = measure m2 s}" + and "range A \ sigma_sets (space m2) a" + hence rA2: "range A \ sets m2" by (metis setsm2) + have eq1: "!!i. measure m1 (f -` A i \ space m1) = measure m2 (A i)" + using rA1 by blast + have "(measure m2 \ A) = measure m1 o (\i. (f -` A i \ space m1))" + by (simp add: o_def eq1) + also have "... ----> measure m1 (\i. f -` A i \ space m1)" + proof (rule measure_space.measure_countable_increasing [OF m1]) + show "range (\i. f -` A i \ space m1) \ sets m1" + using f12 rA2 by (auto simp add: measurable_def) + show "f -` A 0 \ space m1 = {}" using A0 + by blast + show "\n. f -` A n \ space m1 \ f -` A (Suc n) \ space m1" + using ASuc by auto + qed + also have "... = measure m1 (f -` (\i. A i) \ space m1)" + by (simp add: vimage_UN) + finally have "(measure m2 \ A) ----> measure m1 (f -` (\i. A i) \ space m1)" . + moreover + have "(measure m2 \ A) ----> measure m2 (\i. A i)" + by (rule measure_space.measure_countable_increasing + [OF m2 rA2, OF A0 ASuc]) + ultimately + show "measure m1 (f -` (\i. A i) \ space m1) = + measure m2 (\i. A i)" + by (rule LIMSEQ_unique) + next + fix A :: "nat => 'a2 set" + assume dA: "disjoint_family A" + and rA1: "range A \ + {s. measure m1 (f -` s \ space m1) = measure m2 s}" + and "range A \ sigma_sets (space m2) a" + hence rA2: "range A \ sets m2" by (metis setsm2) + hence Um2: "(\i. A i) \ sets m2" + by (metis range_subsetD setsm2 sigma_sets.Union) + have "!!i. measure m1 (f -` A i \ space m1) = measure m2 (A i)" + using rA1 by blast + hence "measure m2 o A = measure m1 o (\i. f -` A i \ space m1)" + by (simp add: o_def) + also have "... sums measure m1 (\i. f -` A i \ space m1)" + proof (rule measure_space.measure_countably_additive [OF m1] ) + show "range (\i. f -` A i \ space m1) \ sets m1" + using f12 rA2 by (auto simp add: measurable_def) + show "disjoint_family (\i. f -` A i \ space m1)" using dA + by (auto simp add: disjoint_family_def) + show "(\i. f -` A i \ space m1) \ sets m1" + proof (rule sigma_algebra.countable_UN [OF sa1]) + show "range (\i. f -` A i \ space m1) \ sets m1" using f12 rA2 + by (auto simp add: measurable_def) + qed + qed + finally have "(measure m2 o A) sums measure m1 (\i. f -` A i \ space m1)" . + with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] + have "measure m1 (\i. f -` A i \ space m1) = measure m2 (\i. A i)" + by (metis sums_unique) + + moreover have "measure m1 (f -` (\i. A i) \ space m1) = measure m1 (\i. f -` A i \ space m1)" + by (simp add: vimage_UN) + ultimately show "measure m1 (f -` (\i. A i) \ space m1) = + measure m2 (\i. A i)" + by metis + qed + finally have "sigma_sets (space m2) a + \ {s . measure m1 ((f -` s) \ space m1) = measure m2 s}" . + hence "measure m1 (f -` y \ space m1) = measure m2 y" using y + by (force simp add: setsm2) + } + thus "f \ measurable m1 m2 \ + (\y\sets m2. + measure m1 (f -` y \ space m1) = measure m2 y)" + by (blast intro: f12) + qed +qed + +lemma measurable_ident: + "sigma_algebra M ==> id \ measurable M M" + apply (simp add: measurable_def) + apply (auto simp add: sigma_algebra_def algebra.Int algebra.top) + done + +lemma measurable_comp: + fixes f :: "'a \ 'b" and g :: "'b \ 'c" + shows "f \ measurable a b \ g \ measurable b c \ (g o f) \ measurable a c" + apply (auto simp add: measurable_def vimage_compose) + apply (subgoal_tac "f -` g -` y \ space a = f -` (g -` y \ space b) \ space a") + apply force+ + done + + lemma measurable_strong: + fixes f :: "'a \ 'b" and g :: "'b \ 'c" + assumes f: "f \ measurable a b" and g: "g \ (space b -> space c)" + and c: "sigma_algebra c" + and t: "f ` (space a) \ t" + and cb: "\s. s \ sets c \ (g -` s) \ t \ sets b" + shows "(g o f) \ measurable a c" +proof - + have a: "sigma_algebra a" and b: "sigma_algebra b" + and fab: "f \ (space a -> space b)" + and ba: "\y. y \ sets b \ (f -` y) \ (space a) \ sets a" using f + by (auto simp add: measurable_def) + have eq: "f -` g -` y \ space a = f -` (g -` y \ t) \ space a" using t + by force + show ?thesis + apply (auto simp add: measurable_def vimage_compose a c) + apply (metis funcset_mem fab g) + apply (subst eq, metis ba cb) + done +qed + +lemma measurable_mono1: + "a \ b \ sigma_algebra \space = X, sets = b\ + \ measurable \space = X, sets = a\ c \ measurable \space = X, sets = b\ c" + by (auto simp add: measurable_def) + +lemma measurable_up_sigma: + "measurable a b \ measurable (sigma (space a) (sets a)) b" + apply (auto simp add: measurable_def) + apply (metis sigma_algebra_iff2 sigma_algebra_sigma) + apply (metis algebra.simps(2) sigma_algebra.sigma_sets_eq sigma_def) + done + +lemma measure_preserving_up: + "f \ measure_preserving \space = space m1, sets = a, measure = measure m1\ m2 \ + measure_space m1 \ sigma_algebra m1 \ a \ sets m1 + \ f \ measure_preserving m1 m2" + by (auto simp add: measure_preserving_def measurable_def) + +lemma measure_preserving_up_sigma: + "measure_space m1 \ (sets m1 = sets (sigma (space m1) a)) + \ measure_preserving \space = space m1, sets = a, measure = measure m1\ m2 + \ measure_preserving m1 m2" + apply (rule subsetI) + apply (rule measure_preserving_up) + apply (simp_all add: measure_space_def sigma_def) + apply (metis sigma_algebra.sigma_sets_eq subsetI sigma_sets.Basic) + done + +lemma (in sigma_algebra) measurable_prod_sigma: + assumes 1: "(fst o f) \ measurable M a1" and 2: "(snd o f) \ measurable M a2" + shows "f \ measurable M (sigma ((space a1) \ (space a2)) + (prod_sets (sets a1) (sets a2)))" +proof - + from 1 have sa1: "sigma_algebra a1" and fn1: "fst \ f \ space M \ space a1" + and q1: "\y\sets a1. (fst \ f) -` y \ space M \ sets M" + by (auto simp add: measurable_def) + from 2 have sa2: "sigma_algebra a2" and fn2: "snd \ f \ space M \ space a2" + and q2: "\y\sets a2. (snd \ f) -` y \ space M \ sets M" + by (auto simp add: measurable_def) + show ?thesis + proof (rule measurable_sigma) + show "prod_sets (sets a1) (sets a2) \ Pow (space a1 \ space a2)" using sa1 sa2 + by (force simp add: prod_sets_def sigma_algebra_iff algebra_def) + next + show "f \ space M \ space a1 \ space a2" + by (rule prod_final [OF fn1 fn2]) + next + fix z + assume z: "z \ prod_sets (sets a1) (sets a2)" + thus "f -` z \ space M \ sets M" + proof (auto simp add: prod_sets_def vimage_Times) + fix x y + assume x: "x \ sets a1" and y: "y \ sets a2" + have "(fst \ f) -` x \ (snd \ f) -` y \ space M = + ((fst \ f) -` x \ space M) \ ((snd \ f) -` y \ space M)" + by blast + also have "... \ sets M" using x y q1 q2 + by blast + finally show "(fst \ f) -` x \ (snd \ f) -` y \ space M \ sets M" . + qed + qed +qed + + +lemma (in measure_space) measurable_range_reduce: + "f \ measurable M \space = s, sets = Pow s\ \ + s \ {} + \ f \ measurable M \space = s \ (f ` space M), sets = Pow (s \ (f ` space M))\" + by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast + +lemma (in measure_space) measurable_Pow_to_Pow: + "(sets M = Pow (space M)) \ f \ measurable M \space = UNIV, sets = Pow UNIV\" + by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def) + +lemma (in measure_space) measurable_Pow_to_Pow_image: + "sets M = Pow (space M) + \ f \ measurable M \space = f ` space M, sets = Pow (f ` space M)\" + by (simp add: measurable_def sigma_algebra_Pow) intro_locales + +lemma (in measure_space) measure_real_sum_image: + assumes s: "s \ sets M" + and ssets: "\x. x \ s ==> {x} \ sets M" + and fin: "finite s" + shows "measure M s = (\x\s. measure M {x})" +proof - + { + fix u + assume u: "u \ s & u \ sets M" + hence "finite u" + by (metis fin finite_subset) + hence "measure M u = (\x\u. measure M {x})" using u + proof (induct u) + case empty + thus ?case by simp + next + case (insert x t) + hence x: "x \ s" and t: "t \ s" + by (simp_all add: insert_subset) + hence ts: "t \ sets M" using insert + by (metis Diff_insert_absorb Diff ssets) + have "measure M (insert x t) = measure M ({x} \ t)" + by simp + also have "... = measure M {x} + measure M t" + by (simp add: measure_additive insert insert_disjoint ssets x ts + del: Un_insert_left) + also have "... = (\x\insert x t. measure M {x})" + by (simp add: x t ts insert) + finally show ?case . + qed + } + thus ?thesis + by (metis subset_refl s) +qed + +lemma (in sigma_algebra) sigma_algebra_extend: + "sigma_algebra \space = space M, sets = sets M, measure_space.measure = f\" +proof - + have 1: "sigma_algebra M \ ?thesis" + by (simp add: sigma_algebra_def algebra_def sigma_algebra_axioms_def) + show ?thesis + by (rule 1) intro_locales +qed + + +lemma (in sigma_algebra) finite_additivity_sufficient: + assumes fin: "finite (space M)" + and posf: "positive M f" and addf: "additive M f" + defines "Mf \ \space = space M, sets = sets M, measure = f\" + shows "measure_space Mf" +proof - + have [simp]: "f {} = 0" using posf + by (simp add: positive_def) + have "countably_additive Mf f" + proof (auto simp add: countably_additive_def positive_def) + fix A :: "nat \ 'a set" + assume A: "range A \ sets Mf" + and disj: "disjoint_family A" + and UnA: "(\i. A i) \ sets Mf" + def I \ "{i. A i \ {}}" + have "Union (A ` I) \ space M" using A + by (auto simp add: Mf_def) (metis range_subsetD subsetD sets_into_space) + hence "finite (A ` I)" + by (metis finite_UnionD finite_subset fin) + moreover have "inj_on A I" using disj + by (auto simp add: I_def disjoint_family_def inj_on_def) + ultimately have finI: "finite I" + by (metis finite_imageD) + hence "\N. \m\N. A m = {}" + proof (cases "I = {}") + case True thus ?thesis by (simp add: I_def) + next + case False + hence "\i\I. i < Suc(Max I)" + by (simp add: Max_less_iff [symmetric] finI) + hence "\m \ Suc(Max I). A m = {}" + by (simp add: I_def) (metis less_le_not_le) + thus ?thesis + by blast + qed + then obtain N where N: "\m\N. A m = {}" by blast + hence "\m\N. (f o A) m = 0" + by simp + hence "(\n. f (A n)) sums setsum (f o A) {0..i (\ x i (\ x sets M" using A + by (force simp add: Mf_def) + show "(\i sets M" + proof (induct n) + case 0 thus ?case by simp + next + case (Suc n) thus ?case using A + by (simp add: lessThan_Suc Mf_def Un range_subsetD) + qed + qed + thus ?case using Suc + by (simp add: lessThan_Suc) + qed + also have "... = f (\i. A i)" + proof - + have "(\ ii. A i)" using N + by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE) + thus ?thesis by simp + qed + finally show "(\n. f (A n)) sums f (\i. A i)" . + qed + thus ?thesis using posf + by (simp add: Mf_def measure_space_def measure_space_axioms_def sigma_algebra_extend positive_def) +qed + +lemma finite_additivity_sufficient: + "sigma_algebra M + \ finite (space M) + \ positive M (measure M) \ additive M (measure M) + \ measure_space M" + by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) + +end + diff -r 02de0317f66f -r 73a0c804840f src/HOL/Probability/Probability.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Probability.thy Wed Oct 28 11:43:06 2009 +0000 @@ -0,0 +1,5 @@ +theory Probability imports + Measure +begin + +end diff -r 02de0317f66f -r 73a0c804840f src/HOL/Probability/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/ROOT.ML Wed Oct 28 11:43:06 2009 +0000 @@ -0,0 +1,6 @@ +(* + no_document use_thy "ThisTheory"; + use_thy "ThatTheory"; +*) + +use_thy "Probability"; diff -r 02de0317f66f -r 73a0c804840f src/HOL/Probability/SeriesPlus.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/SeriesPlus.thy Wed Oct 28 11:43:06 2009 +0000 @@ -0,0 +1,127 @@ +theory SeriesPlus + imports Complex_Main Nat_Int_Bij + +begin + +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} + +lemma choice2: "(!!x. \y z. Q x y z) ==> \f g. \x. Q x (f x) (g x)" + by metis + +lemma range_subsetD: "range f \ B \ f i \ B" + by blast + + +lemma suminf_2dimen: + fixes f:: "nat * nat \ real" + assumes f_nneg: "!!m n. 0 \ f(m,n)" + and fsums: "!!m. (\n. f (m,n)) sums (g m)" + and sumg: "summable g" + shows "(f o nat_to_nat2) sums suminf g" +proof (simp add: sums_def) + { + fix x + have "0 \ f x" + by (cases x) (simp add: f_nneg) + } note [iff] = this + have g_nneg: "!!m. 0 \ g m" + proof - + fix m + have "0 \ suminf (\n. f (m,n))" + by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff) + thus "0 \ g m" using fsums [of m] + by (auto simp add: sums_iff) + qed + show "(\n. \x = 0.. suminf g" + proof (rule increasing_LIMSEQ, simp add: f_nneg) + fix n + def i \ "Max (Domain (nat_to_nat2 ` {0.. "Max (Range (nat_to_nat2 ` {0.. ({0..i} \ {0..j})" + by (force simp add: i_def j_def + intro: finite_imageI Max_ge finite_Domain finite_Range) + have "(\x = 0.. setsum f ({0..i} \ {0..j})" + by (rule setsum_mono2) (auto simp add: ij) + also have "... = setsum (\m. setsum (\n. f (m,n)) {0..j}) {0.. setsum g {0.. i" + thus " (\n = 0..j. f (m, n)) \ g m" using fsums [of m] + by (auto simp add: sums_iff) + (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) + qed + finally have "(\x = 0.. setsum g {0.. suminf g" + by (rule series_pos_le [OF sumg]) (simp add: g_nneg) + finally show "(\x = 0.. suminf g" . + next + fix e :: real + assume e: "0 < e" + with summable_sums [OF sumg] + obtain N where "\setsum g {0.. < e/2" and nz: "N>0" + by (simp add: sums_def LIMSEQ_iff_nz dist_real_def) + (metis e half_gt_zero le_refl that) + hence gless: "suminf g < setsum g {0..j. \(\n = 0.. < e/(2 * real N)" + using fsums [of m] m + by (force simp add: sums_def LIMSEQ_def dist_real_def) + hence "\j. g m < setsum (\n. f (m,n)) {0..jj. \m. m g m < (\n = 0.. g m < (\n = 0.. "SIGMA i : {0..m = 0..n = 0..m = 0..n = 0.. "Max (nat_to_nat2 -` IJ)" + have IJsb: "IJ \ nat_to_nat2 ` {0..NIJ}" + proof (auto simp add: NIJ_def) + fix i j + assume ij:"(i,j) \ IJ" + hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))" + by (metis nat_to_nat2_surj surj_f_inv_f) + thus "(i,j) \ nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}" + by (rule image_eqI) + (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj] + nat_to_nat2_surj surj_f_inv_f) + qed + have "setsum f IJ \ setsum f (nat_to_nat2 `{0..NIJ})" + by (rule setsum_mono2) (auto simp add: IJsb) + also have "... = (\k = 0..NIJ. f (nat_to_nat2 k))" + by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV]) + also have "... = (\k = 0.. (\k = 0..n. suminf g \ (\x = 0.. Pow (space M)" + and empty_sets [iff]: "{} \ sets M" + and compl_sets [intro]: "!!a. a \ sets M \ space M - a \ sets M" + and Un [intro]: "!!a b. a \ sets M \ b \ sets M \ a \ b \ sets M" + +lemma (in algebra) top [iff]: "space M \ sets M" + by (metis Diff_empty compl_sets empty_sets) + +lemma (in algebra) sets_into_space: "x \ sets M \ x \ space M" + by (metis PowD contra_subsetD space_closed) + +lemma (in algebra) Int [intro]: + assumes a: "a \ sets M" and b: "b \ sets M" shows "a \ b \ sets M" +proof - + have "((space M - a) \ (space M - b)) \ sets M" + by (metis a b compl_sets Un) + moreover + have "a \ b = space M - ((space M - a) \ (space M - b))" + using space_closed a b + by blast + ultimately show ?thesis + by (metis compl_sets) +qed + +lemma (in algebra) Diff [intro]: + assumes a: "a \ sets M" and b: "b \ sets M" shows "a - b \ sets M" +proof - + have "(a \ (space M - b)) \ sets M" + by (metis a b compl_sets Int) + moreover + have "a - b = (a \ (space M - b))" + by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space) + ultimately show ?thesis + by metis +qed + +lemma (in algebra) finite_union [intro]: + "finite X \ X \ sets M \ Union X \ sets M" + by (induct set: finite) (auto simp add: Un) + + +subsection {* Sigma Algebras *} + +locale sigma_algebra = algebra + + assumes countable_UN [intro]: + "!!A. range A \ sets M \ (\i::nat. A i) \ sets M" + +lemma (in sigma_algebra) countable_INT: + assumes a: "range a \ sets M" + shows "(\i::nat. a i) \ sets M" +proof - + have "space M - (\i. space M - a i) \ sets M" using a + by (blast intro: countable_UN compl_sets a) + moreover + have "(\i. a i) = space M - (\i. space M - a i)" using space_closed a + by blast + ultimately show ?thesis by metis +qed + + +lemma algebra_Pow: + "algebra (| space = sp, sets = Pow sp |)" + by (auto simp add: algebra_def) + +lemma sigma_algebra_Pow: + "sigma_algebra (| space = sp, sets = Pow sp |)" + by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) + +subsection {* Binary Unions *} + +definition binary :: "'a \ 'a \ nat \ 'a" + where "binary a b = (\\<^isup>x. b)(0 := a)" + +lemma range_binary_eq: "range(binary a b) = {a,b}" + by (auto simp add: binary_def) + +lemma Un_range_binary: "a \ b = (\i::nat. binary a b i)" + by (simp add: UNION_eq_Union_image range_binary_eq) + +lemma Int_range_binary: "a \ b = (\i::nat. binary a b i)" + by (simp add: INTER_eq_Inter_image range_binary_eq) + +lemma sigma_algebra_iff: + "sigma_algebra M \ + algebra M & (\A. range A \ sets M \ (\i::nat. A i) \ sets M)" + by (simp add: sigma_algebra_def sigma_algebra_axioms_def) + +lemma sigma_algebra_iff2: + "sigma_algebra M \ + sets M \ Pow (space M) & + {} \ sets M & (\s \ sets M. space M - s \ sets M) & + (\A. range A \ sets M \ (\i::nat. A i) \ sets M)" + by (force simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def + algebra_def Un_range_binary) + + +subsection {* Initial Sigma Algebra *} + +text {*Sigma algebras can naturally be created as the closure of any set of + sets with regard to the properties just postulated. *} + +inductive_set + sigma_sets :: "'a set \ 'a set set \ 'a set set" + for sp :: "'a set" and A :: "'a set set" + where + Basic: "a \ A \ a \ sigma_sets sp A" + | Empty: "{} \ sigma_sets sp A" + | Compl: "a \ sigma_sets sp A \ sp - a \ sigma_sets sp A" + | Union: "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A" + + +definition + sigma where + "sigma sp A = (| space = sp, sets = sigma_sets sp A |)" + + +lemma space_sigma [simp]: "space (sigma X B) = X" + by (simp add: sigma_def) + +lemma sigma_sets_top: "sp \ sigma_sets sp A" + by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty) + +lemma sigma_sets_into_sp: "A \ Pow sp \ x \ sigma_sets sp A \ x \ sp" + by (erule sigma_sets.induct, auto) + +lemma sigma_sets_Un: + "a \ sigma_sets sp A \ b \ sigma_sets sp A \ a \ b \ sigma_sets sp A" +apply (simp add: Un_range_binary range_binary_eq) +apply (metis Union COMBK_def binary_def fun_upd_apply) +done + +lemma sigma_sets_Inter: + assumes Asb: "A \ Pow sp" + shows "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A" +proof - + assume ai: "\i::nat. a i \ sigma_sets sp A" + hence "\i::nat. sp-(a i) \ sigma_sets sp A" + by (rule sigma_sets.Compl) + hence "(\i. sp-(a i)) \ sigma_sets sp A" + by (rule sigma_sets.Union) + hence "sp-(\i. sp-(a i)) \ sigma_sets sp A" + by (rule sigma_sets.Compl) + also have "sp-(\i. sp-(a i)) = sp Int (\i. a i)" + by auto + also have "... = (\i. a i)" using ai + by (blast dest: sigma_sets_into_sp [OF Asb]) + finally show ?thesis . +qed + +lemma sigma_sets_INTER: + assumes Asb: "A \ Pow sp" + and ai: "\i::nat. i \ S \ a i \ sigma_sets sp A" and non: "S \ {}" + shows "(\i\S. a i) \ sigma_sets sp A" +proof - + from ai have "\i. (if i\S then a i else sp) \ sigma_sets sp A" + by (simp add: sigma_sets.intros sigma_sets_top) + hence "(\i. (if i\S then a i else sp)) \ sigma_sets sp A" + by (rule sigma_sets_Inter [OF Asb]) + also have "(\i. (if i\S then a i else sp)) = (\i\S. a i)" + by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ + finally show ?thesis . +qed + +lemma (in sigma_algebra) sigma_sets_subset: + assumes a: "a \ sets M" + shows "sigma_sets (space M) a \ sets M" +proof + fix x + assume "x \ sigma_sets (space M) a" + from this show "x \ sets M" + by (induct rule: sigma_sets.induct, auto) (metis a subsetD) +qed + +lemma (in sigma_algebra) sigma_sets_eq: + "sigma_sets (space M) (sets M) = sets M" +proof + show "sets M \ sigma_sets (space M) (sets M)" + by (metis Set.subsetI sigma_sets.Basic space_closed) + next + show "sigma_sets (space M) (sets M) \ sets M" + by (metis sigma_sets_subset subset_refl) +qed + +lemma sigma_algebra_sigma_sets: + "a \ Pow (space M) \ sets M = sigma_sets (space M) a \ sigma_algebra M" + apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def + algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) + apply (blast dest: sigma_sets_into_sp) + apply (blast intro: sigma_sets.intros) + done + +lemma sigma_algebra_sigma: + "a \ Pow X \ sigma_algebra (sigma X a)" + apply (rule sigma_algebra_sigma_sets) + apply (auto simp add: sigma_def) + done + +lemma (in sigma_algebra) sigma_subset: + "a \ sets M ==> sets (sigma (space M) a) \ (sets M)" + by (simp add: sigma_def sigma_sets_subset) + +end + diff -r 02de0317f66f -r 73a0c804840f src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Product_Type.thy Wed Oct 28 11:43:06 2009 +0000 @@ -927,6 +927,9 @@ insert (a,b) (A \ insert b B \ insert a A \ B)" by blast +lemma vimage_Times: "f -` (A \ B) = ((fst \ f) -` A) \ ((snd \ f) -` B)" + by (auto, rule_tac p = "f x" in PairE, auto) + subsubsection {* Code generator setup *} instance * :: (eq, eq) eq .. diff -r 02de0317f66f -r 73a0c804840f src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/SEQ.thy Wed Oct 28 11:43:06 2009 +0000 @@ -205,6 +205,9 @@ shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" unfolding LIMSEQ_def dist_norm .. +lemma LIMSEQ_iff_nz: "X ----> L = (\r>0. \no>0. \n\no. dist (X n) L < r)" + by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc) + lemma LIMSEQ_Zseq_iff: "((\n. X n) ----> L) = Zseq (\n. X n - L)" by (simp only: LIMSEQ_iff Zseq_def) diff -r 02de0317f66f -r 73a0c804840f src/HOL/Series.thy --- a/src/HOL/Series.thy Wed Oct 28 00:24:38 2009 +0100 +++ b/src/HOL/Series.thy Wed Oct 28 11:43:06 2009 +0000 @@ -10,7 +10,7 @@ header{*Finite Summation and Infinite Series*} theory Series -imports SEQ +imports SEQ Deriv begin definition @@ -285,6 +285,26 @@ text{*A summable series of positive terms has limit that is at least as great as any partial sum.*} +lemma pos_summable: + fixes f:: "nat \ real" + assumes pos: "!!n. 0 \ f n" and le: "!!n. setsum f {0.. x" + shows "summable f" +proof - + have "convergent (\n. setsum f {0..n. setsum f {0..n. setsum f {0..n. x"]) + (auto simp add: le pos) + next + show "\m n. m \ n \ setsum f {0.. setsum f {0.. L" + by (blast dest: convergentD) + thus ?thesis + by (force simp add: summable_def sums_def) +qed + lemma series_pos_le: fixes f :: "nat \ real" shows "\summable f; \m\n. 0 \ f m\ \ setsum f {0.. suminf f" @@ -361,6 +381,19 @@ shows "norm x < 1 \ summable (\n. x ^ n)" by (rule geometric_sums [THEN sums_summable]) +lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,ordered_field})" + by arith + +lemma power_half_series: "(\n. (1/2::real)^Suc n) sums 1" +proof - + have 2: "(\n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"] + by auto + have "(\n. (1/2::real)^Suc n) = (\n. (1 / 2) ^ n / 2)" + by simp + thus ?thesis using divide.sums [OF 2, of 2] + by simp +qed + text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*} lemma summable_convergent_sumr_iff: diff -r 02de0317f66f -r 73a0c804840f src/HOL/SupInf.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SupInf.thy Wed Oct 28 11:43:06 2009 +0000 @@ -0,0 +1,462 @@ +(* Author: Amine Chaieb and L C Paulson, University of Cambridge *) + +header {*Sup and Inf Operators on Sets of Reals.*} + +theory SupInf +imports RComplete +begin + +lemma minus_max_eq_min: + fixes x :: "'a::{lordered_ab_group_add, linorder}" + shows "- (max x y) = min (-x) (-y)" +by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1) + +lemma minus_min_eq_max: + fixes x :: "'a::{lordered_ab_group_add, linorder}" + shows "- (min x y) = max (-x) (-y)" +by (metis minus_max_eq_min minus_minus) + +lemma minus_Max_eq_Min [simp]: + fixes S :: "'a::{lordered_ab_group_add, linorder} set" + shows "finite S \ S \ {} \ - (Max S) = Min (uminus ` S)" +proof (induct S rule: finite_ne_induct) + case (singleton x) + thus ?case by simp +next + case (insert x S) + thus ?case by (simp add: minus_max_eq_min) +qed + +lemma minus_Min_eq_Max [simp]: + fixes S :: "'a::{lordered_ab_group_add, linorder} set" + shows "finite S \ S \ {} \ - (Min S) = Max (uminus ` S)" +proof (induct S rule: finite_ne_induct) + case (singleton x) + thus ?case by simp +next + case (insert x S) + thus ?case by (simp add: minus_min_eq_max) +qed + +instantiation real :: Sup +begin +definition + Sup_real_def [code del]: "Sup X == (LEAST z::real. \x\X. x\z)" + +instance .. +end + +instantiation real :: Inf +begin +definition + Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))" + +instance .. +end + +subsection{*Supremum of a set of reals*} + +lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*) + fixes x :: real + assumes x: "x \ X" + and z: "!!x. x \ X \ x \ z" + shows "x \ Sup X" +proof (auto simp add: Sup_real_def) + from reals_complete2 + obtain s where s: "(\y\X. y \ s) & (\z. ((\y\X. y \ z) --> s \ z))" + by (blast intro: x z) + hence "x \ s" + by (blast intro: x z) + also with s have "... = (LEAST z. \x\X. x \ z)" + by (fast intro: Least_equality [symmetric]) + finally show "x \ (LEAST z. \x\X. x \ z)" . +qed + +lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*) + fixes z :: real + assumes x: "X \ {}" + and z: "\x. x \ X \ x \ z" + shows "Sup X \ z" +proof (auto simp add: Sup_real_def) + from reals_complete2 x + obtain s where s: "(\y\X. y \ s) & (\z. ((\y\X. y \ z) --> s \ z))" + by (blast intro: z) + hence "(LEAST z. \x\X. x \ z) = s" + by (best intro: Least_equality) + also with s z have "... \ z" + by blast + finally show "(LEAST z. \x\X. x \ z) \ z" . +qed + +lemma Sup_singleton [simp]: "Sup {x::real} = x" + by (force intro: Least_equality simp add: Sup_real_def) + +lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*) + fixes z :: real + assumes X: "z \ X" and z: "!!x. x \ X \ x \ z" + shows "Sup X = z" + by (force intro: Least_equality X z simp add: Sup_real_def) + +lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*) + fixes x :: real + shows "x \ X \ y \ x \ (!!x. x \ X \ x \ z) \ y \ Sup X" + by (metis Sup_upper real_le_trans) + +lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*) + fixes z :: real + shows "X ~= {} ==> (!!x. x \ X ==> x \ z) ==> (\x\X. y y < Sup X" + by (metis Sup_least Sup_upper linorder_not_le le_less_trans) + +lemma Sup_eq: + fixes a :: real + shows "(!!x. x \ X \ x \ a) + \ (!!y. (!!x. x \ X \ x \ y) \ a \ y) \ Sup X = a" + by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb + insert_not_empty real_le_anti_sym) + +lemma Sup_le: + fixes S :: "real set" + shows "S \ {} \ S *<= b \ Sup S \ b" +by (metis SupInf.Sup_least setle_def) + +lemma Sup_upper_EX: + fixes x :: real + shows "x \ X \ \z. \x. x \ X \ x \ z \ x \ Sup X" + by blast + +lemma Sup_insert_nonempty: + fixes x :: real + assumes x: "x \ X" + and z: "!!x. x \ X \ x \ z" + shows "Sup (insert a X) = max a (Sup X)" +proof (cases "Sup X \ a") + case True + thus ?thesis + apply (simp add: max_def) + apply (rule Sup_eq_maximum) + apply (metis insertCI) + apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z) + done +next + case False + hence 1:"a < Sup X" by simp + have "Sup X \ Sup (insert a X)" + apply (rule Sup_least) + apply (metis empty_psubset_nonempty psubset_eq x) + apply (rule Sup_upper_EX) + apply blast + apply (metis insert_iff real_le_linear real_le_refl real_le_trans z) + done + moreover + have "Sup (insert a X) \ Sup X" + apply (rule Sup_least) + apply blast + apply (metis False Sup_upper insertE real_le_linear z) + done + ultimately have "Sup (insert a X) = Sup X" + by (blast intro: antisym ) + thus ?thesis + by (metis 1 min_max.le_iff_sup real_less_def) +qed + +lemma Sup_insert_if: + fixes X :: "real set" + assumes z: "!!x. x \ X \ x \ z" + shows "Sup (insert a X) = (if X={} then a else max a (Sup X))" +by auto (metis Sup_insert_nonempty z) + +lemma Sup: + fixes S :: "real set" + shows "S \ {} \ (\b. S *<= b) \ isLub UNIV S (Sup S)" +by (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) + +lemma Sup_finite_Max: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "Sup S = Max S" +using fS Se +proof- + let ?m = "Max S" + from Max_ge[OF fS] have Sm: "\ x\ S. x \ ?m" by metis + with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def) + from Max_in[OF fS Se] lub have mrS: "?m \ Sup S" + by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) + moreover + have "Sup S \ ?m" using Sm lub + by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) + ultimately show ?thesis by arith +qed + +lemma Sup_finite_in: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "Sup S \ S" + using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis + +lemma Sup_finite_ge_iff: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "a \ Sup S \ (\ x \ S. a \ x)" +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans) + +lemma Sup_finite_le_iff: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "a \ Sup S \ (\ x \ S. a \ x)" +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) + +lemma Sup_finite_gt_iff: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "a < Sup S \ (\ x \ S. a < x)" +by (metis Se Sup_finite_le_iff fS linorder_not_less) + +lemma Sup_finite_lt_iff: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "a > Sup S \ (\ x \ S. a > x)" +by (metis Se Sup_finite_ge_iff fS linorder_not_less) + +lemma Sup_unique: + fixes S :: "real set" + shows "S *<= b \ (\b' < b. \x \ S. b' < x) \ Sup S = b" +unfolding setle_def +apply (rule Sup_eq, auto) +apply (metis linorder_not_less) +done + +lemma Sup_abs_le: + fixes S :: "real set" + shows "S \ {} \ (\x\S. \x\ \ a) \ \Sup S\ \ a" +by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) + +lemma Sup_bounds: + fixes S :: "real set" + assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" + shows "a \ Sup S \ Sup S \ b" +proof- + from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast + hence b: "Sup S \ b" using u + by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) + from Se obtain y where y: "y \ S" by blast + from lub l have "a \ Sup S" + by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) + (metis le_iff_sup le_sup_iff y) + with b show ?thesis by blast +qed + +lemma Sup_asclose: + fixes S :: "real set" + assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\Sup S - l\ \ e" +proof- + have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" by arith + thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th + by (auto simp add: setge_def setle_def) +qed + + +subsection{*Infimum of a set of reals*} + +lemma Inf_lower [intro]: + fixes z :: real + assumes x: "x \ X" + and z: "!!x. x \ X \ z \ x" + shows "Inf X \ x" +proof - + have "-x \ Sup (uminus ` X)" + by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z) + thus ?thesis + by (auto simp add: Inf_real_def) +qed + +lemma Inf_greatest [intro]: + fixes z :: real + assumes x: "X \ {}" + and z: "\x. x \ X \ z \ x" + shows "z \ Inf X" +proof - + have "Sup (uminus ` X) \ -z" using x z by (force intro: Sup_least) + hence "z \ - Sup (uminus ` X)" + by simp + thus ?thesis + by (auto simp add: Inf_real_def) +qed + +lemma Inf_singleton [simp]: "Inf {x::real} = x" + by (simp add: Inf_real_def) + +lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*) + fixes z :: real + assumes x: "z \ X" and z: "!!x. x \ X \ z \ x" + shows "Inf X = z" +proof - + have "Sup (uminus ` X) = -z" using x z + by (force intro: Sup_eq_maximum x z) + thus ?thesis + by (simp add: Inf_real_def) +qed + +lemma Inf_lower2: + fixes x :: real + shows "x \ X \ x \ y \ (!!x. x \ X \ z \ x) \ Inf X \ y" + by (metis Inf_lower real_le_trans) + +lemma Inf_real_iff: + fixes z :: real + shows "X \ {} \ (!!x. x \ X \ z \ x) \ (\x\X. x Inf X < y" + by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear + order_less_le_trans) + +lemma Inf_eq: + fixes a :: real + shows "(!!x. x \ X \ a \ x) \ (!!y. (!!x. x \ X \ y \ x) \ y \ a) \ Inf X = a" + by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel + insert_absorb insert_not_empty real_le_anti_sym) + +lemma Inf_ge: + fixes S :: "real set" + shows "S \ {} \ b <=* S \ Inf S \ b" +by (metis SupInf.Inf_greatest setge_def) + +lemma Inf_lower_EX: + fixes x :: real + shows "x \ X \ \z. \x. x \ X \ z \ x \ Inf X \ x" + by blast + +lemma Inf_insert_nonempty: + fixes x :: real + assumes x: "x \ X" + and z: "!!x. x \ X \ z \ x" + shows "Inf (insert a X) = min a (Inf X)" +proof (cases "a \ Inf X") + case True + thus ?thesis + by (simp add: min_def) + (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) +next + case False + hence 1:"Inf X < a" by simp + have "Inf (insert a X) \ Inf X" + apply (rule Inf_greatest) + apply (metis empty_psubset_nonempty psubset_eq x) + apply (rule Inf_lower_EX) + apply (blast intro: elim:) + apply (metis insert_iff real_le_linear real_le_refl real_le_trans z) + done + moreover + have "Inf X \ Inf (insert a X)" + apply (rule Inf_greatest) + apply blast + apply (metis False Inf_lower insertE real_le_linear z) + done + ultimately have "Inf (insert a X) = Inf X" + by (blast intro: antisym ) + thus ?thesis + by (metis False min_max.inf_absorb2 real_le_linear) +qed + +lemma Inf_insert_if: + fixes X :: "real set" + assumes z: "!!x. x \ X \ z \ x" + shows "Inf (insert a X) = (if X={} then a else min a (Inf X))" +by auto (metis Inf_insert_nonempty z) + +lemma Inf_greater: + fixes z :: real + shows "X \ {} \ Inf X < z \ \x \ X. x < z" + by (metis Inf_real_iff mem_def not_leE) + +lemma Inf_close: + fixes e :: real + shows "X \ {} \ 0 < e \ \x \ X. x < Inf X + e" + by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict) + +lemma Inf_finite_Min: + fixes S :: "real set" + shows "finite S \ S \ {} \ Inf S = Min S" +by (simp add: Inf_real_def Sup_finite_Max image_image) + +lemma Inf_finite_in: + fixes S :: "real set" + assumes fS: "finite S" and Se: "S \ {}" + shows "Inf S \ S" + using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis + +lemma Inf_finite_ge_iff: + fixes S :: "real set" + shows "finite S \ S \ {} \ a \ Inf S \ (\ x \ S. a \ x)" +by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans) + +lemma Inf_finite_le_iff: + fixes S :: "real set" + shows "finite S \ S \ {} \ a \ Inf S \ (\ x \ S. a \ x)" +by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le + real_le_anti_sym real_le_linear) + +lemma Inf_finite_gt_iff: + fixes S :: "real set" + shows "finite S \ S \ {} \ a < Inf S \ (\ x \ S. a < x)" +by (metis Inf_finite_le_iff linorder_not_less) + +lemma Inf_finite_lt_iff: + fixes S :: "real set" + shows "finite S \ S \ {} \ a > Inf S \ (\ x \ S. a > x)" +by (metis Inf_finite_ge_iff linorder_not_less) + +lemma Inf_unique: + fixes S :: "real set" + shows "b <=* S \ (\b' > b. \x \ S. b' > x) \ Inf S = b" +unfolding setge_def +apply (rule Inf_eq, auto) +apply (metis less_le_not_le linorder_not_less) +done + +lemma Inf_abs_ge: + fixes S :: "real set" + shows "S \ {} \ (\x\S. \x\ \ a) \ \Inf S\ \ a" +by (simp add: Inf_real_def) (rule Sup_abs_le, auto) + +lemma Inf_asclose: + fixes S :: "real set" + assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\Inf S - l\ \ e" +proof - + have "\- Sup (uminus ` S) - l\ = \Sup (uminus ` S) - (-l)\" + by auto + also have "... \ e" + apply (rule Sup_asclose) + apply (auto simp add: S) + apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) + done + finally have "\- Sup (uminus ` S) - l\ \ e" . + thus ?thesis + by (simp add: Inf_real_def) +qed + +subsection{*Relate max and min to Sup and Inf.*} + +lemma real_max_Sup: + fixes x :: real + shows "max x y = Sup {x,y}" +proof- + have f: "finite {x, y}" "{x,y} \ {}" by simp_all + from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \ max x y" by simp + moreover + have "max x y \ Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"] + by (simp add: linorder_linear) + ultimately show ?thesis by arith +qed + +lemma real_min_Inf: + fixes x :: real + shows "min x y = Inf {x,y}" +proof- + have f: "finite {x, y}" "{x,y} \ {}" by simp_all + from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \ min x y" + by (simp add: linorder_linear) + moreover + have "min x y \ Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"] + by simp + ultimately show ?thesis by arith +qed + +end