(11), p. 13 — the stage-2 subgame is a weighted potential game with potential Φ and weights v_i
ProvedNetworkQuality.PotentialMax.eq_11network-effectsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1potential-game
In the network market with valuations , benefit and potential , for every consumer , every set of other buyers, every price and every quality ,
Every unilateral deviation changes the deviator's payoff by times the change in , so the stage-2 subgame is a weighted potential game with weights . This is what makes potential maximization available as an equilibrium-selection criterion.
Formalization Note The identity uses , which the standing assumptions () supply; they are taken as a hypothesis for uniformity with the other statements.
Preamble
import Mathlib import Definitions.Def_NetworkQuality_PotentialMax_Setting
Formal statement
namespace NetworkQuality.PotentialMax
open Market
theorem eq_11 {n : ℕ} (M : Market n) (hM : M.Standing) (i : Fin n) (B : Finset (Fin n))
(hi : i ∉ B) (p q : ℝ) :
M.u i (insert i B) p q - M.u i B p q =
M.v i * (M.pot (insert i B) p q - M.pot B p q) := by sorry
end NetworkQuality.PotentialMax
Source
Chan, Quality Strategies in Network Markets, SSRN 4203818 (version of April 2023), p. 13, (11)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.