-- 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)
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
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))
z : (n : ℕ) → X n := iterateInduction (X := X) x₀ ind
main :
  ∀ (k : ℕ) (hk : p ≤ k) (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) (frestrictLe (π := X) k z))
x : (i : ℕ) → X i
n : ℕ
nth_rw :
  (trajContent (X := X) κ (frestrictLe (π := X) p (updateFinset (π := X) x (Iic p) x₀)) :
        (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
      (cylinder (α := X) (Iic (a n)) (S n)) =
    lmarginalPartialTraj (X := X) κ p (a n) ((cylinder (α := X) (Iic (a n)) (S n)).indicator 1)
      (updateFinset (π := X) x (Iic p) x₀)
⊢ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic (a n)) (S n)) =
    lmarginalPartialTraj (X := X) κ p (a n) ((cylinder (α := X) (Iic (a n)) (S n)).indicator 1)
      (updateFinset (π := X) x (Iic p) x₀)

Tactic:
nth_rw 1 [← frestrictLe_updateFinset x x₀]

Premises used: Preorder.frestrictLe_updateFinset