# HG changeset patch # User hoelzl # Date 1444230676 -7200 # Node ID e985b52c3eb3599c7e7571f9a62dffe08b3d11da # Parent 131fc8c1040290128cd934f4cfb0aa0d8b0ddd0c cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Library/FuncSet.thy Wed Oct 07 17:11:16 2015 +0200 @@ -184,6 +184,9 @@ subsection \Bounded Abstraction: @{term restrict}\ +lemma restrict_cong: "I = J \ (\i. i \ J =simp=> f i = g i) \ restrict f I = restrict g J" + by (auto simp: restrict_def fun_eq_iff simp_implies_def) + lemma restrict_in_funcset: "(\x. x \ A \ f x \ B) \ (\x\A. f x) \ A \ B" by (simp add: Pi_def restrict_def) diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Distributions.thy --- a/src/HOL/Probability/Distributions.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Distributions.thy Wed Oct 07 17:11:16 2015 +0200 @@ -973,11 +973,7 @@ by (intro integral_cong) auto finally have "Suc k * (\x. indicator {0..b} x *\<^sub>R ?M k x \lborel) = exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \lborel)" - apply (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric]) - apply (subst integral_mult_right_zero[symmetric]) - apply (intro integral_cong) - apply simp_all - done + by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric]) then show "(k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b" by (simp add: field_simps atLeastAtMost_def indicator_inter_arith) qed diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 07 17:11:16 2015 +0200 @@ -351,6 +351,15 @@ lemma space_PiM: "space (\\<^sub>M i\I. M i) = (\\<^sub>E i\I. space (M i))" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp +lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \ space (PiM I M)" + by (auto simp: prod_emb_def space_PiM) + +lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \ (\i\I. space (M i) = {})" + by (auto simp: space_PiM PiE_eq_empty_iff) + +lemma undefined_in_PiM_empty[simp]: "(\x. undefined) \ space (PiM {} M)" + by (auto simp: space_PiM) + lemma sets_PiM: "sets (\\<^sub>M i\I. M i) = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp @@ -621,6 +630,20 @@ finally show "{\ \ space ?P. case_prod (\f. fun_upd f i) \ j \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_def) +lemma measurable_fun_upd: + assumes I: "I = J \ {i}" + assumes f[measurable]: "f \ measurable N (PiM J M)" + assumes h[measurable]: "h \ measurable N (M i)" + shows "(\x. (f x) (i := h x)) \ measurable N (PiM I M)" +proof (intro measurable_PiM_single') + fix j assume "j \ I" then show "(\\. ((f \)(i := h \)) j) \ measurable N (M j)" + unfolding I by (cases "j = i") auto +next + show "(\x. (f x)(i := h x)) \ space N \ (\\<^sub>E i\I. space (M i))" + using I f[THEN measurable_space] h[THEN measurable_space] + by (auto simp: space_PiM PiE_iff extensional_def) +qed + lemma measurable_component_update: "x \ space (Pi\<^sub>M I M) \ i \ I \ (\v. x(i := v)) \ measurable (M i) (Pi\<^sub>M (insert i I) M)" by simp @@ -673,6 +696,25 @@ unfolding prod_emb_def space_PiM[symmetric] by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) +lemma merge_in_prod_emb: + assumes "y \ space (PiM I M)" "x \ X" and X: "X \ sets (Pi\<^sub>M J M)" and "J \ I" + shows "merge J I (x, y) \ prod_emb I M J X" + using assms sets.sets_into_space[OF X] + by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff + cong: if_cong restrict_cong) + (simp add: extensional_def) + +lemma prod_emb_eq_emptyD: + assumes J: "J \ I" and ne: "space (PiM I M) \ {}" and X: "X \ sets (Pi\<^sub>M J M)" + and *: "prod_emb I M J X = {}" + shows "X = {}" +proof safe + fix x assume "x \ X" + obtain \ where "\ \ space (PiM I M)" + using ne by blast + from merge_in_prod_emb[OF this \x\X\ X J] * show "x \ {}" by auto +qed + lemma sets_in_Pi_aux: "finite I \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ {x\space (PiM I M). x \ Pi I F} \ sets (PiM I M)" @@ -817,6 +859,36 @@ by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space) qed simp +lemma (in product_sigma_finite) PiM_eqI: + assumes "finite I" "sets P = PiM I M" + assumes eq: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" + shows "P = PiM I M" +proof - + interpret finite_product_sigma_finite M I + proof qed fact + from sigma_finite_pairs guess C .. note C = this + show ?thesis + proof (rule measure_eqI_generator_eq[symmetric, OF Int_stable_prod_algebra prod_algebra_sets_into_space]) + show "sets (PiM I M) = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" + by (rule sets_PiM) + then show "sets P = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" + unfolding `sets P = sets (PiM I M)` by simp + def A \ "\n. \\<^sub>E i\I. C i n" + show "range A \ prod_algebra I M" "\i. emeasure (Pi\<^sub>M I M) (A i) \ \" + using C \finite I\ + by (auto intro!: prod_algebraI_finite simp: A_def emeasure_PiM subset_eq setprod_PInf emeasure_nonneg) + show "(\i. A i) = (\\<^sub>E i\I. space (M i))" + using C by (simp add: A_def space_PiM) + + fix X assume X: "X \ prod_algebra I M" + then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)" + and J: "finite J" "J \ I" "\j. j \ J \ E j \ sets (M j)" + by (force elim!: prod_algebraE) + show "emeasure (PiM I M) X = emeasure P X" + unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq emeasure_PiM J \finite I\) + qed +qed + lemma (in product_sigma_finite) sigma_finite: assumes "finite I" shows "sigma_finite_measure (PiM I M)" @@ -843,84 +915,24 @@ using emeasure_PiM[OF finite_index] by auto lemma (in product_sigma_finite) nn_integral_empty: - assumes pos: "0 \ f (\k. undefined)" - shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\k. undefined)" -proof - - interpret finite_product_sigma_finite M "{}" by standard (fact finite.emptyI) - have "\A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1" - using assms by (subst measure_times) auto - then show ?thesis - unfolding nn_integral_def simple_function_def simple_integral_def[abs_def] - proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym) - show "f (\k. undefined) \ (SUP f:{g. g \ max 0 \ f}. f (\k. undefined))" - by (intro SUP_upper) (auto simp: le_fun_def split: split_max) - show "(SUP f:{g. g \ max 0 \ f}. f (\k. undefined)) \ f (\k. undefined)" using pos - by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm) - qed -qed + "0 \ f (\k. undefined) \ integral\<^sup>N (Pi\<^sub>M {} M) f = f (\k. undefined)" + by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2) lemma (in product_sigma_finite) distr_merge: assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" shows "distr (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M) (merge I J) = Pi\<^sub>M (I \ J) M" (is "?D = ?P") -proof - +proof (rule PiM_eqI) interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact - have "finite (I \ J)" using fin by auto - interpret IJ: finite_product_sigma_finite M "I \ J" by standard fact - interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard - let ?g = "merge I J" - - from IJ.sigma_finite_pairs obtain F where - F: "\i. i\ I \ J \ range (F i) \ sets (M i)" - "incseq (\k. \\<^sub>E i\I \ J. F i k)" - "(\k. \\<^sub>E i\I \ J. F i k) = space ?P" - "\k. \i\I\J. emeasure (M i) (F i k) \ \" - by auto - let ?F = "\k. \\<^sub>E i\I \ J. F i k" - - show ?thesis - proof (rule measure_eqI_generator_eq[symmetric]) - show "Int_stable (prod_algebra (I \ J) M)" - by (rule Int_stable_prod_algebra) - show "prod_algebra (I \ J) M \ Pow (\\<^sub>E i \ I \ J. space (M i))" - by (rule prod_algebra_sets_into_space) - show "sets ?P = sigma_sets (\\<^sub>E i\I \ J. space (M i)) (prod_algebra (I \ J) M)" - by (rule sets_PiM) - then show "sets ?D = sigma_sets (\\<^sub>E i\I \ J. space (M i)) (prod_algebra (I \ J) M)" - by simp - - show "range ?F \ prod_algebra (I \ J) M" using F - using fin by (auto simp: prod_algebra_eq_finite) - show "(\i. \\<^sub>E ia\I \ J. F ia i) = (\\<^sub>E i\I \ J. space (M i))" - using F(3) by (simp add: space_PiM) - next - fix k - from F `finite I` setprod_PInf[of "I \ J", OF emeasure_nonneg, of M] - show "emeasure ?P (?F k) \ \" by (subst IJ.measure_times) auto - next - fix A assume A: "A \ prod_algebra (I \ J) M" - with fin obtain F where A_eq: "A = (Pi\<^sub>E (I \ J) F)" and F: "\i\J. F i \ sets (M i)" "\i\I. F i \ sets (M i)" - by (auto simp add: prod_algebra_eq_finite) - let ?B = "Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M" - let ?X = "?g -` A \ space ?B" - have "Pi\<^sub>E I F \ space (Pi\<^sub>M I M)" "Pi\<^sub>E J F \ space (Pi\<^sub>M J M)" - using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+ - then have X: "?X = (Pi\<^sub>E I F \ Pi\<^sub>E J F)" - unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM) - have "emeasure ?D A = emeasure ?B ?X" - using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM) - also have "emeasure ?B ?X = (\i\I. emeasure (M i) (F i)) * (\i\J. emeasure (M i) (F i))" - using `finite J` `finite I` F unfolding X - by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times) - also have "\ = (\i\I \ J. emeasure (M i) (F i))" - using `finite J` `finite I` `I \ J = {}` by (simp add: setprod.union_inter_neutral) - also have "\ = emeasure ?P (Pi\<^sub>E (I \ J) F)" - using `finite J` `finite I` F unfolding A - by (intro IJ.measure_times[symmetric]) auto - finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp - qed -qed + fix A assume A: "\i. i \ I \ J \ A i \ sets (M i)" + have *: "(merge I J -` Pi\<^sub>E (I \ J) A \ space (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M)) = PiE I A \ PiE J A" + using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure) + from A fin show "emeasure (distr (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M) (merge I J)) (Pi\<^sub>E (I \ J) A) = + (\i\I \ J. emeasure (M i) (A i))" + by (subst emeasure_distr) + (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times setprod.union_disjoint) +qed (insert fin, simp_all) lemma (in product_sigma_finite) product_nn_integral_fold: assumes IJ: "I \ J = {}" "finite I" "finite J" @@ -1043,23 +1055,13 @@ lemma (in product_sigma_finite) distr_component: "distr (M i) (Pi\<^sub>M {i} M) (\x. \i\{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P") -proof (intro measure_eqI[symmetric]) - interpret I: finite_product_sigma_finite M "{i}" by standard simp - - have eq: "\x. x \ extensional {i} \ (\j\{i}. x i) = x" - by (auto simp: extensional_def restrict_def) - - have [measurable]: "\j. j \ {i} \ (\x. x) \ measurable (M i) (M j)" by simp - - fix A assume A: "A \ sets ?P" - then have "emeasure ?P A = (\\<^sup>+x. indicator A x \?P)" - by simp - also have "\ = (\\<^sup>+x. indicator ((\x. \i\{i}. x) -` A \ space (M i)) (x i) \PiM {i} M)" - by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq) - also have "\ = emeasure ?D A" - using A by (simp add: product_nn_integral_singleton emeasure_distr) - finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" . -qed simp +proof (intro PiM_eqI) + fix A assume "\ia. ia \ {i} \ A ia \ sets (M ia)" + moreover then have "(\x. \i\{i}. x) -` Pi\<^sub>E {i} A \ space (M i) = A i" + by (auto dest: sets.sets_into_space) + ultimately show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\x. \i\{i}. x)) (Pi\<^sub>E {i} A) = (\i\{i}. emeasure (M i) (A i))" + by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict) +qed simp_all lemma (in product_sigma_finite) assumes IJ: "I \ J = {}" "finite I" "finite J" and A: "A \ sets (Pi\<^sub>M (I \ J) M)" diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Wed Oct 07 17:11:16 2015 +0200 @@ -1405,6 +1405,10 @@ apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return') done +lemma bind_return_distr': + "space M \ {} \ f \ measurable M N \ bind M (\x. return N (f x)) = distr M N f" + using bind_return_distr[of M f N] by (simp add: comp_def) + lemma bind_assoc: fixes f :: "'a \ 'b measure" and g :: "'b \ 'c measure" assumes M1: "f \ measurable M (subprob_algebra N)" and M2: "g \ measurable N (subprob_algebra R)" diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Independent_Family.thy --- a/src/HOL/Probability/Independent_Family.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Independent_Family.thy Wed Oct 07 17:11:16 2015 +0200 @@ -1263,7 +1263,7 @@ note rv_Y = this[measurable] interpret Y: prob_space "distr M borel (Y i)" for i - using I(2) by (cases "i \ I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def) + using I(2) by (cases "i \ I") (auto intro!: prob_space_distr simp: indep_vars_def prob_space_return) interpret product_sigma_finite "\i. distr M borel (Y i)" .. @@ -1305,7 +1305,7 @@ note int_Y = this interpret Y: prob_space "distr M borel (Y i)" for i - using I(2) by (cases "i \ I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def) + using I(2) by (cases "i \ I") (auto intro!: prob_space_distr simp: indep_vars_def prob_space_return) interpret product_sigma_finite "\i. distr M borel (Y i)" .. diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 07 17:11:16 2015 +0200 @@ -8,341 +8,55 @@ imports Probability_Measure Caratheodory Projective_Family begin -lemma (in product_prob_space) emeasure_PiM_emb_not_empty: - assumes X: "J \ {}" "J \ I" "finite J" "\i\J. X i \ sets (M i)" - shows "emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = emeasure (Pi\<^sub>M J M) (Pi\<^sub>E J X)" -proof cases - assume "finite I" with X show ?thesis by simp -next - let ?\ = "\\<^sub>E i\I. space (M i)" - let ?G = generator - assume "\ finite I" - then have I_not_empty: "I \ {}" by auto - interpret G!: algebra ?\ generator by (rule algebra_generator) fact - note mu_G_mono = - G.additive_increasing[OF positive_mu_G[OF I_not_empty] additive_mu_G[OF I_not_empty], - THEN increasingD] - write mu_G ("\G") - - { fix Z J assume J: "J \ {}" "finite J" "J \ I" and Z: "Z \ ?G" - - from `infinite I` `finite J` obtain k where k: "k \ I" "k \ J" - by (metis rev_finite_subset subsetI) - moreover from Z guess K' X' by (rule generatorE) - moreover def K \ "insert k K'" - moreover def X \ "emb K K' X'" - ultimately have K: "K \ {}" "finite K" "K \ I" "X \ sets (Pi\<^sub>M K M)" "Z = emb I K X" - "K - J \ {}" "K - J \ I" "\G Z = emeasure (Pi\<^sub>M K M) X" - by (auto simp: subset_insertI) - let ?M = "\y. (\x. merge J (K - J) (y, x)) -` emb (J \ K) K X \ space (Pi\<^sub>M (K - J) M)" - { fix y assume y: "y \ space (Pi\<^sub>M J M)" - note * = merge_emb[OF `K \ I` `J \ I` y, of X] - moreover - have **: "?M y \ sets (Pi\<^sub>M (K - J) M)" - using J K y by (intro merge_sets) auto - ultimately - have ***: "((\x. merge J (I - J) (y, x)) -` Z \ space (Pi\<^sub>M I M)) \ ?G" - using J K by (intro generatorI) auto - have "\G ((\x. merge J (I - J) (y, x)) -` emb I K X \ space (Pi\<^sub>M I M)) = emeasure (Pi\<^sub>M (K - J) M) (?M y)" - unfolding * using K J by (subst mu_G_eq[OF _ _ _ **]) auto - note * ** *** this } - note merge_in_G = this - - have "finite (K - J)" using K by auto - - interpret J: finite_product_prob_space M J by standard fact+ - interpret KmJ: finite_product_prob_space M "K - J" by standard fact+ - - have "\G Z = emeasure (Pi\<^sub>M (J \ (K - J)) M) (emb (J \ (K - J)) K X)" - using K J by simp - also have "\ = (\\<^sup>+ x. emeasure (Pi\<^sub>M (K - J) M) (?M x) \Pi\<^sub>M J M)" - using K J by (subst emeasure_fold_integral) auto - also have "\ = (\\<^sup>+ y. \G ((\x. merge J (I - J) (y, x)) -` Z \ space (Pi\<^sub>M I M)) \Pi\<^sub>M J M)" - (is "_ = (\\<^sup>+x. \G (?MZ x) \Pi\<^sub>M J M)") - proof (intro nn_integral_cong) - fix x assume x: "x \ space (Pi\<^sub>M J M)" - with K merge_in_G(2)[OF this] - show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \G (?MZ x)" - unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst mu_G_eq) auto - qed - finally have fold: "\G Z = (\\<^sup>+x. \G (?MZ x) \Pi\<^sub>M J M)" . - - { fix x assume x: "x \ space (Pi\<^sub>M J M)" - then have "\G (?MZ x) \ 1" - unfolding merge_in_G(4)[OF x] `Z = emb I K X` - by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) } - note le_1 = this - - let ?q = "\y. \G ((\x. merge J (I - J) (y,x)) -` Z \ space (Pi\<^sub>M I M))" - have "?q \ borel_measurable (Pi\<^sub>M J M)" - unfolding `Z = emb I K X` using J K merge_in_G(3) - by (simp add: merge_in_G mu_G_eq emeasure_fold_measurable cong: measurable_cong) - note this fold le_1 merge_in_G(3) } - note fold = this - - have "\\. (\s\?G. \ s = \G s) \ measure_space ?\ (sigma_sets ?\ ?G) \" - proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G]) - fix A assume "A \ ?G" - with generatorE guess J X . note JX = this - interpret JK: finite_product_prob_space M J by standard fact+ - from JX show "\G A \ \" by simp - next - fix A assume A: "range A \ ?G" "decseq A" "(\i. A i) = {}" - then have "decseq (\i. \G (A i))" - by (auto intro!: mu_G_mono simp: decseq_def) - moreover - have "(INF i. \G (A i)) = 0" - proof (rule ccontr) - assume "(INF i. \G (A i)) \ 0" (is "?a \ 0") - moreover have "0 \ ?a" - using A positive_mu_G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def) - ultimately have "0 < ?a" by auto - - have "\n. \J X. J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ A n = emb I J X \ \G (A n) = emeasure (limP J M (\J. (Pi\<^sub>M J M))) X" - using A by (intro allI generator_Ex) auto - then obtain J' X' where J': "\n. J' n \ {}" "\n. finite (J' n)" "\n. J' n \ I" "\n. X' n \ sets (Pi\<^sub>M (J' n) M)" - and A': "\n. A n = emb I (J' n) (X' n)" - unfolding choice_iff by blast - moreover def J \ "\n. (\i\n. J' i)" - moreover def X \ "\n. emb (J n) (J' n) (X' n)" - ultimately have J: "\n. J n \ {}" "\n. finite (J n)" "\n. J n \ I" "\n. X n \ sets (Pi\<^sub>M (J n) M)" - by auto - with A' have A_eq: "\n. A n = emb I (J n) (X n)" "\n. A n \ ?G" - unfolding J_def X_def by (subst prod_emb_trans) (insert A, auto) - - have J_mono: "\n m. n \ m \ J n \ J m" - unfolding J_def by force - - interpret J: finite_product_prob_space M "J i" for i by standard fact+ - - have a_le_1: "?a \ 1" - using mu_G_spec[of "J 0" "A 0" "X 0"] J A_eq - by (auto intro!: INF_lower2[of 0] J.measure_le_1) - - let ?M = "\K Z y. (\x. merge K (I - K) (y, x)) -` Z \ space (Pi\<^sub>M I M)" - - { fix Z k assume Z: "range Z \ ?G" "decseq Z" "\n. ?a / 2^k \ \G (Z n)" - then have Z_sets: "\n. Z n \ ?G" by auto - fix J' assume J': "J' \ {}" "finite J'" "J' \ I" - interpret J': finite_product_prob_space M J' by standard fact+ - - let ?q = "\n y. \G (?M J' (Z n) y)" - let ?Q = "\n. ?q n -` {?a / 2^(k+1) ..} \ space (Pi\<^sub>M J' M)" - { fix n - have "?q n \ borel_measurable (Pi\<^sub>M J' M)" - using Z J' by (intro fold(1)) auto - then have "?Q n \ sets (Pi\<^sub>M J' M)" - by (rule measurable_sets) auto } - note Q_sets = this +lemma (in product_prob_space) distr_PiM_restrict_finite: + assumes "finite J" "J \ I" + shows "distr (PiM I M) (PiM J M) (\x. restrict x J) = PiM J M" +proof (rule PiM_eqI) + fix X assume X: "\i. i \ J \ X i \ sets (M i)" + { fix J X assume J: "J \ {} \ I = {}" "finite J" "J \ I" and X: "\i. i \ J \ X i \ sets (M i)" + have "emeasure (PiM I M) (emb I J (PiE J X)) = (\i\J. M i (X i))" + proof (subst emeasure_extend_measure_Pair[OF PiM_def, where \'=lim], goal_cases) + case 1 then show ?case + by (simp add: M.emeasure_space_1 emeasure_PiM Pi_iff sets_PiM_I_finite emeasure_lim_emb) + next + case (2 J X) + then have "emb I J (Pi\<^sub>E J X) \ sets (PiM I M)" + by (intro measurable_prod_emb sets_PiM_I_finite) auto + from this[THEN sets.sets_into_space] show ?case + by (simp add: space_PiM) + qed (insert assms J X, simp_all del: sets_lim + add: M.emeasure_space_1 sets_lim[symmetric] emeasure_countably_additive emeasure_positive) } + note * = this - have "?a / 2^(k+1) \ (INF n. emeasure (Pi\<^sub>M J' M) (?Q n))" - proof (intro INF_greatest) - fix n - have "?a / 2^k \ \G (Z n)" using Z by auto - also have "\ \ (\\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \Pi\<^sub>M J' M)" - unfolding fold(2)[OF J' `Z n \ ?G`] - proof (intro nn_integral_mono) - fix x assume x: "x \ space (Pi\<^sub>M J' M)" - then have "?q n x \ 1 + 0" - using J' Z fold(3) Z_sets by auto - also have "\ \ 1 + ?a / 2^(k+1)" - using `0 < ?a` by (intro add_mono) auto - finally have "?q n x \ 1 + ?a / 2^(k+1)" . - with x show "?q n x \ indicator (?Q n) x + ?a / 2^(k+1)" - by (auto split: split_indicator simp del: power_Suc) - qed - also have "\ = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)" - using `0 \ ?a` Q_sets J'.emeasure_space_1 - by (subst nn_integral_add) auto - finally show "?a / 2^(k+1) \ emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \ 1` - by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"]) - (auto simp: field_simps) - qed - also have "\ = emeasure (Pi\<^sub>M J' M) (\n. ?Q n)" - proof (intro INF_emeasure_decseq) - show "range ?Q \ sets (Pi\<^sub>M J' M)" using Q_sets by auto - show "decseq ?Q" - unfolding decseq_def - proof (safe intro!: vimageI[OF refl]) - fix m n :: nat assume "m \ n" - fix x assume x: "x \ space (Pi\<^sub>M J' M)" - assume "?a / 2^(k+1) \ ?q n x" - also have "?q n x \ ?q m x" - proof (rule mu_G_mono) - from fold(4)[OF J', OF Z_sets x] - show "?M J' (Z n) x \ ?G" "?M J' (Z m) x \ ?G" by auto - show "?M J' (Z n) x \ ?M J' (Z m) x" - using `decseq Z`[THEN decseqD, OF `m \ n`] by auto - qed - finally show "?a / 2^(k+1) \ ?q m x" . - qed - qed simp - finally have "(\n. ?Q n) \ {}" - using `0 < ?a` `?a \ 1` by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq) - then have "\w\space (Pi\<^sub>M J' M). \n. ?a / 2 ^ (k + 1) \ ?q n w" by auto } - note Ex_w = this - - let ?q = "\k n y. \G (?M (J k) (A n) y)" + have "emeasure (PiM I M) (emb I J (PiE J X)) = (\i\J. M i (X i))" + proof cases + assume "\ (J \ {} \ I = {})" + then obtain i where "J = {}" "i \ I" by auto + moreover then have "emb I {} {\x. undefined} = emb I {i} (\\<^sub>E i\{i}. space (M i))" + by (auto simp: space_PiM prod_emb_def) + ultimately show ?thesis + by (simp add: * M.emeasure_space_1) + qed (simp add: *[OF _ assms X]) + with assms show "emeasure (distr (Pi\<^sub>M I M) (Pi\<^sub>M J M) (\x. restrict x J)) (Pi\<^sub>E J X) = (\i\J. emeasure (M i) (X i))" + by (subst emeasure_distr_restrict[OF _ refl]) (auto intro!: sets_PiM_I_finite X) +qed (insert assms, auto) - let ?P = "\w k. w \ space (Pi\<^sub>M (J k) M) \ (\n. ?a / 2 ^ (Suc k) \ ?q k n w)" - have "\w. \k. ?P (w k) k \ restrict (w (Suc k)) (J k) = w k" - proof (rule dependent_nat_choice) - have "\n. ?a / 2 ^ 0 \ \G (A n)" by (auto intro: INF_lower) - from Ex_w[OF A(1,2) this J(1-3), of 0] show "\w. ?P w 0" by auto - next - fix w k assume Suc: "?P w k" - show "\w'. ?P w' (Suc k) \ restrict w' (J k) = w" - proof cases - assume [simp]: "J k = J (Suc k)" - have "?a / 2 ^ (Suc (Suc k)) \ ?a / 2 ^ (k + 1)" - using `0 < ?a` `?a \ 1` by (cases ?a) (auto simp: field_simps) - with Suc show ?thesis - by (auto intro!: exI[of _ w] simp: extensional_restrict space_PiM intro: order_trans) - next - assume "J k \ J (Suc k)" - with J_mono[of k "Suc k"] have "J (Suc k) - J k \ {}" (is "?D \ {}") by auto - have "range (\n. ?M (J k) (A n) w) \ ?G" "decseq (\n. ?M (J k) (A n) w)" - "\n. ?a / 2 ^ (k + 1) \ \G (?M (J k) (A n) w)" - using `decseq A` fold(4)[OF J(1-3) A_eq(2), of w k] Suc - by (auto simp: decseq_def) - from Ex_w[OF this `?D \ {}`] J[of "Suc k"] - obtain w' where w': "w' \ space (Pi\<^sub>M ?D M)" - "\n. ?a / 2 ^ (Suc k + 1) \ \G (?M ?D (?M (J k) (A n) w) w')" by auto - let ?w = "merge (J k) ?D (w, w')" - have [simp]: "\x. merge (J k) (I - J k) (w, merge ?D (I - ?D) (w', x)) = - merge (J (Suc k)) (I - (J (Suc k))) (?w, x)" - using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"] - by (auto intro!: ext split: split_merge) - have *: "\n. ?M ?D (?M (J k) (A n) w) w' = ?M (J (Suc k)) (A n) ?w" - using w'(1) J(3)[of "Suc k"] - by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+ - show ?thesis - using Suc w' J_mono[of k "Suc k"] unfolding * - by (intro exI[of _ ?w]) - (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff) - qed - qed - then obtain w where w: - "\k. w k \ space (Pi\<^sub>M (J k) M)" - "\k n. ?a / 2 ^ (Suc k) \ ?q k n (w k)" - "\k. restrict (w (Suc k)) (J k) = w k" - by metis - - { fix k - from w have "?a / 2 ^ (k + 1) \ ?q k k (w k)" by auto - then have "?M (J k) (A k) (w k) \ {}" - using positive_mu_G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \ 1` - by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq) - then obtain x where "x \ ?M (J k) (A k) (w k)" by auto - then have "merge (J k) (I - J k) (w k, x) \ A k" by auto - then have "\x\A k. restrict x (J k) = w k" - using `w k \ space (Pi\<^sub>M (J k) M)` - by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM) } - note w_ext = this +lemma (in product_prob_space) emeasure_PiM_emb': + "J \ I \ finite J \ X \ sets (PiM J M) \ emeasure (Pi\<^sub>M I M) (emb I J X) = PiM J M X" + by (subst distr_PiM_restrict_finite[symmetric, of J]) + (auto intro!: emeasure_distr_restrict[symmetric]) - { fix k l i assume "k \ l" "i \ J k" - { fix l have "w k i = w (k + l) i" - proof (induct l) - case (Suc l) - from `i \ J k` J_mono[of k "k + l"] have "i \ J (k + l)" by auto - with w(3)[of "k + l"] - have "w (k + l) i = w (k + Suc l) i" - by (auto simp: restrict_def fun_eq_iff split: split_if_asm) - with Suc show ?case by simp - qed simp } - from this[of "l - k"] `k \ l` have "w l i = w k i" by simp } - note w_mono = this - - def w' \ "\i. if i \ (\k. J k) then w (LEAST k. i \ J k) i else if i \ I then (SOME x. x \ space (M i)) else undefined" - { fix i k assume k: "i \ J k" - have "w k i = w (LEAST k. i \ J k) i" - by (intro w_mono Least_le k LeastI[of _ k]) - then have "w' i = w k i" - unfolding w'_def using k by auto } - note w'_eq = this - have w'_simps1: "\i. i \ I \ w' i = undefined" - using J by (auto simp: w'_def) - have w'_simps2: "\i. i \ (\k. J k) \ i \ I \ w' i \ space (M i)" - using J by (auto simp: w'_def intro!: someI_ex[OF M.not_empty[unfolded ex_in_conv[symmetric]]]) - { fix i assume "i \ I" then have "w' i \ space (M i)" - using w(1) by (cases "i \ (\k. J k)") (force simp: w'_simps2 w'_eq space_PiM)+ } - note w'_simps[simp] = w'_eq w'_simps1 w'_simps2 this - - have w': "w' \ space (Pi\<^sub>M I M)" - using w(1) by (auto simp add: Pi_iff extensional_def space_PiM) - - { fix n - have "restrict w' (J n) = w n" using w(1)[of n] - by (auto simp add: fun_eq_iff space_PiM) - with w_ext[of n] obtain x where "x \ A n" "restrict x (J n) = restrict w' (J n)" - by auto - then have "w' \ A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) } - then have "w' \ (\i. A i)" by auto - with `(\i. A i) = {}` show False by auto - qed - ultimately show "(\i. \G (A i)) ----> 0" - using LIMSEQ_INF[of "\i. \G (A i)"] by simp - qed fact+ - then guess \ .. note \ = this - show ?thesis - proof (subst emeasure_extend_measure_Pair[OF PiM_def, of I M \ J X]) - from assms show "(J \ {} \ I = {}) \ finite J \ J \ I \ X \ (\ j\J. sets (M j))" - by (simp add: Pi_iff) - next - fix J X assume J: "(J \ {} \ I = {}) \ finite J \ J \ I \ X \ (\ j\J. sets (M j))" - then show "emb I J (Pi\<^sub>E J X) \ Pow (\\<^sub>E i\I. space (M i))" - by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space) - have "emb I J (Pi\<^sub>E J X) \ generator" - using J `I \ {}` by (intro generatorI') (auto simp: Pi_iff) - then have "\ (emb I J (Pi\<^sub>E J X)) = \G (emb I J (Pi\<^sub>E J X))" - using \ by simp - also have "\ = (\ j\J. if j \ J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))" - using J `I \ {}` by (subst mu_G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff) - also have "\ = (\j\J \ {i \ I. emeasure (M i) (space (M i)) \ 1}. - if j \ J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))" - using J `I \ {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1) - finally show "\ (emb I J (Pi\<^sub>E J X)) = \" . - next - let ?F = "\j. if j \ J then emeasure (M j) (X j) else emeasure (M j) (space (M j))" - have "(\j\J \ {i \ I. emeasure (M i) (space (M i)) \ 1}. ?F j) = (\j\J. ?F j)" - using X `I \ {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1) - then show "(\j\J \ {i \ I. emeasure (M i) (space (M i)) \ 1}. ?F j) = - emeasure (Pi\<^sub>M J M) (Pi\<^sub>E J X)" - using X by (auto simp add: emeasure_PiM) - next - show "positive (sets (Pi\<^sub>M I M)) \" "countably_additive (sets (Pi\<^sub>M I M)) \" - using \ unfolding sets_PiM_generator by (auto simp: measure_space_def) - qed -qed +lemma (in product_prob_space) emeasure_PiM_emb: + "J \ I \ finite J \ (\i. i \ J \ X i \ sets (M i)) \ + emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = (\ i\J. emeasure (M i) (X i))" + by (subst emeasure_PiM_emb') (auto intro!: emeasure_PiM) sublocale product_prob_space \ P: prob_space "Pi\<^sub>M I M" proof + have *: "emb I {} {\x. undefined} = space (PiM I M)" + by (auto simp: prod_emb_def space_PiM) show "emeasure (Pi\<^sub>M I M) (space (Pi\<^sub>M I M)) = 1" - proof cases - assume "I = {}" then show ?thesis by (simp add: space_PiM_empty) - next - assume "I \ {}" - then obtain i where i: "i \ I" by auto - then have "emb I {i} (\\<^sub>E i\{i}. space (M i)) = (space (Pi\<^sub>M I M))" - by (auto simp: prod_emb_def space_PiM) - with i show ?thesis - using emeasure_PiM_emb_not_empty[of "{i}" "\i. space (M i)"] - by (simp add: emeasure_PiM emeasure_space_1) - qed -qed - -lemma (in product_prob_space) emeasure_PiM_emb: - assumes X: "J \ I" "finite J" "\i. i \ J \ X i \ sets (M i)" - shows "emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = (\ i\J. emeasure (M i) (X i))" -proof cases - assume "J = {}" - moreover have "emb I {} {\x. undefined} = space (Pi\<^sub>M I M)" - by (auto simp: space_PiM prod_emb_def) - ultimately show ?thesis - by (simp add: space_PiM_empty P.emeasure_space_1) -next - assume "J \ {}" with X show ?thesis - by (subst emeasure_PiM_emb_not_empty) (auto simp: emeasure_PiM) + using emeasure_PiM_emb[of "{}" "\_. {}"] by (simp add: *) qed lemma (in product_prob_space) emeasure_PiM_Collect: @@ -388,7 +102,6 @@ qed simp lemma (in product_prob_space) PiM_eq: - assumes "I \ {}" assumes "sets M' = sets (PiM I M)" assumes eq: "\J F. finite J \ J \ I \ (\j. j \ J \ F j \ sets (M j)) \ emeasure M' (prod_emb I M J (\\<^sub>E j\J. F j)) = (\j\J. emeasure (M j) (F j))" @@ -400,15 +113,15 @@ unfolding `sets M' = sets (PiM I M)` by simp def i \ "SOME i. i \ I" - with `I \ {}` have i: "i \ I" - by (auto intro: someI_ex) + have i: "I \ {} \ i \ I" + unfolding i_def by (rule someI_ex) auto - def A \ "\n::nat. prod_emb I M {i} (\\<^sub>E j\{i}. space (M i))" + def A \ "\n::nat. if I = {} then prod_emb I M {} (\\<^sub>E i\{}. {}) else prod_emb I M {i} (\\<^sub>E i\{i}. space (M i))" then show "range A \ prod_algebra I M" - by (auto intro!: prod_algebraI i) + using prod_algebraI[of "{}" I "\i. space (M i)" M] by (auto intro!: prod_algebraI i) have A_eq: "\i. A i = space (PiM I M)" - by (auto simp: prod_emb_def space_PiM Pi_iff A_def i) + by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI) show "(\i. A i) = (\\<^sub>E i\I. space (M i))" unfolding A_eq by (auto simp: space_PiM) show "\i. emeasure (PiM I M) (A i) \ \" diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Wed Oct 07 17:11:16 2015 +0200 @@ -555,6 +555,53 @@ unfolding ereal_minus_eq_minus_iff using finite A0 by auto qed +lemma emeasure_INT_decseq_subset: + fixes F :: "nat \ 'a set" + assumes I: "I \ {}" and F: "\i j. i \ I \ j \ I \ i \ j \ F j \ F i" + assumes F_sets[measurable]: "\i. i \ I \ F i \ sets M" + and fin: "\i. i \ I \ emeasure M (F i) \ \" + shows "emeasure M (\i\I. F i) = (INF i:I. emeasure M (F i))" +proof cases + assume "finite I" + have "(\i\I. F i) = F (Max I)" + using I \finite I\ by (intro antisym INF_lower INF_greatest F) auto + moreover have "(INF i:I. emeasure M (F i)) = emeasure M (F (Max I))" + using I \finite I\ by (intro antisym INF_lower INF_greatest F emeasure_mono) auto + ultimately show ?thesis + by simp +next + assume "infinite I" + def L \ "\n. LEAST i. i \ I \ i \ n" + have L: "L n \ I \ n \ L n" for n + unfolding L_def + proof (rule LeastI_ex) + show "\x. x \ I \ n \ x" + using \infinite I\ finite_subset[of I "{..< n}"] + by (rule_tac ccontr) (auto simp: not_le) + qed + have L_eq[simp]: "i \ I \ L i = i" for i + unfolding L_def by (intro Least_equality) auto + have L_mono: "i \ j \ L i \ L j" for i j + using L[of j] unfolding L_def by (intro Least_le) (auto simp: L_def) + + have "emeasure M (\i. F (L i)) = (INF i. emeasure M (F (L i)))" + proof (intro INF_emeasure_decseq[symmetric]) + show "decseq (\i. F (L i))" + using L by (intro antimonoI F L_mono) auto + qed (insert L fin, auto) + also have "\ = (INF i:I. emeasure M (F i))" + proof (intro antisym INF_greatest) + show "i \ I \ (INF i. emeasure M (F (L i))) \ emeasure M (F i)" for i + by (intro INF_lower2[of i]) auto + qed (insert L, auto intro: INF_lower) + also have "(\i. F (L i)) = (\i\I. F i)" + proof (intro antisym INF_greatest) + show "i \ I \ (\i. F (L i)) \ F i" for i + by (intro INF_lower2[of i]) auto + qed (insert L, auto) + finally show ?thesis . +qed + lemma Lim_emeasure_decseq: assumes A: "range A \ sets M" "decseq A" and fin: "\i. emeasure M (A i) \ \" shows "(\i. emeasure M (A i)) ----> emeasure M (\i. A i)" diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Oct 07 17:11:16 2015 +0200 @@ -1511,8 +1511,10 @@ qed lemma nn_integral_monotone_convergence_INF: - assumes f: "decseq f" and [measurable]: "\i. f i \ borel_measurable M" - assumes fin: "(\\<^sup>+ x. f i x \M) < \" + fixes f :: "nat \ 'a \ ereal" + assumes f: "\i j x. i \ j \ x \ space M \ f j x \ f i x" + and [measurable]: "\i. f i \ borel_measurable M" + and fin: "(\\<^sup>+ x. f i x \M) < \" shows "(\\<^sup>+ x. (INF i. f i x) \M) = (INF i. integral\<^sup>N M (f i))" proof - { fix f :: "nat \ ereal" and j assume "decseq f" @@ -1523,28 +1525,33 @@ done } note INF_shift = this - have dec: "\f::nat \ 'a \ ereal. decseq f \ decseq (\j x. max 0 (f (j + i) x))" - by (intro antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def) + have dec: "decseq (\j x. max 0 (restrict (f (j + i)) (space M) x))" + using f by (intro antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def) - have "(\\<^sup>+ x. max 0 (INF i. f i x) \M) = (\\<^sup>+ x. (INF i. max 0 (f i x)) \M)" + have "(\\<^sup>+ x. max 0 (INF i. f i x) \M) = (\\<^sup>+ x. (INF i. max 0 (restrict (f i) (space M) x)) \M)" by (intro nn_integral_cong) (simp add: sup_ereal_def[symmetric] sup_INF del: sup_ereal_def) - also have "\ = (\\<^sup>+ x. (INF j. max 0 (f (j + i) x)) \M)" + also have "\ = (\\<^sup>+ x. (INF j. max 0 (restrict (f (j + i)) (space M) x)) \M)" using f by (intro nn_integral_cong INF_shift antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def) - also have "\ = (INF j. (\\<^sup>+ x. max 0 (f (j + i) x) \M))" + also have "\ = (INF j. (\\<^sup>+ x. max 0 (restrict (f (j + i)) (space M) x) \M))" proof (rule nn_integral_monotone_convergence_INF') - show "\j. (\x. max 0 (f (j + i) x)) \ borel_measurable M" - by measurable - show "(\\<^sup>+ x. max 0 (f (0 + i) x) \M) < \" - using fin by (simp add: nn_integral_max_0) + show "(\x. max 0 (restrict (f (j + i)) (space M) x)) \ borel_measurable M" for j + by (subst measurable_cong[where g="\x. max 0 (f (j + i) x)"]) measurable + show "(\\<^sup>+ x. max 0 (restrict (f (0 + i)) (space M) x) \M) < \" + using fin by (simp add: nn_integral_max_0 cong: nn_integral_cong) qed (intro max.cobounded1 dec f)+ - also have "\ = (INF j. (\\<^sup>+ x. max 0 (f j x) \M))" + also have "\ = (INF j. (\\<^sup>+ x. max 0 (restrict (f j) (space M) x) \M))" using f by (intro INF_shift[symmetric] nn_integral_mono antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def) - finally show ?thesis unfolding nn_integral_max_0 . + finally show ?thesis unfolding nn_integral_max_0 by (simp cong: nn_integral_cong) qed +lemma nn_integral_monotone_convergence_INF_decseq: + assumes f: "decseq f" and *: "\i. f i \ borel_measurable M" "(\\<^sup>+ x. f i x \M) < \" + shows "(\\<^sup>+ x. (INF i. f i x) \M) = (INF i. integral\<^sup>N M (f i))" + using nn_integral_monotone_convergence_INF[of M f i, OF _ *] f by (auto simp: antimono_def le_fun_def) + lemma sup_continuous_nn_integral[order_continuous_intros]: assumes f: "\y. sup_continuous (f y)" assumes [measurable]: "\x. (\y. f y x) \ borel_measurable M" @@ -1771,7 +1778,7 @@ fix C :: "nat \ 'b \ ereal" assume "decseq C" "\i. C i \ borel_measurable N \ (\s. integral\<^sup>N (M s) (C i) < \)" then show "(\s. \\<^sup>+x. (INF i. C i) x \M s) = (INF i. (\s. \\<^sup>+x. C i x \M s))" unfolding INF_apply[abs_def] - by (subst nn_integral_monotone_convergence_INF) + by (subst nn_integral_monotone_convergence_INF_decseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets) next show "\x. g x \ (\s. integral\<^sup>N (M s) (f top))" @@ -1782,7 +1789,7 @@ fix C assume "\i::nat. C i \ borel_measurable N \ (\s. integral\<^sup>N (M s) (C i) < \)" "decseq C" with bound show "INFIMUM UNIV C \ borel_measurable N \ (\s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \)" unfolding INF_apply[abs_def] - by (subst nn_integral_monotone_convergence_INF) + by (subst nn_integral_monotone_convergence_INF_decseq) (auto cong: measurable_cong_sets intro!: borel_measurable_INF simp: INF_less_iff simp del: ereal_infty_less(1)) next diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Probability.thy Wed Oct 07 17:11:16 2015 +0200 @@ -12,9 +12,7 @@ Probability_Mass_Function Stream_Space Embed_Measure - Interval_Integral - Set_Integral - Giry_Monad begin end + diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Wed Oct 07 17:11:16 2015 +0200 @@ -43,6 +43,16 @@ by (auto simp: emeasure_distr emeasure_space_1) qed +lemma prob_space_distrD: + assumes f: "f \ measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M" +proof + interpret M!: prob_space "distr M N f" by fact + have "f -` space N \ space M = space M" + using f[THEN measurable_space] by auto + then show "emeasure M (space M) = 1" + using M.emeasure_space_1 by (simp add: emeasure_distr[OF f]) +qed + lemma (in prob_space) prob_space: "prob (space M) = 1" using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def) @@ -1152,4 +1162,53 @@ "finite S \ (\s. s \ S \ 0 \ p s) \ (\s\S. p s) = 1 \ prob_space (point_measure S p)" by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite) +lemma (in prob_space) distr_pair_fst: "distr (N \\<^sub>M M) N fst = N" +proof (intro measure_eqI) + fix A assume A: "A \ sets (distr (N \\<^sub>M M) N fst)" + from A have "emeasure (distr (N \\<^sub>M M) N fst) A = emeasure (N \\<^sub>M M) (A \ space M)" + by (auto simp add: emeasure_distr space_pair_measure dest: sets.sets_into_space intro!: arg_cong2[where f=emeasure]) + with A show "emeasure (distr (N \\<^sub>M M) N fst) A = emeasure N A" + by (simp add: emeasure_pair_measure_Times emeasure_space_1) +qed simp + +lemma (in product_prob_space) distr_reorder: + assumes "inj_on t J" "t \ J \ K" "finite K" + shows "distr (PiM K M) (Pi\<^sub>M J (\x. M (t x))) (\\. \n\J. \ (t n)) = PiM J (\x. M (t x))" +proof (rule product_sigma_finite.PiM_eqI) + show "product_sigma_finite (\x. M (t x))" .. + have "t`J \ K" using assms by auto + then show [simp]: "finite J" + by (rule finite_imageD[OF finite_subset]) fact+ + fix A assume A: "\i. i \ J \ A i \ sets (M (t i))" + moreover have "((\\. \n\J. \ (t n)) -` Pi\<^sub>E J A \ space (Pi\<^sub>M K M)) = + (\\<^sub>E i\K. if i \ t`J then A (the_inv_into J t i) else space (M i))" + using A A[THEN sets.sets_into_space] \t \ J \ K\ \inj_on t J\ + by (subst prod_emb_Pi[symmetric]) (auto simp: space_PiM PiE_iff the_inv_into_f_f prod_emb_def) + ultimately show "distr (Pi\<^sub>M K M) (Pi\<^sub>M J (\x. M (t x))) (\\. \n\J. \ (t n)) (Pi\<^sub>E J A) = (\i\J. M (t i) (A i))" + using assms + apply (subst emeasure_distr) + apply (auto intro!: sets_PiM_I_finite simp: Pi_iff) + apply (subst emeasure_PiM) + apply (auto simp: the_inv_into_f_f \inj_on t J\ setprod.reindex[OF \inj_on t J\] + if_distrib[where f="emeasure (M _)"] setprod.If_cases emeasure_space_1 Int_absorb1 \t`J \ K\) + done +qed simp + +lemma (in product_prob_space) distr_restrict: + "J \ K \ finite K \ (\\<^sub>M i\J. M i) = distr (\\<^sub>M i\K. M i) (\\<^sub>M i\J. M i) (\f. restrict f J)" + using distr_reorder[of "\x. x" J K] by (simp add: Pi_iff subset_eq) + +lemma (in product_prob_space) emeasure_prod_emb[simp]: + assumes L: "J \ L" "finite L" and X: "X \ sets (Pi\<^sub>M J M)" + shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X" + by (subst distr_restrict[OF L]) + (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X) + +lemma emeasure_distr_restrict: + assumes "I \ K" and Q[measurable_cong]: "sets Q = sets (PiM K M)" and A[measurable]: "A \ sets (PiM I M)" + shows "emeasure (distr Q (PiM I M) (\\. restrict \ I)) A = emeasure Q (prod_emb K M I A)" + using \I\K\ sets_eq_imp_space_eq[OF Q] + by (subst emeasure_distr) + (auto simp: measurable_cong_sets[OF Q] prod_emb_def space_PiM[symmetric] intro!: measurable_restrict) + end diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Projective_Family.thy --- a/src/HOL/Probability/Projective_Family.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Projective_Family.thy Wed Oct 07 17:11:16 2015 +0200 @@ -6,342 +6,672 @@ section {*Projective Family*} theory Projective_Family -imports Finite_Product_Measure Probability_Measure +imports Finite_Product_Measure Giry_Monad begin -lemma (in product_prob_space) distr_restrict: - assumes "J \ {}" "J \ K" "finite K" - shows "(\\<^sub>M i\J. M i) = distr (\\<^sub>M i\K. M i) (\\<^sub>M i\J. M i) (\f. restrict f J)" (is "?P = ?D") -proof (rule measure_eqI_generator_eq) - have "finite J" using `J \ K` `finite K` by (auto simp add: finite_subset) - interpret J: finite_product_prob_space M J proof qed fact - interpret K: finite_product_prob_space M K proof qed fact - - let ?J = "{Pi\<^sub>E J E | E. \i\J. E i \ sets (M i)}" - let ?F = "\i. \\<^sub>E k\J. space (M k)" - let ?\ = "(\\<^sub>E k\J. space (M k))" - show "Int_stable ?J" - by (rule Int_stable_PiE) - show "range ?F \ ?J" "(\i. ?F i) = ?\" - using `finite J` by (auto intro!: prod_algebraI_finite) - { fix i show "emeasure ?P (?F i) \ \" by simp } - show "?J \ Pow ?\" by (auto simp: Pi_iff dest: sets.sets_into_space) - show "sets (\\<^sub>M i\J. M i) = sigma_sets ?\ ?J" "sets ?D = sigma_sets ?\ ?J" - using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) - - fix X assume "X \ ?J" - then obtain E where [simp]: "X = Pi\<^sub>E J E" and E: "\i\J. E i \ sets (M i)" by auto - with `finite J` have X: "X \ sets (Pi\<^sub>M J M)" - by simp - - have "emeasure ?P X = (\ i\J. emeasure (M i) (E i))" - using E by (simp add: J.measure_times) - also have "\ = (\ i\J. emeasure (M i) (if i \ J then E i else space (M i)))" - by simp - also have "\ = (\ i\K. emeasure (M i) (if i \ J then E i else space (M i)))" - using `finite K` `J \ K` - by (intro setprod.mono_neutral_left) (auto simp: M.emeasure_space_1) - also have "\ = emeasure (Pi\<^sub>M K M) (\\<^sub>E i\K. if i \ J then E i else space (M i))" - using E by (simp add: K.measure_times) - also have "(\\<^sub>E i\K. if i \ J then E i else space (M i)) = (\f. restrict f J) -` Pi\<^sub>E J E \ (\\<^sub>E i\K. space (M i))" - using `J \ K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm) - finally show "emeasure (Pi\<^sub>M J M) X = emeasure ?D X" - using X `J \ K` apply (subst emeasure_distr) - by (auto intro!: measurable_restrict_subset simp: space_PiM) +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 `J \ I` PiE_cancel_merge[of "J" "I - J" x y S] \x\A\ + 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 `J \ I` PiE_cancel_merge[of "J" "I - J" x y S] \x\A\ eq + by (auto simp del: PiE_cancel_merge simp add: Un_absorb1) + qed (insert \x\A\ sets, auto) qed -lemma (in product_prob_space) emeasure_prod_emb[simp]: - assumes L: "J \ {}" "J \ L" "finite L" and X: "X \ sets (Pi\<^sub>M J M)" - shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X" - by (subst distr_restrict[OF L]) - (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X) - -definition - limP :: "'i set \ ('i \ 'a measure) \ ('i set \ ('i \ 'a) measure) \ ('i \ 'a) measure" where - "limP I M P = extend_measure (\\<^sub>E i\I. space (M i)) - {(J, X). (J \ {} \ I = {}) \ finite J \ J \ I \ X \ (\ j\J. sets (M j))} - (\(J, X). prod_emb I M J (\\<^sub>E j\J. X j)) - (\(J, X). emeasure (P J) (Pi\<^sub>E J X))" - -abbreviation "lim\<^sub>P \ limP" - -lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)" - by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure) - -lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)" - by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure) - -lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\\<^sub>M i\I. M i) M'" - unfolding measurable_def by auto - -lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\\<^sub>M i\I. M i)" - unfolding measurable_def by auto - locale projective_family = - fixes I::"'i set" and P::"'i set \ ('i \ 'a) measure" and M::"('i \ 'a measure)" - assumes projective: "\J H X. J \ {} \ J \ H \ H \ I \ finite H \ X \ sets (PiM J M) \ - (P H) (prod_emb H M J X) = (P J) X" - assumes proj_prob_space: "\J. finite J \ prob_space (P J)" - assumes proj_space: "\J. finite J \ space (P J) = space (PiM J M)" - assumes proj_sets: "\J. finite J \ sets (P J) = sets (PiM J M)" + 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 emeasure_limP: - assumes "finite J" - assumes "J \ I" - assumes A: "\i. i\J \ A i \ sets (M i)" - shows "emeasure (limP J M P) (Pi\<^sub>E J A) = emeasure (P J) (Pi\<^sub>E J A)" -proof - - have "Pi\<^sub>E J (restrict A J) \ (\\<^sub>E i\J. space (M i))" - using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast - hence "emeasure (limP J M P) (Pi\<^sub>E J A) = - emeasure (limP J M P) (prod_emb J M J (Pi\<^sub>E J A))" - using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def) - also have "\ = emeasure (P J) (Pi\<^sub>E J A)" - proof (rule emeasure_extend_measure_Pair[OF limP_def]) - show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto - show "countably_additive (sets (limP J M P)) (P J)" unfolding countably_additive_def - by (auto simp: suminf_emeasure proj_sets[OF `finite J`]) - show "(J \ {} \ J = {}) \ finite J \ J \ J \ A \ (\ j\J. sets (M j))" - using assms by auto - fix K and X::"'i \ 'a set" - show "prod_emb J M K (Pi\<^sub>E K X) \ Pow (\\<^sub>E i\J. space (M i))" - by (auto simp: prod_emb_def) - assume JX: "(K \ {} \ J = {}) \ finite K \ K \ J \ X \ (\ j\K. sets (M j))" - thus "emeasure (P J) (prod_emb J M K (Pi\<^sub>E K X)) = emeasure (P K) (Pi\<^sub>E K X)" - using assms - apply (cases "J = {}") - apply (simp add: prod_emb_id) - apply (fastforce simp add: intro!: projective sets_PiM_I_finite) - done - qed - finally show ?thesis . -qed +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 limP_finite[simp]: - assumes "finite J" - assumes "J \ I" - shows "limP J M P = P J" (is "?P = _") -proof (rule measure_eqI_generator_eq) - let ?J = "{Pi\<^sub>E J E | E. \i\J. E i \ sets (M i)}" - let ?\ = "(\\<^sub>E k\J. space (M k))" - interpret prob_space "P J" using proj_prob_space `finite J` by simp - show "emeasure ?P (\\<^sub>E k\J. space (M k)) \ \" using assms `finite J` by (auto simp: emeasure_limP) - show "sets (limP J M P) = sigma_sets ?\ ?J" "sets (P J) = sigma_sets ?\ ?J" - using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) - fix X assume "X \ ?J" - then obtain E where X: "X = Pi\<^sub>E J E" and E: "\i\J. E i \ sets (M i)" by auto - with `finite J` have "X \ sets (limP J M P)" by simp - have emb_self: "prod_emb J M J (Pi\<^sub>E J E) = Pi\<^sub>E J E" - using E sets.sets_into_space - by (auto intro!: prod_emb_PiE_same_index) - show "emeasure (limP J M P) X = emeasure (P J) X" - unfolding X using E - by (intro emeasure_limP assms) simp -qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE) +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 emeasure_fun_emb[simp]: - assumes L: "J \ {}" "J \ L" "finite L" "L \ I" and X: "X \ sets (PiM J M)" - shows "emeasure (limP L M P) (prod_emb L M J X) = emeasure (limP J M P) X" - using assms - by (subst limP_finite) (auto simp: limP_finite finite_subset projective) +lemma not_empty: "space (PiM I M) \ {}" + by (simp add: not_empty_M) abbreviation - "emb L K X \ prod_emb L M K X" + "emb L K \ prod_emb L M K" -lemma prod_emb_injective: - assumes "J \ L" 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 injective_vimage_restrict) +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) - have "\i\L. \x. x \ space (M i)" - proof - fix i assume "i \ L" - interpret prob_space "P {i}" using proj_prob_space by simp - from not_empty show "\x. x \ space (M i)" by (auto simp add: proj_space space_PiM) - qed - from bchoice[OF this] - show "(\\<^sub>E i\L. space (M i)) \ {}" by (auto simp: PiE_def) - 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 `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def) + show "(\\<^sub>E i\L. space (M i)) \ {}" + using \L \ I\ 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 `prod_emb L M J X \ prod_emb L M J Y` by (simp add: prod_emb_def) qed fact -definition generator :: "('i \ 'a) set set" where - "generator = (\J\{J. J \ {} \ finite J \ J \ I}. emb I J ` sets (Pi\<^sub>M J M))" +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) -lemma generatorI': - "J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ emb I J X \ generator" - unfolding generator_def by auto +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) -lemma algebra_generator: - assumes "I \ {}" shows "algebra (\\<^sub>E i\I. space (M i)) generator" (is "algebra ?\ ?G") - unfolding algebra_def algebra_axioms_def ring_of_sets_iff -proof (intro conjI ballI) - let ?G = generator - show "?G \ Pow ?\" - by (auto simp: generator_def prod_emb_def) - from `I \ {}` obtain i where "i \ I" by auto - then show "{} \ ?G" - by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\i. {}"] - simp: sigma_sets.Empty generator_def prod_emb_def) - from `i \ I` show "?\ \ ?G" - by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^sub>E {i} (\i. space (M i))"] - simp: generator_def prod_emb_def) - fix A assume "A \ ?G" - then obtain JA XA where XA: "JA \ {}" "finite JA" "JA \ I" "XA \ sets (Pi\<^sub>M JA M)" and A: "A = emb I JA XA" - by (auto simp: generator_def) - fix B assume "B \ ?G" - then obtain JB XB where XB: "JB \ {}" "finite JB" "JB \ I" "XB \ sets (Pi\<^sub>M JB M)" and B: "B = emb I JB XB" - by (auto simp: generator_def) - let ?RA = "emb (JA \ JB) JA XA" - let ?RB = "emb (JA \ JB) JB XB" - have *: "A - B = emb I (JA \ JB) (?RA - ?RB)" "A \ B = emb I (JA \ JB) (?RA \ ?RB)" - using XA A XB B by auto - show "A - B \ ?G" "A \ B \ ?G" - unfolding * using XA XB by (safe intro!: generatorI') auto -qed + 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]) -lemma sets_PiM_generator: - "sets (PiM I M) = sigma_sets (\\<^sub>E i\I. space (M i)) generator" -proof cases - assume "I = {}" then show ?thesis - unfolding generator_def - by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong) -next - assume "I \ {}" - show ?thesis - proof - show "sets (Pi\<^sub>M I M) \ sigma_sets (\\<^sub>E i\I. space (M i)) generator" - unfolding sets_PiM - proof (safe intro!: sigma_sets_subseteq) - fix A assume "A \ prod_algebra I M" with `I \ {}` show "A \ generator" - by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE) - qed - qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset) -qed +interpretation generator!: algebra "space (PiM I M)" generator + by (rule algebra_generator) -lemma generatorI: - "J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ A = emb I J X \ A \ generator" - unfolding generator_def by auto +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 \i\I\ A show "{f \ space (Pi\<^sub>M I M). f i \ A} \ 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. J \ {} \ finite J \ J \ I \ (\X\sets (Pi\<^sub>M J M). A = emb I J X \ x = emeasure (limP J M P) X))" + "\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: "J \ {}" "finite J" "J \ I" "A = emb I J X" "X \ sets (Pi\<^sub>M J M)" - shows "\G A = emeasure (limP J M P) X" + 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: "K \ {}" "finite K" "K \ I" "A = emb I K Y" "Y \ sets (Pi\<^sub>M K M)" - have "emeasure (limP K M P) Y = emeasure (limP (K \ J) M P) (emb (K \ J) K Y)" - using K J by (simp del: limP_finite) + 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: prod_emb_injective[of "K \ J" I]) - also have "emeasure (limP (K \ J) M P) (emb (K \ J) J X) = emeasure (limP J M P) X" - using K J by (simp del: limP_finite) - finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" .. + 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 mu_G_eq: - "J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ \G (emb I J X) = emeasure (limP J M P) X" - by (intro mu_G_spec) auto +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 (auto simp: mu_G_spec elim!: generator.cases) +qed -lemma generator_Ex: - assumes *: "A \ generator" - shows "\J X. J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ A = emb I J X \ \G A = emeasure (limP J M P) X" -proof - - from * obtain J X where J: "J \ {}" "finite J" "J \ I" "A = emb I J X" "X \ sets (Pi\<^sub>M J M)" - unfolding generator_def by auto - with mu_G_spec[OF this] show ?thesis by (auto simp del: limP_finite) +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 generatorE: - assumes A: "A \ generator" - obtains J X where "J \ {}" "finite J" "J \ I" "X \ sets (Pi\<^sub>M J M)" "emb I J X = A" "\G A = emeasure (limP J M P) X" - using generator_Ex[OF A] by atomize_elim auto - -lemma merge_sets: - "J \ K = {} \ A \ sets (Pi\<^sub>M (J \ K) M) \ x \ space (Pi\<^sub>M J M) \ (\y. merge J K (x,y)) -` A \ space (Pi\<^sub>M K M) \ sets (Pi\<^sub>M K M)" - by simp - -lemma merge_emb: - assumes "K \ I" "J \ I" and y: "y \ space (Pi\<^sub>M J M)" - shows "((\x. merge J (I - J) (y, x)) -` emb I K X \ space (Pi\<^sub>M I M)) = - emb I (K - J) ((\x. merge J (K - J) (y, x)) -` emb (J \ K) K X \ space (Pi\<^sub>M (K - J) M))" +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 (\i. emb I (J i) (X i)) \ 0 < (INF i. P (J i) (X i)) \ (\i. emb I (J i) (X i)) \ {}" + shows "emeasure lim (emb I J X) = P J X" proof - - have [simp]: "\x J K L. merge J K (y, restrict x L) = merge J (K \ L) (y, x)" - by (auto simp: restrict_def merge_def) - have [simp]: "\x J K L. restrict (merge J K (y, x)) L = merge (J \ L) (K \ L) (y, x)" - by (auto simp: restrict_def merge_def) - have [simp]: "(I - J) \ K = K - J" using `K \ I` `J \ I` by auto - have [simp]: "(K - J) \ (K \ J) = K - J" by auto - have [simp]: "(K - J) \ K = K - J" by auto - from y `K \ I` `J \ I` show ?thesis - by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM) - auto -qed - -lemma positive_mu_G: - assumes "I \ {}" - shows "positive generator \G" -proof - - interpret G!: algebra "\\<^sub>E i\I. space (M i)" generator by (rule algebra_generator) fact + have "\\. (\s\generator. \ s = \G s) \ + measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \" + 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 \ \" + 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 * \decseq A\ 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 \(\i. A i) = {}\ * 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 \decseq A\[THEN decseqD, OF \x\y\] * + by (auto simp: A sets_P del: subsetI intro!: emeasure_mono \x \ y\ + 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 \ where eq: "\s\generator. \ s = \G s" + and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \" + by (metis sets_PiM_generator) show ?thesis - proof (intro positive_def[THEN iffD2] conjI ballI) - from generatorE[OF G.empty_sets] guess J X . note this[simp] - have "X = {}" - by (rule prod_emb_injective[of J I]) simp_all - then show "\G {} = 0" by simp - next - fix A assume "A \ generator" - from generatorE[OF this] guess J X . note this[simp] - show "0 \ \G A" by (simp add: emeasure_nonneg) - qed -qed - -lemma additive_mu_G: - assumes "I \ {}" - shows "additive generator \G" -proof - - interpret G!: algebra "\\<^sub>E i\I. space (M i)" generator by (rule algebra_generator) fact - show ?thesis - proof (intro additive_def[THEN iffD2] ballI impI) - fix A assume "A \ generator" with generatorE guess J X . note J = this - fix B assume "B \ generator" with generatorE guess K Y . note K = this - assume "A \ B = {}" - have JK: "J \ K \ {}" "J \ K \ I" "finite (J \ K)" - using J K by auto - have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}" - apply (rule prod_emb_injective[of "J \ K" I]) - apply (insert `A \ B = {}` JK J K) - apply (simp_all add: sets.Int prod_emb_Int) - done - have AB: "A = emb I (J \ K) (emb (J \ K) J X)" "B = emb I (J \ K) (emb (J \ K) K Y)" - using J K by simp_all - then have "\G (A \ B) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))" - by simp - also have "\ = emeasure (limP (J \ K) M P) (emb (J \ K) J X \ emb (J \ K) K Y)" - using JK J(1, 4) K(1, 4) by (simp add: mu_G_eq sets.Un del: prod_emb_Un) - also have "\ = \G A + \G B" - using J K JK_disj by (simp add: plus_emeasure[symmetric] del: limP_finite) - finally show "\G (A \ B) = \G A + \G B" . + 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 \ projective_family I "\J. PiM J M" M -proof (simp add: projective_family_def, safe) - fix J::"'i set" assume [simp]: "finite J" - interpret f: finite_product_prob_space M J proof qed fact - show "prob_space (Pi\<^sub>M J M)" - proof - show "emeasure (Pi\<^sub>M J M) (space (Pi\<^sub>M J M)) = 1" - by (simp add: space_PiM emeasure_PiM emeasure_space_1) + 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 \ Proof due to Ionescu Tulcea. \ + +locale Ionescu_Tulcea = + fixes P :: "nat \ (nat \ 'a) \ 'a measure" and M :: "nat \ 'a measure" + assumes P[measurable]: "\i. P i \ measurable (PiM {0..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.. {}" + 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.. space (PiM {0.. space (eP n x) = space (PiM {0.. space (PiM {0.. sets (eP n x) = sets (PiM {0.. 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.. \ space (PiM {0.. f \ borel_measurable (PiM {0.. + (\\<^sup>+x. f x \eP n \) = (\\<^sup>+x. f (\(n := x)) \P n \)" + unfolding eP_def + by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..[simp]: "\ \ space (PiM {0.. sets (PiM {0.. A = P n \ ((\x. \(n := x)) -` A \ space (M n))" + using nn_integral_eP[of \ 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 \] 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.. space (PiM {0.. space (C n m x) = space (PiM {0.. space (PiM {0.. sets (C n m x) = sets (PiM {0.. 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..: "\ \ space (PiM {0.. \= C (n + m) l) = C n (m + l) \" +proof (induction l) + case 0 + with \ show ?case + by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty] + distr_cong[OF refl sets_C[symmetric, OF \]]) +next + case (Suc l) with \ 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..x. x \ space (PiM {0.. 0 \ f x" + and x: "x \ space (PiM {0..\<^sup>+x. f x \C n m x) = (\\<^sup>+x. f (restrict x {0..C n m' x)" + using \m \ m'\ +proof (induction rule: dec_induct) + case (step i) + let ?E = "\x. f (restrict x {0..m\i\ 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.. m'" and [simp]: "x \ space (PiM {0..x. restrict x {0.. sets (C n m x)" + with \m \ m'\ show "emeasure (C n m x) A = emeasure (distr (C n m' x) (Pi\<^sub>M {0..x. restrict x {0..m \ m'\]) (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.. 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.. {0.. X \ sets (PiM J M) \ CI J X = C 0 n (\_. undefined) (PF.emb {0.. 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))" + def X \ "\n. (\i\{i. J i \ {0..< n}}. PF.emb {0.. space (PiM {0.. sets (PiM {0.. {0..< n}} = {}") + (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int) + + have dec_X: "n \ m \ X m \ PF.emb {0.. {0..< n}} = {}") + (auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset) + + have dec_X': "PF.emb {0.. PF.emb {0.. {0.. {0.. j" for n i j + by (rule PF.emb_preserve_mono[of "{0.. \ (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:{i. J i \ {0.._. undefined) (PF.emb {0.. = C 0 n (\_. undefined) (\i\{i. J i \ {0.. = 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 \ n assume \: "\ \ space (PiM {0..i. ?C' i \ borel_measurable (P n \)" + using \[measurable, simp] measurable_fun_upd[where J="{0.. \ (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 \ measurable_C[of "Suc n"] + apply (intro INF_cong refl) + apply (subst split_C[symmetric, OF \]) + 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[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 \, THEN prob_space.emeasure_space_1] by simp + finally show "(\\<^sup>+x. ?C' 0 x \P n \) < \" . + next + fix i j :: nat and x assume "i \ j" "x \ space (P n \)" + with \ have \': "\(n := x) \ space (PiM {0..] space_PiM PiE_iff extensional_def) + show "?C' j x \ ?C' i x" + using \i \ j\ by (subst emeasure_C[symmetric, of i]) (auto intro!: emeasure_mono dec_X del: subsetI simp: sets_C space_P \ \') + qed fact + finally have "(\\<^sup>+x. (INF i. ?C' i x) \P n \) \ 0" + by simp + then have "\\<^sub>F x in ae_filter (P n \). 0 < (INF i. ?C' i x)" + using M by (subst (asm) nn_integral_0_iff_AE) + (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le) + 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 \) + 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 ?\ = "\\ n x. (restrict \ {0..i. i < n \ ?\ \ i (\ i) \ X (Suc i)) \ + restrict \ {0.. space (Pi\<^sub>M {0.. 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 \ assume IH: "\i. i < n \ ?\ \ i (\ i) \ X (Suc i) \ 0 < ?L \ i (\ i)" + show "\r. ?\ \ n r \ X (Suc n) \ 0 < ?L \ n r" + proof (rule step) + show "restrict \ {0.. space (Pi\<^sub>M {0.. {0.. where \: "\n. ?\ \ n (\ n) \ X (Suc n)" + by auto + from this[THEN *] have \_space: "\ \ space (PiM UNIV M)" + by (auto simp: space_PiM PiE_iff Ball_def) + have *: "\ \ PF.emb UNIV {0.._space \X 0 \ {}\ 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 \[of i] \_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) + def f \ "from_nat_into (\i. J i)" and 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) ((\\. \n\J i. \ (t n)) \ (\\. restrict \ (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 (UNION UNIV J) 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 \finite (J i)\ 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 diff -r 131fc8c10402 -r e985b52c3eb3 src/HOL/Probability/Projective_Limit.thy --- a/src/HOL/Probability/Projective_Limit.thy Wed Oct 07 15:31:59 2015 +0200 +++ b/src/HOL/Probability/Projective_Limit.thy Wed Oct 07 17:11:16 2015 +0200 @@ -101,440 +101,361 @@ for I::"'i set" and P begin -abbreviation "lim\<^sub>B \ (\J P. limP J (\_. borel) P)" +lemma emeasure_lim_emb: + assumes X: "J \ I" "finite J" "X \ sets (\\<^sub>M i\J. borel)" + shows "lim (emb I J X) = P J X" +proof (rule emeasure_lim) + write mu_G ("\G") + interpret generator: algebra "space (PiM I (\i. borel))" generator + by (rule algebra_generator) + + fix J and B :: "nat \ ('i \ 'a) set" + assume J: "\n. finite (J n)" "\n. J n \ I" "\n. B n \ sets (\\<^sub>M i\J n. borel)" "incseq J" + and B: "decseq (\n. emb I (J n) (B n))" + and "0 < (INF i. P (J i) (B i))" (is "0 < ?a") + moreover have "?a \ 1" + using J by (auto intro!: INF_lower2[of 0] prob_space_P[THEN prob_space.measure_le_1]) + ultimately obtain r where r: "?a = ereal r" "0 < r" "r \ 1" + by (cases "?a") auto + def Z \ "\n. emb I (J n) (B n)" + have Z_mono: "n \ m \ Z m \ Z n" for n m + unfolding Z_def using B[THEN antimonoD, of n m] . + have J_mono: "\n m. n \ m \ J n \ J m" + using \incseq J\ by (force simp: incseq_def) + note [simp] = \\n. finite (J n)\ + interpret prob_space "P (J i)" for i using J prob_space_P by simp + + have P_eq[simp]: + "sets (P (J i)) = sets (\\<^sub>M i\J i. borel)" "space (P (J i)) = space (\\<^sub>M i\J i. borel)" for i + using J by (auto simp: sets_P space_P) + + have "Z i \ generator" for i + unfolding Z_def by (auto intro!: generator.intros J) -lemma emeasure_limB_emb_not_empty: - assumes "I \ {}" - assumes X: "J \ {}" "J \ I" "finite J" "\i\J. B i \ sets borel" - shows "emeasure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = emeasure (lim\<^sub>B J P) (Pi\<^sub>E J B)" -proof - - let ?\ = "\\<^sub>E i\I. space borel" - let ?G = generator - interpret G!: algebra ?\ generator by (intro algebra_generator) fact - note mu_G_mono = - G.additive_increasing[OF positive_mu_G[OF `I \ {}`] additive_mu_G[OF `I \ {}`], - THEN increasingD] - write mu_G ("\G") - - have "\\. (\s\?G. \ s = \G s) \ measure_space ?\ (sigma_sets ?\ ?G) \" - proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G, - OF `I \ {}`, OF `I \ {}`]) - fix A assume "A \ ?G" - with generatorE guess J X . note JX = this - interpret prob_space "P J" using proj_prob_space[OF `finite J`] . - show "\G A \ \" using JX by (simp add: limP_finite) - next - fix Z assume Z: "range Z \ ?G" "decseq Z" "(\i. Z i) = {}" - then have "decseq (\i. \G (Z i))" - by (auto intro!: mu_G_mono simp: decseq_def) - moreover - have "(INF i. \G (Z i)) = 0" + have countable_UN_J: "countable (\n. J n)" by (simp add: countable_finite) + def Utn \ "to_nat_on (\n. J n)" + interpret function_to_finmap "J n" Utn "from_nat_into (\n. J n)" for n + by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J]) + have inj_on_Utn: "inj_on Utn (\n. J n)" + unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on) + hence inj_on_Utn_J: "\n. inj_on Utn (J n)" by (rule subset_inj_on) auto + def P' \ "\n. mapmeasure n (P (J n)) (\_. borel)" + interpret P': prob_space "P' n" for n + unfolding P'_def mapmeasure_def using J + by (auto intro!: prob_space_distr fm_measurable simp: measurable_cong_sets[OF sets_P]) + + let ?SUP = "\n. SUP K : {K. K \ fm n ` (B n) \ compact K}. emeasure (P' n) K" + { fix n + have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))" + using J by (auto simp: P'_def mapmeasure_PiM space_P sets_P) + also + have "\ = ?SUP n" + proof (rule inner_regular) + show "sets (P' n) = sets borel" by (simp add: borel_eq_PiF_borel P'_def) + next + show "fm n ` B n \ sets borel" + unfolding borel_eq_PiF_borel by (auto simp: P'_def fm_image_measurable_finite sets_P J(3)) + qed simp + finally have "emeasure (P (J n)) (B n) = ?SUP n" "?SUP n \ \" "?SUP n \ - \" by auto + } note R = this + have "\n. \K. emeasure (P (J n)) (B n) - emeasure (P' n) K \ 2 powr (-n) * ?a \ compact K \ K \ fm n ` B n" + proof + fix n show "\K. emeasure (P (J n)) (B n) - emeasure (P' n) K \ ereal (2 powr - real n) * ?a \ + compact K \ K \ fm n ` B n" + unfolding R[of n] proof (rule ccontr) - assume "(INF i. \G (Z i)) \ 0" (is "?a \ 0") - moreover have "0 \ ?a" - using Z positive_mu_G[OF `I \ {}`] by (auto intro!: INF_greatest simp: positive_def) - ultimately have "0 < ?a" by auto - hence "?a \ -\" by auto - have "\n. \J B. J \ {} \ finite J \ J \ I \ B \ sets (Pi\<^sub>M J (\_. borel)) \ - Z n = emb I J B \ \G (Z n) = emeasure (lim\<^sub>B J P) B" - using Z by (intro allI generator_Ex) auto - then obtain J' B' where J': "\n. J' n \ {}" "\n. finite (J' n)" "\n. J' n \ I" - "\n. B' n \ sets (\\<^sub>M i\J' n. borel)" - and Z_emb: "\n. Z n = emb I (J' n) (B' n)" - unfolding choice_iff by blast - moreover def J \ "\n. (\i\n. J' i)" - moreover def B \ "\n. emb (J n) (J' n) (B' n)" - ultimately have J: "\n. J n \ {}" "\n. finite (J n)" "\n. J n \ I" - "\n. B n \ sets (\\<^sub>M i\J n. borel)" - by auto - have J_mono: "\n m. n \ m \ J n \ J m" - unfolding J_def by force - have "\n. \j. j \ J n" using J by blast - then obtain j where j: "\n. j n \ J n" - unfolding choice_iff by blast - note [simp] = `\n. finite (J n)` - from J Z_emb have Z_eq: "\n. Z n = emb I (J n) (B n)" "\n. Z n \ ?G" - unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto) - interpret prob_space "P (J i)" for i using proj_prob_space by simp - have "?a \ \G (Z 0)" by (auto intro: INF_lower) - also have "\ < \" using J by (auto simp: Z_eq mu_G_eq limP_finite proj_sets) - finally have "?a \ \" by simp - have "\n. \\G (Z n)\ \ \" unfolding Z_eq using J J_mono - by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq) + assume H: "\ (\K'. ?SUP n - emeasure (P' n) K' \ ereal (2 powr - real n) * ?a \ + compact K' \ K' \ fm n ` B n)" + have "?SUP n \ ?SUP n - 2 powr (-n) * ?a" + proof (intro SUP_least) + fix K + assume "K \ {K. K \ fm n ` B n \ compact K}" + with H have "\ ?SUP n - emeasure (P' n) K \ 2 powr (-n) * ?a" + by auto + hence "?SUP n - emeasure (P' n) K > 2 powr (-n) * ?a" + unfolding not_less[symmetric] by simp + hence "?SUP n - 2 powr (-n) * ?a > emeasure (P' n) K" + using `0 < ?a` by (auto simp add: ereal_less_minus_iff ac_simps) + thus "?SUP n - 2 powr (-n) * ?a \ emeasure (P' n) K" by simp + qed + hence "?SUP n + 0 \ ?SUP n - (2 powr (-n) * ?a)" using `0 < ?a` by simp + hence "?SUP n + 0 \ ?SUP n + - (2 powr (-n) * ?a)" unfolding minus_ereal_def . + hence "0 \ - (2 powr (-n) * ?a)" + using `?SUP n \ \` `?SUP n \ - \` + by (subst (asm) ereal_add_le_add_iff) (auto simp:) + moreover have "ereal (2 powr - real n) * ?a > 0" using `0 < ?a` + by (auto simp: ereal_zero_less_0_iff) + ultimately show False by simp + qed + qed + then obtain K' where K': + "\n. emeasure (P (J n)) (B n) - emeasure (P' n) (K' n) \ ereal (2 powr - real n) * ?a" + "\n. compact (K' n)" "\n. K' n \ fm n ` B n" + unfolding choice_iff by blast + def K \ "\n. fm n -` K' n \ space (Pi\<^sub>M (J n) (\_. borel))" + have K_sets: "\n. K n \ sets (Pi\<^sub>M (J n) (\_. borel))" + unfolding K_def + using compact_imp_closed[OF `compact (K' _)`] + by (intro measurable_sets[OF fm_measurable, of _ "Collect finite"]) + (auto simp: borel_eq_PiF_borel[symmetric]) + have K_B: "\n. K n \ B n" + proof + fix x n assume "x \ K n" + then have fm_in: "fm n x \ fm n ` B n" + using K' by (force simp: K_def) + show "x \ B n" + using `x \ K n` K_sets sets.sets_into_space J(1,2,3)[of n] + by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\_. borel"]) auto + qed + def Z' \ "\n. emb I (J n) (K n)" + have Z': "\n. Z' n \ Z n" + unfolding Z'_def Z_def + proof (rule prod_emb_mono, safe) + fix n x assume "x \ K n" + hence "fm n x \ K' n" "x \ space (Pi\<^sub>M (J n) (\_. borel))" + by (simp_all add: K_def space_P) + note this(1) + also have "K' n \ fm n ` B n" by (simp add: K') + finally have "fm n x \ fm n ` B n" . + thus "x \ B n" + proof safe + fix y assume y: "y \ B n" + hence "y \ space (Pi\<^sub>M (J n) (\_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"] + by (auto simp add: space_P sets_P) + assume "fm n x = fm n y" + note inj_onD[OF inj_on_fm[OF space_borel], + OF `fm n x = fm n y` `x \ space _` `y \ space _`] + with y show "x \ B n" by simp + qed + qed + have "\n. Z' n \ generator" using J K'(2) unfolding Z'_def + by (auto intro!: generator.intros measurable_sets[OF fm_measurable[of _ "Collect finite"]] + simp: K_def borel_eq_PiF_borel[symmetric] compact_imp_closed) + def Y \ "\n. \i\{1..n}. Z' i" + hence "\n k. Y (n + k) \ Y n" by (induct_tac k) (auto simp: Y_def) + hence Y_mono: "\n m. n \ m \ Y m \ Y n" by (auto simp: le_iff_add) + have Y_Z': "\n. n \ 1 \ Y n \ Z' n" by (auto simp: Y_def) + hence Y_Z: "\n. n \ 1 \ Y n \ Z n" using Z' by auto - have countable_UN_J: "countable (\n. J n)" by (simp add: countable_finite) - def Utn \ "to_nat_on (\n. J n)" - interpret function_to_finmap "J n" Utn "from_nat_into (\n. J n)" for n - by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J]) - have inj_on_Utn: "inj_on Utn (\n. J n)" - unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on) - hence inj_on_Utn_J: "\n. inj_on Utn (J n)" by (rule subset_inj_on) auto - def P' \ "\n. mapmeasure n (P (J n)) (\_. borel)" - let ?SUP = "\n. SUP K : {K. K \ fm n ` (B n) \ compact K}. emeasure (P' n) K" - { - fix n - interpret finite_measure "P (J n)" by unfold_locales - have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))" - using J by (auto simp: P'_def mapmeasure_PiM proj_space proj_sets) - also - have "\ = ?SUP n" - proof (rule inner_regular) - show "emeasure (P' n) (space (P' n)) \ \" - unfolding P'_def - by (auto simp: P'_def mapmeasure_PiF fm_measurable proj_space proj_sets) - show "sets (P' n) = sets borel" by (simp add: borel_eq_PiF_borel P'_def) - next - show "fm n ` B n \ sets borel" - unfolding borel_eq_PiF_borel - by (auto simp del: J(2) simp: P'_def fm_image_measurable_finite proj_sets J) - qed - finally - have "emeasure (P (J n)) (B n) = ?SUP n" "?SUP n \ \" "?SUP n \ - \" by auto - } note R = this - have "\n. \K. emeasure (P (J n)) (B n) - emeasure (P' n) K \ 2 powr (-n) * ?a - \ compact K \ K \ fm n ` B n" - proof - fix n - have "emeasure (P' n) (space (P' n)) \ \" - by (simp add: mapmeasure_PiF P'_def proj_space proj_sets) - then interpret finite_measure "P' n" .. - show "\K. emeasure (P (J n)) (B n) - emeasure (P' n) K \ ereal (2 powr - real n) * ?a \ - compact K \ K \ fm n ` B n" - unfolding R - proof (rule ccontr) - assume H: "\ (\K'. ?SUP n - emeasure (P' n) K' \ ereal (2 powr - real n) * ?a \ - compact K' \ K' \ fm n ` B n)" - have "?SUP n \ ?SUP n - 2 powr (-n) * ?a" - proof (intro SUP_least) - fix K - assume "K \ {K. K \ fm n ` B n \ compact K}" - with H have "\ ?SUP n - emeasure (P' n) K \ 2 powr (-n) * ?a" - by auto - hence "?SUP n - emeasure (P' n) K > 2 powr (-n) * ?a" - unfolding not_less[symmetric] by simp - hence "?SUP n - 2 powr (-n) * ?a > emeasure (P' n) K" - using `0 < ?a` by (auto simp add: ereal_less_minus_iff ac_simps) - thus "?SUP n - 2 powr (-n) * ?a \ emeasure (P' n) K" by simp - qed - hence "?SUP n + 0 \ ?SUP n - (2 powr (-n) * ?a)" using `0 < ?a` by simp - hence "?SUP n + 0 \ ?SUP n + - (2 powr (-n) * ?a)" unfolding minus_ereal_def . - hence "0 \ - (2 powr (-n) * ?a)" - using `?SUP _ \ \` `?SUP _ \ - \` - by (subst (asm) ereal_add_le_add_iff) (auto simp:) - moreover have "ereal (2 powr - real n) * ?a > 0" using `0 < ?a` - by (auto simp: ereal_zero_less_0_iff) - ultimately show False by simp - qed - qed - then obtain K' where K': - "\n. emeasure (P (J n)) (B n) - emeasure (P' n) (K' n) \ ereal (2 powr - real n) * ?a" - "\n. compact (K' n)" "\n. K' n \ fm n ` B n" - unfolding choice_iff by blast - def K \ "\n. fm n -` K' n \ space (Pi\<^sub>M (J n) (\_. borel))" - have K_sets: "\n. K n \ sets (Pi\<^sub>M (J n) (\_. borel))" - unfolding K_def - using compact_imp_closed[OF `compact (K' _)`] - by (intro measurable_sets[OF fm_measurable, of _ "Collect finite"]) - (auto simp: borel_eq_PiF_borel[symmetric]) - have K_B: "\n. K n \ B n" - proof - fix x n - assume "x \ K n" hence fm_in: "fm n x \ fm n ` B n" - using K' by (force simp: K_def) - show "x \ B n" - using `x \ K n` K_sets sets.sets_into_space J[of n] - by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\_. borel"]) auto - qed - def Z' \ "\n. emb I (J n) (K n)" - have Z': "\n. Z' n \ Z n" - unfolding Z_eq unfolding Z'_def - proof (rule prod_emb_mono, safe) - fix n x assume "x \ K n" - hence "fm n x \ K' n" "x \ space (Pi\<^sub>M (J n) (\_. borel))" - by (simp_all add: K_def proj_space) - note this(1) - also have "K' n \ fm n ` B n" by (simp add: K') - finally have "fm n x \ fm n ` B n" . - thus "x \ B n" - proof safe - fix y assume y: "y \ B n" - hence "y \ space (Pi\<^sub>M (J n) (\_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"] - by (auto simp add: proj_space proj_sets) - assume "fm n x = fm n y" - note inj_onD[OF inj_on_fm[OF space_borel], - OF `fm n x = fm n y` `x \ space _` `y \ space _`] - with y show "x \ B n" by simp + have Y_notempty: "\n. n \ 1 \ (Y n) \ {}" + proof - + fix n::nat assume "n \ 1" hence "Y n \ Z n" by fact + have "Y n = (\i\{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono + by (auto simp: Y_def Z'_def) + also have "\ = prod_emb I (\_. borel) (J n) (\i\{1..n}. emb (J n) (J i) (K i))" + using `n \ 1` + by (subst prod_emb_INT) auto + finally + have Y_emb: + "Y n = prod_emb I (\_. borel) (J n) (\i\{1..n}. prod_emb (J n) (\_. borel) (J i) (K i))" . + hence "Y n \ generator" using J J_mono K_sets `n \ 1` + by (auto simp del: prod_emb_INT intro!: generator.intros) + have *: "\G (Z n) = P (J n) (B n)" + unfolding Z_def using J by (intro mu_G_spec) auto + then have "\\G (Z n)\ \ \" by auto + note * + moreover have *: "\G (Y n) = P (J n) (\i\{Suc 0..n}. prod_emb (J n) (\_. borel) (J i) (K i))" + unfolding Y_emb using J J_mono K_sets `n \ 1` by (subst mu_G_spec) auto + then have "\\G (Y n)\ \ \" by auto + note * + moreover have "\G (Z n - Y n) = + P (J n) (B n - (\i\{Suc 0..n}. prod_emb (J n) (\_. borel) (J i) (K i)))" + unfolding Z_def Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \ 1` + by (subst mu_G_spec) (auto intro!: sets.Diff) + ultimately + have "\G (Z n) - \G (Y n) = \G (Z n - Y n)" + using J J_mono K_sets `n \ 1` + by (simp only: emeasure_eq_measure Z_def) + (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] set_mp[OF K_B] + simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P) + also have subs: "Z n - Y n \ (\i\{1..n}. (Z i - Z' i))" + using `n \ 1` unfolding Y_def UN_extend_simps(7) by (intro UN_mono Diff_mono Z_mono order_refl) auto + have "Z n - Y n \ generator" "(\i\{1..n}. (Z i - Z' i)) \ generator" + using `Z' _ \ generator` `Z _ \ generator` `Y _ \ generator` by auto + hence "\G (Z n - Y n) \ \G (\i\{1..n}. (Z i - Z' i))" + using subs generator.additive_increasing[OF positive_mu_G additive_mu_G] + unfolding increasing_def by auto + also have "\ \ (\ i\{1..n}. \G (Z i - Z' i))" using `Z _ \ generator` `Z' _ \ generator` + by (intro generator.subadditive[OF positive_mu_G additive_mu_G]) auto + also have "\ \ (\ i\{1..n}. 2 powr -real i * ?a)" + proof (rule setsum_mono) + fix i assume "i \ {1..n}" hence "i \ n" by simp + have "\G (Z i - Z' i) = \G (prod_emb I (\_. borel) (J i) (B i - K i))" + unfolding Z'_def Z_def by simp + also have "\ = P (J i) (B i - K i)" + using J K_sets by (subst mu_G_spec) auto + also have "\ = P (J i) (B i) - P (J i) (K i)" + using K_sets J `K _ \ B _` by (simp add: emeasure_Diff) + also have "\ = P (J i) (B i) - P' i (K' i)" + unfolding K_def P'_def + by (auto simp: mapmeasure_PiF borel_eq_PiF_borel[symmetric] + compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def) + also have "\ \ ereal (2 powr - real i) * ?a" using K'(1)[of i] . + finally show "\G (Z i - Z' i) \ (2 powr - real i) * ?a" . + qed + also have "\ = ereal ((\ i\{1..n}. (2 powr -real i)) * real ?a)" + by (simp add: setsum_left_distrib r) + also have "\ < ereal (1 * real ?a)" unfolding less_ereal.simps + proof (rule mult_strict_right_mono) + have "(\i = 1..n. 2 powr - real i) = (\i = 1.. < 1" by (subst geometric_sum) auto + finally show "(\i = 1..n. 2 powr - real i) < 1" . + qed (auto simp: r ereal_less_real_iff zero_ereal_def[symmetric]) + also have "\ = ?a" by (auto simp: r) + also have "\ \ \G (Z n)" + using J by (auto intro: INF_lower simp: Z_def mu_G_spec) + finally have "\G (Z n) - \G (Y n) < \G (Z n)" . + hence R: "\G (Z n) < \G (Z n) + \G (Y n)" + using `\\G (Y n)\ \ \` by (simp add: ereal_minus_less) + have "0 \ (- \G (Z n)) + \G (Z n)" using `\\G (Z n)\ \ \` by auto + also have "\ < (- \G (Z n)) + (\G (Z n) + \G (Y n))" + apply (rule ereal_less_add[OF _ R]) using `\\G (Z n)\ \ \` by auto + finally have "\G (Y n) > 0" + using `\\G (Z n)\ \ \` by (auto simp: ac_simps zero_ereal_def[symmetric]) + thus "Y n \ {}" using positive_mu_G by (auto simp add: positive_def) + qed + hence "\n\{1..}. \y. y \ Y n" by auto + then obtain y where y: "\n. n \ 1 \ y n \ Y n" unfolding bchoice_iff by force + { + fix t and n m::nat + assume "1 \ n" "n \ m" hence "1 \ m" by simp + from Y_mono[OF `m \ n`] y[OF `1 \ m`] have "y m \ Y n" by auto + also have "\ \ Z' n" using Y_Z'[OF `1 \ n`] . + finally + have "fm n (restrict (y m) (J n)) \ K' n" + unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff) + moreover have "finmap_of (J n) (restrict (y m) (J n)) = finmap_of (J n) (y m)" + using J by (simp add: fm_def) + ultimately have "fm n (y m) \ K' n" by simp + } note fm_in_K' = this + interpret finmap_seqs_into_compact "\n. K' (Suc n)" "\k. fm (Suc k) (y (Suc k))" borel + proof + fix n show "compact (K' n)" by fact + next + fix n + from Y_mono[of n "Suc n"] y[of "Suc n"] have "y (Suc n) \ Y (Suc n)" by auto + also have "\ \ Z' (Suc n)" using Y_Z' by auto + finally + have "fm (Suc n) (restrict (y (Suc n)) (J (Suc n))) \ K' (Suc n)" + unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff) + thus "K' (Suc n) \ {}" by auto + fix k + assume "k \ K' (Suc n)" + with K'[of "Suc n"] sets.sets_into_space have "k \ fm (Suc n) ` B (Suc n)" by auto + then obtain b where "k = fm (Suc n) b" by auto + thus "domain k = domain (fm (Suc n) (y (Suc n)))" + by (simp_all add: fm_def) + next + fix t and n m::nat + assume "n \ m" hence "Suc n \ Suc m" by simp + assume "t \ domain (fm (Suc n) (y (Suc n)))" + then obtain j where j: "t = Utn j" "j \ J (Suc n)" by auto + hence "j \ J (Suc m)" using J_mono[OF `Suc n \ Suc m`] by auto + have img: "fm (Suc n) (y (Suc m)) \ K' (Suc n)" using `n \ m` + by (intro fm_in_K') simp_all + show "(fm (Suc m) (y (Suc m)))\<^sub>F t \ (\k. (k)\<^sub>F t) ` K' (Suc n)" + apply (rule image_eqI[OF _ img]) + using `j \ J (Suc n)` `j \ J (Suc m)` + unfolding j by (subst proj_fm, auto)+ + qed + have "\t. \z. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z" + using diagonal_tendsto .. + then obtain z where z: + "\t. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z t" + unfolding choice_iff by blast + { + fix n :: nat assume "n \ 1" + have "\i. domain (fm n (y (Suc (diagseq i)))) = domain (finmap_of (Utn ` J n) z)" + by simp + moreover + { + fix t + assume t: "t \ domain (finmap_of (Utn ` J n) z)" + hence "t \ Utn ` J n" by simp + then obtain j where j: "t = Utn j" "j \ J n" by auto + have "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> z t" + apply (subst (2) tendsto_iff, subst eventually_sequentially) + proof safe + fix e :: real assume "0 < e" + { fix i and x :: "'i \ 'a" assume i: "i \ n" + assume "t \ domain (fm n x)" + hence "t \ domain (fm i x)" using J_mono[OF `i \ n`] by auto + with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t" + using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn]) + } note index_shift = this + have I: "\i. i \ n \ Suc (diagseq i) \ n" + apply (rule le_SucI) + apply (rule order_trans) apply simp + apply (rule seq_suble[OF subseq_diagseq]) + done + from z + have "\N. \i\N. dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" + unfolding tendsto_iff eventually_sequentially using `0 < e` by auto + then obtain N where N: "\i. i \ N \ + dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" by auto + show "\N. \na\N. dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e " + proof (rule exI[where x="max N n"], safe) + fix na assume "max N n \ na" + hence "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) = + dist ((fm (Suc (diagseq na)) (y (Suc (diagseq na))))\<^sub>F t) (z t)" using t + by (subst index_shift[OF I]) auto + also have "\ < e" using `max N n \ na` by (intro N) simp + finally show "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e" . qed qed - { fix n - have "Z' n \ ?G" using K' unfolding Z'_def - apply (intro generatorI'[OF J(1-3)]) - unfolding K_def proj_space - apply (rule measurable_sets[OF fm_measurable[of _ "Collect finite"]]) - apply (auto simp add: P'_def borel_eq_PiF_borel[symmetric] compact_imp_closed) - done - } - def Y \ "\n. \i\{1..n}. Z' i" - hence "\n k. Y (n + k) \ Y n" by (induct_tac k) (auto simp: Y_def) - hence Y_mono: "\n m. n \ m \ Y m \ Y n" by (auto simp: le_iff_add) - have Y_Z': "\n. n \ 1 \ Y n \ Z' n" by (auto simp: Y_def) - hence Y_Z: "\n. n \ 1 \ Y n \ Z n" using Z' by auto - have Y_notempty: "\n. n \ 1 \ (Y n) \ {}" - proof - - fix n::nat assume "n \ 1" hence "Y n \ Z n" by fact - have "Y n = (\i\{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono - by (auto simp: Y_def Z'_def) - also have "\ = prod_emb I (\_. borel) (J n) (\i\{1..n}. emb (J n) (J i) (K i))" - using `n \ 1` - by (subst prod_emb_INT) auto - finally - have Y_emb: - "Y n = prod_emb I (\_. borel) (J n) - (\i\{1..n}. prod_emb (J n) (\_. borel) (J i) (K i))" . - hence "Y n \ ?G" using J J_mono K_sets `n \ 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto - hence "\\G (Y n)\ \ \" unfolding Y_emb using J J_mono K_sets `n \ 1` - by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq) - interpret finite_measure "(limP (J n) (\_. borel) P)" - proof - have "emeasure (limP (J n) (\_. borel) P) (J n \\<^sub>E space borel) \ \" - using J by (subst emeasure_limP) auto - thus "emeasure (limP (J n) (\_. borel) P) (space (limP (J n) (\_. borel) P)) \ \" - by (simp add: space_PiM) - qed - have "\G (Z n) = limP (J n) (\_. borel) P (B n)" - unfolding Z_eq using J by (auto simp: mu_G_eq) - moreover have "\G (Y n) = - limP (J n) (\_. borel) P (\i\{Suc 0..n}. prod_emb (J n) (\_. borel) (J i) (K i))" - unfolding Y_emb using J J_mono K_sets `n \ 1` by (subst mu_G_eq) auto - moreover have "\G (Z n - Y n) = limP (J n) (\_. borel) P - (B n - (\i\{Suc 0..n}. prod_emb (J n) (\_. borel) (J i) (K i)))" - unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \ 1` - by (subst mu_G_eq) (auto intro!: sets.Diff) - ultimately - have "\G (Z n) - \G (Y n) = \G (Z n - Y n)" - using J J_mono K_sets `n \ 1` - by (simp only: emeasure_eq_measure) - (auto dest!: bspec[where x=n] - simp: extensional_restrict emeasure_eq_measure prod_emb_iff simp del: limP_finite - intro!: measure_Diff[symmetric] set_mp[OF K_B]) - also have subs: "Z n - Y n \ (\i\{1..n}. (Z i - Z' i))" using Z' Z `n \ 1` - unfolding Y_def by (force simp: decseq_def) - have "Z n - Y n \ ?G" "(\i\{1..n}. (Z i - Z' i)) \ ?G" - using `Z' _ \ ?G` `Z _ \ ?G` `Y _ \ ?G` by auto - hence "\G (Z n - Y n) \ \G (\i\{1..n}. (Z i - Z' i))" - using subs G.additive_increasing[OF positive_mu_G[OF `I \ {}`] additive_mu_G[OF `I \ {}`]] - unfolding increasing_def by auto - also have "\ \ (\ i\{1..n}. \G (Z i - Z' i))" using `Z _ \ ?G` `Z' _ \ ?G` - by (intro G.subadditive[OF positive_mu_G additive_mu_G, OF `I \ {}` `I \ {}`]) auto - also have "\ \ (\ i\{1..n}. 2 powr -real i * ?a)" - proof (rule setsum_mono) - fix i assume "i \ {1..n}" hence "i \ n" by simp - have "\G (Z i - Z' i) = \G (prod_emb I (\_. borel) (J i) (B i - K i))" - unfolding Z'_def Z_eq by simp - also have "\ = P (J i) (B i - K i)" - using J K_sets by (subst mu_G_eq) auto - also have "\ = P (J i) (B i) - P (J i) (K i)" - apply (subst emeasure_Diff) using K_sets J `K _ \ B _` apply (auto simp: proj_sets) - done - also have "\ = P (J i) (B i) - P' i (K' i)" - unfolding K_def P'_def - by (auto simp: mapmeasure_PiF proj_space proj_sets borel_eq_PiF_borel[symmetric] - compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def) - also have "\ \ ereal (2 powr - real i) * ?a" using K'(1)[of i] . - finally show "\G (Z i - Z' i) \ (2 powr - real i) * ?a" . - qed - also have "\ = (\ i\{1..n}. ereal (2 powr -real i) * ereal(real ?a))" - using `?a \ \` `?a \ - \` by (subst ereal_real') auto - also have "\ = ereal (\ i\{1..n}. (2 powr -real i) * (real ?a))" by simp - also have "\ = ereal ((\ i\{1..n}. (2 powr -real i)) * real ?a)" - by (simp add: setsum_left_distrib) - also have "\ < ereal (1 * real ?a)" unfolding less_ereal.simps - proof (rule mult_strict_right_mono) - have "(\i = 1..n. 2 powr - real i) = (\i = 1.. < 1" by (subst geometric_sum) auto - finally show "(\i = 1..n. 2 powr - real i) < 1" . - qed (auto simp: - `0 < ?a` `?a \ \` `?a \ - \` ereal_less_real_iff zero_ereal_def[symmetric]) - also have "\ = ?a" using `0 < ?a` `?a \ \` by (auto simp: ereal_real') - also have "\ \ \G (Z n)" by (auto intro: INF_lower) - finally have "\G (Z n) - \G (Y n) < \G (Z n)" . - hence R: "\G (Z n) < \G (Z n) + \G (Y n)" - using `\\G (Y n)\ \ \` by (simp add: ereal_minus_less) - have "0 \ (- \G (Z n)) + \G (Z n)" using `\\G (Z n)\ \ \` by auto - also have "\ < (- \G (Z n)) + (\G (Z n) + \G (Y n))" - apply (rule ereal_less_add[OF _ R]) using `\\G (Z n)\ \ \` by auto - finally have "\G (Y n) > 0" - using `\\G (Z n)\ \ \` by (auto simp: ac_simps zero_ereal_def[symmetric]) - thus "Y n \ {}" using positive_mu_G `I \ {}` by (auto simp add: positive_def) - qed - hence "\n\{1..}. \y. y \ Y n" by auto - then obtain y where y: "\n. n \ 1 \ y n \ Y n" unfolding bchoice_iff by force - { - fix t and n m::nat - assume "1 \ n" "n \ m" hence "1 \ m" by simp - from Y_mono[OF `m \ n`] y[OF `1 \ m`] have "y m \ Y n" by auto - also have "\ \ Z' n" using Y_Z'[OF `1 \ n`] . - finally - have "fm n (restrict (y m) (J n)) \ K' n" - unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff) - moreover have "finmap_of (J n) (restrict (y m) (J n)) = finmap_of (J n) (y m)" - using J by (simp add: fm_def) - ultimately have "fm n (y m) \ K' n" by simp - } note fm_in_K' = this - interpret finmap_seqs_into_compact "\n. K' (Suc n)" "\k. fm (Suc k) (y (Suc k))" borel - proof - fix n show "compact (K' n)" by fact - next - fix n - from Y_mono[of n "Suc n"] y[of "Suc n"] have "y (Suc n) \ Y (Suc n)" by auto - also have "\ \ Z' (Suc n)" using Y_Z' by auto - finally - have "fm (Suc n) (restrict (y (Suc n)) (J (Suc n))) \ K' (Suc n)" - unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff) - thus "K' (Suc n) \ {}" by auto - fix k - assume "k \ K' (Suc n)" - with K'[of "Suc n"] sets.sets_into_space have "k \ fm (Suc n) ` B (Suc n)" by auto - then obtain b where "k = fm (Suc n) b" by auto - thus "domain k = domain (fm (Suc n) (y (Suc n)))" - by (simp_all add: fm_def) - next - fix t and n m::nat - assume "n \ m" hence "Suc n \ Suc m" by simp - assume "t \ domain (fm (Suc n) (y (Suc n)))" - then obtain j where j: "t = Utn j" "j \ J (Suc n)" by auto - hence "j \ J (Suc m)" using J_mono[OF `Suc n \ Suc m`] by auto - have img: "fm (Suc n) (y (Suc m)) \ K' (Suc n)" using `n \ m` - by (intro fm_in_K') simp_all - show "(fm (Suc m) (y (Suc m)))\<^sub>F t \ (\k. (k)\<^sub>F t) ` K' (Suc n)" - apply (rule image_eqI[OF _ img]) - using `j \ J (Suc n)` `j \ J (Suc m)` - unfolding j by (subst proj_fm, auto)+ - qed - have "\t. \z. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z" - using diagonal_tendsto .. - then obtain z where z: - "\t. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z t" - unfolding choice_iff by blast - { - fix n :: nat assume "n \ 1" - have "\i. domain (fm n (y (Suc (diagseq i)))) = domain (finmap_of (Utn ` J n) z)" - by simp - moreover - { - fix t - assume t: "t \ domain (finmap_of (Utn ` J n) z)" - hence "t \ Utn ` J n" by simp - then obtain j where j: "t = Utn j" "j \ J n" by auto - have "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> z t" - apply (subst (2) tendsto_iff, subst eventually_sequentially) - proof safe - fix e :: real assume "0 < e" - { fix i x - assume i: "i \ n" - assume "t \ domain (fm n x)" - hence "t \ domain (fm i x)" using J_mono[OF `i \ n`] by auto - with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t" - using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn]) - } note index_shift = this - have I: "\i. i \ n \ Suc (diagseq i) \ n" - apply (rule le_SucI) - apply (rule order_trans) apply simp - apply (rule seq_suble[OF subseq_diagseq]) - done - from z - have "\N. \i\N. dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" - unfolding tendsto_iff eventually_sequentially using `0 < e` by auto - then obtain N where N: "\i. i \ N \ - dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" by auto - show "\N. \na\N. dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e " - proof (rule exI[where x="max N n"], safe) - fix na assume "max N n \ na" - hence "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) = - dist ((fm (Suc (diagseq na)) (y (Suc (diagseq na))))\<^sub>F t) (z t)" using t - by (subst index_shift[OF I]) auto - also have "\ < e" using `max N n \ na` by (intro N) simp - finally show "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e" . - qed - qed - hence "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> (finmap_of (Utn ` J n) z)\<^sub>F t" - by (simp add: tendsto_intros) - } ultimately - have "(\i. fm n (y (Suc (diagseq i)))) ----> finmap_of (Utn ` J n) z" - by (rule tendsto_finmap) - hence "((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) ----> finmap_of (Utn ` J n) z" - by (intro lim_subseq) (simp add: subseq_def) - moreover - have "(\i. ((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) i \ K' n)" - apply (auto simp add: o_def intro!: fm_in_K' `1 \ n` le_SucI) - apply (rule le_trans) - apply (rule le_add2) - using seq_suble[OF subseq_diagseq] - apply auto - done - moreover - from `compact (K' n)` have "closed (K' n)" by (rule compact_imp_closed) - ultimately - have "finmap_of (Utn ` J n) z \ K' n" - unfolding closed_sequential_limits by blast - also have "finmap_of (Utn ` J n) z = fm n (\i. z (Utn i))" - unfolding finmap_eq_iff - proof clarsimp - fix i assume i: "i \ J n" - hence "from_nat_into (\n. J n) (Utn i) = i" - unfolding Utn_def - by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto - with i show "z (Utn i) = (fm n (\i. z (Utn i)))\<^sub>F (Utn i)" - by (simp add: finmap_eq_iff fm_def compose_def) - qed - finally have "fm n (\i. z (Utn i)) \ K' n" . - moreover - let ?J = "\n. J n" - have "(?J \ J n) = J n" by auto - ultimately have "restrict (\i. z (Utn i)) (?J \ J n) \ K n" - unfolding K_def by (auto simp: proj_space space_PiM) - hence "restrict (\i. z (Utn i)) ?J \ Z' n" unfolding Z'_def - using J by (auto simp: prod_emb_def PiE_def extensional_def) - also have "\ \ Z n" using Z' by simp - finally have "restrict (\i. z (Utn i)) ?J \ Z n" . - } note in_Z = this - hence "(\i\{1..}. Z i) \ {}" by auto - hence "(\i. Z i) \ {}" using Z INT_decseq_offset[OF `decseq Z`] by simp - thus False using Z by simp + hence "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> (finmap_of (Utn ` J n) z)\<^sub>F t" + by (simp add: tendsto_intros) + } ultimately + have "(\i. fm n (y (Suc (diagseq i)))) ----> finmap_of (Utn ` J n) z" + by (rule tendsto_finmap) + hence "((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) ----> finmap_of (Utn ` J n) z" + by (intro lim_subseq) (simp add: subseq_def) + moreover + have "(\i. ((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) i \ K' n)" + apply (auto simp add: o_def intro!: fm_in_K' `1 \ n` le_SucI) + apply (rule le_trans) + apply (rule le_add2) + using seq_suble[OF subseq_diagseq] + apply auto + done + moreover + from `compact (K' n)` have "closed (K' n)" by (rule compact_imp_closed) + ultimately + have "finmap_of (Utn ` J n) z \ K' n" + unfolding closed_sequential_limits by blast + also have "finmap_of (Utn ` J n) z = fm n (\i. z (Utn i))" + unfolding finmap_eq_iff + proof clarsimp + fix i assume i: "i \ J n" + hence "from_nat_into (\n. J n) (Utn i) = i" + unfolding Utn_def + by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto + with i show "z (Utn i) = (fm n (\i. z (Utn i)))\<^sub>F (Utn i)" + by (simp add: finmap_eq_iff fm_def compose_def) qed - ultimately show "(\i. \G (Z i)) ----> 0" - using LIMSEQ_INF[of "\i. \G (Z i)"] by simp - qed - then guess \ .. note \ = this - def f \ "finmap_of J B" - show "emeasure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = emeasure (lim\<^sub>B J P) (Pi\<^sub>E J B)" - proof (subst emeasure_extend_measure_Pair[OF limP_def, of I "\_. borel" \]) - show "positive (sets (lim\<^sub>B I P)) \" "countably_additive (sets (lim\<^sub>B I P)) \" - using \ unfolding sets_limP sets_PiM_generator by (auto simp: measure_space_def) - next - show "(J \ {} \ I = {}) \ finite J \ J \ I \ B \ J \ sets borel" - using assms by (auto simp: f_def) - next - fix J and X::"'i \ 'a set" - show "prod_emb I (\_. borel) J (Pi\<^sub>E J X) \ Pow (I \\<^sub>E space borel)" - by (auto simp: prod_emb_def) - assume JX: "(J \ {} \ I = {}) \ finite J \ J \ I \ X \ J \ sets borel" - hence "emb I J (Pi\<^sub>E J X) \ generator" using assms - by (intro generatorI[where J=J and X="Pi\<^sub>E J X"]) (auto intro: sets_PiM_I_finite) - hence "\ (emb I J (Pi\<^sub>E J X)) = \G (emb I J (Pi\<^sub>E J X))" using \ by simp - also have "\ = emeasure (P J) (Pi\<^sub>E J X)" - using JX assms proj_sets - by (subst mu_G_eq) (auto simp: mu_G_eq limP_finite intro: sets_PiM_I_finite) - finally show "\ (emb I J (Pi\<^sub>E J X)) = emeasure (P J) (Pi\<^sub>E J X)" . - next - show "emeasure (P J) (Pi\<^sub>E J B) = emeasure (limP J (\_. borel) P) (Pi\<^sub>E J B)" - using assms by (simp add: f_def limP_finite Pi_def) - qed -qed + finally have "fm n (\i. z (Utn i)) \ K' n" . + moreover + let ?J = "\n. J n" + have "(?J \ J n) = J n" by auto + ultimately have "restrict (\i. z (Utn i)) (?J \ J n) \ K n" + unfolding K_def by (auto simp: space_P space_PiM) + hence "restrict (\i. z (Utn i)) ?J \ Z' n" unfolding Z'_def + using J by (auto simp: prod_emb_def PiE_def extensional_def) + also have "\ \ Z n" using Z' by simp + finally have "restrict (\i. z (Utn i)) ?J \ Z n" . + } note in_Z = this + hence "(\i\{1..}. Z i) \ {}" by auto + thus "(\i. Z i) \ {}" + using INT_decseq_offset[OF antimonoI[OF Z_mono]] by simp +qed fact+ + +lemma measure_lim_emb: + "J \ I \ finite J \ X \ sets (\\<^sub>M i\J. borel) \ measure lim (emb I J X) = measure (P J) X" + unfolding measure_def by (subst emeasure_lim_emb) auto end @@ -548,70 +469,24 @@ hide_const (open) domain hide_const (open) basis_finmap -sublocale polish_projective \ P!: prob_space "(lim\<^sub>B I P)" +sublocale polish_projective \ P!: prob_space lim proof - show "emeasure (lim\<^sub>B I P) (space (lim\<^sub>B I P)) = 1" - proof cases - assume "I = {}" - interpret prob_space "P {}" using proj_prob_space by simp - show ?thesis - by (simp add: space_PiM_empty limP_finite emeasure_space_1 `I = {}`) - next - assume "I \ {}" - then obtain i where "i \ I" by auto - interpret prob_space "P {i}" using proj_prob_space by simp - have R: "(space (lim\<^sub>B I P)) = (emb I {i} (Pi\<^sub>E {i} (\_. space borel)))" - by (auto simp: prod_emb_def space_PiM) - moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM PiE_def) - ultimately show ?thesis using `i \ I` - apply (subst R) - apply (subst emeasure_limB_emb_not_empty) - apply (auto simp: limP_finite emeasure_space_1 PiE_def) - done - qed + have *: "emb I {} {\x. undefined} = space (\\<^sub>M i\I. borel)" + by (auto simp: prod_emb_def space_PiM) + interpret prob_space "P {}" + using prob_space_P by simp + show "emeasure lim (space lim) = 1" + using emeasure_lim_emb[of "{}" "{\x. undefined}"] emeasure_space_1 + by (simp add: * PiM_empty space_P) qed -context polish_projective begin - -lemma emeasure_limB_emb: - assumes X: "J \ I" "finite J" "\i\J. B i \ sets borel" - shows "emeasure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = emeasure (P J) (Pi\<^sub>E J B)" -proof cases - interpret prob_space "P {}" using proj_prob_space by simp - assume "J = {}" - moreover have "emb I {} {\x. undefined} = space (lim\<^sub>B I P)" - by (auto simp: space_PiM prod_emb_def) - moreover have "{\x. undefined} = space (lim\<^sub>B {} P)" - by (auto simp: space_PiM prod_emb_def simp del: limP_finite) - ultimately show ?thesis - by (simp add: P.emeasure_space_1 limP_finite emeasure_space_1 del: space_limP) -next - assume "J \ {}" with X show ?thesis - by (subst emeasure_limB_emb_not_empty) (auto simp: limP_finite) -qed - -lemma measure_limB_emb: - assumes "J \ I" "finite J" "\i\J. B i \ sets borel" - shows "measure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = measure (P J) (Pi\<^sub>E J B)" -proof - - interpret prob_space "P J" using proj_prob_space assms by simp - show ?thesis - using emeasure_limB_emb[OF assms] - unfolding emeasure_eq_measure limP_finite[OF `finite J` `J \ I`] P.emeasure_eq_measure - by simp -qed - -end - locale polish_product_prob_space = product_prob_space "\_. borel::('a::polish_space) measure" I for I::"'i set" sublocale polish_product_prob_space \ P: polish_projective I "\J. PiM J (\_. borel::('a) measure)" proof qed -lemma (in polish_product_prob_space) limP_eq_PiM: - "I \ {} \ lim\<^sub>P I (\_. borel) (\J. PiM J (\_. borel::('a) measure)) = - PiM I (\_. borel)" - by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb) +lemma (in polish_product_prob_space) limP_eq_PiM: "lim = PiM I (\_. borel)" + by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb) end