Theory Projective_Family

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

section ‹Projective Family›

theory Projective_Family
imports Giry_Monad
begin

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

lemma vimage_restrict_preserve_mono:
  assumes J: "J  I"
  and sets: "A  (ΠE iJ. S i)" "B  (ΠE iJ. S i)" and ne: "(ΠE iI. S i)  {}"
  and eq: "(λx. restrict x J) -` A  (ΠE iI. S i)  (λx. restrict x J) -` B  (ΠE iI. 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  (ΠE iJ. S i)"
    have "merge J (I - J) (x,y)  (λx. restrict x J) -` A  (ΠE iI. S i)"
      using y x J  I PiE_cancel_merge[of "J" "I - J" x y S] xA
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
    also have "  (λx. restrict x J) -` B  (ΠE iI. S i)" by fact
    finally show "x  B"
      using y x J  I PiE_cancel_merge[of "J" "I - J" x y S] xA eq
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
  qed (insert xA 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 (PiM J M)" "Y  sets (PiM J M)"
  assumes "emb L J X  emb L J Y"
  shows "X  Y"
proof (rule vimage_restrict_preserve_mono)
  show "X  (ΠE iJ. space (M i))" "Y  (ΠE iJ. space (M i))"
    using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
  show "(ΠE iL. space (M i))  {}"
    using L  I by (auto simp add: not_empty_M space_PiM[symmetric])
  show "(λx. restrict x J) -` X  (ΠE iL. space (M i))  (λx. restrict x J) -` Y  (ΠE iL. space (M i))"
    using prod_emb L M J X  prod_emb L M J Y by (simp add: prod_emb_def)
qed fact

lemma emb_injective:
  assumes L: "J  L" "L  I" and X: "X  sets (PiM J M)" and Y: "Y  sets (PiM 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 (PiM 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 (PiM 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 (PiM I M). f i  A} = emb I {i} (ΠE j{i}. A)"
      by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def)
    with iI A show "{f  space (PiM 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. JI. finite J  (Xsets (PiM 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 (PiM 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 (PiM 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 (λ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 "μ. (sgenerator. μ 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 (PiM 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 (ni. J n) (emb (ni. J n) (J i) (X i)))  {}"
      proof (rule cont)
        show "decseq (λi. emb I (ni. J n) (emb (ni. J n) (J i) (X i)))"
          using * decseq A by (subst prod_emb_trans) (auto simp: A[abs_def])
        show "0 < (INF i. P (ni. J n) (emb (ni. J n) (J i) (X i)))"
           using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest)
        show "incseq (λi. ni. 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 xy] *
        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: "sgenerator. μ s = μ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 (PiM 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
  unfolding projective_family_def
proof (intro conjI allI impI distr_restrict)
  show "J. finite J  prob_space (PiM 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} M) (subprob_algebra (M i))"
  assumes prob_space_P: "i x. x  space (PiM {0..<i} M)  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..<i}  space (PiM {0..<i} M)"
    by (auto simp: space_PiM PiE_iff)
  then interpret prob_space "P i (restrict x {0..<i})"
    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..<n} M)  space (P n x) = space (M n)"
  by (simp add: P[THEN subprob_measurableD(1)])

lemma sets_P[measurable_cong]: "x  space (PiM {0..<n} M)  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..<Suc n} M) (fun_upd ω n)"

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

lemma space_eP:
  "x  space (PiM {0..<n} M)  space (eP n x) = space (PiM {0..<Suc n} M)"
  by (simp add: eP_def)

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

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

lemma nn_integral_eP:
  "ω  space (PiM {0..<n} M)  f  borel_measurable (PiM {0..<Suc n} M) 
    (+x. f x eP n ω) = (+x. f (fun_upd ω n x) P n ω)"
  unfolding eP_def
  by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..<n}"] simp: space_PiM PiE_iff)

lemma emeasure_eP:
  assumes ω[simp]: "ω  space (PiM {0..<n} M)" and A[measurable]: "A  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 ω 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..<n} M) ω"
| "C n (Suc m) ω = C n m ω  eP (n + m)"

lemma measurable_C[measurable]:
  "C n m  measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))"
  by (induction m) auto

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

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

lemma prob_space_C: "x  space (PiM {0..<n} M)  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..<Suc (n + m)} M"]
             simp: space_C prob_space_eP)
qed (auto intro!: prob_space_return simp: space_PiM)

lemma split_C:
  assumes ω: "ω  space (PiM {0..<n} M)" shows "(C n m ω  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..<n+m} M)"
    and nonneg: "x. x  space (PiM {0..<n+m} M)  0  f x"
    and x: "x  space (PiM {0..<n} M)"
  shows "(+x. f x C n m x) = (+x. f (restrict x {0..<n+m}) C n m' x)"
  using m  m'
proof (induction rule: dec_induct)
  case (step i)
  let ?E = "λx. f (restrict x {0..<n + m})" and ?C = "λi f. +x. f x C n i x"
  from mi 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..<n+m} M)" and [simp]: "x  space (PiM {0..<n} M)"
  shows "emeasure (C n m' x) (prod_emb {0..<n + m'} M {0..<n+m} A) = emeasure (C n m x) A"
  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..<n} M)"
  shows "C n m x = distr (C n m' x) (PiM {0..<n+m} M) (λx. restrict x {0..<n+m})"
