Weighted majority algorithm

AbbreviationRound of prediction with expert advice#✓fully proved

A round with \(n\) experts is a pair \((a, y)\), where \(a\) assigns to each expert \(i \in \{0, \dots, n - 1\}\) its binary advice (true or false) and the binary value \(y\) is the true outcome.

abbrev Round (n : ℕ) := (Fin n → Bool) × Bool

Used by 14

Used byMistakes of an expert · Mistake bound for the penalty \(1/2\) · Littlestone–Warmuth mistake bound · Mistake bound for the penalty \(1/2\) in integers · Mistakes of the weighted majority algorithm · Mistakes split over concatenated runs · Total weight after an update · An update never increases the total weight · A mistake costs weight · Total weight bound in terms of mistakes · Weighted majority update · Weights after a run · Weights over a concatenated run · Final weight of an expert

DefinitionWeight on an answer#✓fully proved

Given weights \(w_0, \dots, w_{n-1}\) in a field \(K\), advice \(a \in \{\mathrm{true}, \mathrm{false}\}^n\) and an answer \(b \in \{\mathrm{true}, \mathrm{false}\}\), the weight on \(b\) is \(\sum_{i : a_i = b} w_i\), the total weight of the experts advising \(b\).

def weightOn (w : Fin n → K) (advice : Fin n → Bool) (b : Bool) : K :=
  ∑ i ∈ univ.filter (fun i => advice i = b), w i

Used by 4

Used byWeighted majority vote · Total weight after an update · An update never increases the total weight · A mistake costs weight

DefinitionWeighted majority vote#✓fully proved

Let \(K\) be a field with a linear order. Given weights in \(K\) on \(n\) experts and a binary advice (true or false) from each expert, the weighted majority vote is true when the total weight of the experts advising false is at most the total weight of the experts advising true, and false otherwise. In particular ties go to true.

def predict (w : Fin n → K) (advice : Fin n → Bool) : Bool :=
  decide (weightOn w advice false ≤ weightOn w advice true)

Uses 1 · Used by 4

Statement usesWeight on an answer

Used byMistakes of the weighted majority algorithm · Mistakes split over concatenated runs · A mistake costs weight · Total weight bound in terms of mistakes

DefinitionWeighted majority update#✓fully proved

Given a penalty factor \(\beta\) and weights \(w_0, \dots, w_{n-1}\) in a field \(K\), and a round with advice \(a \in \{\mathrm{true}, \mathrm{false}\}^n\) and outcome \(y\), the updated weight of expert \(i\) is \(w_i\) if \(a_i = y\) and \(\beta w_i\) otherwise: after the outcome is revealed, every expert that was wrong has its weight multiplied by \(\beta\).

def update (β : K) (w : Fin n → K) (r : Round n) : Fin n → K :=
  fun i => if r.1 i = r.2 then w i else β * w i

Uses 1 · Used by 10

Statement usesRound of prediction with expert advice

Used byLittlestone–Warmuth mistake bound · Mistakes of the weighted majority algorithm · Mistakes split over concatenated runs · Total weight after an update · An update never increases the total weight · A mistake costs weight · Total weight bound in terms of mistakes · Weights after a run · Weights over a concatenated run · Final weight of an expert

DefinitionWeights after a run#✓fully proved

For a penalty factor \(\beta\) in a field \(K\), the weights after a sequence of rounds \(r_1, \dots, r_k\) starting from weights \(w\) in \(K\) are obtained by applying the weighted majority update with penalty \(\beta\) for \(r_1\), then for \(r_2\), and so on up to \(r_k\); for the empty sequence they are \(w\).

def weights (β : K) : List (Round n) → (Fin n → K) → Fin n → K
  | [], w => w
  | r :: rs, w => weights β rs (update β w r)

Uses 2 · Used by 5

Statement usesRound of prediction with expert advice · Weighted majority update

