awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 l)
have inr : ∀ (h : ∃ (l : ℝ≥0∞), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 l)),
  ∃ (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)
-- 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_1 : ∀ (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
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)
have h₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (pure ⊥)
Tactic: rw [OrderBot.atBot_eq] at h
Cleared hypotheses: h
-- 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)
anti_lma :
  ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have this : ∀ (k : ℕ) (x : (n : ℕ) → X n),
  ∃ (l : ℝ≥0∞), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 l)
Tactic: have this k x : ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l) := by
    obtain h | h := tendsto_atTop_of_antitone (anti_lma k x)
    · rw [OrderBot.atBot_eq] at h
      exact ⟨0, h.mono_right <| pure_le_nhds 0⟩
    · exact h
-- 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
this :
  ∀ (k : ℕ) (x : (n : ℕ) → X n),
    ∃ (l : ℝ≥0∞), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 l)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have choose : ∀ (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))),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
Tactic: choose l hl using this
Cleared hypotheses: this
-- 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)
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))
x y : (i : ℕ) → X i
⊢ l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
have this : Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)) atTop
  (𝓝 (l p (updateFinset (π := X) x (Iic p) x₀)))
Tactic: have := hl p (updateFinset x _ x₀)
-- 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)
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))
x y : (i : ℕ) → X i
this :
  Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)) atTop
    (𝓝 (l p (updateFinset (π := X) x (Iic p) x₀)))
⊢ l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
have this₁ : Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) y (Iic p) x₀)) atTop
  (𝓝 (l p (updateFinset (π := X) x (Iic p) x₀)))
Tactic: simp_rw [lma_const x y] at this
Cleared hypotheses: this
-- 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)
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))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
Tactic: have l_const x y : l p (updateFinset x _ x₀) = l p (updateFinset y _ x₀) := by
    have := hl p (updateFinset x _ x₀)
    simp_rw [lma_const x y] at this
    exact tendsto_nhds_unique this (hl p _)
-- 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
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₀)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have obtain : ∀ (ε : ℝ≥0∞) (hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = ε),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
Tactic: obtain ⟨ε, hε⟩ : ∃ ε, ∀ x, l p (updateFinset x _ x₀) = ε :=
      ⟨l p (updateFinset Classical.ofNonempty _ x₀), fun x ↦ l_const _ _⟩
-- 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)
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₀) = ε
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
Tactic: have hpos x n : ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x _ x₀) :=
    hε x ▸ ((anti_lma p _).le_of_tendsto (hl p _)) 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 : (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₀)
n : ℕ
x : (n : ℕ) → X n
⊢ χ n x ≤ 1
have hfg : ∀ a ∈ A n, LE.le (α := ℝ≥0∞) (1 a) 1
Tactic: apply Set.indicator_le
-- 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)
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₀)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
Tactic: have χ_le n x : χ n x ≤ 1 := by
    apply Set.indicator_le
    simp
-- 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
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
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
have choose! : ∀ (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))),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n)) atTop (𝓝 0)
Tactic: choose! ind hind using
    fun k y h ↦ le_lmarginalPartialTraj_succ χ_dep mχ (by simp : (1 : ℝ≥0∞) ≠ ∞)
      χ_le (anti_lma (k + 1)) (hl (k + 1)) ε y h