Documentation

Lean 4 Proof

def amplificationExponent (ρ : ℝ) : ℝ := 1 / (ρ - 1)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:345

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file