Documentation

Lean 4 Proof

theorem spatial_multiplier_decay
    (e : ℕ → ℝ) (ν : ℝ)
    (hν_nonneg : 0 ≤ ν)
    (he_nonneg : ∀ k, 0 ≤ e k)
    (h_contract : ∀ k, e (k + 1) ≤ ν * e k) :
    ∀ k, e k ≤ ν ^ k * e 0 := by
  intro k
  induction k with
  | zero => simp
  | succ n ih =>
    calc e (n + 1) ≤ ν * e n := h_contract n
    _ ≤ ν * (ν ^ n * e 0) := by
        apply mul_le_mul_of_nonneg_left ih hν_nonneg
    _ = ν ^ (n + 1) * e 0 := by ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:309

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file