(* Title: HOL/Probability/Projective_Family.thy Author: Fabian Immler, TU München Author: Johannes Hölzl, TU München *) header {*Projective Family*} theory Projective_Family imports Finite_Product_Measure Probability_Measure 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) 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)" 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 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 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) abbreviation "emb L K X \ prod_emb L M K X" 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) 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) 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 generatorI': "J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ emb I J X \ generator" unfolding generator_def by auto 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 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 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 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))" 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" 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) 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" .. 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 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) 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))" 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 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" . 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) qed qed end