Documentation

Lean 4 Proof

theorem welfare_loss_lyapunov_core {N : ℕ}
    (ℓ : Fin N → ℝ) (hℓ : ∀ n, 0 < ℓ n) (grad : Fin N → ℝ) :
    0 ≤ ∑ n : Fin N, ℓ n * (grad n) ^ 2 := by
  apply Finset.sum_nonneg
  intro n _
  exact mul_nonneg (le_of_lt (hℓ n)) (sq_nonneg _)

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:117

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file