Used byLittlestone–Warmuth mistake bound · Mistakes split over concatenated runs · Total weight bound in terms of mistakes · Weights over a concatenated run · Final weight of an expert

DefinitionMistakes of the weighted majority algorithm#✓fully proved

Let \(K\) be a field with a linear order, let \(\beta \in K\) be a penalty and let \(w\) be initial weights in \(K\) on \(n\) experts. The weighted majority algorithm processes a list of rounds in order: in each round it predicts the weighted majority vote of the experts' advice under the current weights, and then multiplies the weight of every expert whose advice differed from the true outcome by \(\beta\). Its number of mistakes is the number of rounds in which its prediction differs from the true outcome.

def mistakes (β : K) : List (Round n) → (Fin n → K) → ℕ
  | [], _ => 0
  | r :: rs, w => (if predict w r.1 = r.2 then 0 else 1) + mistakes β rs (update β w r)

Uses 3 · Used by 5

Statement usesRound of prediction with expert advice · Weighted majority vote · Weighted majority update

Used byMistake bound for the penalty \(1/2\) · Littlestone–Warmuth mistake bound · Mistake bound for the penalty \(1/2\) in integers · Mistakes split over concatenated runs · Total weight bound in terms of mistakes

DefinitionMistakes of an expert#✓fully proved

Given a list of rounds with \(n\) experts and an expert \(i\), the number of mistakes of \(i\) is the number of rounds in the list in which the advice of expert \(i\) differs from the true outcome.

def expertMistakes (i : Fin n) (rs : List (Round n)) : ℕ := (rs.filter fun r => r.1 i ≠ r.2).length

Uses 1 · Used by 4

Statement usesRound of prediction with expert advice

Used byMistake bound for the penalty \(1/2\) · Littlestone–Warmuth mistake bound · Mistake bound for the penalty \(1/2\) in integers · Final weight of an expert

DefinitionTotal weight#✓fully proved

The total weight of weights \(w_0, \dots, w_{n-1}\) in a field \(K\) is \(\sum_{i < n} w_i\).

def total (w : Fin n → K) : K := ∑ i, w i

Used by 5

Used byLittlestone–Warmuth mistake bound · Total weight after an update · An update never increases the total weight · A mistake costs weight · Total weight bound in terms of mistakes

TheoremTotal weight after an update#✓fully proved

Let \(\beta\) be an element of a linearly ordered field \(K\), let \(w_0, \dots, w_{n-1} \in K\) be weights on \(n\) experts, and let \(r\) be a round with advice \(a \in \{\mathrm{true}, \mathrm{false}\}^n\) and outcome \(y\). If \(w'\) are the weights after the update with penalty \(\beta\) on \(r\), then \(\sum_{i < n} w'_i = \sum_{i < n} w_i - (1 - \beta) \sum_{i : a_i = \lnot y} w_i\): the experts that advised wrongly keep a \(\beta\) fraction of their weight.

theorem total_update (β : K) (w : Fin n → K) (r : Round n) :
    total (update β w r) = total w - (1 - β) * weightOn w r.1 (!r.2)

Uses 4 · Used by 2

Statement usesRound of prediction with expert advice · Total weight · Weighted majority update · Weight on an answer

Used byAn update never increases the total weight · A mistake costs weight

TheoremA mistake costs weight#✓fully proved

Let \(K\) be a linearly ordered field, let \(\beta \in K\) with \(\beta \le 1\), let \(w\) be weights in \(K\) on \(n\) experts, and let \(r\) be a round on which the weighted majority vote under \(w\) differs from the true outcome. If \(W\) is the total weight of \(w\) and \(W'\) is the total weight after updating \(w\) on \(r\) with penalty \(\beta\), then \(2 W' \le (1 + \beta) W\).

At least half of the weight was on the wrong side, and that side keeps only a \(\beta\) fraction of its weight.

theorem total_update_of_mistake {β : K} (hβ1 : β ≤ 1) {w : Fin n → K} {r : Round n}
    (h : predict w r.1 ≠ r.2) : 2 * total (update β w r) ≤ (1 + β) * total w

