Documentation

Lean 4 Proof

theorem knockoutPunishment_pos {ρ : ℝ}
    (hρ0 : 0 < ρ) (_hρ1 : ρ < 1)
    {c : ℝ} (hc : 0 < c) (hJ : 2 ≤ J) :
    0 < knockoutPunishment J ρ c := by
  unfold knockoutPunishment
  apply mul_pos hc
  have hR := knockout_partial_retained hρ0
    (by omega : 0 < J) (by omega : 0 < 1)
    (by omega : 1 < J)
  linarith [hR.2]

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:282

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file