Theory Generated_Subalgebra
section ‹Generated subalgebras›
text ‹This section contains definitions and properties related to generated subalgebras.›
theory Generated_Subalgebra imports "HOL-Probability.Probability"
begin
definition gen_subalgebra where
"gen_subalgebra M G = sigma (space M) G"
lemma gen_subalgebra_space:
shows "space (gen_subalgebra M G) = space M"
by (simp add: gen_subalgebra_def space_measure_of_conv)
lemma gen_subalgebra_sets:
assumes "G ⊆ sets M"
and "A ∈ G"
shows "A ∈ sets (gen_subalgebra M G)"
by (metis assms gen_subalgebra_def sets.space_closed sets_measure_of sigma_sets.Basic subset_trans)
lemma gen_subalgebra_sig_sets:
assumes "G ⊆ Pow (space M)"
shows "sets (gen_subalgebra M G) = sigma_sets (space M) G" unfolding gen_subalgebra_def
by (metis assms gen_subalgebra_def sets_measure_of)
lemma gen_subalgebra_sigma_sets:
assumes "G ⊆ sets M"
and "sigma_algebra (space M) G"
shows "sets (gen_subalgebra M G) = G"
using assms by (simp add: gen_subalgebra_def sigma_algebra.sets_measure_of_eq)
lemma gen_subalgebra_is_subalgebra:
assumes sub: "G ⊆ sets M"
and sigal:"sigma_algebra (space M) G"
shows "subalgebra M (gen_subalgebra M G)" (is "subalgebra M ?N")
unfolding subalgebra_def
proof (intro conjI)
show "space ?N = space M" using space_measure_of_conv[of "(space M)"] unfolding gen_subalgebra_def by simp
have geqn: "G = sets ?N" using assms by (simp add:gen_subalgebra_sigma_sets)
thus "sets ?N ⊆ sets M" using assms by simp
qed
definition fct_gen_subalgebra :: "'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) ⇒ 'a measure" where
"fct_gen_subalgebra M N X = gen_subalgebra M (sigma_sets (space M) {X -` B ∩ (space M) | B. B ∈ sets N})"
lemma fct_gen_subalgebra_sets:
shows "sets (fct_gen_subalgebra M N X) = sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N}"
unfolding fct_gen_subalgebra_def gen_subalgebra_def
proof -
have "{X -` B ∩ space M |B. B ∈ sets N} ⊆ Pow (space M)"
by blast
then show "sets (sigma (space M) (sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N})) = sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N}"
by (meson sigma_algebra.sets_measure_of_eq sigma_algebra_sigma_sets)
qed
lemma fct_gen_subalgebra_space:
shows "space (fct_gen_subalgebra M N X) = space M"
unfolding fct_gen_subalgebra_def by (simp add: gen_subalgebra_space)
lemma fct_gen_subalgebra_eq_sets:
assumes "sets M = sets P"
shows "fct_gen_subalgebra M N X = fct_gen_subalgebra P N X"
proof -
have "space M = space P" using sets_eq_imp_space_eq assms by auto
thus ?thesis unfolding fct_gen_subalgebra_def gen_subalgebra_def by simp
qed
lemma fct_gen_subalgebra_sets_mem:
assumes "B∈ sets N"
shows "X -` B ∩ (space M) ∈ sets (fct_gen_subalgebra M N X)" unfolding fct_gen_subalgebra_def
proof -
have f1: "{X -` A ∩ space M |A. A ∈ sets N} ⊆ Pow (space M)"
by blast
have "∃A. X -` B ∩ space M = X -` A ∩ space M ∧ A ∈ sets N"
by (metis assms)
then show "X -` B ∩ space M ∈ sets (gen_subalgebra M (sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets N}))"
using f1 by (simp add: gen_subalgebra_def sigma_algebra.sets_measure_of_eq sigma_algebra_sigma_sets)
qed
lemma fct_gen_subalgebra_is_subalgebra:
assumes "X∈ measurable M N"
shows "subalgebra M (fct_gen_subalgebra M N X)"
unfolding fct_gen_subalgebra_def
proof (rule gen_subalgebra_is_subalgebra)
show "sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N} ⊆ sets M" (is "?L ⊆ ?R")
proof (rule sigma_algebra.sigma_sets_subset)
show "{X -` B ∩ space M |B. B ∈ sets N} ⊆ sets M"
proof
fix a
assume "a ∈ {X -` B ∩ (space M) | B. B ∈ sets N}"
then obtain B where "B ∈ sets N" and "a = X -` B ∩ (space M)" by auto
thus "a ∈ sets M" using measurable_sets assms by simp
qed
show "sigma_algebra (space M) (sets M)" using measure_space by (auto simp add: measure_space_def)
qed
show "sigma_algebra (space M) ?L"
proof (rule sigma_algebra_sigma_sets)
let ?preimages = "{X -` B ∩ (space M) | B. B ∈ sets N}"
show "?preimages ≤ Pow (space M)" using assms by auto
qed
qed
lemma fct_gen_subalgebra_fct_measurable:
assumes "X ∈ space M → space N"
shows "X∈ measurable (fct_gen_subalgebra M N X) N"
unfolding measurable_def
proof ((intro CollectI), (intro conjI))
have speq: "space M = space (fct_gen_subalgebra M N X)"
by (simp add: fct_gen_subalgebra_space)
show "X ∈ space (fct_gen_subalgebra M N X) → space N"
proof -
have "X ∈ space M → space N" using assms by simp
thus ?thesis using speq by simp
qed
show "∀y∈sets N.
X -` y ∩ space (fct_gen_subalgebra M N X) ∈ sets (fct_gen_subalgebra M N X)"
using fct_gen_subalgebra_sets_mem speq by metis
qed
lemma fct_gen_subalgebra_min:
assumes "subalgebra M P"
and "f∈ measurable P N"
shows "subalgebra P (fct_gen_subalgebra M N f)"
unfolding subalgebra_def
proof (intro conjI)
let ?Mf = "fct_gen_subalgebra M N f"
show "space ?Mf = space P" using assms
by (simp add: fct_gen_subalgebra_def gen_subalgebra_space subalgebra_def)
show inc: "sets ?Mf ⊆ sets P"
proof -
have "space M = space P" using assms by (simp add:subalgebra_def)
have "f∈ measurable M N" using assms using measurable_from_subalg by blast
have "sigma_algebra (space P) (sets P)" using assms measure_space measure_space_def by auto
have "∀ A ∈ sets N. f-`A ∩ space P ∈ sets P" using assms by simp
hence "{f -` A ∩ (space M) | A. A ∈ sets N} ⊆ sets P" using ‹space M = space P› by auto
hence "sigma_sets (space M) {f -` A ∩ (space M) | A. A ∈ sets N} ⊆ sets P"
by (simp add: ‹sigma_algebra (space P) (sets P)› ‹space M = space P› sigma_algebra.sigma_sets_subset)
thus ?thesis using fct_gen_subalgebra_sets ‹f ∈ M →⇩M N› ‹space M = space P› assms(2)
measurable_sets mem_Collect_eq sets.sigma_sets_subset subsetI by blast
qed
qed
lemma fct_preimage_sigma_sets:
assumes "X∈ space M → space N"
shows "sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N} = {X -` B ∩ space M |B. B ∈ sets N}" (is "?L = ?R")
proof
show "?R⊆ ?L" by blast
show "?L⊆ ?R"
proof
fix A
assume "A∈ ?L"
thus "A∈ ?R"
proof (induct rule:sigma_sets.induct, auto)
{
fix B
assume "B∈ sets N"
let ?cB = "space N - B"
have "?cB ∈ sets N" by (simp add: ‹B ∈ sets N› sets.compl_sets)
have "space M - X -` B ∩ space M = X -` ?cB ∩ space M"
proof
show "space M - X -` B ∩ space M ⊆ X -` (space N - B) ∩ space M"
proof
fix w
assume "w ∈ space M - X -` B ∩ space M"
hence "X w ∈ (space N - B)" using assms by blast
thus "w∈ X -` (space N - B) ∩ space M" using ‹w ∈ space M - X -` B ∩ space M› by blast
qed
show "X -` (space N - B) ∩ space M ⊆ space M - X -` B ∩ space M"
proof
fix w
assume "w∈ X -` (space N - B) ∩ space M"
thus "w ∈ space M - X -` B ∩ space M" by blast
qed
qed
thus "∃Ba. space M - X -` B ∩ space M = X -` Ba ∩ space M ∧ Ba ∈ sets N" using ‹?cB ∈ sets N› by auto
}
{
fix S::"nat ⇒ 'a set"
assume "(⋀i. ∃B. S i = X -` B ∩ space M ∧ B ∈ sets N)"
hence "(∀i. ∃B. S i = X -` B ∩ space M ∧ B ∈ sets N)" by auto
hence "∃ f. ∀ x. S x = X -`(f x) ∩ space M ∧ (f x) ∈ sets N"
using choice[of "λi B . S i = X -` B ∩ space M ∧ B ∈ sets N"] by simp
from this obtain rep where "∀i. S i = X -` (rep i) ∩ space M ∧ (rep i) ∈ sets N" by auto note rProp = this
let ?uB = "⋃i∈ UNIV. rep i"
have "?uB ∈ sets N"
by (simp add: ‹∀i. S i = X -` rep i ∩ space M ∧ rep i ∈ sets N› countable_Un_Int(1))
have "(⋃x. S x) = X -` ?uB ∩ space M"
proof
show "(⋃x. S x) ⊆ X -` (⋃i. rep i) ∩ space M"
proof
fix w
assume "w∈ (⋃x. S x)"
hence "∃x. w ∈ S x" by auto
from this obtain x where "w ∈ S x" by auto
hence "w∈ X -` rep x ∩ space M" using rProp by simp
hence "w∈ (⋃i. (X -`(rep i)∩ space M))" by blast
also have "... = X -` (⋃i. rep i) ∩ space M" by auto
finally show "w ∈ X -` (⋃i. rep i) ∩ space M" .
qed
show "X -` (⋃i. rep i) ∩ space M ⊆ (⋃x. S x)"
proof
fix w
assume "w∈ X -` (⋃i. rep i) ∩ space M"
hence "∃ x. w∈ X -` (rep x) ∩ space M" by auto
from this obtain x where "w∈ X -` (rep x) ∩ space M" by auto
hence "w∈ S x" using rProp by simp
thus "w∈ (⋃x. S x)" by blast
qed
qed
thus "∃B. (⋃x. S x) = X -` B ∩ space M ∧ B ∈ sets N" using ‹?uB ∈ sets N› by auto
}
qed
qed
qed
lemma fct_gen_subalgebra_sigma_sets:
assumes "X∈ space M → space N"
shows "sets (fct_gen_subalgebra M N X) = {X -` B ∩ space M |B. B ∈ sets N}"
by (simp add: assms fct_gen_subalgebra_sets fct_preimage_sigma_sets)
lemma fct_gen_subalgebra_info:
assumes "f∈ space M → space N"
and "x∈ space M"
and "w∈ space M"
and "f x = f w"
shows "⋀A. A∈ sets (fct_gen_subalgebra M N f) ⟹ (x∈ A) = (w∈ A)"
proof -
{fix A
assume "A ∈ sigma_sets (space M) {f -` B ∩ (space M) | B. B ∈ sets N}"
from this have "(x∈ A) = (w∈ A)"
proof (induct rule:sigma_sets.induct)
{
fix a
assume "a ∈ {f -` B ∩ space M |B. B ∈ sets N}"
hence "∃ B∈ sets N. a = f -` B ∩ space M" by auto
from this obtain B where "B∈ sets N" and "a = f -` B ∩ space M" by blast note bhyps = this
show "(x∈ a) = (w∈ a)" by (simp add: assms(2) assms(3) assms(4) bhyps(2))
}
{
fix a
assume "a ∈ sigma_sets (space M) {f -` B ∩ space M |B. B ∈ sets N}"
and "(x ∈ a) = (w ∈ a)" note xh = this
show "(x ∈ space M - a) = (w ∈ space M - a)" by (simp add: assms(2) assms(3) xh(2))
}
{
fix a::"nat ⇒ 'a set"
assume "(⋀i. a i ∈ sigma_sets (space M) {f -` B ∩ space M |B. B ∈ sets N})"
and "(⋀i. (x ∈ a i) = (w ∈ a i))"
show "(x ∈ ⋃(a ` UNIV)) = (w ∈ ⋃(a ` UNIV))" by (simp add: ‹⋀i. (x ∈ a i) = (w ∈ a i)›)
}
{show "(x∈ {}) = (w∈ {})" by simp}
qed} note eqsig = this
fix A
assume "A∈ sets (fct_gen_subalgebra M N f)"
hence "A ∈ sigma_sets (space M) {f -` B ∩ (space M) | B. B ∈ sets N}"
using assms(1) fct_gen_subalgebra_sets by blast
thus "(x∈ A) = (w∈ A)" using eqsig by simp
qed
subsection ‹Independence between a random variable and a subalgebra.›
definition (in prob_space) subalgebra_indep_var :: "('a ⇒ real) ⇒ 'a measure ⇒ bool" where
"subalgebra_indep_var X N ⟷
X∈ borel_measurable M &
(subalgebra M N) &
(indep_set (sigma_sets (space M) { X -` A ∩ space M | A. A ∈ sets borel}) (sets N))"
lemma (in prob_space) indep_set_mono:
assumes "indep_set A B"
assumes "A' ⊆ A"
assumes "B' ⊆ B"
shows "indep_set A' B'"
by (meson indep_sets2_eq assms subsetCE subset_trans)
lemma (in prob_space) subalgebra_indep_var_indicator:
fixes X::"'a⇒real"
assumes "subalgebra_indep_var X N"
and "X ∈ borel_measurable M"
and "A ∈ sets N"
shows "indep_var borel X borel (indicator A)"
proof ((rule indep_var_eq[THEN iffD2]), (intro conjI))
let ?IA = "(indicator A)::'a⇒ real"
show bm:"random_variable borel X" by (simp add: assms(2))
show "random_variable borel ?IA" using assms indep_setD_ev2 unfolding subalgebra_indep_var_def by auto
show "indep_set (sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel})
(sigma_sets (space M) {?IA -` Aa ∩ space M |Aa. Aa ∈ sets borel})"
proof (rule indep_set_mono)
show "sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel} ⊆ sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel}" by simp
show "sigma_sets (space M) {?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sets N"
proof -
have "sigma_algebra (space M) (sets N)" using assms
by (metis subalgebra_indep_var_def sets.sigma_algebra_axioms subalgebra_def)
have "sigma_sets (space M) {?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sigma_sets (space M) (sets N)"
proof (rule sigma_sets_subseteq)
show "{?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sets N"
proof
fix x
assume "x ∈ {?IA -` B ∩ space M |B. B ∈ sets borel}"
then obtain B where "B ∈ sets borel" and "x = ?IA -` B ∩ space M" by auto
thus "x ∈ sets N"
by (metis (no_types, lifting) assms(1) assms(3) borel_measurable_indicator measurable_sets subalgebra_indep_var_def subalgebra_def)
qed
qed
also have "... = sets N"
by (simp add: ‹sigma_algebra (space M) (sets N)› sigma_algebra.sigma_sets_eq)
finally show "sigma_sets (space M) {?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sets N" .
qed
show "indep_set (sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel}) (sets N) "
using assms unfolding subalgebra_indep_var_def by simp
qed
qed
lemma fct_gen_subalgebra_cong:
assumes "space M = space P"
and "sets N = sets Q"
shows "fct_gen_subalgebra M N X = fct_gen_subalgebra P Q X"
proof -
have "space M = space P" using assms by simp
thus ?thesis using assms unfolding fct_gen_subalgebra_def gen_subalgebra_def by simp
qed
end