Documentation

Lean 4 Proof

theorem separatrix_symmetric {ρ : ℝ} (_hρ : 1 < ρ)
    {ω : ℝ} (hω : 0 < ω) :
    separatrixRatio ω ω ρ = 1 := by
  unfold separatrixRatio
  rw [div_self (ne_of_gt hω)]
  exact one_rpow _

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:377

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file