`isESS`

definition

show as: view math explainer →

module: IndisputableMonolith.GameTheory.ESSFromSigma
domain: GameTheory
line: 40 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.GameTheory.ESSFromSigma on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  37def cooperatorThreshold : ℝ := 1 / phi
  38
  39/-- ESS predicate: cooperator fraction is at or above the threshold. -/
  40def isESS (cooperator_fraction : ℝ) : Prop :=
  41  cooperatorThreshold ≤ cooperator_fraction
  42
  43/-- The threshold is strictly less than 1. -/
  44theorem cooperatorThreshold_lt_one : cooperatorThreshold < 1 := by
  45  unfold cooperatorThreshold
  46  have : 1 < phi := by have := phi_gt_onePointFive; linarith
  47  rw [div_lt_one phi_pos]
  48  exact this
  49
  50/-- The threshold is strictly positive. -/
  51theorem cooperatorThreshold_pos : 0 < cooperatorThreshold := by
  52  unfold cooperatorThreshold
  53  exact div_pos one_pos phi_pos
  54
  55/-- All-cooperator strategy is an ESS. -/
  56theorem all_cooperator_isESS : isESS 1 :=
  57  le_of_lt cooperatorThreshold_lt_one
  58
  59/-- Empty-cooperator strategy is not an ESS. -/
  60theorem no_cooperator_not_isESS : ¬ isESS 0 := by
  61  unfold isESS
  62  push_neg
  63  exact cooperatorThreshold_pos
  64
  65/-! ## Master certificate -/
  66
  67/-- **ESS FROM SIGMA MASTER CERTIFICATE.** -/
  68structure ESSFromSigmaCert where
  69  threshold_pos : 0 < cooperatorThreshold
  70  threshold_lt_one : cooperatorThreshold < 1

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.