--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 02 15:36:15 2010 +0200
@@ -5027,7 +5027,7 @@
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i<DIM('a). ((a$$i \<le> x$$i \<and> x$$i \<le> b$$i) \<or> (b$$i \<le> x$$i \<and> x$$i \<le> a$$i))) \<longrightarrow> x \<in> s)"
lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
- "is_interval {a<..<b}" (is ?th2) proof -
+ "is_interval {a<..<b}" (is ?th2) proof -
have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
by(meson order_trans le_less_trans less_le_trans *)+ qed
@@ -5051,6 +5051,9 @@
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
+lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
+ unfolding euclidean_component_def by (rule continuous_at_inner)
+
lemma continuous_on_inner:
fixes s :: "'a::real_inner set"
shows "continuous_on s (inner a)"
@@ -5159,6 +5162,9 @@
by (simp add: closed_def open_halfspace_component_lt)
qed
+lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
+ by (auto intro!: continuous_open_vimage)
+
text{* This gives a simple derivation of limit component bounds. *}
lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
--- a/src/HOL/Probability/Borel.thy Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Thu Sep 02 15:36:15 2010 +0200
@@ -81,7 +81,7 @@
"(\<lambda>x. c) \<in> borel_measurable M"
by (auto intro!: measurable_const)
-lemma (in sigma_algebra) borel_measurable_indicator:
+lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
assumes A: "A \<in> sets M"
shows "indicator A \<in> borel_measurable M"
unfolding indicator_def_raw using A
@@ -658,6 +658,30 @@
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
+lemma borel_measureable_euclidean_component:
+ "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel_space"
+ unfolding borel_space_def[where 'a=real]
+proof (rule borel_space.measurable_sigma)
+ fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def .
+ from open_vimage_euclidean_component[OF this]
+ show "(\<lambda>x. x $$ i) -` S \<inter> space borel_space \<in> sets borel_space"
+ by (auto intro: borel_space_open)
+qed auto
+
+lemma (in sigma_algebra) borel_measureable_euclidean_space:
+ fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+ shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
+proof safe
+ fix i assume "f \<in> borel_measurable M"
+ then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
+ using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def]
+ by (auto intro: borel_measureable_euclidean_component)
+next
+ assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M"
+ then show "f \<in> borel_measurable M"
+ unfolding borel_measurable_iff_halfspace_le by auto
+qed
+
subsection "Borel measurable operators"
lemma (in sigma_algebra) affine_borel_measurable_vector:
--- a/src/HOL/Probability/Measure.thy Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Measure.thy Thu Sep 02 15:36:15 2010 +0200
@@ -451,6 +451,32 @@
qed
qed
+lemma (in measure_space) measure_space_vimage:
+ assumes "f \<in> measurable M M'"
+ and "sigma_algebra M'"
+ shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
+proof -
+ interpret M': sigma_algebra M' by fact
+
+ show ?thesis
+ proof
+ show "?T {} = 0" by simp
+
+ show "countably_additive M' ?T"
+ proof (unfold countably_additive_def, safe)
+ fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+ hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
+ using `f \<in> measurable M M'` by (auto simp: measurable_def)
+ moreover have "(\<Union>i. f -` A i \<inter> space M) \<in> sets M"
+ using * by blast
+ moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
+ using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+ ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
+ using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
+ qed
+ qed
+qed
+
section "@{text \<sigma>}-finite Measures"
locale sigma_finite_measure = measure_space +
--- a/src/HOL/Probability/Probability_Space.thy Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy Thu Sep 02 15:36:15 2010 +0200
@@ -1,5 +1,5 @@
theory Probability_Space
-imports Lebesgue_Integration
+imports Lebesgue_Integration Radon_Nikodym
begin
lemma (in measure_space) measure_inter_full_set:
@@ -197,35 +197,17 @@
qed
lemma distribution_prob_space:
- fixes S :: "('c, 'd) algebra_scheme"
- assumes "sigma_algebra S" "random_variable S X"
+ assumes S: "sigma_algebra S" "random_variable S X"
shows "prob_space S (distribution X)"
proof -
- interpret S: sigma_algebra S by fact
+ interpret S: measure_space S "distribution X"
+ using measure_space_vimage[OF S(2,1)] unfolding distribution_def .
show ?thesis
proof
- show "distribution X {} = 0" unfolding distribution_def by simp
have "X -` space S \<inter> space M = space M"
using `random_variable S X` by (auto simp: measurable_def)
- then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def)
-
- show "countably_additive S (distribution X)"
- proof (unfold countably_additive_def, safe)
- fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets S" "disjoint_family A"
- hence *: "\<And>i. X -` A i \<inter> space M \<in> sets M"
- using `random_variable S X` by (auto simp: measurable_def)
- moreover hence "\<And>i. \<mu> (X -` A i \<inter> space M) \<noteq> \<omega>"
- using finite_measure by auto
- moreover have "(\<Union>i. X -` A i \<inter> space M) \<in> sets M"
- using * by blast
- moreover hence "\<mu> (\<Union>i. X -` A i \<inter> space M) \<noteq> \<omega>"
- using finite_measure by auto
- moreover have **: "disjoint_family (\<lambda>i. X -` A i \<inter> space M)"
- using `disjoint_family A` by (auto simp: disjoint_family_on_def)
- ultimately show "(\<Sum>\<^isub>\<infinity> i. distribution X (A i)) = distribution X (\<Union>i. A i)"
- using measure_countably_additive[OF _ **]
- by (auto simp: distribution_def Real_real comp_def vimage_UN)
- qed
+ then show "distribution X (space S) = 1"
+ using measure_space_1 by (simp add: distribution_def)
qed
qed
@@ -463,4 +445,182 @@
by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
qed
+lemma (in prob_space) prob_space_subalgebra:
+ assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+ shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
+
+lemma (in measure_space) measure_space_subalgebra:
+ assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+ shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
+
+lemma pinfreal_0_less_mult_iff[simp]:
+ fixes x y :: pinfreal shows "0 < x * y \<longleftrightarrow> 0 < x \<and> 0 < y"
+ by (cases x, cases y) (auto simp: zero_less_mult_iff)
+
+lemma (in sigma_algebra) simple_function_subalgebra:
+ assumes "sigma_algebra.simple_function (M\<lparr>sets:=N\<rparr>) f"
+ and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets:=N\<rparr>)"
+ shows "simple_function f"
+ using assms
+ unfolding simple_function_def
+ unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)]
+ by auto
+
+lemma (in measure_space) simple_integral_subalgebra[simp]:
+ assumes "measure_space (M\<lparr>sets := N\<rparr>) \<mu>"
+ shows "measure_space.simple_integral (M\<lparr>sets := N\<rparr>) \<mu> = simple_integral"
+ unfolding simple_integral_def_raw
+ unfolding measure_space.simple_integral_def_raw[OF assms] by simp
+
+lemma (in sigma_algebra) borel_measurable_subalgebra:
+ assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
+ shows "f \<in> borel_measurable M"
+ using assms unfolding measurable_def by auto
+
+lemma (in measure_space) positive_integral_subalgebra[simp]:
+ assumes borel: "f \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
+ and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets := N\<rparr>)"
+ shows "measure_space.positive_integral (M\<lparr>sets := N\<rparr>) \<mu> f = positive_integral f"
+proof -
+ note msN = measure_space_subalgebra[OF N_subalgebra]
+ then interpret N: measure_space "M\<lparr>sets:=N\<rparr>" \<mu> .
+
+ from N.borel_measurable_implies_simple_function_sequence[OF borel]
+ obtain fs where Nsf: "\<And>i. N.simple_function (fs i)" and "fs \<up> f" by blast
+ then have sf: "\<And>i. simple_function (fs i)"
+ using simple_function_subalgebra[OF _ N_subalgebra] by blast
+
+ from positive_integral_isoton_simple[OF `fs \<up> f` sf] N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf]
+ show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
+qed
+
+section "Conditional Expectation and Probability"
+
+lemma (in prob_space) conditional_expectation_exists:
+ fixes X :: "'a \<Rightarrow> pinfreal"
+ assumes borel: "X \<in> borel_measurable M"
+ and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+ shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
+ positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)"
+proof -
+ interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
+ using prob_space_subalgebra[OF N_subalgebra] .
+
+ let "?f A" = "\<lambda>x. X x * indicator A x"
+ let "?Q A" = "positive_integral (?f A)"
+
+ from measure_space_density[OF borel]
+ have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q"
+ by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra])
+ then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q .
+
+ have "P.absolutely_continuous ?Q"
+ unfolding P.absolutely_continuous_def
+ proof (safe, simp)
+ fix A assume "A \<in> N" "\<mu> A = 0"
+ moreover then have f_borel: "?f A \<in> borel_measurable M"
+ using borel N_subalgebra by (auto intro: borel_measurable_indicator)
+ moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A"
+ by (auto simp: indicator_def)
+ moreover have "\<mu> \<dots> \<le> \<mu> A"
+ using `A \<in> N` N_subalgebra f_borel
+ by (auto intro!: measure_mono Int[of _ A] measurable_sets)
+ ultimately show "?Q A = 0"
+ by (simp add: positive_integral_0_iff)
+ qed
+ from P.Radon_Nikodym[OF Q this]
+ obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
+ "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
+ by blast
+ with N_subalgebra show ?thesis
+ by (auto intro!: bexI[OF _ Y(1)])
+qed
+
+definition (in prob_space)
+ "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
+ \<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))"
+
+abbreviation (in prob_space)
+ "conditional_probabiltiy N A \<equiv> conditional_expectation N (indicator A)"
+
+lemma (in prob_space)
+ fixes X :: "'a \<Rightarrow> pinfreal"
+ assumes borel: "X \<in> borel_measurable M"
+ and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+ shows borel_measurable_conditional_expectation:
+ "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+ and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
+ positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) =
+ positive_integral (\<lambda>x. X x * indicator C x)"
+ (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
+proof -
+ note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
+ then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+ unfolding conditional_expectation_def by (rule someI2_ex) blast
+
+ from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
+ unfolding conditional_expectation_def by (rule someI2_ex) blast
+qed
+
+lemma (in sigma_algebra) factorize_measurable_function:
+ fixes Z :: "'a \<Rightarrow> pinfreal" and Y :: "'a \<Rightarrow> 'c"
+ assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"
+ shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)
+ \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))"
+proof safe
+ interpret M': sigma_algebra M' by fact
+ have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto
+ from M'.sigma_algebra_vimage[OF this]
+ interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" .
+
+ { fix g :: "'c \<Rightarrow> pinfreal" assume "g \<in> borel_measurable M'"
+ with M'.measurable_vimage_algebra[OF Y]
+ have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+ by (rule measurable_comp)
+ moreover assume "\<forall>x\<in>space M. Z x = g (Y x)"
+ then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow>
+ g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+ by (auto intro!: measurable_cong)
+ ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+ by simp }
+
+ assume "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+ from va.borel_measurable_implies_simple_function_sequence[OF this]
+ obtain f where f: "\<And>i. va.simple_function (f i)" and "f \<up> Z" by blast
+
+ have "\<forall>i. \<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
+ proof
+ fix i
+ from f[of i] have "finite (f i`space M)" and B_ex:
+ "\<forall>z\<in>(f i)`space M. \<exists>B. B \<in> sets M' \<and> (f i) -` {z} \<inter> space M = Y -` B \<inter> space M"
+ unfolding va.simple_function_def by auto
+ from B_ex[THEN bchoice] guess B .. note B = this
+
+ let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x"
+
+ show "\<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
+ proof (intro exI[of _ ?g] conjI ballI)
+ show "M'.simple_function ?g" using B by auto
+
+ fix x assume "x \<in> space M"
+ then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::pinfreal)"
+ unfolding indicator_def using B by auto
+ then show "f i x = ?g (Y x)" using `x \<in> space M` f[of i]
+ by (subst va.simple_function_indicator_representation) auto
+ qed
+ qed
+ from choice[OF this] guess g .. note g = this
+
+ show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
+ proof (intro ballI bexI)
+ show "(SUP i. g i) \<in> borel_measurable M'"
+ using g by (auto intro: M'.borel_measurable_simple_function)
+ fix x assume "x \<in> space M"
+ have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
+ also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
+ using g `x \<in> space M` by simp
+ finally show "Z x = (SUP i. g i) (Y x)" .
+ qed
+qed
+
end
--- a/src/HOL/Probability/Product_Measure.thy Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy Thu Sep 02 15:36:15 2010 +0200
@@ -2,12 +2,11 @@
imports Lebesgue_Integration
begin
-definition dynkin
-where "dynkin M =
- ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
- space M \<in> sets M \<and> (\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M) \<and>
- (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
- (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
+definition "dynkin M \<longleftrightarrow>
+ space M \<in> sets M \<and>
+ (\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
+ (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
+ (\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
lemma dynkinI:
assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
@@ -15,7 +14,7 @@
assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
\<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
shows "dynkin M"
-using assms unfolding dynkin_def by auto
+using assms unfolding dynkin_def sorry
lemma dynkin_subset:
assumes "dynkin M"
@@ -42,16 +41,16 @@
assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
assumes "\<And> i :: nat. a i \<in> sets M"
shows "UNION UNIV a \<in> sets M"
-using assms unfolding dynkin_def by auto
+using assms unfolding dynkin_def sorry
-definition Int_stable
-where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
+definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
lemma dynkin_trivial:
shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
by (rule dynkinI) auto
lemma dynkin_lemma:
+ fixes D :: "'a algebra"
assumes stab: "Int_stable E"
and spac: "space E = space D"
and subsED: "sets E \<subseteq> sets D"
@@ -72,23 +71,9 @@
proof (rule dynkinI, safe)
fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
{ fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
- hence "A \<subseteq> space d"
- using dynkin_subset by auto }
- show "x \<in> space \<delta>E" using asm
- unfolding \<delta>E_def sets_\<delta>E_def using not_empty
- proof auto
- fix x A fix d :: "'a algebra"
- assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
- dynkin d \<and>
- space d = space E \<and>
- sets E \<subseteq> sets d) \<longrightarrow>
- A \<in> x" "x \<in> A"
- and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
- have "A \<in> sets d"
- apply (rule impE[OF spec[OF asm(1), of "sets d"]])
- using exI[of _ d] asm' by auto
- thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
- qed
+ hence "A \<subseteq> space d" using dynkin_subset by auto }
+ show "x \<in> space \<delta>E" using asm unfolding \<delta>E_def sets_\<delta>E_def using not_empty
+ by simp (metis dynkin_subset in_mono mem_def)
next
show "space \<delta>E \<in> sets \<delta>E"
unfolding \<delta>E_def sets_\<delta>E_def
@@ -103,28 +88,14 @@
unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
by blast
qed
+
def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
{ fix d assume dasm: "d \<in> sets_\<delta>E"
have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
- proof (rule dynkinI, auto)
+ proof (rule dynkinI, safe, simp_all)
fix A x assume "A \<in> Dy d" "x \<in> A"
thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
- proof auto fix x A fix da :: "'a algebra"
- assume asm: "x \<in> A"
- "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
- dynkin d \<and> space d = space E \<and>
- sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
- "\<forall>x. (\<exists>d. x = sets d \<and>
- dynkin d \<and> space d = space E \<and>
- sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
- "space da = space E" "dynkin da"
- "sets E \<subseteq> sets da"
- have "A \<in> sets da"
- apply (rule impE[OF spec[OF asm(2)], of "sets da"])
- apply (rule exI[of _ da])
- using exI[of _ da] asm(4,5,6) by auto
- thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
- qed
+ by simp (metis dynkin_subset in_mono mem_def)
next
show "space E \<in> Dy d"
unfolding Dy_def \<delta>E_def sets_\<delta>E_def
@@ -192,20 +163,7 @@
have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
hence "sets_\<delta>E \<subseteq> Dy e"
- unfolding sets_\<delta>E_def
- proof auto fix x
- assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
- dynkin d \<and>
- space d = space E \<and>
- sets E \<subseteq> sets d) \<longrightarrow>
- x \<in> xa"
- "dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
- "sets E \<subseteq> Dy e"
- show "x \<in> Dy e"
- apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
- apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
- using asm by auto
- qed
+ unfolding sets_\<delta>E_def by auto (metis E_Dy simps(1) simps(2) spac)
hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
hence "d \<inter> e \<in> sets \<delta>E"
using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
@@ -214,18 +172,8 @@
by (auto simp add:Int_commute) }
hence "sets E \<subseteq> Dy d" by auto
hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
- unfolding \<delta>E_def sets_\<delta>E_def
- proof auto
- fix x
- assume asm: "sets E \<subseteq> Dy d"
- "dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
- "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
- space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
- show "x \<in> Dy d"
- apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
- apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
- using asm by auto
- qed
+ unfolding \<delta>E_def sets_\<delta>E_def
+ by auto (metis `sets E <= Dy d` simps(1) simps(2) spac)
hence *: "sets \<delta>E = Dy d"
unfolding Dy_def \<delta>E_def by auto
fix a assume aasm: "a \<in> sets \<delta>E"
@@ -394,19 +342,72 @@
have "\<mu> (A i \<inter> B) = \<nu> (A i \<inter> B)"
apply (rule measure_eq[of \<mu> ?M \<nu> "\<lparr> space = space E \<inter> A i, sets = op \<inter> (A i) ` sets E\<rparr>" "A i \<inter> B", simplified])
using assms nu_i mu_i
- apply (auto simp add:image_def) (* TODO *)
+ apply (auto simp add:image_def) (* TODO *) sorry
+ show ?thesis sorry
qed
-lemma
-(*
definition prod_sets where
"prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
definition
- "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
+ "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
+
+lemma
+ fixes M1 :: "'a algebra" and M2 :: "'b algebra"
+ assumes "algebra M1" "algebra M2"
+ shows measureable_fst[intro!, simp]:
+ "fst \<in> measurable (prod_measure_space M1 M2) M1" (is ?fst)
+ and measureable_snd[intro!, simp]:
+ "snd \<in> measurable (prod_measure_space M1 M2) M2" (is ?snd)
+proof -
+ interpret M1: algebra M1 by fact
+ interpret M2: algebra M2 by fact
+
+ { fix X assume "X \<in> sets M1"
+ then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. fst -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
+ apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])
+ using M1.sets_into_space by force+ }
+ moreover
+ { fix X assume "X \<in> sets M2"
+ then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. snd -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
+ apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])
+ using M2.sets_into_space by force+ }
+ ultimately show ?fst ?snd
+ by (force intro!: sigma_sets.Basic
+ simp: measurable_def prod_measure_space_def prod_sets_def sets_sigma)+
+qed
+
+lemma (in sigma_algebra) measureable_prod:
+ fixes M1 :: "'a algebra" and M2 :: "'b algebra"
+ assumes "algebra M1" "algebra M2"
+ shows "f \<in> measurable M (prod_measure_space M1 M2) \<longleftrightarrow>
+ (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
+using assms proof (safe intro!: measurable_comp[where b="prod_measure_space M1 M2"])
+ interpret M1: algebra M1 by fact
+ interpret M2: algebra M2 by fact
+ assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
+
+ show "f \<in> measurable M (prod_measure_space M1 M2)" unfolding prod_measure_space_def
+ proof (rule measurable_sigma)
+ show "prod_sets (sets M1) (sets M2) \<subseteq> Pow (space M1 \<times> space M2)"
+ unfolding prod_sets_def using M1.sets_into_space M2.sets_into_space by auto
+ show "f \<in> space M \<rightarrow> space M1 \<times> space M2"
+ using f s by (auto simp: mem_Times_iff measurable_def comp_def)
+ fix A assume "A \<in> prod_sets (sets M1) (sets M2)"
+ then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C"
+ unfolding prod_sets_def by auto
+ moreover have "(fst \<circ> f) -` B \<inter> space M \<in> sets M"
+ using f `B \<in> sets M1` unfolding measurable_def by auto
+ moreover have "(snd \<circ> f) -` C \<inter> space M \<in> sets M"
+ using s `C \<in> sets M2` unfolding measurable_def by auto
+ moreover have "f -` A \<inter> space M = ((fst \<circ> f) -` B \<inter> space M) \<inter> ((snd \<circ> f) -` C \<inter> space M)"
+ unfolding `A = B \<times> C` by (auto simp: vimage_Times)
+ ultimately show "f -` A \<inter> space M \<in> sets M" by auto
+ qed
+qed
definition
- "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
+ "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
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)
@@ -550,5 +551,4 @@
unfolding finite_prod_measure_space[OF N, symmetric]
using finite_measure_space_finite_prod_measure[OF N] .
-*)
-end
\ No newline at end of file
+end
--- a/src/HOL/Probability/Sigma_Algebra.thy Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu Sep 02 15:36:15 2010 +0200
@@ -626,6 +626,51 @@
thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
qed
+subsection {* Sigma algebra generated by function preimages *}
+
+definition (in sigma_algebra)
+ "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M \<rparr>"
+
+lemma (in sigma_algebra) in_vimage_algebra[simp]:
+ "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
+ by (simp add: vimage_algebra_def image_iff)
+
+lemma (in sigma_algebra) space_vimage_algebra[simp]:
+ "space (vimage_algebra S f) = S"
+ by (simp add: vimage_algebra_def)
+
+lemma (in sigma_algebra) sigma_algebra_vimage:
+ fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
+ shows "sigma_algebra (vimage_algebra S f)"
+proof
+ fix A assume "A \<in> sets (vimage_algebra S f)"
+ then guess B unfolding in_vimage_algebra ..
+ then show "space (vimage_algebra S f) - A \<in> sets (vimage_algebra S f)"
+ using sets_into_space assms
+ by (auto intro!: bexI[of _ "space M - B"])
+next
+ fix A assume "A \<in> sets (vimage_algebra S f)"
+ then guess A' unfolding in_vimage_algebra .. note A' = this
+ fix B assume "B \<in> sets (vimage_algebra S f)"
+ then guess B' unfolding in_vimage_algebra .. note B' = this
+ then show "A \<union> B \<in> sets (vimage_algebra S f)"
+ using sets_into_space assms A' B'
+ by (auto intro!: bexI[of _ "A' \<union> B'"])
+next
+ fix A::"nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets (vimage_algebra S f)"
+ then have "\<forall>i. \<exists>B. A i = f -` B \<inter> S \<and> B \<in> sets M"
+ by (simp add: subset_eq) blast
+ from this[THEN choice] obtain B
+ where B: "\<And>i. A i = f -` B i \<inter> S" "range B \<subseteq> sets M" by auto
+ show "(\<Union>i. A i) \<in> sets (vimage_algebra S f)"
+ using B by (auto intro!: bexI[of _ "\<Union>i. B i"])
+qed auto
+
+lemma (in sigma_algebra) measurable_vimage_algebra:
+ fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
+ shows "f \<in> measurable (vimage_algebra S f) M"
+ unfolding measurable_def using assms by force
+
subsection {* A Two-Element Series *}
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "