Quelle Projective_Family.thy Sprache: Isabelle

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

section \<open>Projective Family\<close>

theory Projective_Family
imports Giry_Monad
begin

(** Something strange going on here regarding the syntax \<omega>(n := x) vs fun_upd \<omega> n x
    See nn_integral_eP, etc. **)

lemma vimage_restrict_preserve_mono:
  assumes J: "J \ I"
  and sets: "A \ (\\<^sub>E i\J. S i)" "B \ (\\<^sub>E i\J. S i)" and ne: "(\\<^sub>E i\I. S i) \ {}"
  and eq: "(\x. restrict x J) -` A \ (\\<^sub>E i\I. S i) \ (\x. restrict x J) -` B \ (\\<^sub>E i\I. S i)"
  shows "A \ B"
proof  (intro subsetI)
  fix x assume "x \ A"
  from ne obtain y where y: "\i. i \ I \ y i \ S i" by auto
  have "J \ (I - J) = {}" by auto
  show "x \ B"
  proof cases
    assume x: "x \ (\\<^sub>E i\J. S i)"
    have "merge J (I - J) (x,y) \ (\x. restrict x J) -` A \ (\\<^sub>E i\I. S i)"
      using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close>
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
    also have "\ \ (\x. restrict x J) -` B \ (\\<^sub>E i\I. S i)" by fact
    finally show "x \ B"
      using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> eq
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
  qed (insert \<open>x\<in>A\<close> sets, auto)
qed

locale projective_family =
  fixes I :: "'i set" and P :: "'i set \ ('i \ 'a) measure" and M :: "'i \ 'a measure"
  assumes P: "\J H. J \ H \ finite H \ H \ I \ P J = distr (P H) (PiM J M) (\f. restrict f J)"
  assumes prob_space_P: "\J. finite J \ J \ I \ prob_space (P J)"
begin

lemma sets_P: "finite J \ J \ I \ sets (P J) = sets (PiM J M)"
  by (subst P[of J J]) simp_all

lemma space_P: "finite J \ J \ I \ space (P J) = space (PiM J M)"
  using sets_P by (rule sets_eq_imp_space_eq)

lemma not_empty_M: "i \ I \ space (M i) \ {}"
  using prob_space_P[THEN prob_space.not_empty] by (auto simp: space_PiM space_P)

lemma not_empty: "space (PiM I M) \ {}"
  by (simp add: not_empty_M)

abbreviation
  "emb L K \ prod_emb L M K"

lemma emb_preserve_mono:
  assumes "J \ L" "L \ I" and sets: "X \ sets (Pi\<^sub>M J M)" "Y \ sets (Pi\<^sub>M J M)"
  assumes "emb L J X \ emb L J Y"
  shows "X \ Y"
proof (rule vimage_restrict_preserve_mono)
  show "X \ (\\<^sub>E i\J. space (M i))" "Y \ (\\<^sub>E i\J. space (M i))"
    using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
  show "(\\<^sub>E i\L. space (M i)) \ {}"
    using \<open>L \<subseteq> I\<close> by (auto simp add: not_empty_M space_PiM[symmetric])
  show "(\x. restrict x J) -` X \ (\\<^sub>E i\L. space (M i)) \ (\x. restrict x J) -` Y \ (\\<^sub>E i\L. space (M i))"
    using \<open>prod_emb L M J X \<subseteq> prod_emb L M J Y\<close> by (simp add: prod_emb_def)
qed fact

lemma emb_injective:
  assumes L: "J \ L" "L \ I" and X: "X \ sets (Pi\<^sub>M J M)" and Y: "Y \ sets (Pi\<^sub>M J M)"
  shows "emb L J X = emb L J Y \ X = Y"
  by (intro antisym emb_preserve_mono[OF L X Y] emb_preserve_mono[OF L Y X]) auto

lemma emeasure_P: "J \ K \ finite K \ K \ I \ X \ sets (PiM J M) \ P K (emb K J X) = P J X"
  by (auto intro!: emeasure_distr_restrict[symmetric] simp: P sets_P)

inductive_set generator :: "('i \ 'a) set set" where
  "finite J \ J \ I \ X \ sets (Pi\<^sub>M J M) \ emb I J X \ generator"

lemma algebra_generator: "algebra (space (PiM I M)) generator"
  unfolding algebra_iff_Int
proof (safe elim!: generator.cases)
  fix J X assume J: "finite J" "J \ I" and X: "X \ sets (PiM J M)"

  from X[THEN sets.sets_into_space] J show "x \ emb I J X \ x \ space (PiM I M)" for x
    by (auto simp: prod_emb_def space_PiM)

  have "emb I J (space (PiM J M) - X) \ generator"
    by (intro generator.intros J sets.Diff sets.top X)
  with J show "space (Pi\<^sub>M I M) - emb I J X \ generator"
    by (simp add: space_PiM prod_emb_PiE)

  fix K Y assume K: "finite K" "K \ I" and Y: "Y \ sets (PiM K M)"
  have "emb I (J \ K) (emb (J \ K) J X) \ emb I (J \ K) (emb (J \ K) K Y) \ generator"
    unfolding prod_emb_Int[symmetric]
    by (intro generator.intros sets.Int measurable_prod_emb) (auto intro!: J K X Y)
  with J K X Y show "emb I J X \ emb I K Y \ generator"
    by simp
