awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq.{u_1 + 1} (α := Set ((n : ℕ) → X n)) (⋂ (n : ℕ), A n) ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X (↑i : ℕ)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
a : (n : ℕ) → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X (↑i : ℕ))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (Iic (a n)) (S n)
χ : (n : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (α := X) (χ n) (↑(Iic (a n)) : Set ℕ)
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv :
  ∀ (k M n : ℕ) (h : a n ≤ M), lmarginalPartialTraj (X := X) κ k M (χ n) = lmarginalPartialTraj (X := X) κ k (a n) (χ n)
anti_lma :
  ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x
l : (k : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞
hl :
  ∀ (k : ℕ) (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = ε
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → (y : (i : ↥(Iic k)) → X (↑i : ℕ)) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X (↑i : ℕ))
    (h :
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) y))
    (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤
      lmarginalPartialTraj (X := X) κ (k + 1) (a n) (χ n)
        (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction (X := X) x₀ ind
main :
  ∀ (k : ℕ) (hk : p ≤ k) (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) (frestrictLe (π := X) k z))
aux :
  ∀ (x : (i : ℕ) → X i) (n : ℕ),
    (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
this : 0 ≠ ε
⊢ ∀ (n : ℕ), z ∈ A n

Tactic:
have mem n : z ∈ A n := by
    have : 0 < χ n z := by
      rw [← lmarginalPartialTraj_le κ (le_max_right p (a n)) (mχ n),
        ← updateFinset_frestrictLe (a := a n) z]
      simpa using lt_of_lt_of_le this.symm.bot_lt (main _ (le_max_left _ _) z n)
    exact Set.mem_of_indicator_ne_zero (ne_of_lt this).symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq.{u_1 + 1} (α := Set ((n : ℕ) → X n)) (⋂ (n : ℕ), A n) ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X (↑i : ℕ)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
a : (n : ℕ) → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X (↑i : ℕ))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (Iic (a n)) (S n)
χ : (n : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (α := X) (χ n) (↑(Iic (a n)) : Set ℕ)
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv :
  ∀ (k M n : ℕ) (h : a n ≤ M), lmarginalPartialTraj (X := X) κ k M (χ n) = lmarginalPartialTraj (X := X) κ k (a n) (χ n)
anti_lma :
  ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x
l : (k : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞
hl :
  ∀ (k : ℕ) (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = ε
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → (y : (i : ↥(Iic k)) → X (↑i : ℕ)) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X (↑i : ℕ))
    (h :
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) y))
    (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤
      lmarginalPartialTraj (X := X) κ (k + 1) (a n) (χ n)
        (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction (X := X) x₀ ind
main :
  ∀ (k : ℕ) (hk : p ≤ k) (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) (frestrictLe (π := X) k z))
aux :
  ∀ (x : (i : ℕ) → X i) (n : ℕ),
    (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
this : 0 ≠ ε
mem : ∀ (n : ℕ), z ∈ A n
⊢ False

Tactic:
exact (A_inter ▸ Set.mem_iInter.2 mem).elim
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ (trajContent (X := X) κ x₀).IsSigmaSubadditive (C := measurableCylinders X)

Tactic:
isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)

Premises used: MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum, MeasureTheory.isSetRing_measurableCylinders
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
refine :
  ∀ (f : ℕ → Set ((i : ℕ) → X i)) (hf : ∀ (i : ℕ), f i ∈ measurableCylinders X)
    (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X) (hf' : Pairwise (Disjoint on f)),
    Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ (trajContent (X := X) κ x₀).IsSigmaSubadditive (C := measurableCylinders X)

Tactic:
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)

Premises used: MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum, MeasureTheory.isSetRing_measurableCylinders
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
⊢ Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders
    (trajContent κ x₀) (fun _ _ ↦ trajContent_ne_top) ?_ hf hf_Union hf'

Premises used: MeasureTheory.isSetRing_measurableCylinders, ProbabilityTheory.Kernel.trajContent, MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero, ProbabilityTheory.Kernel.trajContent_ne_top
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
refine :
  ∀ ⦃s : ℕ → Set ((i : ℕ) → X i)⦄,
    (∀ (n : ℕ), s n ∈ measurableCylinders X) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set ((i : ℕ) → X i)) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (s n)) atTop
            (𝓝 0)
