Documentation

Lean 4 Proof

theorem fitness_advantage_expands_basin {ρ : ℝ} (hρ : 1 < ρ)
    {ωi ωj : ℝ} (_hωi : 0 < ωi) (hωj : 0 < ωj)
    (hadv : ωj < ωi) :
    1 < separatrixRatio ωi ωj ρ := by
  unfold separatrixRatio
  exact Real.one_lt_rpow ((one_lt_div hωj).mpr hadv)
    (amplification_pos hρ)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:392

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file