Documentation

Lean 4 Proof

def cesGamePayoff (ρ : ℝ) (x₁ x₂ : ℝ) (e : ℝ) (i : Fin 2) : ℝ :=
  ((1 / 2 : ℝ) * (x₁ ^ ρ + x₂ ^ ρ)) ^ (1 / ρ) - e * if i = 0 then x₁ else x₂

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:94

Module Section

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

In the same file