qed (force simp: generator.simps prod_emb_empty[symmetric])

interpretation generator: algebra "space (PiM I M)" generator
  by (rule algebra_generator)

lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
proof (intro antisym sets.sigma_sets_subset)
  show "sets (PiM I M) \ sigma_sets (space (PiM I M)) generator"
    unfolding sets_PiM_single space_PiM[symmetric]
  proof (intro sigma_sets_mono', safe)
    fix i A assume "i \ I" and A: "A \ sets (M i)"
    then have "{f \ space (Pi\<^sub>M I M). f i \ A} = emb I {i} (\\<^sub>E j\{i}. A)"
      by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def)
    with \<open>i\<in>I\<close> A show "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} \<in> generator"
      by (auto intro!: generator.intros sets_PiM_I_finite)
  qed
qed (auto elim!: generator.cases)

definition mu_G (\<open>\<mu>G\<close>) where
  "\G A = (THE x. \J\I. finite J \ (\X\sets (Pi\<^sub>M J M). A = emb I J X \ x = emeasure (P J) X))"

definition lim :: "('i \ 'a) measure" where
  "lim = extend_measure (space (PiM I M)) generator (\x. x) \G"

lemma space_lim[simp]: "space lim = space (PiM I M)"
  using generator.space_closed
  unfolding lim_def by (intro space_extend_measure) simp

lemma sets_lim[simp, measurable]: "sets lim = sets (PiM I M)"
  using generator.space_closed by (simp add: lim_def sets_PiM_generator sets_extend_measure)

lemma mu_G_spec:
  assumes J: "finite J" "J \ I" "X \ sets (Pi\<^sub>M J M)"
  shows "\G (emb I J X) = emeasure (P J) X"
  unfolding mu_G_def
proof (intro the_equality allI impI ballI)
  fix K Y assume K: "finite K" "K \ I" "Y \ sets (Pi\<^sub>M K M)"
    and [simp]: "emb I J X = emb I K Y"
  have "emeasure (P K) Y = emeasure (P (K \ J)) (emb (K \ J) K Y)"
    using K J by (simp add: emeasure_P)
  also have "emb (K \ J) K Y = emb (K \ J) J X"
    using K J by (simp add: emb_injective[of "K \ J" I])
  also have "emeasure (P (K \ J)) (emb (K \ J) J X) = emeasure (P J) X"
    using K J by (subst emeasure_P) simp_all
  finally show "emeasure (P J) X = emeasure (P K) Y" ..
qed (insert J, force)

lemma positive_mu_G: "positive generator \G"
proof -
  show ?thesis
  proof (safe intro!: positive_def[THEN iffD2])
    obtain J where "finite J" "J \ I" by auto
    then have "\G (emb I J {}) = 0"
      by (subst mu_G_spec) auto
    then show "\G {} = 0" by simp
  qed
qed

lemma additive_mu_G: "additive generator \G"
proof (safe intro!: additive_def[THEN iffD2] elim!: generator.cases)
  fix J X K Y assume J: "finite J" "J \ I" "X \ sets (PiM J M)"
    and K: "finite K" "K \ I" "Y \ sets (PiM K M)"
    and "emb I J X \ emb I K Y = {}"
  then have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}"
    by (intro emb_injective[of "J \ K" I _ "{}"]) (auto simp: sets.Int prod_emb_Int)
  have "\G (emb I J X \ emb I K Y) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))"
    using J K by simp
  also have "\ = emeasure (P (J \ K)) (emb (J \ K) J X \ emb (J \ K) K Y)"
    using J K by (simp add: mu_G_spec sets.Un del: prod_emb_Un)
  also have "\ = \G (emb I J X) + \G (emb I K Y)"
    using J K JK_disj by (simp add: plus_emeasure[symmetric] mu_G_spec emeasure_P sets_P)
  finally show "\G (emb I J X \ emb I K Y) = \G (emb I J X) + \G (emb I K Y)" .
qed

lemma emeasure_lim:
  assumes JX: "finite J" "J \ I" "X \ sets (PiM J M)"
  assumes cont: "\J X. (\i. J i \ I) \ incseq J \ (\i. finite (J i)) \ (\i. X i \ sets (PiM (J i) M)) \
    decseq (\<lambda>i. emb I (J i) (X i)) \<Longrightarrow> 0 < (INF i. P (J i) (X i)) \<Longrightarrow> (\<Inter>i. emb I (J i) (X i)) \<noteq> {}"
  shows "emeasure lim (emb I J X) = P J X"
