(* Title: HOL/Probability/Projective_Family.thy
Author: Fabian Immler, TU München
Author: Johannes Hölzl, TU München
*)
section \<open>Projective Family\<close>
theory Projective_Family
imports Giry_Monad
begin
lemma vimage_restrict_preseve_mono:
assumes J: "J \ I"
and sets: "A \ (\\<^sub>E i\J. S i)" "B \ (\\<^sub>E i\J. S i)" and ne: "(\\<^sub>E i\I. S i) \ {}"
and eq: "(\x. restrict x J) -` A \ (\\<^sub>E i\I. S i) \ (\x. restrict x J) -` B \ (\\<^sub>E i\I. S i)"
shows "A \ B"
proof (intro subsetI)
fix x assume "x \ A"
from ne obtain y where y: "\i. i \ I \ y i \ S i" by auto
have "J \ (I - J) = {}" by auto
show "x \ B"
proof cases
assume x: "x \ (\\<^sub>E i\J. S i)"
have "merge J (I - J) (x,y) \ (\x. restrict x J) -` A \ (\\<^sub>E i\I. S i)"
using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close>
by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
also have "\ \ (\x. restrict x J) -` B \ (\\<^sub>E i\I. S i)" by fact
finally show "x \ B"
using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> eq
by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
qed (insert \<open>x\<in>A\<close> sets, auto)
qed
locale projective_family =
fixes I :: "'i set" and P :: "'i set \ ('i \ 'a) measure" and M :: "'i \ 'a measure"
assumes P: "\J H. J \ H \ finite H \ H \ I \ P J = distr (P H) (PiM J M) (\f. restrict f J)"
assumes prob_space_P: "\J. finite J \ J \ I \ prob_space (P J)"
begin
lemma sets_P: "finite J \ J \ I \ sets (P J) = sets (PiM J M)"
by (subst P[of J J]) simp_all
lemma space_P: "finite J \ J \ I \ space (P J) = space (PiM J M)"
using sets_P by (rule sets_eq_imp_space_eq)
lemma not_empty_M: "i \ I \ space (M i) \ {}"
using prob_space_P[THEN prob_space.not_empty] by (auto simp: space_PiM space_P)
lemma not_empty: "space (PiM I M) \ {}"
by (simp add: not_empty_M)
abbreviation
"emb L K \ prod_emb L M K"
lemma emb_preserve_mono:
assumes "J \ L" "L \ I" and sets: "X \ sets (Pi\<^sub>M J M)" "Y \ sets (Pi\<^sub>M J M)"
assumes "emb L J X \ emb L J Y"
shows "X \ Y"
proof (rule vimage_restrict_preseve_mono)
show "X \ (\\<^sub>E i\J. space (M i))" "Y \ (\\<^sub>E i\J. space (M i))"
using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
show "(\\<^sub>E i\L. space (M i)) \ {}"
using \<open>L \<subseteq> I\<close> by (auto simp add: not_empty_M space_PiM[symmetric])
show "(\x. restrict x J) -` X \ (\\<^sub>E i\L. space (M i)) \ (\x. restrict x J) -` Y \ (\\<^sub>E i\L. space (M i))"
using \<open>prod_emb L M J X \<subseteq> prod_emb L M J Y\<close> by (simp add: prod_emb_def)
qed fact
lemma emb_injective:
assumes L: "J \ L" "L \ I" and X: "X \ sets (Pi\<^sub>M J M)" and Y: "Y \ sets (Pi\<^sub>M J M)"
shows "emb L J X = emb L J Y \ X = Y"
by (intro antisym emb_preserve_mono[OF L X Y] emb_preserve_mono[OF L Y X]) auto
lemma emeasure_P: "J \ K \ finite K \ K \ I \ X \ sets (PiM J M) \ P K (emb K J X) = P J X"
by (auto intro!: emeasure_distr_restrict[symmetric] simp: P sets_P)
inductive_set generator :: "('i \ 'a) set set" where
"finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ emb I J X \ generator"
lemma algebra_generator: "algebra (space (PiM I M)) generator"
unfolding algebra_iff_Int
proof (safe elim!: generator.cases)
fix J X assume J: "finite J" "J \ I" and X: "X \ sets (PiM J M)"
from X[THEN sets.sets_into_space] J show "x \ emb I J X \ x \ space (PiM I M)" for x
by (auto simp: prod_emb_def space_PiM)
have "emb I J (space (PiM J M) - X) \ generator"
by (intro generator.intros J sets.Diff sets.top X)
with J show "space (Pi\<^sub>M I M) - emb I J X \ generator"
by (simp add: space_PiM prod_emb_PiE)
fix K Y assume K: "finite K" "K \ I" and Y: "Y \ sets (PiM K M)"
have "emb I (J \ K) (emb (J \ K) J X) \ emb I (J \ K) (emb (J \ K) K Y) \ generator"
unfolding prod_emb_Int[symmetric]
by (intro generator.intros sets.Int measurable_prod_emb) (auto intro!: J K X Y)
with J K X Y show "emb I J X \ emb I K Y \ generator"
by simp
qed (force simp: generator.simps prod_emb_empty[symmetric])
interpretation generator: algebra "space (PiM I M)" generator
by (rule algebra_generator)
lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
proof (intro antisym sets.sigma_sets_subset)
show "sets (PiM I M) \ sigma_sets (space (PiM I M)) generator"
unfolding sets_PiM_single space_PiM[symmetric]
proof (intro sigma_sets_mono', safe)
fix i A assume "i \ I" and A: "A \ sets (M i)"
then have "{f \ space (Pi\<^sub>M I M). f i \ A} = emb I {i} (\\<^sub>E j\{i}. A)"
by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def)
with \<open>i\<in>I\<close> A show "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} \<in> generator"
by (auto intro!: generator.intros sets_PiM_I_finite)
qed
qed (auto elim!: generator.cases)
definition mu_G ("\G") where
"\G A = (THE x. \J\I. finite J \ (\X\sets (Pi\<^sub>M J M). A = emb I J X \ x = emeasure (P J) X))"
definition lim :: "('i \ 'a) measure" where
"lim = extend_measure (space (PiM I M)) generator (\x. x) \G"
lemma space_lim[simp]: "space lim = space (PiM I M)"
using generator.space_closed
unfolding lim_def by (intro space_extend_measure) simp
lemma sets_lim[simp, measurable]: "sets lim = sets (PiM I M)"
using generator.space_closed by (simp add: lim_def sets_PiM_generator sets_extend_measure)
lemma mu_G_spec:
assumes J: "finite J" "J \ I" "X \ sets (Pi\<^sub>M J M)"
shows "\G (emb I J X) = emeasure (P J) X"
unfolding mu_G_def
proof (intro the_equality allI impI ballI)
fix K Y assume K: "finite K" "K \ I" "Y \ sets (Pi\<^sub>M K M)"
and [simp]: "emb I J X = emb I K Y"
have "emeasure (P K) Y = emeasure (P (K \ J)) (emb (K \ J) K Y)"
using K J by (simp add: emeasure_P)
also have "emb (K \ J) K Y = emb (K \ J) J X"
using K J by (simp add: emb_injective[of "K \ J" I])
also have "emeasure (P (K \ J)) (emb (K \ J) J X) = emeasure (P J) X"
using K J by (subst emeasure_P) simp_all
finally show "emeasure (P J) X = emeasure (P K) Y" ..
qed (insert J, force)
lemma positive_mu_G: "positive generator \G"
proof -
show ?thesis
proof (safe intro!: positive_def[THEN iffD2])
obtain J where "finite J" "J \ I" by auto
then have "\G (emb I J {}) = 0"
by (subst mu_G_spec) auto
then show "\G {} = 0" by simp
qed
qed
lemma additive_mu_G: "additive generator \G"
proof (safe intro!: additive_def[THEN iffD2] elim!: generator.cases)
fix J X K Y assume J: "finite J" "J \ I" "X \ sets (PiM J M)"
and K: "finite K" "K \ I" "Y \ sets (PiM K M)"
and "emb I J X \ emb I K Y = {}"
then have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}"
by (intro emb_injective[of "J \ K" I _ "{}"]) (auto simp: sets.Int prod_emb_Int)
have "\G (emb I J X \ emb I K Y) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))"
using J K by simp
also have "\ = emeasure (P (J \ K)) (emb (J \ K) J X \ emb (J \ K) K Y)"
using J K by (simp add: mu_G_spec sets.Un del: prod_emb_Un)
also have "\ = \G (emb I J X) + \G (emb I K Y)"
using J K JK_disj by (simp add: plus_emeasure[symmetric] mu_G_spec emeasure_P sets_P)
finally show "\G (emb I J X \ emb I K Y) = \G (emb I J X) + \G (emb I K Y)" .
qed
lemma emeasure_lim:
assumes JX: "finite J" "J \ I" "X \ sets (PiM J M)"
assumes cont: "\J X. (\i. J i \ I) \ incseq J \ (\i. finite (J i)) \ (\i. X i \ sets (PiM (J i) M)) \
decseq (\<lambda>i. emb I (J i) (X i)) \<Longrightarrow> 0 < (INF i. P (J i) (X i)) \<Longrightarrow> (\<Inter>i. emb I (J i) (X i)) \<noteq> {}"
shows "emeasure lim (emb I J X) = P J X"
proof -
have "\\. (\s\generator. \ s = \G s) \
measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \<mu>"
proof (rule generator.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
show "\A. A \ generator \ \G A \ \"
proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI)
fix J assume "finite J" "J \ I"
then interpret prob_space "P J" by (rule prob_space_P)
show "\X. X \ sets (Pi\<^sub>M J M) \ emeasure (P J) X \ top"
by simp
qed
next
fix A assume "range A \ generator" and "decseq A" "(\i. A i) = {}"
then have "\i. \J X. A i = emb I J X \ finite J \ J \ I \ X \ sets (PiM J M)"
unfolding image_subset_iff generator.simps by blast
then obtain J X where A: "\i. A i = emb I (J i) (X i)"
and *: "\i. finite (J i)" "\i. J i \ I" "\i. X i \ sets (PiM (J i) M)"
by metis
have "(INF i. P (J i) (X i)) = 0"
proof (rule ccontr)
assume INF_P: "(INF i. P (J i) (X i)) \ 0"
have "(\i. emb I (\n\i. J n) (emb (\n\i. J n) (J i) (X i))) \ {}"
proof (rule cont)
show "decseq (\i. emb I (\n\i. J n) (emb (\n\i. J n) (J i) (X i)))"
using * \<open>decseq A\<close> by (subst prod_emb_trans) (auto simp: A[abs_def])
show "0 < (INF i. P (\n\i. J n) (emb (\n\i. J n) (J i) (X i)))"
using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest)
show "incseq (\i. \n\i. J n)"
by (force simp: incseq_def)
qed (insert *, auto)
with \<open>(\<Inter>i. A i) = {}\<close> * show False
by (subst (asm) prod_emb_trans) (auto simp: A[abs_def])
qed
moreover have "(\i. P (J i) (X i)) \ (INF i. P (J i) (X i))"
proof (intro LIMSEQ_INF antimonoI)
fix x y :: nat assume "x \ y"
have "P (J y \ J x) (emb (J y \ J x) (J y) (X y)) \ P (J y \ J x) (emb (J y \ J x) (J x) (X x))"
using \<open>decseq A\<close>[THEN decseqD, OF \<open>x\<le>y\<close>] *
by (auto simp: A sets_P del: subsetI intro!: emeasure_mono \<open>x \<le> y\<close>
emb_preserve_mono[of "J y \ J x" I, where X="emb (J y \ J x) (J y) (X y)"])
then show "P (J y) (X y) \ P (J x) (X x)"
using * by (simp add: emeasure_P)
qed
ultimately show "(\i. \G (A i)) \ 0"
by (auto simp: A[abs_def] mu_G_spec *)
qed
then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s"
and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \"
by (metis sets_PiM_generator)
show ?thesis
proof (subst emeasure_extend_measure[OF lim_def])
show "A \ generator \ \ A = \G A" for A
using eq by simp
show "positive (sets lim) \" "countably_additive (sets lim) \"
using ms by (auto simp add: measure_space_def)
show "(\x. x) ` generator \ Pow (space (Pi\<^sub>M I M))"
using generator.space_closed by simp
show "emb I J X \ generator" "\G (emb I J X) = emeasure (P J) X"
using JX by (auto intro: generator.intros simp: mu_G_spec)
qed
qed
end
sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
unfolding projective_family_def
proof (intro conjI allI impI distr_restrict)
show "\J. finite J \ prob_space (Pi\<^sub>M J M)"
by (intro prob_spaceI) (simp add: space_PiM emeasure_PiM emeasure_space_1)
qed auto
txt \<open> Proof due to Ionescu Tulcea. \<close>
locale Ionescu_Tulcea =
fixes P :: "nat \ (nat \ 'a) \ 'a measure" and M :: "nat \ 'a measure"
assumes P[measurable]: "\i. P i \ measurable (PiM {0..
assumes prob_space_P: "\i x. x \ space (PiM {0.. prob_space (P i x)"
begin
lemma non_empty[simp]: "space (M i) \ {}"
proof (induction i rule: less_induct)
case (less i)
then obtain x where "\j. j < i \ x j \ space (M j)"
unfolding ex_in_conv[symmetric] by metis
then have *: "restrict x {0.. space (PiM {0..
by (auto simp: space_PiM PiE_iff)
then interpret prob_space "P i (restrict x {0..
by (rule prob_space_P)
show ?case
using not_empty subprob_measurableD(1)[OF P, OF *] by simp
qed
lemma space_PiM_not_empty[simp]: "space (PiM UNIV M) \ {}"
unfolding space_PiM_empty_iff by auto
lemma space_P: "x \ space (PiM {0.. space (P n x) = space (M n)"
by (simp add: P[THEN subprob_measurableD(1)])
lemma sets_P[measurable_cong]: "x \ space (PiM {0.. sets (P n x) = sets (M n)"
by (simp add: P[THEN subprob_measurableD(2)])
definition eP :: "nat \ (nat \ 'a) \ (nat \ 'a) measure" where
"eP n \ = distr (P n \) (PiM {0.. n)"
lemma measurable_eP[measurable]:
"eP n \ measurable (PiM {0..< n} M) (subprob_algebra (PiM {0..
by (auto simp: eP_def[abs_def] measurable_split_conv
intro!: measurable_fun_upd[where J="{0..] measurable_distr2[OF _ P])
lemma space_eP:
"x \ space (PiM {0.. space (eP n x) = space (PiM {0..
by (simp add: measurable_eP[THEN subprob_measurableD(1)])
lemma sets_eP[measurable]:
"x \ space (PiM {0.. sets (eP n x) = sets (PiM {0..
by (simp add: measurable_eP[THEN subprob_measurableD(2)])
lemma prob_space_eP: "x \ space (PiM {0.. prob_space (eP n x)"
unfolding eP_def
by (intro prob_space.prob_space_distr prob_space_P measurable_fun_upd[where J="{0..]) auto
lemma nn_integral_eP:
"\ \ space (PiM {0.. f \ borel_measurable (PiM {0..
(\<integral>\<^sup>+x. f x \<partial>eP n \<omega>) = (\<integral>\<^sup>+x. f (\<omega>(n := x)) \<partial>P n \<omega>)"
unfolding eP_def
by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..] simp: space_PiM PiE_iff)
lemma emeasure_eP:
assumes \<omega>[simp]: "\<omega> \<in> space (PiM {0..<n} M)" and A[measurable]: "A \<in> sets (PiM {0..<Suc n} M)"
shows "eP n \ A = P n \ ((\x. \(n := x)) -` A \ space (M n))"
using nn_integral_eP[of \<omega> n "indicator A"]
apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator)
apply (subst nn_integral_indicator[symmetric])
using measurable_sets[OF measurable_fun_upd[OF _ measurable_const[OF \<omega>] measurable_id] A, of n]
apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator
intro!: nn_integral_cong split: split_indicator)
done
primrec C :: "nat \ nat \ (nat \ 'a) \ (nat \ 'a) measure" where
"C n 0 \ = return (PiM {0.."
| "C n (Suc m) \ = C n m \ \ eP (n + m)"
lemma measurable_C[measurable]:
"C n m \ measurable (PiM {0..
by (induction m) auto
lemma space_C:
"x \ space (PiM {0.. space (C n m x) = space (PiM {0..
by (simp add: measurable_C[THEN subprob_measurableD(1)])
lemma sets_C[measurable_cong]:
"x \ space (PiM {0.. sets (C n m x) = sets (PiM {0..
by (simp add: measurable_C[THEN subprob_measurableD(2)])
lemma prob_space_C: "x \ space (PiM {0.. prob_space (C n m x)"
proof (induction m)
case (Suc m) then show ?case
by (auto intro!: prob_space.prob_space_bind[where S="PiM {0..]
simp: space_C prob_space_eP)
qed (auto intro!: prob_space_return simp: space_PiM)
lemma split_C:
assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<bind> C (n + m) l) = C n (m + l) \<omega>"
proof (induction l)
case 0
with \<omega> show ?case
by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty]
distr_cong[OF refl sets_C[symmetric, OF \<omega>]])
next
case (Suc l) with \<omega> show ?case
by (simp add: bind_assoc[symmetric, OF _ measurable_eP]) (simp add: ac_simps)
qed
lemma nn_integral_C:
assumes "m \ m'" and f[measurable]: "f \ borel_measurable (PiM {0..
and nonneg: "\x. x \ space (PiM {0.. 0 \ f x"
and x: "x \ space (PiM {0..
shows "(\\<^sup>+x. f x \C n m x) = (\\<^sup>+x. f (restrict x {0..C n m' x)"
using \<open>m \<le> m'\<close>
proof (induction rule: dec_induct)
case (step i)
let ?E = "\x. f (restrict x {0..
from \<open>m\<le>i\<close> x have "?C i ?E = ?C (Suc i) ?E"
by (auto simp: nn_integral_bind[where B="PiM {0 ..< Suc (n + i)} M"] space_C nn_integral_eP
intro!: nn_integral_cong)
(simp add: space_PiM PiE_iff nonneg prob_space.emeasure_space_1[OF prob_space_P])
with step show ?case by (simp del: restrict_apply)
qed (auto simp: space_PiM space_C[OF x] simp del: restrict_apply intro!: nn_integral_cong)
lemma emeasure_C:
assumes "m \ m'" and A[measurable]: "A \ sets (PiM {0.. space (PiM {0..
shows "emeasure (C n m' x) (prod_emb {0..
using assms
by (subst (1 2) nn_integral_indicator[symmetric])
(auto intro!: nn_integral_cong split: split_indicator simp del: nn_integral_indicator
simp: nn_integral_C[of m m' _ n] prod_emb_iff space_PiM PiE_iff sets_C space_C)
lemma distr_C:
assumes "m \ m'" and [simp]: "x \ space (PiM {0..
shows "C n m x = distr (C n m' x) (PiM {0..x. restrict x {0..
proof (rule measure_eqI)
fix A assume "A \ sets (C n m x)"
with \<open>m \<le> m'\<close> show "emeasure (C n m x) A = emeasure (distr (C n m' x) (Pi\<^sub>M {0..<n + m} M) (\<lambda>x. restrict x {0..<n + m})) A"
by (subst emeasure_C[symmetric, OF \<open>m \<le> m'\<close>]) (auto intro!: emeasure_distr_restrict[symmetric] simp: sets_C)
qed (simp add: sets_C)
definition up_to :: "nat set \ nat" where
"up_to J = (LEAST n. \i\n. i \ J)"
lemma up_to_less: "finite J \ i \ J \ i < up_to J"
unfolding up_to_def
by (rule LeastI2[of _ "Suc (Max J)"]) (auto simp: Suc_le_eq not_le[symmetric])
lemma up_to_iff: "finite J \ up_to J \ n \ (\i\J. i < n)"
proof safe
show "finite J \ up_to J \ n \ i \ J \ i < n" for i
using up_to_less[of J i] by auto
qed (auto simp: up_to_def intro!: Least_le)
lemma up_to_iff_Ico: "finite J \ up_to J \ n \ J \ {0..
by (auto simp: up_to_iff)
lemma up_to: "finite J \ J \ {0..< up_to J}"
by (auto simp: up_to_less)
lemma up_to_mono: "J \ H \ finite H \ up_to J \ up_to H"
by (auto simp add: up_to_iff finite_subset up_to_less)
definition CI :: "nat set \ (nat \ 'a) measure" where
"CI J = distr (C 0 (up_to J) (\x. undefined)) (PiM J M) (\f. restrict f J)"
sublocale PF: projective_family UNIV CI
unfolding projective_family_def
proof safe
show "finite J \ prob_space (CI J)" for J
using up_to[of J] unfolding CI_def
by (intro prob_space.prob_space_distr prob_space_C measurable_restrict) auto
note measurable_cong_sets[OF sets_C, simp]
have [simp]: "J \ H \ (\f. restrict f J) \ measurable (Pi\<^sub>M H M) (Pi\<^sub>M J M)" for H J
by (auto intro!: measurable_restrict)
show "J \ H \ finite H \ CI J = distr (CI H) (Pi\<^sub>M J M) (\f. restrict f J)" for J H
by (simp add: CI_def distr_C[OF up_to_mono[of J H]] up_to up_to_mono distr_distr comp_def
inf.absorb2 finite_subset)
qed
lemma emeasure_CI':
"finite J \ X \ sets (PiM J M) \ CI J X = C 0 (up_to J) (\_. undefined) (PF.emb {0..
unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C)
lemma emeasure_CI:
"J \ {0.. X \ sets (PiM J M) \ CI J X = C 0 n (\_. undefined) (PF.emb {0..
apply (subst emeasure_CI', simp_all add: finite_subset)
apply (subst emeasure_C[symmetric, of "up_to J" n])
apply (auto simp: finite_subset up_to_iff_Ico up_to_less)
apply (subst prod_emb_trans)
apply (auto simp: up_to_less finite_subset up_to_iff_Ico)
done
lemma lim:
assumes J: "finite J" and X: "X \ sets (PiM J M)"
shows "emeasure PF.lim (PF.emb UNIV J X) = emeasure (CI J) X"
proof (rule PF.emeasure_lim[OF J subset_UNIV X])
fix J X' assume J[simp]: "\i. finite (J i)" and X'[measurable]: "\i. X' i \ sets (Pi\<^sub>M (J i) M)"
and dec: "decseq (\i. PF.emb UNIV (J i) (X' i))"
define X where "X n =
(\<Inter>i\<in>{i. J i \<subseteq> {0..< n}}. PF.emb {0..<n} (J i) (X' i)) \<inter> space (PiM {0..<n} M)" for n
have sets_X[measurable]: "X n \ sets (PiM {0..
by (cases "{i. J i \ {0..< n}} = {}")
(simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int)
have dec_X: "n \ m \ X m \ PF.emb {0..
unfolding X_def using ivl_subset[of 0 n 0 m]
by (cases "{i. J i \ {0..< n}} = {}")
(auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset)
have dec_X': "PF.emb {0.. j) \<subseteq> PF.emb {0..<n} (J i) (X' i)"
if [simp]: "J i \ {0.. {0.. j" for n i j
by (rule PF.emb_preserve_mono[of "{0.. UNIV]) (auto del: subsetI intro: dec[THEN antimonoD])
assume "0 < (INF i. CI (J i) (X' i))"
also have "\ \ (INF i. C 0 i (\x. undefined) (X i))"
proof (intro INF_greatest)
fix n
interpret C: prob_space "C 0 n (\x. undefined)"
by (rule prob_space_C) simp
show "(INF i. CI (J i) (X' i)) \ C 0 n (\x. undefined) (X n)"
proof cases
assume "{i. J i \ {0..< n}} = {}" with C.emeasure_space_1 show ?thesis
by (auto simp add: X_def space_C intro!: INF_lower2[of 0] prob_space.measure_le_1 PF.prob_space_P)
next
assume *: "{i. J i \ {0..< n}} \ {}"
have "(INF i. CI (J i) (X' i)) \
(INF i\<in>{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
by (intro INF_superset_mono) (auto simp: emeasure_CI)
also have "\ = C 0 n (\_. undefined) (\i\{i. J i \ {0..
using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
also have "\ = C 0 n (\_. undefined) (X n)"
using * by (auto simp add: X_def INT_extend_simps)
finally show "(INF i. CI (J i) (X' i)) \ C 0 n (\_. undefined) (X n)" .
qed
qed
finally have pos: "0 < (INF i. C 0 i (\x. undefined) (X i))" .
from less_INF_D[OF this, of 0] have "X 0 \ {}"
by auto
{ fix \<omega> n assume \<omega>: "\<omega> \<in> space (PiM {0..<n} M)"
let ?C = "\i. emeasure (C n i \) (X (n + i))"
let ?C' = "\i x. emeasure (C (Suc n) i (\(n:=x))) (X (Suc n + i))"
have M: "\i. ?C' i \ borel_measurable (P n \)"
using \<omega>[measurable, simp] measurable_fun_upd[where J="{0..<n}"] by measurable auto
assume "0 < (INF i. ?C i)"
also have "\ \ (INF i. emeasure (C n (1 + i) \) (X (n + (1 + i))))"
by (intro INF_greatest INF_lower) auto
also have "\ = (INF i. \\<^sup>+x. ?C' i x \P n \)"
using \<omega> measurable_C[of "Suc n"]
apply (intro INF_cong refl)
apply (subst split_C[symmetric, OF \<omega>])
apply (subst emeasure_bind[OF _ _ sets_X])
apply (simp_all del: C.simps add: space_C)
apply measurable
apply simp
apply (simp add: bind_return[OF measurable_eP] nn_integral_eP)
done
also have "\ = (\\<^sup>+x. (INF i. ?C' i x) \P n \)"
proof (rule nn_integral_monotone_convergence_INF_AE[symmetric])
have "(\\<^sup>+x. ?C' 0 x \P n \) \ (\\<^sup>+x. 1 \P n \)"
by (intro nn_integral_mono) (auto split: split_indicator)
also have "\ < \"
using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp
finally show "(\\<^sup>+x. ?C' 0 x \P n \) < \" .
next
show "AE x in P n \. ?C' (Suc i) x \ ?C' i x" for i
proof (rule AE_I2)
fix x assume "x \ space (P n \)"
with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)"
by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
with \<omega> show "?C' (Suc i) x \<le> ?C' i x"
apply (subst emeasure_C[symmetric, of i "Suc i"])
apply (auto intro!: emeasure_mono[OF dec_X] del: subsetI
simp: sets_C space_P)
apply (subst sets_bind[OF sets_eP])
apply (simp_all add: space_C space_P)
done
qed
qed fact
finally have "(\\<^sup>+x. (INF i. ?C' i x) \P n \) \ 0"
by simp
with M have "\\<^sub>F x in ae_filter (P n \). 0 < (INF i. ?C' i x)"
by (subst (asm) nn_integral_0_iff_AE)
(auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le zero_less_iff_neq_zero)
then have "\\<^sub>F x in ae_filter (P n \). x \ space (M n) \ 0 < (INF i. ?C' i x)"
by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>)
then obtain x where "x \ space (M n)" "0 < (INF i. ?C' i x)"
by (auto dest: frequently_ex)
from this(2)[THEN less_INF_D, of 0] this(2)
have "\x. \(n := x) \ X (Suc n) \ 0 < (INF i. ?C' i x)"
by (intro exI[of _ x]) (simp split: split_indicator_asm) }
note step = this
let ?\<omega> = "\<lambda>\<omega> n x. (restrict \<omega> {0..<n})(n := x)"
let ?L = "\\ n r. INF i. emeasure (C (Suc n) i (?\ \ n r)) (X (Suc n + i))"
have *: "(\i. i < n \ ?\ \ i (\ i) \ X (Suc i)) \
restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" for \<omega> n
using sets.sets_into_space[OF sets_X, of n]
by (cases n) (auto simp: atLeastLessThanSuc restrict_def[of _ "{}"])
have "\\. \n. ?\ \ n (\ n) \ X (Suc n) \ 0 < ?L \ n (\ n)"
proof (rule dependent_wellorder_choice)
fix n \<omega> assume IH: "\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i) \<and> 0 < ?L \<omega> i (\<omega> i)"
show "\r. ?\ \ n r \ X (Suc n) \ 0 < ?L \ n r"
proof (rule step)
show "restrict \ {0.. space (Pi\<^sub>M {0..
using IH[THEN conjunct1] by (rule *)
show "0 < (INF i. emeasure (C n i (restrict \ {0..
proof (cases n)
case 0 with pos show ?thesis
by (simp add: CI_def restrict_def)
next
case (Suc i) then show ?thesis
using IH[of i, THEN conjunct2] by (simp add: atLeastLessThanSuc)
qed
qed
qed (simp cong: restrict_cong)
then obtain \<omega> where \<omega>: "\<And>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n)"
by auto
from this[THEN *] have \<omega>_space: "\<omega> \<in> space (PiM UNIV M)"
by (auto simp: space_PiM PiE_iff Ball_def)
have *: "\ \ PF.emb UNIV {0..
proof (cases n)
case 0 with \<omega>_space \<open>X 0 \<noteq> {}\<close> sets.sets_into_space[OF sets_X, of 0] show ?thesis
by (auto simp add: space_PiM prod_emb_def restrict_def PiE_iff)
next
case (Suc i) then show ?thesis
using \<omega>[of i] \<omega>_space by (auto simp: prod_emb_def space_PiM PiE_iff atLeastLessThanSuc)
qed
have **: "{i. J i \ {0.. {}" for n
by (auto intro!: exI[of _ n] up_to J)
have "\ \ PF.emb UNIV (J n) (X' n)" for n
using *[of "up_to (J n)"] up_to[of "J n"] by (simp add: X_def prod_emb_Int prod_emb_INT[OF **])
then show "(\i. PF.emb UNIV (J i) (X' i)) \ {}"
by auto
qed
lemma distr_lim: assumes J[simp]: "finite J" shows "distr PF.lim (PiM J M) (\x. restrict x J) = CI J"
apply (rule measure_eqI)
apply (simp add: CI_def)
apply (simp add: emeasure_distr measurable_cong_sets[OF PF.sets_lim] lim[symmetric] prod_emb_def space_PiM)
done
end
lemma (in product_prob_space) emeasure_lim_emb:
assumes *: "finite J" "J \ I" "X \ sets (PiM J M)"
shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X"
proof (rule emeasure_lim[OF *], goal_cases)
case (1 J X)
have "\Q. (\i. sets Q = PiM (\i. J i) M \ distr Q (PiM (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M)"
proof cases
assume "finite (\i. J i)"
then have "distr (PiM (\i. J i) M) (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M" for i
by (intro distr_restrict[symmetric]) auto
then show ?thesis
by auto
next
assume inf: "infinite (\i. J i)"
moreover have count: "countable (\i. J i)"
using 1(3) by (auto intro: countable_finite)
define f where "f = from_nat_into (\i. J i)"
define t where "t = to_nat_on (\i. J i)"
have ft[simp]: "x \ J i \ f (t x) = x" for x i
unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto
have tf[simp]: "t (f i) = i" for i
unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count)
have inj_t: "inj_on t (\i. J i)"
using count by (auto simp: t_def)
then have inj_t_J: "inj_on t (J i)" for i
by (rule subset_inj_on) auto
interpret IT: Ionescu_Tulcea "\i \. M (f i)" "\i. M (f i)"
by standard auto
interpret Mf: product_prob_space "\x. M (f x)" UNIV
by standard
have C_eq_PiM: "IT.C 0 n (\_. undefined) = PiM {0..x. M (f x))" for n
proof (induction n)
case 0 then show ?case
by (auto simp: PiM_empty intro!: measure_eqI dest!: subset_singletonD)
next
case (Suc n) then show ?case
apply (auto intro!: measure_eqI simp: sets_bind[OF IT.sets_eP] emeasure_bind[OF _ IT.measurable_eP])
apply (auto simp: Mf.product_nn_integral_insert nn_integral_indicator[symmetric] atLeastLessThanSuc IT.emeasure_eP space_PiM
split: split_indicator simp del: nn_integral_indicator intro!: nn_integral_cong)
done
qed
have CI_eq_PiM: "IT.CI X = PiM X (\x. M (f x))" if X: "finite X" for X
by (auto simp: IT.up_to_less X IT.CI_def C_eq_PiM intro!: Mf.distr_restrict[symmetric])
let ?Q = "distr IT.PF.lim (PiM (\i. J i) M) (\\. \x\\i. J i. \ (t x))"
{ fix i
have "distr ?Q (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) =
distr IT.PF.lim (Pi\<^sub>M (J i) M) ((\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<circ> (\<lambda>\<omega>. restrict \<omega> (t`J i)))"
proof (subst distr_distr)
have "(\\. \ (t x)) \ measurable (Pi\<^sub>M UNIV (\x. M (f x))) (M x)" if x: "x \ J i" for x i
using measurable_component_singleton[of "t x" "UNIV" "\x. M (f x)"] unfolding ft[OF x] by simp
then show "(\\. \x\\i. J i. \ (t x)) \ measurable IT.PF.lim (Pi\<^sub>M (\(J ` UNIV)) M)"
by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
also have "\ = distr (distr IT.PF.lim (PiM (t`J i) (\x. M (f x))) (\\. restrict \ (t`J i))) (Pi\<^sub>M (J i) M) (\\. \n\J i. \ (t n))"
proof (intro distr_distr[symmetric])
have "(\\. \ (t x)) \ measurable (Pi\<^sub>M (t`J i) (\x. M (f x))) (M x)" if x: "x \ J i" for x
using measurable_component_singleton[of "t x" "t`J i" "\x. M (f x)"] x unfolding ft[OF x] by auto
then show "(\\. \n\J i. \ (t n)) \ measurable (Pi\<^sub>M (t ` J i) (\x. M (f x))) (Pi\<^sub>M (J i) M)"
by (auto intro!: measurable_restrict)
qed (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
also have "\ = distr (PiM (t`J i) (\x. M (f x))) (Pi\<^sub>M (J i) M) (\\. \n\J i. \ (t n))"
using \<open>finite (J i)\<close> by (subst IT.distr_lim) (auto simp: CI_eq_PiM)
also have "\ = Pi\<^sub>M (J i) M"
using Mf.distr_reorder[of t "J i"] by (simp add: 1 inj_t_J cong: PiM_cong)
finally have "distr ?Q (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M" . }
then show "\Q. \i. sets Q = PiM (\i. J i) M \ distr Q (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M"
by (intro exI[of _ ?Q]) auto
qed
then obtain Q where sets_Q: "sets Q = PiM (\i. J i) M"
and Q: "\i. distr Q (PiM (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M" by blast
from 1 interpret Q: prob_space Q
by (intro prob_space_distrD[of "\x. restrict x (J 0)" Q "PiM (J 0) M"])
(auto simp: Q measurable_cong_sets[OF sets_Q]
intro!: prob_space_P measurable_restrict measurable_component_singleton)
have "0 < (INF i. emeasure (Pi\<^sub>M (J i) M) (X i))" by fact
also have "\ = (INF i. emeasure Q (emb (\i. J i) (J i) (X i)))"
by (simp add: emeasure_distr_restrict[OF _ sets_Q 1(4), symmetric] SUP_upper Q)
also have "\ = emeasure Q (\i. emb (\i. J i) (J i) (X i))"
proof (rule INF_emeasure_decseq)
from 1 show "decseq (\n. emb (\i. J i) (J n) (X n))"
by (intro antimonoI emb_preserve_mono[where X="emb (\i. J i) (J n) (X n)" and L=I and J="\i. J i" for n]
measurable_prod_emb)
(auto simp: SUP_least SUP_upper antimono_def)
qed (insert 1, auto simp: sets_Q)
finally have "(\i. emb (\i. J i) (J i) (X i)) \ {}"
by auto
moreover have "(\i. emb I (J i) (X i)) = {} \ (\i. emb (\i. J i) (J i) (X i)) = {}"
using 1 by (intro emb_injective[of "\i. J i" I _ "{}"] sets.countable_INT) (auto simp: SUP_least SUP_upper)
ultimately show ?case by auto
qed
end
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
