CES Game Critical Ratio Eq

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem cesGameCriticalRatio_eq (ρ : ℝ) (hρ : 0 < ρ) :
    cesGameCriticalRatio ρ = (2 : ℝ) ^ (-(1 / ρ)) := by
  simp [cesGameCriticalRatio, hρ]

Dependency Graph

Used by

cesGameCriticalRatio_bounds

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:104

Module Section

Strategic independence of CES (Paper 1, Sections 7-8):

In the same file

manipulationPayoff ces_log_supermodular strategic_independence_qualitative strategic_bound cesGamePayoff cesGameCriticalRatio cesGameCriticalRatio_bounds cesGame_classification