proof -
  have "\\. (\s\generator. \ s = \G s) \
    measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \<mu>"
  proof (rule generator.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
    show "\A. A \ generator \ \G A \ \"
    proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI)
      fix J assume "finite J" "J \ I"
      then interpret prob_space "P J" by (rule prob_space_P)
      show "\X. X \ sets (Pi\<^sub>M J M) \ emeasure (P J) X \ top"
        by simp
    qed
  next
    fix A assume "range A \ generator" and "decseq A" "(\i. A i) = {}"
    then have "\i. \J X. A i = emb I J X \ finite J \ J \ I \ X \ sets (PiM J M)"
      unfolding image_subset_iff generator.simps by blast
    then obtain J X where A: "\i. A i = emb I (J i) (X i)"
      and *: "\i. finite (J i)" "\i. J i \ I" "\i. X i \ sets (PiM (J i) M)"
      by metis
    have "(INF i. P (J i) (X i)) = 0"
    proof (rule ccontr)
      assume INF_P: "(INF i. P (J i) (X i)) \ 0"
      have "(\i. emb I (\n\i. J n) (emb (\n\i. J n) (J i) (X i))) \ {}"
      proof (rule cont)
        show "decseq (\i. emb I (\n\i. J n) (emb (\n\i. J n) (J i) (X i)))"
          using * \<open>decseq A\<close> by (subst prod_emb_trans) (auto simp: A[abs_def])
        show "0 < (INF i. P (\n\i. J n) (emb (\n\i. J n) (J i) (X i)))"
           using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest)
        show "incseq (\i. \n\i. J n)"
          by (force simp: incseq_def)
      qed (insert *, auto)
      with \<open>(\<Inter>i. A i) = {}\<close> * show False
        by (subst (asm) prod_emb_trans) (auto simp: A[abs_def])
    qed
    moreover have "(\i. P (J i) (X i)) \ (INF i. P (J i) (X i))"
    proof (intro LIMSEQ_INF antimonoI)
      fix x y :: nat assume "x \ y"
      have "P (J y \ J x) (emb (J y \ J x) (J y) (X y)) \ P (J y \ J x) (emb (J y \ J x) (J x) (X x))"
        using \<open>decseq A\<close>[THEN decseqD, OF \<open>x\<le>y\<close>] *
        by (auto simp: A sets_P del: subsetI intro!: emeasure_mono  \<open>x \<le> y\<close>
              emb_preserve_mono[of "J y \ J x" I, where X="emb (J y \ J x) (J y) (X y)"])
      then show "P (J y) (X y) \ P (J x) (X x)"
        using * by (simp add: emeasure_P)
    qed
    ultimately show "(\i. \G (A i)) \ 0"
      by (auto simp: A[abs_def] mu_G_spec *)
  qed
  then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s"
    and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \"
    by (metis sets_PiM_generator)
  show ?thesis
  proof (subst emeasure_extend_measure[OF lim_def])
    show "A \ generator \ \ A = \G A" for A
      using eq by simp
    show "positive (sets lim) \" "countably_additive (sets lim) \"
      using ms by (auto simp add: measure_space_def)
    show "(\x. x) ` generator \ Pow (space (Pi\<^sub>M I M))"
      using generator.space_closed by simp
    show "emb I J X \ generator" "\G (emb I J X) = emeasure (P J) X"
      using JX by (auto intro: generator.intros simp: mu_G_spec)
  qed
qed

end

sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
  unfolding projective_family_def
proof (intro conjI allI impI distr_restrict)
  show "\J. finite J \ prob_space (Pi\<^sub>M J M)"
    by (intro prob_spaceI) (simp add: space_PiM emeasure_PiM emeasure_space_1)
qed auto

txt \<open> Proof due to Ionescu Tulcea. \<close>

locale Ionescu_Tulcea =
  fixes P :: "nat \ (nat \ 'a) \ 'a measure" and M :: "nat \ 'a measure"
  assumes P[measurable]: "\i. P i \ measurable (PiM {0..
  assumes prob_space_P: "\i x. x \ space (PiM {0.. prob_space (P i x)"
begin

lemma non_empty[simp]: "space (M i) \ {}"
proof (induction i rule: less_induct)
  case (less i)
  then obtain x where "\j. j < i \ x j \ space (M j)"
    unfolding ex_in_conv[symmetric] by metis
  then have *: "restrict x {0.. space (PiM {0..
    by (auto simp: space_PiM PiE_iff)
  then interpret prob_space "P i (restrict x {0..
    by (rule prob_space_P)
  show ?case
    using not_empty subprob_measurableD(1)[OF P, OF *] by simp
qed

lemma space_PiM_not_empty[simp]: "space (PiM UNIV M) \ {}"
  unfolding space_PiM_empty_iff by auto

