Documentation

Lean 4 Proof

def contestPayoff (a x cost : Fin J → ℝ) (ρ : ℝ)
    (j : Fin J) : ℝ :=
  contestShare a x ρ j - cost j * x j

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:107

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file