Documentation

Lean 4 Proof

theorem spatial_decay_strictly_decreasing
    (ν : ℝ) (hν_pos : 0 < ν) (hν_lt : ν < 1) (k : ℕ) :
    ν ^ (k + 1) < ν ^ k := by
  have hpk : 0 < ν ^ k := pow_pos hν_pos k
  calc ν ^ (k + 1) = ν ^ k * ν := pow_succ ν k
  _ < ν ^ k * 1 := by apply mul_lt_mul_of_pos_left hν_lt hpk
  _ = ν ^ k := by ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:334

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file