Documentation

Lean 4 Proof

theorem symmetric_equilibrium_share [NeZero J]
    {a₀ cost₀ : ℝ} {ρ : ℝ}
    (ha : 0 < a₀) (hcost : 0 < cost₀) :
    equilibriumShare (fun _ : Fin J => a₀) (fun _ => cost₀) ρ ⟨0, NeZero.pos J⟩ =
      1 / ↑J := by
  simp only [equilibriumShare, agentFitness]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hω : a₀ * cost₀ ^ (-ρ) ≠ 0 := by
    apply mul_ne_zero (ne_of_gt ha)
    exact ne_of_gt (rpow_pos_of_pos hcost _)
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne J)
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:146

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file