Documentation

Lean 4 Proof

theorem contraction_factor_le_one
    (lam : ℝ) (hlam_pos : 0 < lam) (hlam_le : lam ≤ 1) (k : ℕ) :
    (1 - lam) ^ k ≤ 1 := by
  apply pow_le_one₀ (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:266

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file