--- a/src/HOL/Probability/Borel.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Borel.thy Mon Nov 09 19:42:33 2009 +0100
@@ -17,8 +17,8 @@
definition mono_convergent where
"mono_convergent u f s \<equiv>
- (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
- (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+ (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+ (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
lemma in_borel_measurable:
"f \<in> borel_measurable M \<longleftrightarrow>
@@ -222,7 +222,7 @@
shows "{w \<in> space M. f w < g w} \<in> sets M"
proof -
have "{w \<in> space M. f w < g w} =
- (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
+ (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
by (auto simp add: Rats_dense_in_real)
thus ?thesis using f g
by (simp add: borel_measurable_less_iff [of f]
@@ -247,7 +247,7 @@
shows "{w \<in> space M. f w = g w} \<in> sets M"
proof -
have "{w \<in> space M. f w = g w} =
- {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
+ {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
by auto
thus ?thesis using f g
by (simp add: borel_measurable_leq_borel_measurable Int)
--- a/src/HOL/Probability/Caratheodory.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Caratheodory.thy Mon Nov 09 19:42:33 2009 +0100
@@ -2,7 +2,6 @@
theory Caratheodory
imports Sigma_Algebra SupInf SeriesPlus
-
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -136,7 +135,7 @@
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)
+ by (induct n) (auto simp add: binaryset_def f)
qed
moreover
have "... ----> f A + f B" by (rule LIMSEQ_const)
@@ -198,30 +197,30 @@
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"
+ 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)
+ 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" .
+ 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
@@ -478,11 +477,11 @@
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])
+ 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])
+ 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
+ lambda_system_positive lambda_system_additive
subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in)
qed
{
@@ -491,58 +490,58 @@
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
+ 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
+ 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
+ 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
+ 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))" .
+ 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
}
@@ -654,20 +653,20 @@
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
+ by blast
show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
- by (auto simp add: disjoint_family_def)
+ 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)
+ 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])
+ by (force intro: increasingD [OF inc])
show "summable (\<lambda>i. f (A i \<inter> s))" using sums
- by (simp add: sums_iff)
+ by (simp add: sums_iff)
qed
also have "... = z" by (rule si)
finally show "f s \<le> z" .
@@ -722,9 +721,9 @@
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)
+ 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)
+ 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]
@@ -787,32 +786,32 @@
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
+ 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))) +
+ 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))) +
+ 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
+ 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"
@@ -822,24 +821,24 @@
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
+ 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
+ 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"
@@ -882,24 +881,24 @@
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
+ 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)
+ 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)
+ 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)
+ 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]
+ 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)"
+ 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)"
+ 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)
@@ -920,14 +919,14 @@
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)+
+ 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)
+ 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)
+ by (simp add: x) (simp add: o_def)
also have "... \<le> Inf (measure_set M f s) + e"
- by (metis fsums l sums_unique)
+ 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
@@ -940,7 +939,7 @@
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)
+ inf_measure_positive inf_measure_countably_subadditive posf inc)
apply (auto simp add: subsetD [OF s])
done
finally show ?thesis .
--- a/src/HOL/Probability/Measure.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Measure.thy Mon Nov 09 19:42:33 2009 +0100
@@ -46,8 +46,8 @@
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)}"
+ f \<in> (space a -> space b) &
+ (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
definition
measure_preserving where
@@ -258,23 +258,23 @@
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
+ 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
@@ -292,12 +292,12 @@
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)
+ 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)
+ 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)
+ IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
qed
thus ?thesis
by blast
@@ -349,7 +349,7 @@
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)
+ 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"
@@ -371,17 +371,17 @@
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)
+ 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)) =
+ 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)
+ by (subst measure_additive)
(auto simp add: measure_additive range_subsetD [OF A])
- with Suc show ?case
- by simp
+ 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})"
@@ -390,13 +390,13 @@
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
+ 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)
@@ -461,23 +461,23 @@
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
+ 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.
@@ -496,26 +496,26 @@
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)
+ proof induct
+ case (Basic a)
+ thus ?case
+ by (auto simp add: ba) (metis B subsetD PowD)
next
- case Empty
- thus ?case
- by auto
+ 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
+ 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)
@@ -553,122 +553,122 @@
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"
+ 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])
+ by (rule subsetD [OF measurable_subset fm])
also have "... = measurable m1 m2"
- by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def)
+ 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)
+ by (simp add: measurable_def)
have "space m1 \<subseteq> f -` (space m2)"
- by auto (metis PiE ffn)
+ by auto (metis PiE ffn)
hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
- by blast
+ 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) =
+ 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) =
+ 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)
+ 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) =
+ 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
+ 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)
+ 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)
+ by (blast intro: f12)
qed
qed
--- a/src/HOL/Probability/Probability.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Probability.thy Mon Nov 09 19:42:33 2009 +0100
@@ -1,5 +1,5 @@
-theory Probability imports
- Measure
+theory Probability
+imports Measure
begin
end
--- a/src/HOL/Probability/ROOT.ML Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/ROOT.ML Mon Nov 09 19:42:33 2009 +0100
@@ -1,6 +1,1 @@
-(*
- no_document use_thy "ThisTheory";
- use_thy "ThatTheory";
-*)
-
use_thy "Probability";
--- a/src/HOL/Probability/SeriesPlus.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/SeriesPlus.thy Mon Nov 09 19:42:33 2009 +0100
@@ -1,6 +1,5 @@
theory SeriesPlus
imports Complex_Main Nat_Int_Bij
-
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -28,9 +27,9 @@
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)
+ 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)
+ 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)
@@ -48,14 +47,14 @@
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)
+ 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)
+ 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"
@@ -73,13 +72,13 @@
{ fix m
assume m: "m<N"
hence enneg: "0 < e / (2 * real N)" using e
- by (simp add: zero_less_divide_iff)
+ 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
+ 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)
+ 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)"
@@ -103,13 +102,13 @@
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]
+ 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})"
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 09 19:42:33 2009 +0100
@@ -235,4 +235,3 @@
by (simp add: sigma_def sigma_sets_subset)
end
-
--- a/src/HOL/Series.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Series.thy Mon Nov 09 19:42:33 2009 +0100
@@ -293,11 +293,11 @@
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"])
+ 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)
+ by (auto intro: setsum_mono2 pos)
qed
then obtain L where "(%n. setsum f {0..<n}) ----> L"
by (blast dest: convergentD)