Documentation

Lean 4 Proof

def deviationGain (J : ℕ) (ρ c : ℝ) : ℝ :=
  (1 - ρ) / (2 * ↑J * c)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:243

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file