Documentation

Lean 4 Proof

theorem contraction_factor_nonneg
    (lam : ℝ) (hlam_le : lam ≤ 1) (k : ℕ) :
    0 ≤ (1 - lam) ^ k := by
  exact pow_nonneg (by linarith) k

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:272

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file