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 b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
rw :
  Eq (α := ℝ≥0∞)
    ((projectiveFamilyContent (α := X) ⋯ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic b) S) : ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic b) S) : ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥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 b) :
          Measure ((k : ↥(Iic b)) → X (↑k : ℕ))) :
        (a : Set ((j : ↥(Iic b)) → X (↑j : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
          Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
        (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [trajContent, projectiveFamilyContent_cylinder _ mS, inducedFamily_Iic]
-- 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 b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
rw :
  Eq (α := ℝ≥0∞)
    ((projectiveFamilyContent (α := X) ⋯ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic b) S) : ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥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 b) :
            Measure ((k : ↥(Iic b)) → X (↑k : ℕ))) :
          (a : Set ((j : ↥(Iic b)) → X (↑j : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic b) S) : ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
          Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
        (a : Set ((j : ↥(Iic b)) → X (↑j : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
          Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
        (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [trajContent, projectiveFamilyContent_cylinder _ mS, inducedFamily_Iic]
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ (trajContent (X := X) κ (frestrictLe (π := X) a x₀) : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
      (cylinder (α := X) (Iic b) S) =
    lmarginalPartialTraj (X := X) κ a b ((cylinder (α := X) (Iic b) S).indicator 1) x₀
have rw : ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
    S.indicator 1
      a ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      (frestrictLe (π := X) a x₀) =
  ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
    (cylinder (α := X) (Iic b) S).indicator 1
      (updateFinset (π := X) x₀ (Iic b)
        z) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      (frestrictLe (π := X) a x₀)
Tactic: rw [trajContent_cylinder mS, ← lintegral_indicator_one mS, lmarginalPartialTraj]
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      S.indicator 1
        a ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (cylinder (α := X) (Iic b) S).indicator 1
        (updateFinset (π := X) x₀ (Iic b)
          z) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have e_f : ∀ (x : (i : ↥(Iic b)) → X (↑i : ℕ)),
  Eq (α := ℝ≥0∞) (S.indicator 1 x) ((cylinder (α := X) (Iic b) S).indicator 1 (updateFinset (π := X) x₀ (Iic b) x))
Tactic: congr with x
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
⊢ Eq (α := ℝ≥0∞) (S.indicator 1 x) ((cylinder (α := X) (Iic b) S).indicator 1 (updateFinset (π := X) x₀ (Iic b) x))
have e_f : x ∈ S ↔ updateFinset (π := X) x₀ (Iic b) x ∈ cylinder (α := X) (Iic b) S
Tactic: apply Set.indicator_const_eq_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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
⊢ x ∈ S ↔ updateFinset (π := X) x₀ (Iic b) x ∈ cylinder (α := X) (Iic b) S
have e_f : x ∈ S ↔ (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) ∈ S
Tactic: rw [mem_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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
⊢ x ∈ S ↔ (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) ∈ S
have e_f : ∀ (i : ↥(Iic b)), x i = (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) i
Tactic: congrm (fun i ↦ ?_) ∈ S
-- 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)
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)
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)
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 ⟨y ⟨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)
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)
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 ⟨y ⟨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)
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)
⊢ ∃ (z : X (k + 1)),
    ∀ (x : (i : ℕ) → X i) (n : ℕ),
      ε ≤
        lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
          (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) z)
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 ⟨y ⟨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 (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)
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))
x : (n : ℕ) → X n
n : ℕ
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
have inl : ∀ (h : k + 1 < a n),
  lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
Tactic: obtain h | h | h := lt_trichotomy (k + 1) (a 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)
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))
x : (n : ℕ) → X n
n : ℕ
inl :
  ∀ (h : k + 1 < a n),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
      lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
have inr : ∀ (h : k + 1 = a n),
  lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
Tactic: obtain h | h | h := lt_trichotomy (k + 1) (a 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)
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))
x : (n : ℕ) → X n
n : ℕ
inl :
  ∀ (h : k + 1 < a n),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
      lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
inr :
  ∀ (h : k + 1 = a n),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
      lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
have inr₁ : ∀ (h : a n < k + 1),
  lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
Tactic: obtain h | h | h := lt_trichotomy (k + 1) (a 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)
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_1 : ∀ (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))
x : (n : ℕ) → X n
n : ℕ
h : k + 1 < a n
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
have inl : lmarginalPartialTraj (X := X) κ k k.succ (lmarginalPartialTraj (X := X) κ k.succ (a n) (f n)) x =
  lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
Tactic: rw [← lmarginalPartialTraj_self k.le_succ h.le (mf 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)
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_1 : ∀ (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))
x : (n : ℕ) → X n
n : ℕ
h : k + 1 = a n
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
have inr : lmarginalPartialTraj (X := X) κ k (k + 1) (f n) x =
  lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (k + 1) (f n)) x
Tactic: rw [← h, lmarginalPartialTraj_le _ le_rfl (mf 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)
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_1 : ∀ (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))
x : (n : ℕ) → X n
n : ℕ
h : k + 1 = a n
inr :
  lmarginalPartialTraj (X := X) κ k (k + 1) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (k + 1) (f n)) x
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
have inr₁ : lmarginalPartialTraj (X := X) κ k (k + 1) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (f n) x
Tactic: rw [← h, lmarginalPartialTraj_le _ le_rfl (mf n)]