5.2 Multiplicative weights update

Definition 5.3 MWU config

Lean: ProbabilityTheory.MWUConfig

An MWUConfig \(C\) is a pair \(\langle w, h_{{\gt}0} \rangle \) where \(w : C \to \mathbb {R}\) is the strictly positive weight vector. The potential is \(\Phi (w) := \sum _c w(c)\), the induced PMF is \(\mathrm{toPMF}(w)(c) := w(c) / \Phi (w)\) [ 3 , Thm 2.1 ] .

Definition 5.4 Update and closed-form

Lean: ProbabilityTheory.mwuUpdateWeights

Given a row \(r : R\) and step size \(\eta {\lt} 1\), the update is \(w'(c) := w(c) \cdot (1 - \eta )\) if \(M\, r\, c = \mathrm{true}\), else \(w'(c) := w(c)\). This is the Freund-Schapire \(\beta = (1 - \eta )\) Hedge convention [ 9 ] . The closed form

\[ w_T(c) \; =\; w_0(c) \cdot (1 - \eta )^{\mathrm{hitCount}_T(c)} \]

is Theorem mwu_weight_eq_pow_hitCount.

Theorem 5.5 One-step potential bound

Lean: ProbabilityTheory.potential_one_step_bound

If the row player can guarantee value \(v\) against every mixed column and \(0 \le \eta {\lt} 1\), then after one MWU step \(\Phi _{t+1} \le \Phi _t \cdot (1 - \eta v)\) [ 3 , Cor. 2.2 ] .

Theorem 5.6 \(T\)-step potential bound

Lean: ProbabilityTheory.mwu_potential_T_bound

Induction gives \(\Phi _T \; \le \; |C| \cdot (1 - \eta v)^T\) [ 3 , Thm 2.1 ] .

Theorem 5.7 Closed-form weight

Lean: ProbabilityTheory.mwu_weight_eq_pow_hitCount

\(w_T(c) = w_0(c) \cdot (1 - \eta )^{\mathrm{hitCount}_T(c)}\) [ 9 , eq. (2) ] .