-- 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_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
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
k_1 k : ℕ
hn : p ≤ k
h :
  ∀ (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 i : ℕ
pos :
  ∀ (h1 : i ≤ k + 1) (h2 : i = k + 1),
    iterateInduction (X := X) x₀ ind i =
      Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x)
        (ind k fun (i : ↥(Iic k)) ↦ iterateInduction (X := X) x₀ ind (↑i : ℕ)) ⋯
pos₁ :
  ∀ (h1 : i ≤ k + 1) (h2 : ¬i = k + 1) (h3 : i ≤ k),
    iterateInduction (X := X) x₀ ind i = iterateInduction (X := X) x₀ ind i
neg : ∀ (h1 : i ≤ k + 1) (h2 : ¬i = k + 1) (h3 : ¬i ≤ k), iterateInduction (X := X) x₀ ind i = x i
pos₂ :
  ∀ (h1 : ¬i ≤ k + 1) (h4 : i = k + 1),
    x i =
      Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x)
        (ind k fun (i : ↥(Iic k)) ↦ iterateInduction (X := X) x₀ ind (↑i : ℕ)) ⋯
pos₃ : ∀ (h1 : ¬i ≤ k + 1) (h4 : ¬i = k + 1) (h5 : i ≤ k), x i = iterateInduction (X := X) x₀ ind i
neg₁ : ∀ (h1 : ¬i ≤ k + 1) (h4 : ¬i = k + 1) (h5 : ¬i ≤ k), x i = x i
⊢ (if i ≤ k + 1 then iterateInduction (X := X) x₀ ind i else x i) =
    if h : i = k + 1 then
      Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x)
        (ind k fun (i : ↥(Iic k)) ↦ iterateInduction (X := X) x₀ ind (↑i : ℕ)) ⋯
    else if i ≤ k then iterateInduction (X := X) x₀ ind i else x i

Tactic:
split_ifs with h1 h2 h3 h4 h5