Documentation

Lean 4 Proof

def AxiomA1_LinearPayoff (_Φ : (Fin J → ℝ) → (Fin J → ℝ) → ℝ) : Prop :=
  ∀ (_p _ε : Fin J → ℝ),
    -- The payoff component of Φ is Σ pⱼ εⱼ
    True  -- structural axiom

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:34

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file