Uses 6 · Used by 1

Statement usesRound of prediction with expert advice · Weighted majority vote · Total weight · Weighted majority update

Proof usesTotal weight after an update · Weight on an answer

Used byTotal weight bound in terms of mistakes

TheoremAn update never increases the total weight#✓fully proved

Let \(K\) be a linearly ordered field, let \(\beta \in K\) with \(\beta \le 1\), and let \(w\) be nonnegative weights in \(K\) on \(n\) experts. For every round \(r\), the total weight after updating \(w\) on \(r\) with penalty \(\beta\) is at most the total weight of \(w\).

theorem total_update_le {β : K} (hβ1 : β ≤ 1) {w : Fin n → K} (hw : ∀ i, 0 ≤ w i)
    (r : Round n) : total (update β w r) ≤ total w

Uses 5 · Used by 1

Statement usesRound of prediction with expert advice · Total weight · Weighted majority update

Proof usesTotal weight after an update · Weight on an answer

Used byTotal weight bound in terms of mistakes

TheoremTotal weight bound in terms of mistakes#✓fully proved

Let \(0 \le \beta \le 1\) in a linearly ordered field \(K\), let \(w\) be nonnegative weights in \(K\) on \(n\) experts, and let \(\rho\) be a sequence of rounds. Let \(M\) be the number of mistakes the weighted majority algorithm with penalty \(\beta\) makes on \(\rho\) starting from \(w\), and let \(W\) and \(W'\) be the total weights before and after \(\rho\). Then \(W' \cdot 2^M \le (1 + \beta)^M \cdot W\).

theorem total_weights_mul_le {β : K} (hβ0 : 0 ≤ β) (hβ1 : β ≤ 1) :
    ∀ (rs : List (Round n)) (w : Fin n → K), (∀ i, 0 ≤ w i) →
    total (weights β rs w) * 2 ^ mistakes β rs w ≤ (1 + β) ^ mistakes β rs w * total w

Uses 8 · Used by 1

Statement usesRound of prediction with expert advice · Mistakes of the weighted majority algorithm · Total weight · Weights after a run

Proof usesWeighted majority vote · An update never increases the total weight · A mistake costs weight · Weighted majority update

Used byLittlestone–Warmuth mistake bound

TheoremFinal weight of an expert#✓fully proved

For a penalty factor \(\beta\) in a field \(K\), initial weights \(w_0, \dots, w_{n-1} \in K\) and a sequence of rounds, the weight of expert \(i\) after these rounds is \(w_i \beta^{m_i}\), where \(m_i\) is the number of rounds in which the advice of expert \(i\) differs from the outcome.

theorem weights_apply (β : K) : ∀ (rs : List (Round n)) (w : Fin n → K) (i : Fin n),
    weights β rs w i = w i * β ^ expertMistakes i rs

Uses 4 · Used by 1

Statement usesRound of prediction with expert advice · Mistakes of an expert · Weights after a run

Proof usesWeighted majority update

Used byLittlestone–Warmuth mistake bound

TheoremLittlestone–Warmuth mistake bound#✓fully proved

Let \(K\) be a linearly ordered field and let \(\beta \in K\) with \(0 \le \beta \le 1\). Run the weighted majority algorithm with penalty \(\beta\) on a list of rounds with \(n\) experts, starting from weight \(1\) on every expert, and let \(M\) be its number of mistakes. Then every expert \(i\), with \(m\) mistakes on these rounds, satisfies \(\beta^m 2^M \le n (1 + \beta)^M\).

theorem mistake_bound_general {β : K} (hβ0 : 0 ≤ β) (hβ1 : β ≤ 1) (rs : List (Round n))
    (i : Fin n) :
    β ^ expertMistakes i rs * 2 ^ mistakes β rs (fun _ => 1) ≤
      n * (1 + β) ^ mistakes β rs (fun _ => 1)

