awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ (↑(Iic (k + 1)) : Set ℕ)
h1 : ¬i = k + 1
h2 : ¬i ≤ k
⊢ x' i = x_ i
have hi₁ : i ≤ k + 1
Tactic: rw [mem_coe, mem_Iic] at hi
Cleared hypotheses: hi, h1, h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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 : ℕ)
m : ℕ
hm : ∀ m_1 ≤ m, Nonempty.{u_1 + 1} (X m_1)
⊢ Nonempty.{u_1 + 1} (X (m + 1))
have this : Nonempty.{u_1 + 1} ((i : ↥(Iic m)) → X (↑i : ℕ))
Tactic: have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ℕ)
n : ℕ
⊢ Nonempty.{u_1 + 1} (X n)
have hz : Nonempty.{u_1 + 1} (X 0)
Tactic: induction n using Nat.case_strong_induction_on with
    | hz => exact ⟨x₀ ⟨0, mem_Iic.2 zero_le⟩⟩
    | hi m hm =>
      have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
      exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ℕ)
n : ℕ
hz : Nonempty.{u_1 + 1} (X 0)
⊢ Nonempty.{u_1 + 1} (X n)
have hi : ∀ (m : ℕ) (hm : ∀ m_1 ≤ m, Nonempty.{u_1 + 1} (X m_1)), Nonempty.{u_1 + 1} (X (m + 1))
Tactic: induction n using Nat.case_strong_induction_on with
    | hz => exact ⟨x₀ ⟨0, mem_Iic.2 zero_le⟩⟩
    | hi m hm =>
      have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
      exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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 : ℕ)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have x : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
Tactic: have _ n : Nonempty (X n) := by
    induction n using Nat.case_strong_induction_on with
    | hz => exact ⟨x₀ ⟨0, mem_Iic.2 zero_le⟩⟩
    | hi m hm =>
      have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
      exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have A_cyl : ∀ (n : ℕ), ∃ (a : ℕ) (S : Set ((i : ↥(Iic a)) → X (↑i : ℕ))), MeasurableSet S ∧ A n = cylinder (α := X) (Iic a) S
Tactic: have A_cyl n : ∃ a S, MeasurableSet S ∧ A n = cylinder (Iic a) S := by
    simpa [measurableCylinders_nat] using A_mem n
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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_cyl :
  ∀ (n : ℕ), ∃ (a : ℕ) (S : Set ((i : ↥(Iic a)) → X (↑i : ℕ))), MeasurableSet S ∧ A n = cylinder (α := X) (Iic a) S
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have choose : ∀ (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)),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
Tactic: choose a S mS A_eq using A_cyl
Cleared hypotheses: A_cyl
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
n : ℕ
⊢ Measurable (χ n)
have simp_rw : Measurable (β := ℝ≥0∞) ((cylinder (α := X) (Iic (a n)) (S n)).indicator 1)
Tactic: simp_rw [χ, A_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have mχ : ∀ (n : ℕ), Measurable (χ n)
Tactic: have mχ n : Measurable (χ n) := by
    simp_rw [χ, A_eq]
    exact (measurable_indicator_const_iff 1).2 <| (mS n).cylinder
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
n : ℕ
⊢ DependsOn (α := X) (χ n) (↑(Iic (a n)) : Set ℕ)
have simp_rw : DependsOn (α := X) (β := ℝ≥0∞) ((cylinder (α := X) (Iic (a n)) (S n)).indicator 1) (↑(Iic (a n)) : Set ℕ)
Tactic: simp_rw [χ, A_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have χ_dep : ∀ (n : ℕ), DependsOn (α := X) (χ n) (↑(Iic (a n)) : Set ℕ)
Tactic: have χ_dep n : DependsOn (χ n) (Iic (a n)) := by
    simp_rw [χ, A_eq]
    exact dependsOn_cylinder_indicator_const ..
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 ℕ)
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₀)
have refine : ∀ (i : ℕ) (hi : i ∈ (↑(Iic p) : Set ℕ)), updateFinset (π := X) x (Iic p) x₀ i = updateFinset (π := X) y (Iic p) x₀ i
Tactic: refine (χ_dep n).dependsOn_lmarginalPartialTraj p (mχ n) fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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 ℕ)
x y : (i : ℕ) → X i
n i : ℕ
hi : i ∈ (↑(Iic p) : Set ℕ)
⊢ updateFinset (π := X) x (Iic p) x₀ i = updateFinset (π := X) y (Iic p) x₀ i
have hi₁ : i ≤ p
Tactic: rw [mem_coe, mem_Iic] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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 ℕ)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have 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₀)
Tactic: have lma_const x y n :
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x _ x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y _ x₀) := by
    refine (χ_dep n).dependsOn_lmarginalPartialTraj p (mχ n) fun i hi ↦ ?_
    rw [mem_coe, mem_Iic] at hi
    simp [updateFinset, hi]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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₀)
m n : ℕ
hmn : m ≤ n
y : (n : ℕ) → X n
⊢ χ n y ≤ χ m y
have apply : ∀ (a : (n : ℕ) → X n) (ha : a ∈ A n), 1 a ≤ χ m a
Tactic: apply Set.indicator_le fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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₀)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have χ_anti : Antitone χ
Tactic: have χ_anti : Antitone χ := fun m n hmn y ↦ by
    apply Set.indicator_le fun a ha ↦ ?_
    simp [χ, A_anti hmn ha]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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 χ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have lma_inv : ∀ (k M n : ℕ) (h : a n ≤ M), lmarginalPartialTraj (X := X) κ k M (χ n) = lmarginalPartialTraj (X := X) κ k (a n) (χ n)
Tactic: have lma_inv k M n (h : a n ≤ M) :
      lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n) :=
    (χ_dep n).lmarginalPartialTraj_const_right (mχ n) h le_rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
k : ℕ
x : (n : ℕ) → X n
m n : ℕ
hmn : m ≤ n
⊢ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x ≤ lmarginalPartialTraj (X := X) κ k (a m) (χ m) x
have rw : lmarginalPartialTraj (X := X) κ k ((a n).max (a m)) (χ n) x ≤
  lmarginalPartialTraj (X := X) κ k ((a n).max (a m)) (χ m) x
Tactic: rw [← lma_inv k ((a n).max (a m)) n (le_max_left _ _),
      ← lma_inv k ((a n).max (a m)) m (le_max_right _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x
Tactic: have anti_lma k x : Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x := by
    intro m n hmn
    simp only
    rw [← lma_inv k ((a n).max (a m)) n (le_max_left _ _),
      ← lma_inv k ((a n).max (a m)) m (le_max_right _ _)]
    exact lmarginalPartialTraj_mono _ _ (χ_anti hmn) _
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
k : ℕ
x : (n : ℕ) → X n
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 l)
have inl : ∀ (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop atBot),
  ∃ (l : ℝ≥0∞), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 l)
Tactic: obtain h | h := tendsto_atTop_of_antitone (anti_lma k x)