Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Probability/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 24 kB

Quelle Infinite_Product_Measure.thy Sprache: Isabelle

(*  Title:      HOL/Probability/Infinite_Product_Measure.thy
    Author:     Johannes Hölzl, TU München
*)

section \<open>Infinite Product Measure\<close>

theory Infinite_Product_Measure
  imports Probability_Measure Projective_Family
begin

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 (Pi\<^sub>E J X)) = (\i\J. M i (X i))"
    proof (subst emeasure_extend_measure_Pair[OF PiM_def, where \<mu>'=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 "emeasure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\i\J. M i (X i))"
  proof (cases "J \ {} \ I = {}")
    case False
    then obtain i where i: "J = {}" "i \ I" by auto
    then have "emb I {} {\x. undefined} = emb I {i} (\\<^sub>E i\{i}. space (M i))"
      by (auto simp: space_PiM prod_emb_def)
    with i show ?thesis
      by (simp add: * M.emeasure_space_1)
  next
    case True
    then show ?thesis
      by (simp add: *[OF _ assms X])
  qed
  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)

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])

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)) = (\<Prod> i\<in>J. emeasure (M i) (X i))"
  by (subst emeasure_PiM_emb') (auto intro!: emeasure_PiM)

sublocale product_prob_space \<subseteq> 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"
    using emeasure_PiM_emb[of "{}" "\_. {}"] by (simp add: *)
qed

lemma prob_space_PiM:
  assumes M: "\i. i \ I \ prob_space (M i)" shows "prob_space (PiM I M)"
proof -
  let ?M = "\i. if i \ I then M i else count_space {undefined}"
  interpret M': prob_space "?M i" for i
    using M by (cases "i \ I") (auto intro!: prob_spaceI)
  interpret product_prob_space ?M I
    by unfold_locales
  have "prob_space (\\<^sub>M i\I. ?M i)"
    by unfold_locales
  also have "(\\<^sub>M i\I. ?M i) = (\\<^sub>M i\I. M i)"
    by (intro PiM_cong) auto
  finally show ?thesis .
qed

lemma (in product_prob_space) emeasure_PiM_Collect:
  assumes X: "J \ I" "finite J" "\i. i \ J \ X i \ sets (M i)"
  shows "emeasure (Pi\<^sub>M I M) {x\space (Pi\<^sub>M I M). \i\J. x i \ X i} = (\ i\J. emeasure (M i) (X i))"
proof -
  have "{x\space (Pi\<^sub>M I M). \i\J. x i \ X i} = emb I J (Pi\<^sub>E J X)"
    unfolding prod_emb_def using assms by (auto simp: space_PiM Pi_iff)
  with emeasure_PiM_emb[OF assms] show ?thesis by simp
qed

lemma (in product_prob_space) emeasure_PiM_Collect_single:
  assumes X: "i \ I" "A \ sets (M i)"
  shows "emeasure (Pi\<^sub>M I M) {x\space (Pi\<^sub>M I M). x i \ A} = emeasure (M i) A"
  using emeasure_PiM_Collect[of "{i}" "\i. A"] assms
  by simp

lemma (in product_prob_space) measure_PiM_emb:
  assumes "J \ I" "finite J" "\i. i \ J \ X i \ sets (M i)"
  shows "measure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\ i\J. measure (M i) (X i))"
  using emeasure_PiM_emb[OF assms]
  unfolding emeasure_eq_measure M.emeasure_eq_measure
  by (simp add: prod_ennreal measure_nonneg prod_nonneg)

lemma sets_Collect_single':
  "i \ I \ {x\space (M i). P x} \ sets (M i) \ {x\space (PiM I M). P (x i)} \ sets (PiM I M)"
  by auto

lemma (in finite_product_prob_space) finite_measure_PiM_emb:
  "(\i. i \ I \ A i \ sets (M i)) \ measure (PiM I M) (Pi\<^sub>E I A) = (\i\I. measure (M i) (A i))"
  by (rule prob_times)

lemma (in product_prob_space) PiM_component:
  assumes "i \ I"
  shows "distr (PiM I M) (M i) (\\. \ i) = M i"
proof (rule measure_eqI[symmetric])
  fix A assume "A \ sets (M i)"
  moreover have "((\\. \ i) -` A \ space (PiM I M)) = {x\space (PiM I M). x i \ A}"
    by auto
  ultimately show "emeasure (M i) A = emeasure (distr (PiM I M) (M i) (\\. \ i)) A"
    by (auto simp: \<open>i\<in>I\<close> emeasure_distr measurable_component_singleton emeasure_PiM_Collect_single)
qed simp

lemma (in product_prob_space) PiM_eq:
  assumes M': "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))"
  shows "M' = (PiM I M)"
proof (rule measure_eqI_PiM_infinite[symmetric, OF refl M'])
  show "finite_measure (Pi\<^sub>M I M)"
    by standard (simp add: P.emeasure_space_1)
qed (simp add: eq emeasure_PiM_emb)

lemma (in product_prob_space) AE_component: "i \ I \ AE x in M i. P x \ AE x in PiM I M. P (x i)"
  apply (rule AE_distrD[of "\\. \ i" "PiM I M" "M i" P])
  apply simp
  apply (subst PiM_component)
  apply simp_all
  done

lemma emeasure_PiM_emb:
  assumes M: "\i. i \ I \ prob_space (M i)"
  assumes J: "J \ I" "finite J" and A: "\i. i \ J \ A i \ sets (M i)"
  shows "emeasure (Pi\<^sub>M I M) (prod_emb I M J (Pi\<^sub>E J A)) = (\i\J. emeasure (M i) (A i))"
proof -
  let ?M = "\i. if i \ I then M i else count_space {undefined}"
  interpret M': prob_space "?M i" for i
    using M by (cases "i \ I") (auto intro!: prob_spaceI)
  interpret P: product_prob_space ?M I
    by unfold_locales
  have "emeasure (Pi\<^sub>M I M) (prod_emb I M J (Pi\<^sub>E J A)) = emeasure (Pi\<^sub>M I ?M) (P.emb I J (Pi\<^sub>E J A))"
    by (auto simp: prod_emb_def PiE_iff intro!: arg_cong2[where f=emeasure] PiM_cong)
  also have "\ = (\i\J. emeasure (M i) (A i))"
    using J A by (subst P.emeasure_PiM_emb[OF J]) (auto intro!: prod.cong)
  finally show ?thesis .
qed

lemma distr_pair_PiM_eq_PiM:
  fixes i' :: "'i" and I :: "'i set" and M :: "'i \<Rightarrow> 'a measure"
  assumes M: "\i. i \ I \ prob_space (M i)" "prob_space (M i')"
  shows "distr (M i' \\<^sub>M (\\<^sub>M i\I. M i)) (\\<^sub>M i\insert i' I. M i) (\(x, X). X(i' := x)) =
    (\<Pi>\<^sub>M i\<in>insert i' I. M i)" (is "?L = _")
proof (rule measure_eqI_PiM_infinite[symmetric, OF refl])
  interpret M': prob_space "M i'" by fact
  interpret I: prob_space "(\\<^sub>M i\I. M i)"
    using M by (intro prob_space_PiM) auto
  interpret I': prob_space "(\\<^sub>M i\insert i' I. M i)"
    using M by (intro prob_space_PiM) auto
  show "finite_measure (\\<^sub>M i\insert i' I. M i)"
    by unfold_locales
  fix J A assume J: "finite J" "J \ insert i' I" and A: "\i. i \ J \ A i \ sets (M i)"
  let ?X = "prod_emb (insert i' I) M J (Pi\<^sub>E J A)"
  have "Pi\<^sub>M (insert i' I) M ?X = (\i\J. M i (A i))"
    using M J A by (intro emeasure_PiM_emb) auto
  also have "\ = M i' (if i' \ J then (A i') else space (M i')) * (\i\J-{i'}. M i (A i))"
    using prod.insert_remove[of J "\i. M i (A i)" i'] J M'.emeasure_space_1
    by (cases "i' \ J") (auto simp: insert_absorb)
  also have "(\i\J-{i'}. M i (A i)) = Pi\<^sub>M I M (prod_emb I M (J - {i'}) (Pi\<^sub>E (J - {i'}) A))"
    using M J A by (intro emeasure_PiM_emb[symmetric]) auto
  also have "M i' (if i' \ J then (A i') else space (M i')) * \ =
    (M i' \\<^sub>M Pi\<^sub>M I M) ((if i' \ J then (A i') else space (M i')) \ prod_emb I M (J - {i'}) (Pi\<^sub>E (J - {i'}) A))"
    using J A by (intro I.emeasure_pair_measure_Times[symmetric] sets_PiM_I) auto
  also have "((if i' \ J then (A i') else space (M i')) \ prod_emb I M (J - {i'}) (Pi\<^sub>E (J - {i'}) A)) =
    (\<lambda>(x, X). X(i' := x)) -` ?X \<inter> space (M i' \<Otimes>\<^sub>M Pi\<^sub>M I M)"
    using A[of i', THEN sets.sets_into_space] unfolding set_eq_iff
    by (simp add: prod_emb_def space_pair_measure space_PiM PiE_fun_upd ac_simps cong: conj_cong)
       (auto simp add: Pi_iff Ball_def all_conj_distrib)
  finally show "Pi\<^sub>M (insert i' I) M ?X = ?L ?X"
    using J A by (simp add: emeasure_distr)
qed simp

lemma distr_PiM_reindex:
  assumes M: "\i. i \ K \ prob_space (M i)"
  assumes f: "inj_on f I" "f \ I \ K"
  shows "distr (Pi\<^sub>M K M) (\\<^sub>M i\I. M (f i)) (\\. \n\I. \ (f n)) = (\\<^sub>M i\I. M (f i))"
    (is "distr ?K ?I ?t = ?I")
proof (rule measure_eqI_PiM_infinite[symmetric, OF refl])
  interpret prob_space ?I
    using f M by (intro prob_space_PiM) auto
  show "finite_measure ?I"
    by unfold_locales
  fix A J assume J: "finite J" "J \ I" and A: "\i. i \ J \ A i \ sets (M (f i))"
  have [simp]: "i \ J \ the_inv_into I f (f i) = i" for i
    using J f by (intro the_inv_into_f_f) auto
  have "?I (prod_emb I (\i. M (f i)) J (Pi\<^sub>E J A)) = (\j\J. M (f j) (A j))"
    using f J A by (intro emeasure_PiM_emb M) auto
  also have "\ = (\j\f`J. M j (A (the_inv_into I f j)))"
    using f J by (subst prod.reindex) (auto intro!: prod.cong intro: inj_on_subset simp: the_inv_into_f_f)
  also have "\ = ?K (prod_emb K M (f`J) (\\<^sub>E j\f`J. A (the_inv_into I f j)))"
    using f J A by (intro emeasure_PiM_emb[symmetric] M) (auto simp: the_inv_into_f_f)
  also have "prod_emb K M (f`J) (\\<^sub>E j\f`J. A (the_inv_into I f j)) = ?t -` prod_emb I (\i. M (f i)) J (Pi\<^sub>E J A) \ space ?K"
    using f J A by (auto simp: prod_emb_def space_PiM Pi_iff PiE_iff Int_absorb1)
  also have "?K \ = distr ?K ?I ?t (prod_emb I (\i. M (f i)) J (Pi\<^sub>E J A))"
    using f J A by (intro emeasure_distr[symmetric] sets_PiM_I) (auto simp: Pi_iff)
  finally show "?I (prod_emb I (\i. M (f i)) J (Pi\<^sub>E J A)) = distr ?K ?I ?t (prod_emb I (\i. M (f i)) J (Pi\<^sub>E J A))" .
qed simp

lemma distr_PiM_component:
  assumes M: "\i. i \ I \ prob_space (M i)"
  assumes "i \ I"
  shows "distr (Pi\<^sub>M I M) (M i) (\\. \ i) = M i"
proof -
  have *: "(\\. \ i) -` A \ space (Pi\<^sub>M I M) = prod_emb I M {i} (\\<^sub>E i'\{i}. A)" for A
    by (auto simp: prod_emb_def space_PiM)
  show ?thesis
    apply (intro measure_eqI)
    apply (auto simp add: emeasure_distr \<open>i\<in>I\<close> * emeasure_PiM_emb M)
    apply (subst emeasure_PiM_emb)
    apply (simp_all add: M \<open>i\<in>I\<close>)
    done
qed

lemma AE_PiM_component:
  "(\i. i \ I \ prob_space (M i)) \ i \ I \ AE x in M i. P x \ AE x in PiM I M. P (x i)"
  using AE_distrD[of "\x. x i" "PiM I M" "M i"]
  by (subst (asm) distr_PiM_component[of I _ i]) (auto intro: AE_distrD[of "\x. x i" _ _ P])

lemma decseq_emb_PiE:
  "incseq J \ decseq (\i. prod_emb I M (J i) (\\<^sub>E j\J i. X j))"
  by (fastforce simp: decseq_def prod_emb_def incseq_def Pi_iff)

subsection \<open>Sequence space\<close>

definition comb_seq :: "nat \ (nat \ 'a) \ (nat \ 'a) \ (nat \ 'a)" where
  "comb_seq i \ \' j = (if j < i then \ j else \' (j - i))"

lemma split_comb_seq: "P (comb_seq i \ \' j) \ (j < i \ P (\ j)) \ (\k. j = i + k \ P (\' k))"
  by (auto simp: comb_seq_def not_less)

lemma split_comb_seq_asm: "P (comb_seq i \ \' j) \ \ ((j < i \ \ P (\ j)) \ (\k. j = i + k \ \ P (\' k)))"
  by (auto simp: comb_seq_def)

lemma measurable_comb_seq:
  "(\(\, \'). comb_seq i \ \') \ measurable ((\\<^sub>M i\UNIV. M) \\<^sub>M (\\<^sub>M i\UNIV. M)) (\\<^sub>M i\UNIV. M)"
proof (rule measurable_PiM_single)
  show "(\(\, \'). comb_seq i \ \') \ space ((\\<^sub>M i\UNIV. M) \\<^sub>M (\\<^sub>M i\UNIV. M)) \ (UNIV \\<^sub>E space M)"
    by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
  fix j :: nat and A assume A: "A \ sets M"
  then have *: "{\ \ space ((\\<^sub>M i\UNIV. M) \\<^sub>M (\\<^sub>M i\UNIV. M)). case_prod (comb_seq i) \ j \ A} =
    (if j < i then {\<omega> \<in> space (\<Pi>\<^sub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^sub>M i\<in>UNIV. M)
              else space (\<Pi>\<^sub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^sub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
  show "{\ \ space ((\\<^sub>M i\UNIV. M) \\<^sub>M (\\<^sub>M i\UNIV. M)). case_prod (comb_seq i) \ j \ A} \ sets ((\\<^sub>M i\UNIV. M) \\<^sub>M (\\<^sub>M i\UNIV. M))"
    unfolding * by (auto simp: A intro!: sets_Collect_single)
qed

lemma measurable_comb_seq'[measurable (raw)]:
  assumes f: "f \ measurable N (\\<^sub>M i\UNIV. M)" and g: "g \ measurable N (\\<^sub>M i\UNIV. M)"
  shows "(\x. comb_seq i (f x) (g x)) \ measurable N (\\<^sub>M i\UNIV. M)"
  using measurable_compose[OF measurable_Pair[OF f g] measurable_comb_seq] by simp

lemma comb_seq_0: "comb_seq 0 \ \' = \'"
  by (auto simp add: comb_seq_def)

lemma comb_seq_Suc: "comb_seq (Suc n) \ \' = comb_seq n \ (case_nat (\ n) \')"
  by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)

lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \ = case_nat (\ 0)"
  by (intro ext) (simp add: comb_seq_Suc comb_seq_0)

lemma comb_seq_less: "i < n \ comb_seq n \ \' i = \ i"
  by (auto split: split_comb_seq)

lemma comb_seq_add: "comb_seq n \ \' (i + n) = \' i"
  by (auto split: nat.split split_comb_seq)

lemma case_nat_comb_seq: "case_nat s' (comb_seq n \ \') (i + n) = case_nat (case_nat s' \ n) \' i"
  by (auto split: nat.split split_comb_seq)

lemma case_nat_comb_seq':
  "case_nat s (comb_seq i \ \') = comb_seq (Suc i) (case_nat s \) \'"
  by (auto split: split_comb_seq nat.split)

locale sequence_space = product_prob_space "\i. M" "UNIV :: nat set" for M
begin

abbreviation "S \ \\<^sub>M i\UNIV::nat set. M"

lemma infprod_in_sets[intro]:
  fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets M"
  shows "Pi UNIV E \ sets S"
proof -
  have "Pi UNIV E = (\i. emb UNIV {..i} (\\<^sub>E j\{..i}. E j))"
    using E E[THEN sets.sets_into_space]
    by (auto simp: prod_emb_def Pi_iff extensional_def)
  with E show ?thesis by auto
qed

lemma measure_PiM_countable:
  fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets M"
  shows "(\n. \i\n. measure M (E i)) \ measure S (Pi UNIV E)"
proof -
  let ?E = "\n. emb UNIV {..n} (Pi\<^sub>E {.. n} E)"
  have "\n. (\i\n. measure M (E i)) = measure S (?E n)"
    using E by (simp add: measure_PiM_emb)
  moreover have "Pi UNIV E = (\n. ?E n)"
    using E E[THEN sets.sets_into_space]
    by (auto simp: prod_emb_def extensional_def Pi_iff)
  moreover have "range ?E \ sets S"
    using E by auto
  moreover have "decseq ?E"
    by (auto simp: prod_emb_def Pi_iff decseq_def)
  ultimately show ?thesis
    by (simp add: finite_Lim_measure_decseq)
qed

lemma nat_eq_diff_eq:
  fixes a b c :: nat
  shows "c \ b \ a = b - c \ a + c = b"
  by auto

lemma PiM_comb_seq:
  "distr (S \\<^sub>M S) S (\(\, \'). comb_seq i \ \') = S" (is "?D = _")
proof (rule PiM_eq)
  let ?I = "UNIV::nat set" and ?M = "\n. M"
  let "distr _ _ ?f" = "?D"

  fix J E assume J: "finite J" "J \ ?I" "\j. j \ J \ E j \ sets M"
  let ?X = "prod_emb ?I ?M J (\\<^sub>E j\J. E j)"
  have "\j x. j \ J \ x \ E j \ x \ space M"
    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
  with J have "?f -` ?X \ space (S \\<^sub>M S) =
    (prod_emb ?I ?M (J \<inter> {..<i}) (\<Pi>\<^sub>E j\<in>J \<inter> {..<i}. E j)) \<times>
    (prod_emb ?I ?M (((+) i) -` J) (\<Pi>\<^sub>E j\<in>((+) i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
               split: split_comb_seq split_comb_seq_asm)
  then have "emeasure ?D ?X = emeasure (S \\<^sub>M S) (?E \ ?F)"
    by (subst emeasure_distr[OF measurable_comb_seq])
       (auto intro!: sets_PiM_I simp: split_beta' J)
  also have "\ = emeasure S ?E * emeasure S ?F"
    using J by (intro P.emeasure_pair_measure_Times)  (auto intro!: sets_PiM_I finite_vimageI simp: inj_on_def)
  also have "emeasure S ?F = (\j\((+) i) -` J. emeasure M (E (i + j)))"
    using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def)
  also have "\ = (\j\J - (J \ {..
    by (rule prod.reindex_cong [of "\x. x - i"])
      (auto simp: image_iff ac_simps nat_eq_diff_eq cong: conj_cong intro!: inj_onI)
  also have "emeasure S ?E = (\j\J \ {..
    using J by (intro emeasure_PiM_emb) simp_all
  also have "(\j\J \ {..j\J - (J \ {..j\J. emeasure M (E j))"
    by (subst mult.commute) (auto simp: J prod.subset_diff[symmetric])
  finally show "emeasure ?D ?X = (\j\J. emeasure M (E j))" .
qed simp_all

lemma PiM_iter:
  "distr (M \\<^sub>M S) S (\(s, \). case_nat s \) = S" (is "?D = _")
proof (rule PiM_eq)
  let ?I = "UNIV::nat set" and ?M = "\n. M"
  let "distr _ _ ?f" = "?D"

  fix J E assume J: "finite J" "J \ ?I" "\j. j \ J \ E j \ sets M"
  let ?X = "prod_emb ?I ?M J (\\<^sub>E j\J. E j)"
  have "\j x. j \ J \ x \ E j \ x \ space M"
    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
  with J have "?f -` ?X \ space (M \\<^sub>M S) = (if 0 \ J then E 0 else space M) \
    (prod_emb ?I ?M (Suc -` J) (\<Pi>\<^sub>E j\<in>Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
   by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
      split: nat.split nat.split_asm)
  then have "emeasure ?D ?X = emeasure (M \\<^sub>M S) (?E \ ?F)"
    by (subst emeasure_distr)
       (auto intro!: sets_PiM_I simp: split_beta' J)
  also have "\ = emeasure M ?E * emeasure S ?F"
    using J by (intro P.emeasure_pair_measure_Times) (auto intro!: sets_PiM_I finite_vimageI)
  also have "emeasure S ?F = (\j\Suc -` J. emeasure M (E (Suc j)))"
    using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI)
  also have "\ = (\j\J - {0}. emeasure M (E j))"
    by (rule prod.reindex_cong [of "\x. x - 1"])
      (auto simp: image_iff nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
  also have "emeasure M ?E * (\j\J - {0}. emeasure M (E j)) = (\j\J. emeasure M (E j))"
    by (auto simp: M.emeasure_space_1 prod.remove J)
  finally show "emeasure ?D ?X = (\j\J. emeasure M (E j))" .
qed simp_all

end

lemma PiM_return:
  assumes "finite I"
  assumes [measurable]: "\i. i \ I \ {a i} \ sets (M i)"
  shows "PiM I (\i. return (M i) (a i)) = return (PiM I M) (restrict a I)"
proof -
  have [simp]: "a i \ space (M i)" if "i \ I" for i
    using assms(2)[OF that] by (meson insert_subset sets.sets_into_space)
  interpret prob_space "PiM I (\i. return (M i) (a i))"
    by (intro prob_space_PiM prob_space_return) auto
  have "AE x in PiM I (\i. return (M i) (a i)). \i\I. x i = restrict a I i"
    by (intro eventually_ball_finite ballI AE_PiM_component prob_space_return assms)
       (auto simp: AE_return)
  moreover have "AE x in PiM I (\i. return (M i) (a i)). x \ space (PiM I (\i. return (M i) (a i)))"
    by simp
  ultimately have "AE x in PiM I (\i. return (M i) (a i)). x = restrict a I"
    by eventually_elim (auto simp: fun_eq_iff space_PiM)
  hence "Pi\<^sub>M I (\i. return (M i) (a i)) = return (Pi\<^sub>M I (\i. return (M i) (a i))) (restrict a I)"
    by (rule AE_eq_constD)
  also have "\ = return (PiM I M) (restrict a I)"
    by (intro return_cong sets_PiM_cong) auto
  finally show ?thesis .
qed

lemma distr_PiM_finite_prob_space':
  assumes fin: "finite I"
  assumes "\i. i \ I \ prob_space (M i)"
  assumes "\i. i \ I \ prob_space (M' i)"
  assumes [measurable]: "\i. i \ I \ f \ measurable (M i) (M' i)"
  shows   "distr (PiM I M) (PiM I M') (compose I f) = PiM I (\i. distr (M i) (M' i) f)"
proof -
  define N where "N = (\i. if i \ I then M i else return (count_space UNIV) undefined)"
  define N' where "N' = (\<lambda>i. if i \<in> I then M' i else return (count_space UNIV) undefined)"
  have [simp]: "PiM I N = PiM I M" "PiM I N' = PiM I M'"
    by (intro PiM_cong; simp add: N_def N'_def)+

  have "distr (PiM I N) (PiM I N') (compose I f) = PiM I (\i. distr (N i) (N' i) f)"
  proof (rule distr_PiM_finite_prob_space)
    show "product_prob_space N"
      by (rule product_prob_spaceI) (auto simp: N_def intro!: prob_space_return assms)
    show "product_prob_space N'"
      by (rule product_prob_spaceI) (auto simp: N'_def intro!: prob_space_return assms)
  qed (auto simp: N_def N'_def fin)
  also have "Pi\<^sub>M I (\i. distr (N i) (N' i) f) = Pi\<^sub>M I (\i. distr (M i) (M' i) f)"
    by (intro PiM_cong) (simp_all add: N_def N'_def)
  finally show ?thesis by simp
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.9 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.