selfishStrategy

formal source

  49  apply := fun sigmas i => sigmas i / 2
  50
  51/-- A selfish strategy zeroes one agent's sigma but doubles another's. -/
  52def selfishStrategy (beneficiary victim : Fin 2) : Strategy where
  53  apply := fun sigmas i =>
  54    if i = beneficiary then 0
  55    else if i = victim then 2 * sigmas i
  56    else sigmas i
  57
  58/-- **Love minimizes sigma spread**: The love strategy reduces total squared sigma
  59    by a factor of 4 (halving each σ). -/
  60theorem love_minimizes_sigma_spread (pop : SigmaPopulation) :
  61    spreadAfter loveStrategy pop = sigmaSpread pop / 4 := by
  62  simp [spreadAfter, sigmaSpread, loveStrategy]
  63  rw [← Finset.sum_div]
  64  congr 1
  65  apply Finset.sum_congr rfl
  66  intro i _
  67  ring
  68
  69/-- Sigma spread is non-negative. -/
  70theorem sigmaSpread_nonneg (pop : SigmaPopulation) : 0 ≤ sigmaSpread pop :=
  71  Finset.sum_nonneg fun i _ => sq_nonneg _
  72
  73/-- **Love is fastest equilibration**: Love strictly reduces spread when any σ ≠ 0. -/
  74theorem love_is_fastest_equilibration (pop : SigmaPopulation)
  75    (h_nonzero : ∃ i, pop.sigmas i ≠ 0) :
  76    spreadAfter loveStrategy pop < sigmaSpread pop := by
  77  rw [love_minimizes_sigma_spread]
  78  have h_pos : 0 < sigmaSpread pop := by
  79    obtain ⟨i, hi⟩ := h_nonzero
  80    apply Finset.sum_pos' (fun j _ => sq_nonneg (pop.sigmas j))
  81    exact ⟨i, Finset.mem_univ i, sq_pos_of_ne_zero _ hi⟩
  82  linarith