Documentation

Lean 4 Proof

theorem welfare_loss_decrease_rate {N : ℕ}
    (ℓ : Fin N → ℝ) (hℓ : ∀ n, 0 < ℓ n) (grad : Fin N → ℝ)
    (hgrad : ∃ n, grad n ≠ 0) :
    0 < ∑ n : Fin N, ℓ n * (grad n) ^ 2 := by
  obtain ⟨n₀, hn₀⟩ := hgrad
  apply Finset.sum_pos'
  · intro n _; exact mul_nonneg (le_of_lt (hℓ n)) (sq_nonneg _)
  · exact ⟨n₀, Finset.mem_univ _, mul_pos (hℓ n₀) (by positivity)⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:125

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file