Documentation

Lean 4 Proof

theorem unique_equilibrium_complements
    (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v)
    (hv_ne : ∃ j, v j ≠ 0) :
    cesHessianQF J ρ c v < 0 :=
  ces_strict_concavity_on_perp hJ hρ hc v hv hv_ne

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:59

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file