⊢ Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
refine addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders
    (trajContent κ x₀) (fun _ _ ↦ trajContent_ne_top) ?_ hf hf_Union hf'

Premises used: MeasureTheory.isSetRing_measurableCylinders, ProbabilityTheory.Kernel.trajContent, MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero, ProbabilityTheory.Kernel.trajContent_ne_top
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
⊢ ∀ ⦃s : ℕ → Set ((i : ℕ) → X i)⦄,
    (∀ (n : ℕ), s n ∈ measurableCylinders X) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set ((i : ℕ) → X i)) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (s n)) atTop
            (𝓝 0)

Tactic:
fun s hs anti_s inter_s ↦ trajContent_tendsto_zero hs anti_s inter_s x₀

Premises used: ProbabilityTheory.Kernel.trajContent_tendsto_zero
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
⊢ ∀ ⦃s : ℕ → Set ((i : ℕ) → X i)⦄,
    (∀ (n : ℕ), s n ∈ measurableCylinders X) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set ((i : ℕ) → X i)) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (s n)) atTop
            (𝓝 0)

Tactic:
exact fun s hs anti_s inter_s ↦ trajContent_tendsto_zero hs anti_s inter_s x₀

Premises used: ProbabilityTheory.Kernel.trajContent_tendsto_zero
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hC_gen : MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)
hs : cylinder (α := X) (Iic 0) Set.univ ∈ measurableCylinders X
⊢ Eq (α := ℝ≥0∞) ((trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← cylinder_univ (Iic 0), trajFun, AddContent.measure_eq, trajContent_cylinder .univ,
      measure_univ]

Premises used: ProbabilityTheory.Kernel.trajContent_cylinder, MeasureTheory.AddContent.measure_eq, MeasureTheory.cylinder_univ, MeasureTheory.IsProbabilityMeasure.measure_univ, Finset.Iic, ProbabilityTheory.Kernel.trajFun, OfNat.ofNat, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)

Tactic:
generateFrom_measurableCylinders.symm

Premises used: MeasureTheory.generateFrom_measurableCylinders, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)

Tactic:
exact generateFrom_measurableCylinders.symm

Premises used: MeasureTheory.generateFrom_measurableCylinders, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ cylinder (α := X) (Iic 0) Set.univ ∈ measurableCylinders X

Tactic:
cylinder_mem_measurableCylinders _ _ .univ

Premises used: MeasureTheory.cylinder_mem_measurableCylinders, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ cylinder (α := X) (Iic 0) Set.univ ∈ measurableCylinders X

Tactic:
exact cylinder_mem_measurableCylinders _ _ .univ

Premises used: MeasureTheory.cylinder_mem_measurableCylinders, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ IsProjectiveLimit (α := X) (trajFun (X := X) κ a x₀)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x₀)

Tactic:
isProjectiveLimit_nat_iff (isProjectiveMeasureFamily_partialTraj κ x₀) _ |>.2 fun n ↦ ?_

