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)
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 : 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
have inr : a n ≤ k
Tactic: rw [lmarginalPartialTraj_le _ _ (mf n), (hcte n).lmarginalPartialTraj_of_le _ (mf n),
        (hcte n).lmarginalPartialTraj_of_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 : a n < k + 1
inr : a n ≤ k
⊢ 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₁ : a n ≤ k + 1
Tactic: rw [lmarginalPartialTraj_le _ _ (mf n), (hcte n).lmarginalPartialTraj_of_le _ (mf n),
        (hcte n).lmarginalPartialTraj_of_le _ (mf 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)
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))
⊢ ∃ (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 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
Tactic: have f_eq x n : lmarginalPartialTraj κ k (a n) (f n) x =
      lmarginalPartialTraj κ k (k + 1) (F n) x := by
    simp_rw [F]
    obtain h | h | h := lt_trichotomy (k + 1) (a n)
    · rw [← lmarginalPartialTraj_self k.le_succ h.le (mf n)]
    · rw [← h, lmarginalPartialTraj_le _ le_rfl (mf n)]
    · rw [lmarginalPartialTraj_le _ _ (mf n), (hcte n).lmarginalPartialTraj_of_le _ (mf n),
        (hcte n).lmarginalPartialTraj_of_le _ (mf n)]
      all_goals lia
-- 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
⊢ ∃ (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 F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
Tactic: have F_le n x : F n x ≤ bound := by
    simpa [F, lmarginalPartialTraj] using lintegral_le_const (ae_of_all _ fun z ↦ le_bound _ _)
-- 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))
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
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))
have simp_rw : Tendsto
  (fun (n : ℕ) ↦
    ∫⁻ (z : (i : ↥(Iic (k + 1))) → X (↑i : ℕ)),
      F n
        (updateFinset (π := X) x (Iic (k + 1))
          z) ∂(partialTraj (X := X) κ k (k + 1) :
          (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
        (frestrictLe (π := X) k x))
  atTop
  (𝓝
    (∫⁻ (z : (i : ↥(Iic (k + 1))) → X (↑i : ℕ)),
      l
        (updateFinset (π := X) x (Iic (k + 1))
          z) ∂(partialTraj (X := X) κ k (k + 1) :
          (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
        (frestrictLe (π := X) k x)))
Tactic: simp_rw [f_eq, lmarginalPartialTraj]
-- 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
⊢ ∃ (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 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))
Tactic: have tendsto_int x : Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj κ k (k + 1) l x)) := by
    simp_rw [f_eq, lmarginalPartialTraj]
    exact tendsto_lintegral_of_dominated_convergence (fun _ ↦ bound)
      (fun n ↦ (measurable_lmarginalPartialTraj _ _ (mf n)).comp measurable_updateFinset)
      (fun n ↦ Eventually.of_forall <| fun y ↦ F_le n _)
      (by simp [fin_bound]) (Eventually.of_forall (fun _ ↦ tendstoF _))
-- 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))
⊢ ∃ (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 ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
Tactic: have ε_le_lint x : ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x _ y) :=
    ge_of_tendsto (tendsto_int _) (by simp [hpos])
-- 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)), ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
have this : ∫⁻ (x : X (k + 1)),
    l
      (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
        x) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≠
  ∞
Tactic: have : ∫⁻ x, l (update (updateFinset x_ _ y) (k + 1) x) ∂(κ k y) ≠ ∞ :=
      ne_top_of_le_ne_top fin_bound <| lintegral_le_const <| ae_of_all _
        fun y ↦ le_of_tendsto' (tendstoF _) <| fun _ ↦ F_le _ _
-- 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))
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
this :
  ∫⁻ (x : X (k + 1)),
      l
        (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
          x) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≠
    ∞
⊢ ∃ (x : X (k + 1)), ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
have obtain : ∀ (x : X (k + 1))
  (hx :
    ∫⁻ (a : X (k + 1)),
        l
          (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
            a) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≤
      l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)),
  ∃ (x : X (k + 1)), ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
Tactic: obtain ⟨x, hx⟩ := exists_lintegral_le this
-- 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))
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
this :
  ∫⁻ (x : X (k + 1)),
      l
        (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
          x) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≠
    ∞
x : X (k + 1)
hx :
  ∫⁻ (a : X (k + 1)),
      l
        (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
          a) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≤
    l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
⊢ ∃ (x : X (k + 1)), ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
have refine : lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x_ (Iic k) y) ≤
  l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
Tactic: refine ⟨x, (ε_le_lint x_).trans ?_⟩
-- 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))
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
this :
  ∫⁻ (x : X (k + 1)),
      l
        (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
          x) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≠
    ∞
x : X (k + 1)
hx :
  ∫⁻ (a : X (k + 1)),
      l
        (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1)
          a) ∂(κ k : (a : (i : ↥(Iic k)) → X (↑i : ℕ)) → Measure (X (k + 1))) y ≤
    l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
⊢ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x_ (Iic k) y) ≤
    l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
have mf₁ : Measurable l
Tactic: rwa [lmarginalPartialTraj_succ, frestrictLe_updateFinset]