Documentation

Lean 4 Proof

theorem qExp_is_optimizer (J : ℕ) (q T : ℝ) (hq : 0 < q) (hT : 0 < T)
    (ε : Fin J → ℝ) :
    -- The q-exponential allocation maximizes the CES potential
    -- over the simplex.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/QEquilibrium.lean:49

Module Section

Propositions 3-4: q-Exponential Equilibrium and Tail Behavior

In the same file