proof (rule measure_eqI)
  fix A assume "A  sets (C n m x)"
  with m  m' show "emeasure (C n m x) A = emeasure (distr (C n m' x) (PiM {0..<n + m} M) (λx. restrict x {0..<n + m})) A"
    by (subst emeasure_C[symmetric, OF 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. in. 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  (iJ. 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..<n}"
  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 (PiM H M) (PiM J M)" for H J
    by (auto intro!: measurable_restrict)

  show "J  H  finite H  CI J = distr (CI H) (PiM 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..<up_to J} J X)"
  unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C)

lemma emeasure_CI:
  "J  {0..<n}  X  sets (PiM J M)  CI J X = C 0 n (λ_. undefined) (PF.emb {0..<n} J X)"
  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 (PiM (J i) M)"
    and dec: "decseq (λi. PF.emb UNIV (J i) (X' i))"
  define X where "X n =
    (i{i. J i  {0..< n}}. PF.emb {0..<n} (J i) (X' i))  space (PiM {0..<n} M)" for n

  have sets_X[measurable]: "X n  sets (PiM {0..<n} M)" for n
    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..<m} {0..<n} (X n)" for n m
    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..<n} (J j) (X' j)  PF.emb {0..<n} (J i) (X' i)"
    if [simp]: "J i  {0..<n}" "J j  {0..<n}" "i  j" for n i j
    by (rule PF.emb_preserve_mono[of "{0..<n}" 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{i. J i  {0..<n}}. C 0 n (λ_. 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..<n}}. (PF.emb {0..<n} (J i) (X' i)))"
        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 ω n assume ω: "ω  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 ω[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. +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 " = (+x. (INF i. ?C' i x) P n ω)"
    proof (rule nn_integral_monotone_convergence_INF_AE[symmetric])
      have "(+x. ?C' 0 x P n ω)  (+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 "(+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 ω have ω': "fun_upd ω n x  space (PiM {0..<Suc n} M)"
          by (auto simp: space_P[OF ω] space_PiM PiE_iff extensional_def)
        with ω show "?C' (Suc i) x  ?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 "(+x. (INF i. ?C' i x) P n ω)  0"
      by simp
    with M have "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 "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. 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  = "λω n x. (restrict ω {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 ω {0..<n}  space (PiM {0..<n} M)" for ω 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..<n}  space (PiM {0..<n} M)"
        using IH[THEN conjunct1] by (rule *)
      show "0 < (INF i. emeasure (C n i (restrict ω {0..<n})) (X (n + i)))"
      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 ω 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..<n} (X n)" for n
  proof (cases n)
    case 0 with ω_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..<up_to (J n)}}  {}" 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 (PiM 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)) = PiM (J i) M)"
  proof cases
    assume "finite (i. J i)"
    then have "distr (PiM (i. J i) M) (PiM (J i) M) (λx. restrict x (J i)) = PiM (J i) M" for i
      by (intro distr_restrict[symmetric]) auto
    then show ?thesis
      by auto
  next
    assume inf: "infinite (i. J i)"
    moreover have count: "countable (i. J i)"
      using 1(3) by (auto intro: countable_finite)
    define f where "f = from_nat_into (i. J i)"
    define t where "t = to_nat_on (i. J i)"
    have ft[simp]: "x  J i  f (t x) = x" for x i
      unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto
    have tf[simp]: "t (f i) = i" for i
      unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count)
    have inj_t: "inj_on t (i. J i)"
      using count by (auto simp: t_def)
    then have inj_t_J: "inj_on t (J i)" for i
      by (rule subset_inj_on) auto
    interpret IT: Ionescu_Tulcea "λi ω. M (f i)" "λi. M (f i)"
      by standard auto
    interpret Mf: product_prob_space "λx. M (f x)" UNIV
      by standard
    have C_eq_PiM: "IT.C 0 n (λ_. undefined) = PiM {0..<n} (λ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) (λω. λxi. J i. ω (t x))"
    { fix i
      have "distr ?Q (PiM (J i) M) (λx. restrict x (J i)) =
        distr IT.PF.lim (PiM (J i) M) ((λω. λnJ i. ω (t n))  (λω. restrict ω (t`J i)))"
      proof (subst distr_distr)
        have "(λω. ω (t x))  measurable (PiM 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 "(λω. λxi. J i. ω (t x))  measurable IT.PF.lim (PiM ((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))) (PiM (J i) M) (λω. λnJ i. ω (t n))"
      proof (intro distr_distr[symmetric])
        have "(λω. ω (t x))  measurable (PiM (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 "(λω. λnJ i. ω (t n))  measurable (PiM (t ` J i) (λx. M (f x))) (PiM (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))) (PiM (J i) M) (λω. λnJ i. ω (t n))"
        using finite (J i) by (subst IT.distr_lim) (auto simp: CI_eq_PiM)
      also have " = PiM (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 (PiM (J i) M) (λx. restrict x (J i)) = PiM (J i) M" . }
    then show "Q. i. sets Q = PiM (i. J i) M  distr Q (PiM (J i) M) (λx. restrict x (J i)) = PiM (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)) = PiM (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 (PiM (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