Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = ε
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → ((i : ↥(Iic k)) → X ↑i) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X ↑i),
    (∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) y)) →
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (update (updateFinset x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction x₀ ind
⊢ Tendsto (fun n ↦ (trajContent κ x₀) (A n)) atTop (𝓝 0)

Tactic:
have main k (hk : p ≤ k) : ∀ x n,
      ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x _ (frestrictLe k z)) := by
    induction k, hk using Nat.le_induction with
    | base => exact fun x n ↦ by simpa [z, frestrictLe_iterateInduction] using hpos x n
    | succ k hn h =>
      intro x n
      convert! hind k (fun i ↦ z i.1) h x n
      ext i
      simp only [updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite, update, z]
      split_ifs with h1 h2 h3 h4 h5
      any_goals lia
      cases h2
      rw [iterateInduction, dif_neg (by lia)]

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = ε
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → ((i : ↥(Iic k)) → X ↑i) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X ↑i),
    (∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) y)) →
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (update (updateFinset x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction x₀ ind
main :
  ∀ (k : ℕ),
    p ≤ k →
      ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) (frestrictLe k z))
⊢ Tendsto (fun n ↦ (trajContent κ x₀) (A n)) atTop (𝓝 0)