Documentation

Lean 4 Proof

def contestShare (a x : Fin J → ℝ) (ρ : ℝ)
    (j : Fin J) : ℝ :=
  a j * x j ^ ρ / ∑ k : Fin J, a k * x k ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:100

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file