lemma space_P: "x \ space (PiM {0.. space (P n x) = space (M n)"
  by (simp add: P[THEN subprob_measurableD(1)])

lemma sets_P[measurable_cong]: "x \ space (PiM {0.. sets (P n x) = sets (M n)"
  by (simp add: P[THEN subprob_measurableD(2)])

definition eP :: "nat \ (nat \ 'a) \ (nat \ 'a) measure" where
  "eP n \ = distr (P n \) (PiM {0.. n)"

lemma measurable_eP[measurable]:
  "eP n \ measurable (PiM {0..< n} M) (subprob_algebra (PiM {0..
  by (auto simp: eP_def[abs_def] measurable_split_conv
           intro!: measurable_fun_upd[where J="{0..] measurable_distr2[OF _ P])

lemma space_eP:
  "x \ space (PiM {0.. space (eP n x) = space (PiM {0..
  by (simp add: eP_def)

lemma sets_eP[measurable]:
  "x \ space (PiM {0.. sets (eP n x) = sets (PiM {0..
  by (simp add: eP_def)

lemma prob_space_eP: "x \ space (PiM {0.. prob_space (eP n x)"
  unfolding eP_def
  by (intro prob_space.prob_space_distr prob_space_P measurable_fun_upd[where J="{0..]) auto

lemma nn_integral_eP:
  "\ \ space (PiM {0.. f \ borel_measurable (PiM {0..
    (\<integral>\<^sup>+x. f x \<partial>eP n \<omega>) = (\<integral>\<^sup>+x. f (fun_upd \<omega> n x) \<partial>P n \<omega>)"
  unfolding eP_def
  by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..] simp: space_PiM PiE_iff)

lemma emeasure_eP:
  assumes \<omega>[simp]: "\<omega> \<in> space (PiM {0..<n} M)" and A[measurable]: "A \<in> sets (PiM {0..<Suc n} M)"
  shows "eP n \ A = P n \ ((\x. fun_upd \ n x) -` A \ space (M n))"
  using nn_integral_eP[of \<omega> n "indicator A"]
  apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator)
  apply (subst nn_integral_indicator[symmetric])
  using measurable_sets[OF measurable_fun_upd[OF _ measurable_const[OF \<omega>] measurable_id] A, of n]
  apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator
     intro!: nn_integral_cong split: split_indicator)
  done

primrec C :: "nat \ nat \ (nat \ 'a) \ (nat \ 'a) measure" where
  "C n 0 \ = return (PiM {0.."
| "C n (Suc m) \ = C n m \ \ eP (n + m)"

lemma measurable_C[measurable]:
  "C n m \ measurable (PiM {0..
  by (induction m) auto

lemma space_C:
  "x \ space (PiM {0.. space (C n m x) = space (PiM {0..
  by (simp add: measurable_C[THEN subprob_measurableD(1)])

lemma sets_C[measurable_cong]:
  "x \ space (PiM {0.. sets (C n m x) = sets (PiM {0..
  by (simp add: measurable_C[THEN subprob_measurableD(2)])

lemma prob_space_C: "x \ space (PiM {0.. prob_space (C n m x)"
proof (induction m)
  case (Suc m) then show ?case
    by (auto intro!: prob_space.prob_space_bind[where S="PiM {0..]
             simp: space_C prob_space_eP)
qed (auto intro!: prob_space_return simp: space_PiM)

lemma split_C:
  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<bind> C (n + m) l) = C n (m + l) \<omega>"
proof (induction l)
  case 0
  with \<omega> show ?case
    by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty]
                  distr_cong[OF refl sets_C[symmetric, OF \<omega>]])
next
  case (Suc l) with \<omega> show ?case
    by (simp add: bind_assoc[symmetric, OF _ measurable_eP]) (simp add: ac_simps)
qed

lemma nn_integral_C:
  assumes "m \ m'" and f[measurable]: "f \ borel_measurable (PiM {0..
    and nonneg: "\x. x \ space (PiM {0.. 0 \ f x"
    and x: "x \ space (PiM {0..
  shows "(\\<^sup>+x. f x \C n m x) = (\\<^sup>+x. f (restrict x {0..C n m' x)"
  using \<open>m \<le> m'\<close>
proof (induction rule: dec_induct)
  case (step i)
  let ?E = "\x. f (restrict x {0..
  from \<open>m\<le>i\<close> x have "?C i ?E = ?C (Suc i) ?E"
    by (auto simp: nn_integral_bind[where B="PiM {0 ..< Suc (n + i)} M"] space_C nn_integral_eP
             intro!: nn_integral_cong)
       (simp add: space_PiM PiE_iff  nonneg prob_space.emeasure_space_1[OF prob_space_P])
  with step show ?case by (simp del: restrict_apply)
qed (auto simp: space_PiM space_C[OF x] simp del: restrict_apply intro!: nn_integral_cong)

