def
definition
isSigmaConservative
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.GameTheory.CooperationFromSigma on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
103-/
104
105/-- σ-conservative outcomes: mutual cooperation or mixed. -/
106def isSigmaConservative (o : JointOutcome) : Prop :=
107 jointSigma o ≥ 0
108
109/-- Mutual defection is not σ-conservative. -/
110theorem DD_not_sigma_conservative :
111 ¬ isSigmaConservative ⟨.defect, .defect⟩ := by
112 unfold isSigmaConservative
113 rw [DD_sigma_neg]
114 push_neg
115 norm_num
116
117/-- All other outcomes are σ-conservative. -/
118theorem nonDD_sigma_conservative (o : JointOutcome)
119 (h : ¬ (o.p1 = .defect ∧ o.p2 = .defect)) :
120 isSigmaConservative o := by
121 rcases o with ⟨p1, p2⟩
122 cases p1 <;> cases p2
123 · -- C, C
124 show jointSigma _ ≥ 0
125 rw [CC_sigma_pos]; norm_num
126 · -- C, D
127 show jointSigma _ ≥ 0
128 rw [CD_sigma_zero]
129 · -- D, C
130 show jointSigma _ ≥ 0
131 rw [DC_sigma_zero]
132 · -- D, D contradicts h
133 exfalso
134 apply h
135 exact ⟨rfl, rfl⟩
136