Premises used: Iff.mpr, MeasureTheory.isProjectiveLimit_nat_iff, ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
refine :
  ∀ (n : ℕ),
    Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀))
      (inducedFamily (X := X)
        (fun (b : ℕ) ↦
          (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
        (Iic n))
⊢ IsProjectiveLimit (α := X) (trajFun (X := X) κ a x₀)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x₀)

Tactic:
refine isProjectiveLimit_nat_iff (isProjectiveMeasureFamily_partialTraj κ x₀) _ |>.2 fun n ↦ ?_

Premises used: Iff.mpr, MeasureTheory.isProjectiveLimit_nat_iff, ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
h :
  ∀ (s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀) : Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((inducedFamily (X := X)
                (fun (b : ℕ) ↦
                  (partialTraj (X := X) κ a b :
                      (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                    x₀)
                (Iic n) :
              Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) :
            (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀))
    (inducedFamily (X := X)
      (fun (b : ℕ) ↦
        (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      (Iic n))

Tactic:
ext s ms
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
h : MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)
h₁ : frestrictLe (π := X) n ⁻¹' s ∈ measurableCylinders X
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀) : Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((inducedFamily (X := X)
              (fun (b : ℕ) ↦
                (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                  x₀)
              (Iic n) :
            Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Measure.map_apply (measurable_frestrictLe n) ms, trajFun, AddContent.measure_eq, trajContent,
    projectiveFamilyContent_congr _ (frestrictLe n ⁻¹' s) rfl ms]

Premises used: MeasureTheory.AddContent.measure_eq, MeasureTheory.Measure.map_apply, MeasureTheory.projectiveFamilyContent_congr, ProbabilityTheory.Kernel.trajContent, Set.preimage, Preorder.measurable_frestrictLe, ProbabilityTheory.Kernel.trajFun, Preorder.frestrictLe, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
⊢ MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)

Tactic:
generateFrom_measurableCylinders.symm

Premises used: MeasureTheory.generateFrom_measurableCylinders, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
⊢ MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)

Tactic:
exact generateFrom_measurableCylinders.symm

Premises used: MeasureTheory.generateFrom_measurableCylinders, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
⊢ frestrictLe (π := X) n ⁻¹' s ∈ measurableCylinders X

Tactic:
cylinder_mem_measurableCylinders _ _ ms

Premises used: Set.Mem, MeasureTheory.cylinder, MeasureTheory.cylinder_mem_measurableCylinders, Preorder.frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
⊢ frestrictLe (π := X) n ⁻¹' s ∈ measurableCylinders X

Tactic:
exact cylinder_mem_measurableCylinders _ _ ms

Premises used: MeasureTheory.cylinder_mem_measurableCylinders
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
h :
  ∀ (s : Set ((n : ℕ) → X n)),
    MeasurableSet s →
      Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a b : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) s
⊢ Measurable (trajFun (X := X) κ a)

Tactic:
apply Measure.measurable_of_measurable_coe

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    ∅ ⋯

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
cylinder :
  ∀ (t : Set ((n : ℕ) → X n)) (ht : t ∈ measurableCylinders X),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      t ⋯
compl :
  ∀ (t : Set ((n : ℕ) → X n)) (mt : MeasurableSet t)
    (ht :
      (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
          Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
            (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
        t mt),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      tᶜ ⋯
union :
  ∀ (f : ℕ → Set ((n : ℕ) → X n)) (disf : Pairwise (Disjoint on f)) (mf : ∀ (i : ℕ), MeasurableSet (f i))
    (hf :
      ∀ (i : ℕ),
        (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
            Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
              (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
          (f i) ⋯),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      (⋃ (i : ℕ), f i) ⋯
⊢ ∀ (s : Set ((n : ℕ) → X n)),
    MeasurableSet s →
      Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a b : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) s

Tactic:
refine MeasurableSpace.induction_on_inter
    (C := fun t ht ↦ Measurable (fun x₀ ↦ trajFun κ a x₀ t))
    (s := measurableCylinders X) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (by simp) (fun t ht ↦ ?cylinder) (fun t mt ht ↦ ?compl)
    (fun f disf mf hf ↦ ?union)
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
⊢ ∃ (N : ℕ) (S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))), MeasurableSet S ∧ t = cylinder (α := X) (Iic N) S

Tactic:
simpa [measurableCylinders_nat] using ht

Premises used: MeasureTheory.measurableCylinders_nat