lemma emeasure_C:
  assumes "m \ m'" and A[measurable]: "A \ sets (PiM {0.. space (PiM {0..
  shows "emeasure (C n m' x) (prod_emb {0..
  using assms
  by (subst (1 2) nn_integral_indicator[symmetric])
     (auto intro!: nn_integral_cong split: split_indicator simp del: nn_integral_indicator
           simp: nn_integral_C[of m m' _ n] prod_emb_iff space_PiM PiE_iff sets_C space_C)

lemma distr_C:
  assumes "m \ m'" and [simp]: "x \ space (PiM {0..
  shows "C n m x = distr (C n m' x) (PiM {0..x. restrict x {0..
proof (rule measure_eqI)
  fix A assume "A \ sets (C n m x)"
  with \<open>m \<le> m'\<close> show "emeasure (C n m x) A = emeasure (distr (C n m' x) (Pi\<^sub>M {0..<n + m} M) (\<lambda>x. restrict x {0..<n + m})) A"
    by (subst emeasure_C[symmetric, OF \<open>m \<le> m'\<close>]) (auto intro!: emeasure_distr_restrict[symmetric] simp: sets_C)
qed (simp add: sets_C)

definition up_to :: "nat set \ nat" where
  "up_to J = (LEAST n. \i\n. i \ J)"

lemma up_to_less: "finite J \ i \ J \ i < up_to J"
  unfolding up_to_def
  by (rule LeastI2[of _ "Suc (Max J)"]) (auto simp: Suc_le_eq not_le[symmetric])

lemma up_to_iff: "finite J \ up_to J \ n \ (\i\J. i < n)"
proof safe
  show "finite J \ up_to J \ n \ i \ J \ i < n" for i
    using up_to_less[of J i] by auto
qed (auto simp: up_to_def intro!: Least_le)

lemma up_to_iff_Ico: "finite J \ up_to J \ n \ J \ {0..
  by (auto simp: up_to_iff)

lemma up_to: "finite J \ J \ {0..< up_to J}"
  by (auto simp: up_to_less)

lemma up_to_mono: "J \ H \ finite H \ up_to J \ up_to H"
  by (auto simp add: up_to_iff finite_subset up_to_less)

definition CI :: "nat set \ (nat \ 'a) measure" where
  "CI J = distr (C 0 (up_to J) (\x. undefined)) (PiM J M) (\f. restrict f J)"

sublocale PF: projective_family UNIV CI
  unfolding projective_family_def
proof safe
  show "finite J \ prob_space (CI J)" for J
    using up_to[of J] unfolding CI_def
    by (intro prob_space.prob_space_distr prob_space_C measurable_restrict) auto
  note measurable_cong_sets[OF sets_C, simp]
  have [simp]: "J \ H \ (\f. restrict f J) \ measurable (Pi\<^sub>M H M) (Pi\<^sub>M J M)" for H J
    by (auto intro!: measurable_restrict)

  show "J \ H \ finite H \ CI J = distr (CI H) (Pi\<^sub>M J M) (\f. restrict f J)" for J H
    by (simp add: CI_def distr_C[OF up_to_mono[of J H]] up_to up_to_mono distr_distr comp_def
                  inf.absorb2 finite_subset)
qed

lemma emeasure_CI':
  "finite J \ X \ sets (PiM J M) \ CI J X = C 0 (up_to J) (\_. undefined) (PF.emb {0..
  unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C)

lemma emeasure_CI:
  "J \ {0.. X \ sets (PiM J M) \ CI J X = C 0 n (\_. undefined) (PF.emb {0..
  apply (subst emeasure_CI', simp_all add: finite_subset)
  apply (subst emeasure_C[symmetric, of "up_to J" n])
  apply (auto simp: finite_subset up_to_iff_Ico up_to_less)
  apply (subst prod_emb_trans)
  apply (auto simp: up_to_less finite_subset up_to_iff_Ico)
  done

lemma lim:
  assumes J: "finite J" and X: "X \ sets (PiM J M)"
  shows "emeasure PF.lim (PF.emb UNIV J X) = emeasure (CI J) X"
proof (rule PF.emeasure_lim[OF J subset_UNIV X])
  fix J X' assume J[simp]: "\i. finite (J i)" and X'[measurable]: "\i. X' i \ sets (Pi\<^sub>M (J i) M)"
    and dec: "decseq (\i. PF.emb UNIV (J i) (X' i))"
  define X where "X n =
    (\<Inter>i\<in>{i. J i \<subseteq> {0..< n}}. PF.emb {0..<n} (J i) (X' i)) \<inter> space (PiM {0..<n} M)" for n

  have sets_X[measurable]: "X n \ sets (PiM {0..
    by (cases "{i. J i \ {0..< n}} = {}")
       (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int)

  have dec_X: "n \ m \ X m \ PF.emb {0..
    unfolding X_def using ivl_subset[of 0 n 0 m]
    by (cases "{i. J i \ {0..< n}} = {}")
       (auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset)

  have dec_X': "PF.emb {0.. j) \<subseteq> PF.emb {0..<n} (J i) (X' i)"
    if [simp]: "J i \ {0.. {0.. j" for n i j
    by (rule PF.emb_preserve_mono[of "{0.. UNIV]) (auto del: subsetI intro: dec[THEN antimonoD])

  assume "0 < (INF i. CI (J i) (X' i))"
  also have "\ \ (INF i. C 0 i (\x. undefined) (X i))"
  proof (intro INF_greatest)
    fix n
    interpret C: prob_space "C 0 n (\x. undefined)"
      by (rule prob_space_C) simp
    show "(INF i. CI (J i) (X' i)) \ C 0 n (\x. undefined) (X n)"
    proof cases
      assume "{i. J i \ {0..< n}} = {}" with C.emeasure_space_1 show ?thesis
        by (auto simp add: X_def space_C intro!: INF_lower2[of 0] prob_space.measure_le_1 PF.prob_space_P)
    next
      assume *: "{i. J i \ {0..< n}} \ {}"
      have "(INF i. CI (J i) (X' i)) \
          (INF i\<in>{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
        by (intro INF_superset_mono) (auto simp: emeasure_CI)
      also have "\ = C 0 n (\_. undefined) (\i\{i. J i \ {0..
        using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
      also have "\ = C 0 n (\_. undefined) (X n)"
        using * by (auto simp add: X_def INT_extend_simps)
      finally show "(INF i. CI (J i) (X' i)) \ C 0 n (\_. undefined) (X n)" .
    qed
  qed
  finally have pos: "0 < (INF i. C 0 i (\x. undefined) (X i))" .
  from less_INF_D[OF this, of 0] have "X 0 \ {}"
    by auto

  { fix \<omega> n assume \<omega>: "\<omega> \<in> space (PiM {0..<n} M)"
    let ?C = "\i. emeasure (C n i \) (X (n + i))"
    let ?C' = "\i x. emeasure (C (Suc n) i (fun_upd \ n x)) (X (Suc n + i))"
    have M: "\i. ?C' i \ borel_measurable (P n \)"
      using \<omega>[measurable, simp] measurable_fun_upd[where J="{0..<n}"] by measurable auto

    assume "0 < (INF i. ?C i)"
    also have "\ \ (INF i. emeasure (C n (1 + i) \) (X (n + (1 + i))))"
      by (intro INF_greatest INF_lower) auto
    also have "\ = (INF i. \\<^sup>+x. ?C' i x \P n \)"
      using \<omega> measurable_C[of "Suc n"]
      apply (intro INF_cong refl)
      apply (subst split_C[symmetric, OF \<omega>])
      apply (subst emeasure_bind[OF _ _ sets_X])
      apply (simp_all del: C.simps add: space_C)
      apply measurable
      apply simp
      apply (simp add: bind_return[OF measurable_eP] nn_integral_eP)
      done
    also have "\ = (\\<^sup>+x. (INF i. ?C' i x) \P n \)"
    proof (rule nn_integral_monotone_convergence_INF_AE[symmetric])
      have "(\\<^sup>+x. ?C' 0 x \P n \) \ (\\<^sup>+x. 1 \P n \)"
        by (intro nn_integral_mono) (auto split: split_indicator)
      also have "\ < \"
        using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp
      finally show "(\\<^sup>+x. ?C' 0 x \P n \) < \" .
    next
      show "AE x in P n \. ?C' (Suc i) x \ ?C' i x" for i
      proof (rule AE_I2)
        fix x assume "x \ space (P n \)"
        with \<omega> have \<omega>': "fun_upd \<omega> n x \<in> space (PiM {0..<Suc n} M)"
          by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
        with \<omega> show "?C' (Suc i) x \<le> ?C' i x"
          apply (subst emeasure_C[symmetric, of i "Suc i"])
          apply (auto intro!: emeasure_mono[OF dec_X] del: subsetI
                      simp: sets_C space_P)
          apply (subst sets_bind[OF sets_eP])
          apply (simp_all add: space_C space_P)
          done
      qed
    qed fact
    finally have "(\\<^sup>+x. (INF i. ?C' i x) \P n \) \ 0"
      by simp
    with M have "\\<^sub>F x in ae_filter (P n \). 0 < (INF i. ?C' i x)"
       by (subst (asm) nn_integral_0_iff_AE)
          (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le zero_less_iff_neq_zero)
    then have "\\<^sub>F x in ae_filter (P n \). x \ space (M n) \ 0 < (INF i. ?C' i x)"
      by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>)
    then obtain x where "x \ space (M n)" "0 < (INF i. ?C' i x)"
      by (auto dest: frequently_ex)
    from this(2)[THEN less_INF_D, of 0] this(2)
    have "\x. fun_upd \ n x \ X (Suc n) \ 0 < (INF i. ?C' i x)"
      by (intro exI[of _ x]) (simp split: split_indicator_asm) }
  note step = this

  let ?\<omega> = "\<lambda>\<omega> n x. (restrict \<omega> {0..<n})(n := x)"
  let ?L = "\\ n r. INF i. emeasure (C (Suc n) i (?\ \ n r)) (X (Suc n + i))"
  have *: "(\i. i < n \ ?\ \ i (\ i) \ X (Suc i)) \
    restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" for \<omega> n
    using sets.sets_into_space[OF sets_X, of n]
    by (cases n) (auto simp: atLeastLessThanSuc restrict_def[of _ "{}"])
  have "\\. \n. ?\ \ n (\ n) \ X (Suc n) \ 0 < ?L \ n (\ n)"
  proof (rule dependent_wellorder_choice)
    fix n \<omega> assume IH: "\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i) \<and> 0 < ?L \<omega> i (\<omega> i)"
    show "\r. ?\ \ n r \ X (Suc n) \ 0 < ?L \ n r"
    proof (rule step)
      show "restrict \ {0.. space (Pi\<^sub>M {0..
        using IH[THEN conjunct1] by (rule *)
      show "0 < (INF i. emeasure (C n i (restrict \ {0..
      proof (cases n)
        case 0 with pos show ?thesis
          by (simp add: CI_def restrict_def)
      next
        case (Suc i) then show ?thesis
          using IH[of i, THEN conjunct2] by (simp add: atLeastLessThanSuc)
      qed
    qed
  qed (simp cong: restrict_cong)
  then obtain \<omega> where \<omega>: "\<And>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n)"
    by auto
  from this[THEN *] have \<omega>_space: "\<omega> \<in> space (PiM UNIV M)"
    by (auto simp: space_PiM PiE_iff Ball_def)
  have *: "\ \ PF.emb UNIV {0..
  proof (cases n)
    case 0 with \<omega>_space \<open>X 0 \<noteq> {}\<close> sets.sets_into_space[OF sets_X, of 0] show ?thesis
      by (auto simp add: space_PiM prod_emb_def restrict_def PiE_iff)
  next
    case (Suc i) then show ?thesis
      using \<omega>[of i] \<omega>_space by (auto simp: prod_emb_def space_PiM PiE_iff atLeastLessThanSuc)
  qed
  have **: "{i. J i \ {0.. {}" for n
    by (auto intro!: exI[of _ n] up_to J)
  have "\ \ PF.emb UNIV (J n) (X' n)" for n
    using *[of "up_to (J n)"] up_to[of "J n"] by (simp add: X_def prod_emb_Int prod_emb_INT[OF **])
  then show "(\i. PF.emb UNIV (J i) (X' i)) \ {}"
    by auto
qed

lemma distr_lim: assumes J[simp]: "finite J" shows "distr PF.lim (PiM J M) (\x. restrict x J) = CI J"
  apply (rule measure_eqI)
  apply (simp add: CI_def)
  apply (simp add: emeasure_distr measurable_cong_sets[OF PF.sets_lim] lim[symmetric] prod_emb_def space_PiM)
  done

end

lemma (in product_prob_space) emeasure_lim_emb:
  assumes *: "finite J" "J \ I" "X \ sets (PiM J M)"
  shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X"
proof (rule emeasure_lim[OF *], goal_cases)
  case (1 J X)

  have "\Q. (\i. sets Q = PiM (\i. J i) M \ distr Q (PiM (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M)"
  proof cases
    assume "finite (\i. J i)"
    then have "distr (PiM (\i. J i) M) (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M" for i
      by (intro distr_restrict[symmetric]) auto
    then show ?thesis
      by auto
  next
    assume inf: "infinite (\i. J i)"
    moreover have count: "countable (\i. J i)"
      using 1(3) by (auto intro: countable_finite)
    define f where "f = from_nat_into (\i. J i)"
    define t where "t = to_nat_on (\i. J i)"
    have ft[simp]: "x \ J i \ f (t x) = x" for x i
      unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto
    have tf[simp]: "t (f i) = i" for i
      unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count)
    have inj_t: "inj_on t (\i. J i)"
      using count by (auto simp: t_def)
    then have inj_t_J: "inj_on t (J i)" for i
      by (rule inj_on_subset) auto
    interpret IT: Ionescu_Tulcea "\i \. M (f i)" "\i. M (f i)"
      by standard auto
    interpret Mf: product_prob_space "\x. M (f x)" UNIV
      by standard
    have C_eq_PiM: "IT.C 0 n (\_. undefined) = PiM {0..x. M (f x))" for n
    proof (induction n)
      case 0 then show ?case
        by (auto simp: PiM_empty intro!: measure_eqI dest!: subset_singletonD)
    next
      case (Suc n) then show ?case
        apply (auto intro!: measure_eqI simp: sets_bind[OF IT.sets_eP] emeasure_bind[OF _ IT.measurable_eP])
        apply (auto simp: Mf.product_nn_integral_insert nn_integral_indicator[symmetric] atLeastLessThanSuc IT.emeasure_eP space_PiM
                    split: split_indicator simp del: nn_integral_indicator intro!: nn_integral_cong)
        done
    qed
    have CI_eq_PiM: "IT.CI X = PiM X (\x. M (f x))" if X: "finite X" for X
      by (auto simp: IT.up_to_less X  IT.CI_def C_eq_PiM intro!: Mf.distr_restrict[symmetric])

    let ?Q = "distr IT.PF.lim (PiM (\i. J i) M) (\\. \x\\i. J i. \ (t x))"
    { fix i
      have "distr ?Q (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) =
        distr IT.PF.lim (Pi\<^sub>M (J i) M) ((\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<circ> (\<lambda>\<omega>. restrict \<omega> (t`J i)))"
      proof (subst distr_distr)
        have "(\\. \ (t x)) \ measurable (Pi\<^sub>M UNIV (\x. M (f x))) (M x)" if x: "x \ J i" for x i
          using measurable_component_singleton[of "t x" "UNIV" "\x. M (f x)"] unfolding ft[OF x] by simp
        then show "(\\. \x\\i. J i. \ (t x)) \ measurable IT.PF.lim (Pi\<^sub>M (\(J ` UNIV)) M)"
          by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
      qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
      also have "\ = distr (distr IT.PF.lim (PiM (t`J i) (\x. M (f x))) (\\. restrict \ (t`J i))) (Pi\<^sub>M (J i) M) (\\. \n\J i. \ (t n))"
      proof (intro distr_distr[symmetric])
        have "(\\. \ (t x)) \ measurable (Pi\<^sub>M (t`J i) (\x. M (f x))) (M x)" if x: "x \ J i" for x
          using measurable_component_singleton[of "t x" "t`J i" "\x. M (f x)"] x unfolding ft[OF x] by auto
        then show "(\\. \n\J i. \ (t n)) \ measurable (Pi\<^sub>M (t ` J i) (\x. M (f x))) (Pi\<^sub>M (J i) M)"
          by (auto intro!: measurable_restrict)
      qed (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
      also have "\ = distr (PiM (t`J i) (\x. M (f x))) (Pi\<^sub>M (J i) M) (\\. \n\J i. \ (t n))"
        using \<open>finite (J i)\<close> by (subst IT.distr_lim) (auto simp: CI_eq_PiM)
      also have "\ = Pi\<^sub>M (J i) M"
        using Mf.distr_reorder[of t "J i"] by (simp add: 1 inj_t_J cong: PiM_cong)
      finally have "distr ?Q (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M" . }
    then show "\Q. \i. sets Q = PiM (\i. J i) M \ distr Q (Pi\<^sub>M (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M"
      by (intro exI[of _ ?Q]) auto
  qed
  then obtain Q where sets_Q: "sets Q = PiM (\i. J i) M"
    and Q: "\i. distr Q (PiM (J i) M) (\x. restrict x (J i)) = Pi\<^sub>M (J i) M" by blast

  from 1 interpret Q: prob_space Q
    by (intro prob_space_distrD[of "\x. restrict x (J 0)" Q "PiM (J 0) M"])
       (auto simp: Q measurable_cong_sets[OF sets_Q]
                intro!: prob_space_P measurable_restrict measurable_component_singleton)

  have "0 < (INF i. emeasure (Pi\<^sub>M (J i) M) (X i))" by fact
  also have "\ = (INF i. emeasure Q (emb (\i. J i) (J i) (X i)))"
    by (simp add: emeasure_distr_restrict[OF _ sets_Q 1(4), symmetric] SUP_upper Q)
  also have "\ = emeasure Q (\i. emb (\i. J i) (J i) (X i))"
  proof (rule INF_emeasure_decseq)
    from 1 show "decseq (\n. emb (\i. J i) (J n) (X n))"
      by (intro antimonoI emb_preserve_mono[where X="emb (\i. J i) (J n) (X n)" and L=I and J="\i. J i" for n]
         measurable_prod_emb)
         (auto simp: SUP_least SUP_upper antimono_def)
  qed (insert 1, auto simp: sets_Q)
  finally have "(\i. emb (\i. J i) (J i) (X i)) \ {}"
    by auto
  moreover have "(\i. emb I (J i) (X i)) = {} \ (\i. emb (\i. J i) (J i) (X i)) = {}"
    using 1 by (intro emb_injective[of "\i. J i" I _ "{}"] sets.countable_INT) (auto simp: SUP_least SUP_upper)
  ultimately show ?case by auto
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.38 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.