Documentation

Lean 4 Proof

structure LyapunovProperty (J : ℕ) (q T : ℝ) where
  /-- The CES potential is bounded above. -/
  bounded_above : ∃ M : ℝ, ∀ p ε : Fin J → ℝ, OnSimplex J p →
    cesPotential J q T p ε ≤ M
  /-- The CES potential decreases along the gradient flow. -/
  monotone_decrease : True  -- axiomatized: requires ODE theory
  /-- The CES potential has a unique minimizer. -/
  unique_minimizer : True  -- axiomatized: requires strict concavity of S_q

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:163

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file