Documentation

Lean 4 Proof

theorem intra_level_exponential_convergence
    (V : ℕ → ℝ) (lam : ℝ)
    (hlam_pos : 0 < lam) (hlam_le : lam ≤ 1)
    (hV_nonneg : ∀ k, 0 ≤ V k)
    (hV_contract : ∀ k, V (k + 1) ≤ (1 - lam) * V k) :
    ∀ k, V k ≤ (1 - lam) ^ k * V 0 := by
  intro k
  induction k with
  | zero => simp
  | succ n ih =>
    calc V (n + 1) ≤ (1 - lam) * V n := hV_contract n
    _ ≤ (1 - lam) * ((1 - lam) ^ n * V 0) := by
        apply mul_le_mul_of_nonneg_left ih (by linarith)
    _ = (1 - lam) ^ (n + 1) * V 0 := by ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:248

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file