awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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))
⊢ ∀ (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])
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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) ∂(κ 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 _ _
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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 ≠
    ∞
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)
⊢ ∃ (x : X (k + 1)), ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)

Tactic:
obtain ⟨x, hx⟩ := exists_lintegral_le this

Premises used: MeasureTheory.exists_lintegral_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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)

Tactic:
⟨x, (ε_le_lint x_).trans ?_⟩

Premises used: Exists.intro, LE.le.trans
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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)
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)
⊢ ∃ (x : X (k + 1)), ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)

Tactic:
refine ⟨x, (ε_le_lint x_).trans ?_⟩
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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)
mf₁ : Measurable l
⊢ 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:
rwa [lmarginalPartialTraj_succ, frestrictLe_updateFinset]

Premises used: Preorder.frestrictLe_updateFinset, ProbabilityTheory.Kernel.lmarginalPartialTraj_succ
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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)
⊢ ∀ (i : ℕ), Measurable (lmarginalPartialTraj (X := X) κ (k + 1) (a i) (f i))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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)
⊢ Measurable l

Tactic:
exact ENNReal.measurable_of_tendsto (by fun_prop) (tendsto_pi_nhds.2 htendsto)

Premises used: Iff.mpr, ENNReal.measurable_of_tendsto, tendsto_pi_nhds
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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
obtain :
  ∀ (x : X (k + 1)) (hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) 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)
⊢ ∃ (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)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, ε ≤ l (update (updateFinset x_ _ y) (k + 1) x) := by
    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 _ _
    obtain ⟨x, hx⟩ := exists_lintegral_le this
    refine ⟨x, (ε_le_lint x_).trans ?_⟩
    rwa [lmarginalPartialTraj_succ, frestrictLe_updateFinset]
    exact ENNReal.measurable_of_tendsto (by fun_prop) (tendsto_pi_nhds.2 htendsto)
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
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)
⊢ ∃ (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)

Tactic:
⟨x, fun x' n ↦ ?_⟩

Premises used: Exists.intro