Uses 8 · Used by 1

Statement usesRound of prediction with expert advice · Mistakes of an expert · Mistakes of the weighted majority algorithm

Proof usesTotal weight · Total weight bound in terms of mistakes · Weighted majority update · Weights after a run · Final weight of an expert

Used byMistake bound for the penalty \(1/2\)

TheoremMistake bound for the penalty \(1/2\)#✓fully proved

Run the weighted majority algorithm with rational weights and penalty \(1/2\) on a list of rounds with \(n\) experts, starting from weight \(1\) on every expert, and let \(M\) be its number of mistakes. Then every expert \(i\), with \(m\) mistakes on these rounds, satisfies \((4/3)^M \le n \cdot 2^m\).

theorem mistake_bound (rs : List (Round n)) (i : Fin n) :
    (4 / 3 : ℚ) ^ mistakes (1 / 2 : ℚ) rs (fun _ => 1) ≤ n * 2 ^ expertMistakes i rs

Uses 4 · Used by 1

Statement usesRound of prediction with expert advice · Mistakes of an expert · Mistakes of the weighted majority algorithm

Proof usesLittlestone–Warmuth mistake bound

Used byMistake bound for the penalty \(1/2\) in integers

TheoremMistake bound for the penalty \(1/2\) in integers#✓fully proved

Run the weighted majority algorithm with rational weights and penalty \(1/2\) on a list of rounds with \(n\) experts, starting from weight \(1\) on every expert, and let \(M\) be its number of mistakes. Then every expert \(i\), with \(m\) mistakes on these rounds, satisfies \(4^M \le n \cdot 3^M \cdot 2^m\) in the natural numbers.

Taking logarithms, \(M \le (m + \log_2 n) / \log_2 (4/3) \approx 2.41 (m + \log_2 n)\).

theorem mistake_bound_nat (rs : List (Round n)) (i : Fin n) :
    4 ^ mistakes (1 / 2 : ℚ) rs (fun _ => 1) ≤
      n * 3 ^ mistakes (1 / 2 : ℚ) rs (fun _ => 1) * 2 ^ expertMistakes i rs

Uses 4

Statement usesRound of prediction with expert advice · Mistakes of an expert · Mistakes of the weighted majority algorithm

Proof usesMistake bound for the penalty \(1/2\)

TheoremWeights over a concatenated run#✓fully proved

For a penalty factor \(\beta\) in a field \(K\), initial weights \(w\) in \(K\) and sequences of rounds \(\rho\) and \(\rho'\), the weights after running \(\rho\) followed by \(\rho'\) from \(w\) equal the weights after running \(\rho'\) from the weights obtained by running \(\rho\) from \(w\).

theorem weights_append (β : K) : ∀ (rs rs' : List (Round n)) (w : Fin n → K),
    weights β (rs ++ rs') w = weights β rs' (weights β rs w)

Uses 3

Statement usesRound of prediction with expert advice · Weights after a run

Proof usesWeighted majority update

TheoremMistakes split over concatenated runs#✓fully proved

Let \(K\) be a field with a linear order, let \(\beta \in K\) be a penalty, let \(w\) be weights in \(K\) on \(n\) experts, and let \(R\) and \(R'\) be lists of rounds. The number of mistakes of the weighted majority algorithm with penalty \(\beta\) on \(R\) followed by \(R'\), starting from \(w\), equals its number of mistakes on \(R\) starting from \(w\) plus its number of mistakes on \(R'\) starting from the weights reached after \(R\).

theorem mistakes_append (β : K) : ∀ (rs rs' : List (Round n)) (w : Fin n → K),
    mistakes β (rs ++ rs') w = mistakes β rs w + mistakes β rs' (weights β rs w)

Uses 5

Statement usesRound of prediction with expert advice · Mistakes of the weighted majority algorithm · Weights after a run

Proof usesWeighted majority vote · Weighted majority update

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.