spreadAfter

formal source

  41  apply : {n : ℕ} → (Fin n → ℝ) → (Fin n → ℝ)
  42
  43/-- Sigma spread after applying a strategy. -/
  44def spreadAfter (s : Strategy) (pop : SigmaPopulation) : ℝ :=
  45  Finset.sum Finset.univ fun i => (s.apply pop.sigmas i) ^ 2
  46
  47/-- A love strategy maps all sigmas toward zero uniformly. -/
  48def loveStrategy : Strategy where
  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)