Running MWU for T rounds and the T-step potential bound #
mwuRun iterates mwuUpdateWeights for T rounds, threading the
best-response selector produced by the hrow hypothesis. The T-step
potential bound Φ_T ≤ |C| · (1 - η · v)^T follows by induction from
the one-step bound.
def
ProbabilityTheory.mwuRun
{R : Type u_1}
{C : Type u_2}
[Fintype R]
[Fintype C]
[Nonempty C]
(M : R → C → Bool)
(η : ℝ)
(hη1 : η < 1)
(v : ℝ)
(hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0)
(T : ℕ)
:
Run MWU for T rounds: returns the final configuration and the row sequence.
Equations
- One or more equations did not get rendered due to their size.
- ProbabilityTheory.mwuRun M η hη1 v hrow 0 = (ProbabilityTheory.mwuInit C, Fin.elim0)
Instances For
@[reducible, inline]
noncomputable abbrev
ProbabilityTheory.mwuConfig
{R : Type u_1}
{C : Type u_2}
[Fintype R]
[Fintype C]
[Nonempty C]
(M : R → C → Bool)
(η : ℝ)
(hη1 : η < 1)
(v : ℝ)
(hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0)
(T : ℕ)
:
The MWU configuration after T rounds.
Equations
- ProbabilityTheory.mwuConfig M η hη1 v hrow T = (ProbabilityTheory.mwuRun M η hη1 v hrow T).1
Instances For
@[reducible, inline]
noncomputable abbrev
ProbabilityTheory.mwuRows
{R : Type u_1}
{C : Type u_2}
[Fintype R]
[Fintype C]
[Nonempty C]
(M : R → C → Bool)
(η : ℝ)
(hη1 : η < 1)
(v : ℝ)
(hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0)
(T : ℕ)
:
Fin T → R
The MWU row sequence after T rounds.
Equations
- ProbabilityTheory.mwuRows M η hη1 v hrow T = (ProbabilityTheory.mwuRun M η hη1 v hrow T).2
Instances For
theorem
ProbabilityTheory.mwu_potential_T_bound
{R : Type u_1}
{C : Type u_2}
[Fintype R]
[Fintype C]
[Nonempty C]
(M : R → C → Bool)
(η : ℝ)
(hη : 0 ≤ η)
(hη1 : η < 1)
(v : ℝ)
(hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0)
(T : ℕ)
:
T-step MWU potential bound: after T rounds, Φ_T ≤ |C| · (1 - η · v)^T.