Documentation

Lean 4 Proof

theorem spatial_decay_bounded
    (ν : ℝ) (hν_nonneg : 0 ≤ ν) (hν_lt : ν < 1) (k : ℕ) :
    ν ^ k ≤ 1 := by
  exact pow_le_one₀ hν_nonneg (le_of_lt hν_lt)

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:326

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file