--- a/NEWS Tue Oct 27 14:46:03 2009 +0000
+++ b/NEWS Wed Oct 28 11:42:31 2009 +0000
@@ -67,6 +67,8 @@
* 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/IsaMakefile Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/IsaMakefile Wed Oct 28 11:42:31 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 \
@@ -1060,6 +1061,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 Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Library/FuncSet.thy Wed Oct 28 11:42:31 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}*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Caratheodory.thy Wed Oct 28 11:42:31 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:42:31 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:42:31 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:42:31 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:42:31 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:42:31 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 Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Product_Type.thy Wed Oct 28 11:42:31 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 Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/SEQ.thy Wed Oct 28 11:42:31 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 Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Series.thy Wed Oct 28 11:42:31 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:
--- a/src/HOL/SupInf.thy Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/SupInf.thy Wed Oct 28 11:42:31 2009 +0000
@@ -361,11 +361,6 @@
shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
by auto (metis Inf_insert_nonempty z)
-text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
-lemma Inf_binary:
- "Inf{a, b::real} = min a b"
- by (subst Inf_insert_nonempty, auto)
-
lemma Inf_greater:
fixes z :: real
shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
@@ -437,7 +432,7 @@
by (simp add: Inf_real_def)
qed
-subsection{*Relate max and min to sup and inf.*}
+subsection{*Relate max and min to Sup and Inf.*}
lemma real_max_Sup:
fixes x :: real