Documentation

Lean 4 Proof

theorem equilibriumShare_sum [NeZero J]
    (a cost : Fin J → ℝ)
    (hω : 0 < ∑ k : Fin J, agentFitness a cost ρ k) :
    ∑ j, equilibriumShare a cost ρ j = 1 := by
  unfold equilibriumShare
  rw [← Finset.sum_div]
  exact div_self (ne_of_gt hω)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:132

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file