--- 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;
--- 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
--- 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
--- 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 \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
+ shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
+proof (rule Pi_I)
+ fix z
+ assume z: "z \<in> A"
+ have "f z = (fst (f z), snd (f z))"
+ by simp
+ also have "... \<in> B z \<times> C z"
+ by (metis SigmaI PiE o_apply 1 2 z)
+ finally show "f z \<in> B z \<times> C z" .
+qed
+
subsection{*Composition With a Restricted Domain: @{term compose}*}
--- 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 \<in> 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:"\<forall>x\<in>s. \<forall>y\<in>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 \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
+ def k \<equiv> "Sup ((\<lambda>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 "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
- hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
+ hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
next
fix x assume "x\<in>s"
- hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
- unfolding setle_def
+ hence "k \<le> 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 \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
- obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" using assms(3-5) by auto
- hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> 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 ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>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\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
+ using assms(3-5) by auto
+ hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
+ by (force simp add: inner_diff)
+ thus ?thesis
+ apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>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 \<le> 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 \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
--- 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 \<Rightarrow> real" where
- "rsup S = (SOME a. isLub UNIV S a)"
-
-lemma rsup_alt: "rsup S = (SOME a. (\<forall>x \<in> S. x \<le> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<le> b) \<longrightarrow> a \<le> b))" by (auto simp add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def)
-
-lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>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 \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> 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 \<noteq> {}"
- shows "rsup S = Max S"
-using fS Se
-proof-
- let ?m = "Max S"
- from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?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 \<le> rsup S"
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- moreover
- have "rsup S \<le> ?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 \<noteq> {}"
- shows "rsup S \<in> 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 \<noteq> {}"
- 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 \<noteq> {}"
- shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> 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 \<noteq> {}"
- shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> 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 \<noteq> {}"
- shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> 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 \<noteq> {}"
- shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> 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: "\<forall>b' < b. \<exists>x \<in> 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\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> 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 = (\<lambda>x. S *<= x \<and> x \<in> 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 \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
- shows "a \<le> rsup S \<and> rsup S \<le> b"
-proof-
- from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
- hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
- from Se obtain y where y: "y \<in> S" by blast
- from lub l have "a \<le> 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 \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> 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 \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rsup S - l\<bar> \<le> e"
-proof-
- have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> 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 \<Rightarrow> real" where
- "rinf S = (SOME a. isGlb UNIV S a)"
-
-lemma rinf_alt: "rinf S = (SOME a. (\<forall>x \<in> S. x \<ge> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<ge> b) \<longrightarrow> a \<ge> b))" by (auto simp add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def)
-
-lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
- shows "\<exists>(t::real). isGlb UNIV S t"
-proof-
- let ?M = "uminus ` S"
- from lb have th: "\<exists>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: "\<exists>x. x \<in> ?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 \<noteq> {}" and b: "\<exists>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 \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> 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 \<noteq> {}"
- shows "rinf S = Min S"
-using fS Se
-proof-
- let ?m = "Min S"
- from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?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 \<ge> rinf S"
- by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
- moreover
- have "rinf S \<ge> ?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 \<noteq> {}"
- shows "rinf S \<in> 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 \<noteq> {}"
- 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 \<noteq> {}"
- shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> 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 \<noteq> {}"
- shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> 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 \<noteq> {}"
- shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> 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 \<noteq> {}"
- shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> 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: "\<forall>b' > b. \<exists>x \<in> 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\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> 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 = (\<lambda>x. x <=* S \<and> x \<in> R)"
- apply (rule ext)
- by (metis isLb_def)
-
-lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
- shows "a \<le> rinf S \<and> rinf S \<le> b"
-proof-
- from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
- hence b: "a \<le> 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 \<in> S" by blast
- from lub u have "b \<ge> 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 \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> 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 \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rinf S - l\<bar> \<le> e"
-proof-
- have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> 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 \<Rightarrow> real^'m::finite"
@@ -2578,7 +2345,7 @@
have Se: "?S \<noteq> {}" using norm_basis by auto
from linear_bounded[OF lf] have b: "\<exists> 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 "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> 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 \<Rightarrow> 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} \<noteq> {}" by simp_all
- from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
- moreover
- have "max x y \<le> 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} \<noteq> {}" by simp_all
- from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
- by (simp add: linorder_linear)
- moreover
- have "min x y \<le> 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\<in> (UNIV :: 'n set)}"
+definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
by auto
@@ -5065,7 +4807,7 @@
lemma infnorm_pos_le: "0 \<le> 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: "\<And>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 \<longleftrightarrow> 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 \<noteq> {}" by blast
have th1: "\<And>S f. f ` S = { f i| i. i \<in> 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) <= \<bar>a\<bar> * 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 \<le> 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)
--- 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 \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x <= a)"
by (simp add: bounded_iff)
-lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
- shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
+lemma bounded_has_Sup:
+ fixes S :: "real set"
+ assumes "bounded S" "S \<noteq> {}"
+ shows "\<forall>x\<in>S. x <= Sup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> Sup S <= b"
+proof
+ fix x assume "x\<in>S"
+ thus "x \<le> Sup S"
+ by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
+next
+ show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> 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 \<Longrightarrow> 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 \<noteq> {}"
+ shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
proof
fix x assume "x\<in>S"
from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
- hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
- thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
-next
- show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> 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 \<ge> Inf S" using `x\<in>S`
+ by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
next
- let ?S = "insert x S"
- case False
- hence *:"\<forall>x\<in>S. x \<le> 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) \<le> y" unfolding isUb_def using rsup_le[OF `S\<noteq>{}`]
- 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\<noteq>{}` by auto
-qed
-
-lemma sup_insert_finite: "finite S \<Longrightarrow> 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 \<noteq> {}"
- shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
-proof
- fix x assume "x\<in>S"
- from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
- hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
- thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
-next
- show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> 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 "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> 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 *:"\<forall>x\<in>S. x \<ge> 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) \<ge> y" unfolding isLb_def using rinf_ge[OF `S\<noteq>{}`]
- 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\<noteq>{}` 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 "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
proof-
from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
- { fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s" "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> 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: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s" "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> 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 \<noteq> {} ==> (\<exists>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 \<noteq> {}" shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
proof-
from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
- { fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s" "rinf s \<notin> s" "0 < e"
- "\<forall>x'\<in>s. x' = rinf s \<or> \<not> 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: "\<forall>x\<in>s. x \<ge> Inf s" "Inf s \<notin> s" "0 < e"
+ "\<forall>x'\<in>s. x' = Inf s \<or> \<not> 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 \<in> s"
- hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto
- have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>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 \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>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 \<in> s \<and> y \<in> s})"
+definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
(* TODO: generalize to class metric_space *)
lemma diameter_bounded:
@@ -4427,12 +4404,22 @@
hence "norm (x - y) \<le> 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\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
- have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
+ have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
+ apply auto (*FIXME: something horrible has happened here!*)
+ apply atomize
+ apply safe
+ apply metis +
+ done
have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s` isLubD1[OF lub] unfolding setle_def by auto }
moreover
{ fix d::real assume "d>0" "d < diameter s"
hence "s\<noteq>{}" 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 "\<exists>d' \<in> ?D. d' > d"
proof(rule ccontr)
assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> 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\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
- hence "diameter s \<le> norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}" "norm (x - y)"]
- unfolding setle_def and diameter_def by auto
+ hence "diameter s \<le> 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
--- /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 \<Rightarrow> real"
+
+definition
+ disjoint_family where
+ "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
+
+definition
+ positive where
+ "positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)"
+
+definition
+ additive where
+ "additive M f \<longleftrightarrow>
+ (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
+ \<longrightarrow> f (x \<union> y) = f x + f y)"
+
+definition
+ countably_additive where
+ "countably_additive M f \<longleftrightarrow>
+ (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
+ disjoint_family A \<longrightarrow>
+ (\<Union>i. A i) \<in> sets M \<longrightarrow>
+ (\<lambda>n. f (A n)) sums f (\<Union>i. A i))"
+
+definition
+ increasing where
+ "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
+
+definition
+ subadditive where
+ "subadditive M f \<longleftrightarrow>
+ (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
+ \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
+
+definition
+ countably_subadditive where
+ "countably_subadditive M f \<longleftrightarrow>
+ (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
+ disjoint_family A \<longrightarrow>
+ (\<Union>i. A i) \<in> sets M \<longrightarrow>
+ summable (f o A) \<longrightarrow>
+ f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))"
+
+definition
+ lambda_system where
+ "lambda_system M f =
+ {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
+
+definition
+ outer_measure_space where
+ "outer_measure_space M f \<longleftrightarrow>
+ positive M f & increasing M f & countably_subadditive M f"
+
+definition
+ measure_set where
+ "measure_set M f X =
+ {r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
+
+
+locale measure_space = sigma_algebra +
+ assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> 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 \<Longrightarrow> f {} = 0"
+ by (simp add: positive_def)
+
+lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x"
+ by (simp add: positive_def)
+
+lemma increasingD:
+ "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
+ by (auto simp add: increasing_def)
+
+lemma subadditiveD:
+ "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
+ \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
+ by (auto simp add: subadditive_def)
+
+lemma additiveD:
+ "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
+ \<Longrightarrow> f (x \<union> y) = f x + f y"
+ by (auto simp add: additive_def)
+
+lemma countably_additiveD:
+ "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
+ \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n)) sums f (\<Union>i. A i)"
+ by (simp add: countably_additive_def)
+
+lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
+ by blast
+
+lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
+ by blast
+
+lemma disjoint_family_subset:
+ "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
+ by (force simp add: disjoint_family_def)
+
+subsection {* A Two-Element Series *}
+
+definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
+ where "binaryset A B = (\<lambda>\<^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: "(\<Union>i. binaryset A B i) = A \<union> B"
+ by (simp add: UNION_eq_Union_image range_binaryset_eq)
+
+lemma LIMSEQ_binaryset:
+ assumes f: "f {} = 0"
+ shows "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
+proof -
+ have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
+ proof
+ fix n
+ show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
+ by (induct n) (auto simp add: binaryset_def f)
+ qed
+ moreover
+ have "... ----> f A + f B" by (rule LIMSEQ_const)
+ ultimately
+ have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
+ by metis
+ hence "(\<lambda>n. \<Sum>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 "(\<lambda>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 \<Longrightarrow> suminf (\<lambda>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 \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
+proof -
+ have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> 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 \<Longrightarrow> {} \<in> lambda_system M f"
+ by (auto simp add: positive_def lambda_system_eq)
+
+lemma lambda_system_sets:
+ "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
+ by (simp add: lambda_system_def)
+
+lemma (in algebra) lambda_system_Compl:
+ fixes f:: "'a set \<Rightarrow> real"
+ assumes x: "x \<in> lambda_system M f"
+ shows "space M - x \<in> lambda_system M f"
+ proof -
+ have "x \<subseteq> 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 \<Rightarrow> real"
+ assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+ shows "x \<inter> y \<in> 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 \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
+ and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
+ and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
+ have "u - x \<inter> y \<in> sets M"
+ by (metis Diff Diff_Int Un u x y)
+ moreover
+ have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
+ moreover
+ have "u - x \<inter> y - y = u - y" by blast
+ ultimately
+ have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
+ by force
+ have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
+ = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
+ by (simp add: ey)
+ also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
+ by (simp add: Int_ac)
+ also have "... = f (u \<inter> y) + f (u - y)"
+ using fx [THEN bspec, of "u \<inter> y"] Int y u
+ by force
+ also have "... = f u"
+ by (metis fy u)
+ finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
+ qed
+ qed
+
+
+lemma (in algebra) lambda_system_Un:
+ fixes f:: "'a set \<Rightarrow> real"
+ assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+ shows "x \<union> y \<in> lambda_system M f"
+proof -
+ have "(space M - x) \<inter> (space M - y) \<in> sets M"
+ by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
+ moreover
+ have "x \<union> y = space M - ((space M - x) \<inter> (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 \<Longrightarrow> 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 \<in> sets M" and disj: "x \<inter> y = {}"
+ and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+ shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
+ proof -
+ have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
+ moreover
+ have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
+ moreover
+ have "(z \<inter> (x \<union> y)) \<in> 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 \<in> sets M \<Longrightarrow> space M \<inter> x = x"
+ by (metis Int_absorb1 sets_into_space)
+
+lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> 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 \<inter> y = {}"
+ and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+ hence "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
+ thus "f (x \<union> 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 \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
+ hence "disjoint_family (binaryset x y)"
+ by (auto simp add: disjoint_family_def binaryset_def)
+ hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
+ (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
+ summable (f o (binaryset x y)) \<longrightarrow>
+ f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
+ using cs by (simp add: countably_subadditive_def)
+ hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
+ summable (f o (binaryset x y)) \<longrightarrow>
+ f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
+ by (simp add: range_binaryset_eq UN_binaryset_eq)
+ thus "f (x \<union> y) \<le> 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 \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
+ where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
+
+lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case (Suc n)
+ thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
+qed
+
+lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
+ apply (rule UN_finite2_eq [where k=0])
+ apply (simp add: finite_UN_disjointed_eq)
+ done
+
+lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> 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 \<subseteq> A n"
+ by (auto simp add: disjointed_def)
+
+
+lemma (in algebra) UNION_in_sets:
+ fixes A:: "nat \<Rightarrow> 'a set"
+ assumes A: "range A \<subseteq> sets M "
+ shows "(\<Union>i\<in>{0..<n}. A i) \<in> 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 \<subseteq> sets M "
+ shows "range (disjointed A) \<subseteq> sets M"
+proof (auto simp add: disjointed_def)
+ fix n
+ show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> 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 \<longleftrightarrow>
+ algebra M &
+ (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
+ (\<Union>i::nat. A i) \<in> sets M)"
+proof (auto simp add: sigma_algebra_iff)
+ fix A :: "nat \<Rightarrow> 'a set"
+ assume M: "algebra M"
+ and A: "range A \<subseteq> sets M"
+ and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
+ disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+ hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
+ disjoint_family (disjointed A) \<longrightarrow>
+ (\<Union>i. disjointed A i) \<in> sets M" by blast
+ hence "(\<Union>i. disjointed A i) \<in> sets M"
+ by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
+ thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
+qed
+
+
+lemma (in algebra) additive_sum:
+ fixes A:: "nat \<Rightarrow> 'a set"
+ assumes f: "positive M f" and ad: "additive M f"
+ and A: "range A \<subseteq> sets M"
+ and disj: "disjoint_family A"
+ shows "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
+proof (induct n)
+ case 0 show ?case using f by (simp add: positive_def)
+next
+ case (Suc n)
+ have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
+ by (auto simp add: disjoint_family_def neq_iff) blast
+ moreover
+ have "A n \<in> sets M" using A by blast
+ moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+ by (metis A UNION_in_sets atLeast0LessThan)
+ moreover
+ ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
+ using ad UNION_in_sets A by (auto simp add: additive_def)
+ with Suc.hyps show ?case using ad
+ by (auto simp add: atLeastLessThanSuc additive_def)
+qed
+
+
+lemma countably_subadditiveD:
+ "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
+ (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)"
+ by (auto simp add: countably_subadditive_def o_def)
+
+lemma (in algebra) increasing_additive_summable:
+ fixes A:: "nat \<Rightarrow> 'a set"
+ assumes f: "positive M f" and ad: "additive M f"
+ and inc: "increasing M f"
+ and A: "range A \<subseteq> sets M"
+ and disj: "disjoint_family A"
+ shows "summable (f o A)"
+proof (rule pos_summable)
+ fix n
+ show "0 \<le> (f \<circ> A) n" using f A
+ by (force simp add: positive_def)
+ next
+ fix n
+ have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
+ by (rule additive_sum [OF f ad A disj])
+ also have "... \<le> f (space M)" using space_closed A
+ by (blast intro: increasingD [OF inc] UNION_in_sets top)
+ finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" .
+qed
+
+lemma lambda_system_positive:
+ "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f"
+ by (simp add: positive_def lambda_system_def)
+
+lemma lambda_system_increasing:
+ "increasing M f \<Longrightarrow> 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 \<Rightarrow> 'a set"
+ assumes f: "positive M f" and a: "a \<in> sets M"
+ and A: "range A \<subseteq> lambda_system M f"
+ and disj: "disjoint_family A"
+ shows "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
+proof (induct n)
+ case 0 show ?case using f by (simp add: positive_def)
+next
+ case (Suc n)
+ have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
+ by (force simp add: disjoint_family_def neq_iff)
+ have 3: "A n \<in> lambda_system M f" using A
+ by blast
+ have 4: "UNION {0..<n} A \<in> 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 \<subseteq> lambda_system M f"
+ and disj: "disjoint_family A"
+ shows "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A) sums f (\<Union>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 \<subseteq> 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 \<subseteq> sets M"
+ by (metis A image_subset_iff lambda_system_sets)
+ have sumfA: "summable (f \<circ> 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: "(\<Union>i. A i) \<in> sets M"
+ by (metis A countable_UN image_subset_iff lambda_system_sets)
+ have U_eq: "f (\<Union>i. A i) = suminf (f o A)"
+ proof (rule antisym)
+ show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
+ by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
+ show "suminf (f \<circ> A) \<le> f (\<Union>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 \<in> sets M"
+ have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
+ proof -
+ have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> 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 (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
+ by blast
+ moreover
+ have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
+ by (auto simp add: disjoint_family_def)
+ moreover
+ have "a \<inter> (\<Union>i. A i) \<in> sets M"
+ by (metis Int U_in a)
+ ultimately
+ have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
+ using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
+ by (simp add: o_def)
+ moreover
+ have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) \<le> f a - f (a - (\<Union>i. A i))"
+ proof (rule suminf_le [OF summ])
+ fix n
+ have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+ by (metis A'' UNION_in_sets)
+ have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+ by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
+ have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
+ using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
+ by (simp add: A)
+ hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
+ by (simp add: lambda_system_eq UNION_in Diff_Compl a)
+ have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
+ by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
+ UNION_in U_in a)
+ thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>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 \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
+ by arith
+ next
+ have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
+ by (blast intro: increasingD [OF inc] a U_in)
+ also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
+ by (blast intro: subadditiveD [OF sa] Int Diff U_in)
+ finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>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 \<in> sets M" and a: "a \<subseteq> b"
+ shows "f b \<in> measure_set M f a"
+proof -
+ have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>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 \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
+ thus ?thesis using a
+ by (auto intro!: exI [of _ "(\<lambda>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 \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> 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 \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> 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 \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
+ have "f x \<le> f x + f (y-x)" using posf
+ by (simp add: positive_def) (metis Diff xy)
+ also have "... = f (x \<union> (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 \<le> 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 \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
+ hence "disjoint_family (binaryset x y)"
+ by (auto simp add: disjoint_family_def binaryset_def)
+ hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
+ (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
+ f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
+ using ca
+ by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique)
+ hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
+ f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))"
+ by (simp add: range_binaryset_eq UN_binaryset_eq)
+ thus "f (x \<union> 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 \<in> sets M"
+ shows "Inf (measure_set M f s) = f s"
+proof (rule Inf_eq)
+ fix z
+ assume z: "z \<in> measure_set M f s"
+ from this obtain A where
+ A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
+ and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)"
+ and si: "suminf (f \<circ> A) = z"
+ by (auto simp add: measure_set_def sums_iff)
+ hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
+ have inc: "increasing M f"
+ by (metis additive_increasing ca countably_additive_additive posf)
+ have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
+ proof (rule countably_additiveD [OF ca])
+ show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
+ by blast
+ show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
+ by (auto simp add: disjoint_family_def)
+ show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
+ by (metis UN_extend_simps(4) s seq)
+ qed
+ hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
+ by (metis Int_commute UN_simps(4) seq sums_iff)
+ also have "... \<le> suminf (f \<circ> A)"
+ proof (rule summable_le [OF _ _ sm])
+ show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
+ by (force intro: increasingD [OF inc])
+ show "summable (\<lambda>i. f (A i \<inter> s))" using sums
+ by (simp add: sums_iff)
+ qed
+ also have "... = z" by (rule si)
+ finally show "f s \<le> z" .
+next
+ fix y
+ assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u"
+ thus "y \<le> 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 \<le> Inf (measure_set M f {})"
+ by (metis empty_subsetI inf_measure_pos posf)
+ show "Inf (measure_set M f {}) \<le> 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 \<Longrightarrow>
+ positive (| space = space M, sets = Pow (space M) |)
+ (\<lambda>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) |)
+ (\<lambda>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 \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
+ shows "Inf (measure_set M f s) \<le> x"
+proof -
+ from x
+ obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
+ and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x"
+ by (auto simp add: sums_iff)
+ have dA: "range (disjointed A) \<subseteq> sets M"
+ by (metis A range_disjointed_sets)
+ have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n"
+ proof (auto)
+ fix n
+ have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
+ by (auto simp add: positive_def image_subset_iff)
+ also have "... \<le> f (A n)"
+ by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
+ finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
+ qed
+ from Series.summable_le2 [OF this sm]
+ have sda: "summable (f o disjointed A)"
+ "suminf (f o disjointed A) \<le> suminf (f \<circ> A)"
+ by blast+
+ hence ley: "suminf (f o disjointed A) \<le> x"
+ by (metis xeq)
+ from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)"
+ by (simp add: sums_iff)
+ hence y: "suminf (f o disjointed A) \<in> 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 \<subseteq> (space M)"
+ shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) &
+ (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e"
+proof -
+ have " measure_set M f s \<noteq> {}"
+ by (metis emptyE ss inf_measure_nonempty [OF posf top])
+ hence "\<exists>l \<in> 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) |)
+ (\<lambda>x. Inf (measure_set M f x))"
+proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon)
+ fix A :: "nat \<Rightarrow> 'a set" and e :: real
+ assume A: "range A \<subseteq> Pow (space M)"
+ and disj: "disjoint_family A"
+ and sb: "(\<Union>i. A i) \<subseteq> space M"
+ and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))"
+ and e: "0 < e"
+ have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and>
+ (f o B) sums l \<and>
+ l \<le> 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 "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
+ A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and>
+ ll n \<le> 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) \<subseteq> sets M)"
+ and disjBB: "!!n. disjoint_family (BB n)"
+ and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)"
+ and BBsums: "!!n. (f o BB n) sums ll n"
+ and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
+ by auto blast
+ have llpos: "!!n. 0 \<le> 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 \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
+ proof -
+ have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
+ by (rule sums_mult [OF power_half_series])
+ hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
+ and eqe: "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
+ by (auto simp add: sums_iff)
+ have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
+ suminf (\<lambda>n. e * (1/2)^(Suc n)) =
+ suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
+ by (rule suminf_add [OF sum1 sum0])
+ have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
+ by (metis ll llpos abs_of_nonneg)
+ have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
+ by (rule summable_add [OF sum1 sum0])
+ have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
+ using Series.summable_le2 [OF 1 2] by auto
+ also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
+ (\<Sum>n. e * (1 / 2) ^ Suc n)"
+ by (metis 0)
+ also have "... = (\<Sum>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 \<equiv> "(split BB) o nat_to_nat2"
+ have C: "!!n. C n \<in> 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: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
+ proof (auto simp add: C_def)
+ fix x i
+ assume x: "x \<in> A i"
+ with sbBB [of i] obtain j where "x \<in> BB i j"
+ by blast
+ thus "\<exists>i. x \<in> 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 \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
+ by (rule ext) (auto simp add: C_def)
+ also have "... sums suminf ll"
+ proof (rule suminf_2dimen)
+ show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
+ by (force simp add: positive_def)
+ show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(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 \<circ> C) sums suminf ll" .
+ have "Inf (measure_set M f (\<Union>i. A i)) \<le> 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 "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
+ by blast
+ finally show "Inf (measure_set M f (\<Union>i. A i)) \<le>
+ (\<Sum>n. Inf (measure_set M f (A n))) + e" .
+qed
+
+lemma (in algebra) inf_measure_outer:
+ "positive M f \<Longrightarrow> increasing M f
+ \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
+ (\<lambda>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 \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
+ (\<lambda>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 \<in> sets M"
+ and s: "s \<subseteq> space M"
+ have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
+ by blast
+ have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+ \<le> 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 \<subseteq> sets M" and disj: "disjoint_family A"
+ and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
+ and l: "l \<le> Inf (measure_set M f s) + e"
+ by auto
+ have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
+ (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
+ by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
+ have [simp]: "!!n. f (A n \<inter> 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 \<circ> A)"
+ by (metis fsums sums_iff)
+ { fix u
+ assume u: "u \<in> sets M"
+ have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> 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 (\<lambda>z. z\<inter>u) o A)"
+ by (rule summable_comparison_test [OF _ fsumb]) simp
+ have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
+ proof (rule Inf_lower)
+ show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
+ apply (simp add: measure_set_def)
+ apply (rule_tac x="(\<lambda>z. z \<inter> 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 "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x"
+ by (blast intro: inf_measure_pos0 [OF posf])
+ qed
+ note 1 2
+ } note lesum = this
+ have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)"
+ and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)"
+ and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
+ and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
+ \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
+ by (metis Diff lesum top x)+
+ hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+ \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
+ by (simp add: x)
+ also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2]
+ by (simp add: x) (simp add: o_def)
+ also have "... \<le> Inf (measure_set M f s) + e"
+ by (metis fsums l sums_unique)
+ finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+ \<le> Inf (measure_set M f s) + e" .
+ qed
+ moreover
+ have "Inf (measure_set M f s)
+ \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
+ proof -
+ have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
+ by (metis Un_Diff_Int Un_commute)
+ also have "... \<le> Inf (measure_set M f (s\<inter>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\<inter>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 \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
+ (measure M = measure N) \<Longrightarrow> 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 "\<exists>MS :: 'a measure_space.
+ (\<forall>s \<in> sets M. measure MS s = f s) \<and>
+ ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and>
+ measure_space MS"
+ proof -
+ have inc: "increasing M f"
+ by (metis additive_increasing ca countably_additive_additive posf)
+ let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
+ def ls \<equiv> "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 \<subseteq> 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) \<subseteq> 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
--- /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. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
+
+lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
+ by (auto simp add: prod_sets_def)
+
+definition
+ closed_cdi where
+ "closed_cdi M \<longleftrightarrow>
+ sets M \<subseteq> Pow (space M) &
+ (\<forall>s \<in> sets M. space M - s \<in> sets M) &
+ (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
+ (\<Union>i. A i) \<in> sets M) &
+ (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+
+
+inductive_set
+ smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
+ for M
+ where
+ Basic [intro]:
+ "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
+ | Compl [intro]:
+ "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
+ | Inc:
+ "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
+ \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
+ | Disj:
+ "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
+ \<Longrightarrow> (\<Union>i::nat. A i) \<in> 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 \<in> (space a -> space b) &
+ (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
+
+definition
+ measure_preserving where
+ "measure_preserving m1 m2 =
+ measurable m1 m2 \<inter>
+ {f . measure_space m1 & measure_space m2 &
+ (\<forall>y \<in> sets m2. measure m1 ((f -` y) \<inter> (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 \<subseteq> sets (smallest_closed_cdi M)"
+ by (auto simp add: smallest_closed_cdi_def)
+
+lemma (in algebra) smallest_ccdi_sets:
+ "smallest_ccdi_sets M \<subseteq> 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) \<subseteq> Pow (space M)"
+ by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
+
+lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
+ by (simp add: closed_cdi_def)
+
+lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
+ by (simp add: closed_cdi_def)
+
+lemma closed_cdi_Inc:
+ "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
+ (\<Union>i. A i) \<in> sets M"
+ by (simp add: closed_cdi_def)
+
+lemma closed_cdi_Disj:
+ "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+ by (simp add: closed_cdi_def)
+
+lemma closed_cdi_Un:
+ assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
+ and A: "A \<in> sets M" and B: "B \<in> sets M"
+ and disj: "A \<inter> B = {}"
+ shows "A \<union> B \<in> sets M"
+proof -
+ have ra: "range (binaryset A B) \<subseteq> 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 \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
+ and disj: "A \<inter> B = {}"
+ shows "A \<union> B \<in> smallest_ccdi_sets M"
+proof -
+ have ra: "range (binaryset A B) \<in> 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 \<in> sets M"
+ shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> 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 \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
+ by blast
+ also have "... \<in> 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: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
+ by blast
+ have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
+ by blast
+ moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
+ by (simp add: Inc)
+ moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
+ by blast
+ ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
+ by (rule smallest_ccdi_sets.Inc)
+ show ?case
+ by (metis 1 2)
+next
+ case (Disj A)
+ have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
+ by blast
+ have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
+ by blast
+ moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
+ by (auto simp add: disjoint_family_def)
+ ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> 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 \<in> smallest_ccdi_sets M"
+ shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> 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) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
+ by blast
+ also have "... \<in> 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: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
+ by blast
+ have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
+ by blast
+ moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
+ by (simp add: Inc)
+ moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
+ by blast
+ ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
+ by (rule smallest_ccdi_sets.Inc)
+ show ?case
+ by (metis 1 2)
+next
+ case (Disj A)
+ have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
+ by blast
+ have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
+ by blast
+ moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
+ by (auto simp add: disjoint_family_def)
+ ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> 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 \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
+ \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
+ by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
+
+lemma algebra_iff_Int:
+ "algebra M \<longleftrightarrow>
+ sets M \<subseteq> Pow (space M) & {} \<in> sets M &
+ (\<forall>a \<in> sets M. space M - a \<in> sets M) &
+ (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
+proof (auto simp add: algebra.Int, auto simp add: algebra_def)
+ fix a b
+ assume ab: "sets M \<subseteq> Pow (space M)"
+ "\<forall>a\<in>sets M. space M - a \<in> sets M"
+ "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
+ "a \<in> sets M" "b \<in> sets M"
+ hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
+ by blast
+ also have "... \<in> sets M"
+ by (metis ab)
+ finally show "a \<union> b \<in> sets M" .
+qed
+
+lemma (in algebra) sigma_property_disjoint_lemma:
+ assumes sbC: "sets M \<subseteq> C"
+ and ccdi: "closed_cdi (|space = space M, sets = C|)"
+ shows "sigma_sets (space M) (sets M) \<subseteq> C"
+proof -
+ have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> 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) \<subseteq> smallest_ccdi_sets M"
+ by auto
+ (metis sigma_algebra.sigma_sets_subset algebra.simps(1)
+ algebra.simps(2) subsetD)
+ also have "... \<subseteq> C"
+ proof
+ fix x
+ assume x: "x \<in> smallest_ccdi_sets M"
+ thus "x \<in> 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 \<subseteq> C"
+ and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
+ and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
+ \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
+ \<Longrightarrow> (\<Union>i. A i) \<in> C"
+ and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
+ \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
+ shows "sigma_sets (space M) (sets M) \<subseteq> C"
+proof -
+ have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
+ proof (rule sigma_property_disjoint_lemma)
+ show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
+ by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
+ next
+ show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
+ 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 \<subseteq> sets M
+ \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M
+ \<Longrightarrow> (measure M o A) sums measure M (\<Union>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 \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}
+ \<Longrightarrow> measure M a + measure M b = measure M (a \<union> b)"
+ by (metis additiveD additive)
+
+lemma (in measure_space) measure_compl:
+ assumes s: "s \<in> sets M"
+ shows "measure M (space M - s) = measure M (space M) - measure M s"
+proof -
+ have "measure M (space M) = measure M (s \<union> (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 \<subseteq> A (Suc n)"
+ shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
+proof -
+ {
+ fix m
+ have "!!n. A n \<subseteq> 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 \<Longrightarrow> A m \<subseteq> 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 \<subseteq> sets M"
+ and A0: "A 0 = {}"
+ and ASuc: "!!n. A n \<subseteq> A (Suc n)"
+ shows "(measure M o A) ----> measure M (\<Union>i. A i)"
+proof -
+ {
+ fix n
+ have "(measure M \<circ> A) n =
+ setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
+ proof (induct n)
+ case 0 thus ?case by (auto simp add: A0 empty_measure)
+ next
+ case (Suc m)
+ have "A (Suc m) = A m \<union> (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 = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
+ by (blast intro: ext)
+ have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
+ proof (rule UN_finite2_eq [where k=1], simp)
+ fix i
+ show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
+ proof (induct i)
+ case 0 thus ?case by (simp add: A0)
+ next
+ case (Suc i)
+ thus ?case
+ by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
+ qed
+ qed
+ have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
+ by (metis A Diff range_subsetD)
+ have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
+ by (blast intro: countable_UN range_subsetD [OF A])
+ have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
+ by (rule measure_countably_additive)
+ (auto simp add: disjoint_family_Suc ASuc A1 A2)
+ also have "... = measure M (\<Union>i. A i)"
+ by (simp add: Aeq)
+ finally have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>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 \<subseteq> sets M"
+ and ASuc: "!!n. A n \<subseteq> A (Suc n)"
+ shows "(measure M \<circ> A) ----> measure M (\<Union>i. A i)"
+proof -
+ have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
+ by (auto simp add: split: nat.splits)
+ have meq: "measure M \<circ> A = (\<lambda>n. (measure M \<circ> nat_case {} A) (Suc n))"
+ by (rule ext) simp
+ have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>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 (\<Union>i. A i)"
+ by (simp add: ueq)
+ finally have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>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 \<in> space a -> space b"
+ and ba: "!!y. y \<in> sets b ==> f -` y \<in> 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 \<subseteq> Pow (space a)"
+ by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI)
+next
+ show "{} \<in> op -` f ` sets b"
+ by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty)
+next
+ { fix y
+ assume y: "y \<in> 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) \<in> (vimage f) ` sets b"
+ by auto
+ (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
+ sigma_sets.Compl)
+ }
+ thus "\<forall>s\<in>sets b. space a - f -` s \<in> (vimage f) ` sets b"
+ by blast
+next
+ {
+ fix A:: "nat \<Rightarrow> 'a set"
+ assume A: "range A \<subseteq> (vimage f) ` (sets b)"
+ have "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
+ proof -
+ def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
+ {
+ fix i
+ have "A i \<in> (vimage f) ` (sets b)" using A
+ by blast
+ hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
+ by blast
+ hence "B i \<in> sets b \<and> f -` B i = A i"
+ by (simp add: B_def) (erule someI_ex)
+ } note B = this
+ show ?thesis
+ proof
+ show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
+ by (simp add: vimage_UN B)
+ show "(\<Union>i. B i) \<in> sets b" using B
+ by (auto intro: sigma_algebra.countable_UN [OF b])
+ qed
+ qed
+ }
+ thus "\<forall>A::nat \<Rightarrow> 'a set.
+ range A \<subseteq> (vimage f) ` sets b \<longrightarrow> (\<Union>i. A i) \<in> (vimage f) ` sets b"
+ by blast
+qed
+
+lemma (in sigma_algebra) measurable_sigma:
+ assumes B: "B \<subseteq> Pow X"
+ and f: "f \<in> space M -> X"
+ and ba: "!!y. y \<in> B ==> (f -` y) \<inter> space M \<in> sets M"
+ shows "f \<in> measurable M (sigma X B)"
+proof -
+ have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
+ proof clarify
+ fix x
+ assume "x \<in> sigma_sets X B"
+ thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> 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 \<inter> 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 \<subseteq> 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' \<Longrightarrow> space m2 = space m2'
+ \<Longrightarrow> sets m1 = sets m1' \<Longrightarrow> sets m2 = sets m2'
+ \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
+ by (simp add: measurable_def sigma_algebra_iff2)
+
+lemma measure_preserving_lift:
+ fixes f :: "'a1 \<Rightarrow> '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 \<equiv> (|space = space m2, sets = x, measure = measure m2, ... = more m2|)"
+ assumes setsm2: "sets m2 = sigma_sets (space m2) a"
+ and fmp: "f \<in> measure_preserving m1 (m a)"
+ shows "f \<in> 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 \<in> measurable m1 (m a)"
+ and mam: "measure_space (m a)"
+ and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
+ have "f \<in> 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 \<in> measurable m1 m2" .
+ hence ffn: "f \<in> space m1 \<rightarrow> space m2"
+ by (simp add: measurable_def)
+ have "space m1 \<subseteq> f -` (space m2)"
+ by auto (metis PiE ffn)
+ hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
+ by blast
+ {
+ fix y
+ assume y: "y \<in> sets m2"
+ have ama: "algebra (m a)" using mam
+ by (simp add: measure_space_def sigma_algebra_iff)
+ have spa: "space m2 \<in> 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 "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
+ proof (rule algebra.sigma_property_disjoint, auto simp add: ama)
+ fix x
+ assume x: "x \<in> a"
+ thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
+ by (simp add: meq)
+ next
+ fix s
+ assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
+ and s: "s \<in> sigma_sets (space m2) a"
+ hence s2: "s \<in> sets m2"
+ by (simp add: setsm2)
+ thus "measure m1 (f -` (space m2 - s) \<inter> 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 \<subseteq> A (Suc n)"
+ and rA1: "range A \<subseteq>
+ {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+ and "range A \<subseteq> sigma_sets (space m2) a"
+ hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+ have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+ using rA1 by blast
+ have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))"
+ by (simp add: o_def eq1)
+ also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+ proof (rule measure_space.measure_countable_increasing [OF m1])
+ show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+ using f12 rA2 by (auto simp add: measurable_def)
+ show "f -` A 0 \<inter> space m1 = {}" using A0
+ by blast
+ show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
+ using ASuc by auto
+ qed
+ also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+ by (simp add: vimage_UN)
+ finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
+ moreover
+ have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
+ by (rule measure_space.measure_countable_increasing
+ [OF m2 rA2, OF A0 ASuc])
+ ultimately
+ show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+ measure m2 (\<Union>i. A i)"
+ by (rule LIMSEQ_unique)
+ next
+ fix A :: "nat => 'a2 set"
+ assume dA: "disjoint_family A"
+ and rA1: "range A \<subseteq>
+ {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+ and "range A \<subseteq> sigma_sets (space m2) a"
+ hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+ hence Um2: "(\<Union>i. A i) \<in> sets m2"
+ by (metis range_subsetD setsm2 sigma_sets.Union)
+ have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+ using rA1 by blast
+ hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
+ by (simp add: o_def)
+ also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+ proof (rule measure_space.measure_countably_additive [OF m1] )
+ show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+ using f12 rA2 by (auto simp add: measurable_def)
+ show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
+ by (auto simp add: disjoint_family_def)
+ show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
+ proof (rule sigma_algebra.countable_UN [OF sa1])
+ show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
+ by (auto simp add: measurable_def)
+ qed
+ qed
+ finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
+ with measure_space.measure_countably_additive [OF m2 rA2 dA Um2]
+ have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
+ by (metis sums_unique)
+
+ moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+ by (simp add: vimage_UN)
+ ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+ measure m2 (\<Union>i. A i)"
+ by metis
+ qed
+ finally have "sigma_sets (space m2) a
+ \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
+ hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
+ by (force simp add: setsm2)
+ }
+ thus "f \<in> measurable m1 m2 \<and>
+ (\<forall>y\<in>sets m2.
+ measure m1 (f -` y \<inter> space m1) = measure m2 y)"
+ by (blast intro: f12)
+ qed
+qed
+
+lemma measurable_ident:
+ "sigma_algebra M ==> id \<in> 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 \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
+ shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
+ apply (auto simp add: measurable_def vimage_compose)
+ apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
+ apply force+
+ done
+
+ lemma measurable_strong:
+ fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
+ assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
+ and c: "sigma_algebra c"
+ and t: "f ` (space a) \<subseteq> t"
+ and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
+ shows "(g o f) \<in> measurable a c"
+proof -
+ have a: "sigma_algebra a" and b: "sigma_algebra b"
+ and fab: "f \<in> (space a -> space b)"
+ and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
+ by (auto simp add: measurable_def)
+ have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> 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 \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
+ \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
+ by (auto simp add: measurable_def)
+
+lemma measurable_up_sigma:
+ "measurable a b \<subseteq> 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 \<in> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 \<Longrightarrow>
+ measure_space m1 \<Longrightarrow> sigma_algebra m1 \<Longrightarrow> a \<subseteq> sets m1
+ \<Longrightarrow> f \<in> measure_preserving m1 m2"
+ by (auto simp add: measure_preserving_def measurable_def)
+
+lemma measure_preserving_up_sigma:
+ "measure_space m1 \<Longrightarrow> (sets m1 = sets (sigma (space m1) a))
+ \<Longrightarrow> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2
+ \<subseteq> 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) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
+ shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))
+ (prod_sets (sets a1) (sets a2)))"
+proof -
+ from 1 have sa1: "sigma_algebra a1" and fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
+ and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
+ by (auto simp add: measurable_def)
+ from 2 have sa2: "sigma_algebra a2" and fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
+ and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
+ by (auto simp add: measurable_def)
+ show ?thesis
+ proof (rule measurable_sigma)
+ show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
+ by (force simp add: prod_sets_def sigma_algebra_iff algebra_def)
+ next
+ show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
+ by (rule prod_final [OF fn1 fn2])
+ next
+ fix z
+ assume z: "z \<in> prod_sets (sets a1) (sets a2)"
+ thus "f -` z \<inter> space M \<in> sets M"
+ proof (auto simp add: prod_sets_def vimage_Times)
+ fix x y
+ assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
+ have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
+ ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
+ by blast
+ also have "... \<in> sets M" using x y q1 q2
+ by blast
+ finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
+ qed
+ qed
+qed
+
+
+lemma (in measure_space) measurable_range_reduce:
+ "f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> \<Longrightarrow>
+ s \<noteq> {}
+ \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
+ 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)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
+ 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)
+ \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
+ by (simp add: measurable_def sigma_algebra_Pow) intro_locales
+
+lemma (in measure_space) measure_real_sum_image:
+ assumes s: "s \<in> sets M"
+ and ssets: "\<And>x. x \<in> s ==> {x} \<in> sets M"
+ and fin: "finite s"
+ shows "measure M s = (\<Sum>x\<in>s. measure M {x})"
+proof -
+ {
+ fix u
+ assume u: "u \<subseteq> s & u \<in> sets M"
+ hence "finite u"
+ by (metis fin finite_subset)
+ hence "measure M u = (\<Sum>x\<in>u. measure M {x})" using u
+ proof (induct u)
+ case empty
+ thus ?case by simp
+ next
+ case (insert x t)
+ hence x: "x \<in> s" and t: "t \<subseteq> s"
+ by (simp_all add: insert_subset)
+ hence ts: "t \<in> sets M" using insert
+ by (metis Diff_insert_absorb Diff ssets)
+ have "measure M (insert x t) = measure M ({x} \<union> 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 "... = (\<Sum>x\<in>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 \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
+proof -
+ have 1: "sigma_algebra M \<Longrightarrow> ?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 \<equiv> \<lparr>space = space M, sets = sets M, measure = f\<rparr>"
+ 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 \<Rightarrow> 'a set"
+ assume A: "range A \<subseteq> sets Mf"
+ and disj: "disjoint_family A"
+ and UnA: "(\<Union>i. A i) \<in> sets Mf"
+ def I \<equiv> "{i. A i \<noteq> {}}"
+ have "Union (A ` I) \<subseteq> 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 "\<exists>N. \<forall>m\<ge>N. A m = {}"
+ proof (cases "I = {}")
+ case True thus ?thesis by (simp add: I_def)
+ next
+ case False
+ hence "\<forall>i\<in>I. i < Suc(Max I)"
+ by (simp add: Max_less_iff [symmetric] finI)
+ hence "\<forall>m \<ge> 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: "\<forall>m\<ge>N. A m = {}" by blast
+ hence "\<forall>m\<ge>N. (f o A) m = 0"
+ by simp
+ hence "(\<lambda>n. f (A n)) sums setsum (f o A) {0..<N}"
+ by (simp add: series_zero o_def)
+ also have "... = f (\<Union>i<N. A i)"
+ proof (induct N)
+ case 0 thus ?case by simp
+ next
+ case (Suc n)
+ have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
+ proof (rule Caratheodory.additiveD [OF addf])
+ show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
+ by (auto simp add: disjoint_family_def nat_less_le) blast
+ show "A n \<in> sets M" using A
+ by (force simp add: Mf_def)
+ show "(\<Union>i<n. A i) \<in> 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 (\<Union>i. A i)"
+ proof -
+ have "(\<Union> i<N. A i) = (\<Union>i. 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 "(\<lambda>n. f (A n)) sums f (\<Union>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
+ \<Longrightarrow> finite (space M)
+ \<Longrightarrow> positive M (measure M) \<Longrightarrow> additive M (measure M)
+ \<Longrightarrow> measure_space M"
+ by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto)
+
+end
+
--- /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
--- /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";
--- /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. \<exists>y z. Q x y z) ==> \<exists>f g. \<forall>x. Q x (f x) (g x)"
+ by metis
+
+lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
+ by blast
+
+
+lemma suminf_2dimen:
+ fixes f:: "nat * nat \<Rightarrow> real"
+ assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
+ and fsums: "!!m. (\<lambda>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 \<le> f x"
+ by (cases x) (simp add: f_nneg)
+ } note [iff] = this
+ have g_nneg: "!!m. 0 \<le> g m"
+ proof -
+ fix m
+ have "0 \<le> suminf (\<lambda>n. f (m,n))"
+ by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
+ thus "0 \<le> g m" using fsums [of m]
+ by (auto simp add: sums_iff)
+ qed
+ show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
+ proof (rule increasing_LIMSEQ, simp add: f_nneg)
+ fix n
+ def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
+ def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
+ have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
+ by (force simp add: i_def j_def
+ intro: finite_imageI Max_ge finite_Domain finite_Range)
+ have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})"
+ using setsum_reindex [of nat_to_nat2 "{0..<n}" f]
+ by (simp add: o_def)
+ (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj)
+ also have "... \<le> setsum f ({0..i} \<times> {0..j})"
+ by (rule setsum_mono2) (auto simp add: ij)
+ also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
+ by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
+ setsum_cartesian_product split_eta)
+ also have "... \<le> setsum g {0..<Suc i}"
+ proof (rule setsum_mono, simp add: less_Suc_eq_le)
+ fix m
+ assume m: "m \<le> i"
+ thus " (\<Sum>n = 0..j. f (m, n)) \<le> 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 "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
+ also have "... \<le> suminf g"
+ by (rule series_pos_le [OF sumg]) (simp add: g_nneg)
+ finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
+ next
+ fix e :: real
+ assume e: "0 < e"
+ with summable_sums [OF sumg]
+ obtain N where "\<bar>setsum g {0..<N} - suminf g\<bar> < 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..<N} + e/2" using series_pos_le [OF sumg]
+ by (simp add: g_nneg)
+ { fix m
+ assume m: "m<N"
+ hence enneg: "0 < e / (2 * real N)" using e
+ by (simp add: zero_less_divide_iff)
+ hence "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
+ using fsums [of m] m
+ by (force simp add: sums_def LIMSEQ_def dist_real_def)
+ hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)"
+ using fsums [of m]
+ by (auto simp add: sums_iff)
+ (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq')
+ }
+ hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
+ by (force intro: choice)
+ then obtain jj where jj:
+ "!!m. m<N \<Longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
+ by auto
+ def IJ \<equiv> "SIGMA i : {0..<N}. {0..<jj i}"
+ have "setsum g {0..<N} <
+ (\<Sum>m = 0..<N. (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N))"
+ by (auto simp add: nz jj intro: setsum_strict_mono)
+ also have "... = (\<Sum>m = 0..<N. \<Sum>n = 0..<jj m. f (m, n)) + e/2" using nz
+ by (auto simp add: setsum_addf real_of_nat_def)
+ also have "... = setsum f IJ + e/2"
+ by (simp add: IJ_def setsum_Sigma)
+ finally have "setsum g {0..<N} < setsum f IJ + e/2" .
+ hence glessf: "suminf g < setsum f IJ + e" using gless
+ by auto
+ have finite_IJ: "finite IJ"
+ by (simp add: IJ_def)
+ def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
+ have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
+ proof (auto simp add: NIJ_def)
+ fix i j
+ assume ij:"(i,j) \<in> 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) \<in> 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 \<le> setsum f (nat_to_nat2 `{0..NIJ})"
+ by (rule setsum_mono2) (auto simp add: IJsb)
+ also have "... = (\<Sum>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 "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
+ by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
+ finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
+ thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
+ by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Oct 28 11:43:06 2009 +0000
@@ -0,0 +1,229 @@
+(* Title: Sigma_Algebra.thy
+ Author: Stefan Richter, Markus Wenzel, TU Muenchen
+ Plus material from the Hurd/Coble measure theory development,
+ translated by Lawrence Paulson.
+*)
+
+header {* Sigma Algebras *}
+
+theory Sigma_Algebra imports Complex_Main begin
+
+text {* Sigma algebras are an elementary concept in measure
+ theory. To measure --- that is to integrate --- functions, we first have
+ to measure sets. Unfortunately, when dealing with a large universe,
+ it is often not possible to consistently assign a measure to every
+ subset. Therefore it is necessary to define the set of measurable
+ subsets of the universe. A sigma algebra is such a set that has
+ three very natural and desirable properties. *}
+
+subsection {* Algebras *}
+
+record 'a algebra =
+ space :: "'a set"
+ sets :: "'a set set"
+
+locale algebra =
+ fixes M
+ assumes space_closed: "sets M \<subseteq> Pow (space M)"
+ and empty_sets [iff]: "{} \<in> sets M"
+ and compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
+ and Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
+
+lemma (in algebra) top [iff]: "space M \<in> sets M"
+ by (metis Diff_empty compl_sets empty_sets)
+
+lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
+ by (metis PowD contra_subsetD space_closed)
+
+lemma (in algebra) Int [intro]:
+ assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
+proof -
+ have "((space M - a) \<union> (space M - b)) \<in> sets M"
+ by (metis a b compl_sets Un)
+ moreover
+ have "a \<inter> b = space M - ((space M - a) \<union> (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 \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
+proof -
+ have "(a \<inter> (space M - b)) \<in> sets M"
+ by (metis a b compl_sets Int)
+ moreover
+ have "a - b = (a \<inter> (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 \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
+ by (induct set: finite) (auto simp add: Un)
+
+
+subsection {* Sigma Algebras *}
+
+locale sigma_algebra = algebra +
+ assumes countable_UN [intro]:
+ "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+
+lemma (in sigma_algebra) countable_INT:
+ assumes a: "range a \<subseteq> sets M"
+ shows "(\<Inter>i::nat. a i) \<in> sets M"
+proof -
+ have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
+ by (blast intro: countable_UN compl_sets a)
+ moreover
+ have "(\<Inter>i. a i) = space M - (\<Union>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 \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
+ where "binary a b = (\<lambda>\<^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 \<union> b = (\<Union>i::nat. binary a b i)"
+ by (simp add: UNION_eq_Union_image range_binary_eq)
+
+lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
+ by (simp add: INTER_eq_Inter_image range_binary_eq)
+
+lemma sigma_algebra_iff:
+ "sigma_algebra M \<longleftrightarrow>
+ algebra M & (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+ by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
+
+lemma sigma_algebra_iff2:
+ "sigma_algebra M \<longleftrightarrow>
+ sets M \<subseteq> Pow (space M) &
+ {} \<in> sets M & (\<forall>s \<in> sets M. space M - s \<in> sets M) &
+ (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> 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 \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+ for sp :: "'a set" and A :: "'a set set"
+ where
+ Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
+ | Empty: "{} \<in> sigma_sets sp A"
+ | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
+ | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> 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 \<in> sigma_sets sp A"
+ by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
+
+lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
+ by (erule sigma_sets.induct, auto)
+
+lemma sigma_sets_Un:
+ "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> 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 \<subseteq> Pow sp"
+ shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
+proof -
+ assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
+ hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A"
+ by (rule sigma_sets.Compl)
+ hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
+ by (rule sigma_sets.Union)
+ hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
+ by (rule sigma_sets.Compl)
+ also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)"
+ by auto
+ also have "... = (\<Inter>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 \<subseteq> Pow sp"
+ and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
+ shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
+proof -
+ from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
+ by (simp add: sigma_sets.intros sigma_sets_top)
+ hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
+ by (rule sigma_sets_Inter [OF Asb])
+ also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>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 \<subseteq> sets M"
+ shows "sigma_sets (space M) a \<subseteq> sets M"
+proof
+ fix x
+ assume "x \<in> sigma_sets (space M) a"
+ from this show "x \<in> 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 \<subseteq> sigma_sets (space M) (sets M)"
+ by (metis Set.subsetI sigma_sets.Basic space_closed)
+ next
+ show "sigma_sets (space M) (sets M) \<subseteq> sets M"
+ by (metis sigma_sets_subset subset_refl)
+qed
+
+lemma sigma_algebra_sigma_sets:
+ "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> 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 \<subseteq> Pow X \<Longrightarrow> 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 \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)"
+ by (simp add: sigma_def sigma_sets_subset)
+
+end
+
--- 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 \<times> insert b B \<union> insert a A \<times> B)"
by blast
+lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
+ by (auto, rule_tac p = "f x" in PairE, auto)
+
subsubsection {* Code generator setup *}
instance * :: (eq, eq) eq ..
--- 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) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
unfolding LIMSEQ_def dist_norm ..
+lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
+ by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)
+
lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
by (simp only: LIMSEQ_iff Zseq_def)
--- 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 \<Rightarrow> real"
+ assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
+ shows "summable f"
+proof -
+ have "convergent (\<lambda>n. setsum f {0..<n})"
+ proof (rule Bseq_mono_convergent)
+ show "Bseq (\<lambda>n. setsum f {0..<n})"
+ by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
+ (auto simp add: le pos)
+ next
+ show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
+ by (auto intro: setsum_mono2 pos)
+ qed
+ then obtain L where "(%n. setsum f {0..<n}) ----> L"
+ by (blast dest: convergentD)
+ thus ?thesis
+ by (force simp add: summable_def sums_def)
+qed
+
lemma series_pos_le:
fixes f :: "nat \<Rightarrow> real"
shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
@@ -361,6 +381,19 @@
shows "norm x < 1 \<Longrightarrow> summable (\<lambda>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: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
+proof -
+ have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
+ by auto
+ have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>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:
--- /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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (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. \<forall>x\<in>X. x\<le>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 \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "x \<le> Sup X"
+proof (auto simp add: Sup_real_def)
+ from reals_complete2
+ obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+ by (blast intro: x z)
+ hence "x \<le> s"
+ by (blast intro: x z)
+ also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
+ by (fast intro: Least_equality [symmetric])
+ finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
+qed
+
+lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
+ fixes z :: real
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup X \<le> z"
+proof (auto simp add: Sup_real_def)
+ from reals_complete2 x
+ obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+ by (blast intro: z)
+ hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
+ by (best intro: Least_equality)
+ also with s z have "... \<le> z"
+ by blast
+ finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> 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 \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> 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 \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> 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 \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
+ by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
+
+lemma Sup_eq:
+ fixes a :: real
+ shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a)
+ \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+by (metis SupInf.Sup_least setle_def)
+
+lemma Sup_upper_EX:
+ fixes x :: real
+ shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
+ by blast
+
+lemma Sup_insert_nonempty:
+ fixes x :: real
+ assumes x: "x \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup (insert a X) = max a (Sup X)"
+proof (cases "Sup X \<le> 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 \<le> 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) \<le> 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 \<in> X \<Longrightarrow> x \<le> 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 \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> 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 \<noteq> {}"
+ shows "Sup S = Max S"
+using fS Se
+proof-
+ let ?m = "Max S"
+ from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?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 \<le> Sup S"
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ moreover
+ have "Sup S \<le> ?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 \<noteq> {}"
+ shows "Sup S \<in> 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 \<noteq> {}"
+ shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> 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 \<noteq> {}"
+ shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> 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 \<noteq> {}"
+ shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> 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 \<noteq> {}"
+ shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
+by (metis Se Sup_finite_ge_iff fS linorder_not_less)
+
+lemma Sup_unique:
+ fixes S :: "real set"
+ shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+by (auto simp add: abs_le_interval_iff) (metis Sup_upper2)
+
+lemma Sup_bounds:
+ fixes S :: "real set"
+ assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
+ shows "a \<le> Sup S \<and> Sup S \<le> b"
+proof-
+ from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
+ hence b: "Sup S \<le> b" using u
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ from Se obtain y where y: "y \<in> S" by blast
+ from lub l have "a \<le> 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 \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
+proof-
+ have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> 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 \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf X \<le> x"
+proof -
+ have "-x \<le> 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 \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "z \<le> Inf X"
+proof -
+ have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
+ hence "z \<le> - 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 \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> 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 \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
+ by (metis Inf_lower real_le_trans)
+
+lemma Inf_real_iff:
+ fixes z :: real
+ shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> 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 \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+by (metis SupInf.Inf_greatest setge_def)
+
+lemma Inf_lower_EX:
+ fixes x :: real
+ shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
+ by blast
+
+lemma Inf_insert_nonempty:
+ fixes x :: real
+ assumes x: "x \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf (insert a X) = min a (Inf X)"
+proof (cases "a \<le> 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) \<le> 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 \<le> 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 \<in> X \<Longrightarrow> z \<le> 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 \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
+ by (metis Inf_real_iff mem_def not_leE)
+
+lemma Inf_close:
+ fixes e :: real
+ shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> 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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> 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 \<noteq> {}"
+ shows "Inf S \<in> 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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> 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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> 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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
+by (metis Inf_finite_le_iff linorder_not_less)
+
+lemma Inf_finite_lt_iff:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
+by (metis Inf_finite_ge_iff linorder_not_less)
+
+lemma Inf_unique:
+ fixes S :: "real set"
+ shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
+by (simp add: Inf_real_def) (rule Sup_abs_le, auto)
+
+lemma Inf_asclose:
+ fixes S :: "real set"
+ assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+ have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>"
+ by auto
+ also have "... \<le> 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 "\<bar>- Sup (uminus ` S) - l\<bar> \<le> 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} \<noteq> {}" by simp_all
+ from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
+ moreover
+ have "max x y \<le> 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} \<noteq> {}" by simp_all
+ from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
+ by (simp add: linorder_linear)
+ moreover
+ have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
+ by simp
+ ultimately show ?thesis by arith
+qed
+
+end