Hedge algorithm

DefinitionHedge weight update#✓fully proved

After a round with losses ℓ, each expert's weight is multiplied by exp (-η ℓ i).

noncomputable def update (η : ℝ) (w ℓ : Fin n → ℝ) : Fin n → ℝ := fun i => w i * exp (-η * ℓ i)

Used by 11

Used byLoss of the Hedge algorithm · The Hedge loss splits at any round · Summed second moments of the Hedge losses · The summed second moments split at any round · A round costs weight in proportion to the algorithm's loss · A round costs weight in proportion to the algorithm's loss, up to a second-order term · Weight decay over a Hedge run · Weight decay over a Hedge run, second-order form · Hedge weights after a sequence of rounds · A Hedge run splits at any round · Closed form of the Hedge weights

DefinitionHedge weights after a sequence of rounds#✓fully proved

Let \(\eta \in \mathbb{R}\) be a learning rate, let \(w \in \mathbb{R}^n\) be initial weights on \(n\) experts, and let \(\ell_1, \dots, \ell_T \in \mathbb{R}^n\) be the loss vectors of \(T\) rounds, given as a list. The weights after these rounds are obtained from \(w\) by applying the Hedge update once per round, in the order of the list: round \(t\) multiplies the weight of each expert \(i\) by \(e^{-\eta \ell_t(i)}\). For the empty list of rounds the weights are \(w\).

noncomputable def weights (η : ℝ) : List (Fin n → ℝ) → (Fin n → ℝ) → Fin n → ℝ
  | [], w => w
  | ℓ :: ls, w => weights η ls (update η w ℓ)

Uses 1 · Used by 8

Statement usesHedge weight update

Used byThe Hedge loss splits at any round · The Hedge loss bound · The second-order Hedge bound · The summed second moments split at any round · Weight decay over a Hedge run · Weight decay over a Hedge run, second-order form · A Hedge run splits at any round · Closed form of the Hedge weights

DefinitionTotal weight of the Hedge experts#✓fully proved

The total weight of weights \(w\) on \(n\) experts is \(\sum_i w_i\).

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

Used by 8

Used byThe Hedge loss bound · The second-order Hedge bound · Loss of a Hedge round · Weighted second moment of a Hedge round · A round costs weight in proportion to the algorithm's loss · A round costs weight in proportion to the algorithm's loss, up to a second-order term · Weight decay over a Hedge run · Weight decay over a Hedge run, second-order form

DefinitionLoss of a Hedge round#✓fully proved

For weights \(w\) and losses \(\ell\) on \(n\) experts, the algorithm's loss in the round is \(\left(\sum_i w_i \ell_i\right) / W\), where \(W = \sum_i w_i\) is the total weight. This is its expected loss when it follows expert \(i\) with probability \(w_i / W\).

noncomputable def roundLoss (w ℓ : Fin n → ℝ) : ℝ := (∑ i, w i * ℓ i) / total w

Uses 1 · Used by 6

Statement usesTotal weight of the Hedge experts

Used byLoss of the Hedge algorithm · The Hedge loss splits at any round · A round costs weight in proportion to the algorithm's loss · A round costs weight in proportion to the algorithm's loss, up to a second-order term · Weight decay over a Hedge run · Weight decay over a Hedge run, second-order form

DefinitionLoss of the Hedge algorithm#✓fully proved

Let \(\eta\) be a learning rate, \(w \in \mathbb{R}^n\) initial weights on \(n\) experts and \(\ell_1, \dots, \ell_T \in \mathbb{R}^n\) the losses of \(T\) rounds. Set \(w_1 = w\) and \(w_{t+1}(j) = w_t(j) e^{-\eta \ell_t(j)}\). The algorithm's total loss is \(\sum_{t=1}^T \bigl(\sum_j w_t(j) \ell_t(j)\bigr) / \sum_j w_t(j)\), the sum over the rounds of the weighted average of that round's losses; a round whose total weight is \(0\) contributes \(0\).

noncomputable def algLoss (η : ℝ) : List (Fin n → ℝ) → (Fin n → ℝ) → ℝ
  | [], _ => 0
  | ℓ :: ls, w => roundLoss w ℓ + algLoss η ls (update η w ℓ)

Uses 2 · Used by 5

Statement usesLoss of a Hedge round · Hedge weight update

Used byThe Hedge loss splits at any round · The Hedge loss bound · The second-order Hedge bound · Weight decay over a Hedge run · Weight decay over a Hedge run, second-order form

DefinitionTotal loss of an expert#✓fully proved

For an expert \(i\) among \(n\) experts and a finite sequence of loss vectors \(\ell_1, \dots, \ell_T \in \mathbb{R}^n\), the total loss of expert \(i\) is \(\sum_{t=1}^T \ell_t(i)\).

def expertLoss (i : Fin n) (ls : List (Fin n → ℝ)) : ℝ := (ls.map fun ℓ => ℓ i).sum

Used by 3

Used byThe Hedge loss bound · The second-order Hedge bound · Closed form of the Hedge weights

TheoremThe exponential lies below its chord on the unit interval#✓fully proved

For every real \(\eta\) and every \(x \in [0, 1]\), \(e^{-\eta x} \le 1 - (1 - e^{-\eta}) x\).

theorem exp_neg_mul_le {η x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    exp (-η * x) ≤ 1 - (1 - exp (-η)) * x

Used by 1

Used byA round costs weight in proportion to the algorithm's loss

TheoremA round costs weight in proportion to the algorithm's loss#✓fully proved

Let \(n > 0\), let \(w\) be positive weights on \(n\) experts, let \(\ell\) be losses with \(0 \le \ell_i \le 1\) for every \(i\), and let \(\eta\) be a real number. Let \(w'\) be the Hedge update of \(w\) with learning rate \(\eta\), so that \(w'_i = w_i e^{-\eta \ell_i}\), and let \(W\) and \(W'\) be the total weights of \(w\) and \(w'\). Then \(W' \le W \exp(-(1 - e^{-\eta}) L)\), where \(L\) is the round's loss under the weights \(w\).

theorem total_update_le {η : ℝ} {w ℓ : Fin n → ℝ} (hw : ∀ i, 0 < w i) (hn : 0 < n)
    (hℓ0 : ∀ i, 0 ≤ ℓ i) (hℓ1 : ∀ i, ℓ i ≤ 1) :
    total (update η w ℓ) ≤ total w * exp (-(1 - exp (-η)) * roundLoss w ℓ)

Uses 4 · Used by 1

Statement usesLoss of a Hedge round · Total weight of the Hedge experts · Hedge weight update

Proof usesThe exponential lies below its chord on the unit interval

Used byWeight decay over a Hedge run

DefinitionLosses in the unit interval#✓fully proved

A finite sequence of loss vectors \(\ell_1, \dots, \ell_T \in \mathbb{R}^n\) on \(n\) experts has losses in \([0, 1]\) when \(0 \le \ell_t(i) \le 1\) for every round \(t\) and every expert \(i\).

def Bounded (ls : List (Fin n → ℝ)) : Prop := ∀ ℓ ∈ ls, ∀ i, 0 ≤ ℓ i ∧ ℓ i ≤ 1

Used by 2

Used byThe Hedge loss bound · Weight decay over a Hedge run

TheoremWeight decay over a Hedge run#✓fully proved

Let \(n > 0\) and let \(\eta\) be a real number. For every sequence of rounds with losses in \([0, 1]\) and all positive initial weights \(w\) on \(n\) experts, the total weight after running Hedge with learning rate \(\eta\) from \(w\) is at most \(W \exp(-(1 - e^{-\eta}) L)\), where \(W\) is the total weight of \(w\) and \(L\) is the algorithm's total loss over the rounds for the run from \(w\) with learning rate \(\eta\).

theorem total_weights_le {η : ℝ} (hn : 0 < n) : ∀ (ls : List (Fin n → ℝ)) (w : Fin n → ℝ),
    (∀ i, 0 < w i) → Bounded ls →
    total (weights η ls w) ≤ total w * exp (-(1 - exp (-η)) * algLoss η ls w)

Uses 7 · Used by 1

Statement usesLosses in the unit interval · Loss of the Hedge algorithm · Total weight of the Hedge experts · Hedge weights after a sequence of rounds

Proof usesLoss of a Hedge round · A round costs weight in proportion to the algorithm's loss · Hedge weight update

Used byThe Hedge loss bound

TheoremClosed form of the Hedge weights#✓fully proved

For every learning rate \(\eta\), sequence of rounds, initial weights \(w\) and expert \(i\), the weight of expert \(i\) after running Hedge on the rounds from \(w\) is \(w_i e^{-\eta L_i}\), where \(L_i\) is expert \(i\)'s total loss over the rounds.

theorem weights_apply (η : ℝ) : ∀ (ls : List (Fin n → ℝ)) (w : Fin n → ℝ) (i : Fin n),
    weights η ls w i = w i * exp (-η * expertLoss i ls)

Uses 3 · Used by 2

Statement usesTotal loss of an expert · Hedge weights after a sequence of rounds

Proof usesHedge weight update

Used byThe Hedge loss bound · The second-order Hedge bound

TheoremThe Hedge loss bound#✓fully proved

Let \(\eta\) be a real number, and let \(\ell_1, \dots, \ell_T\) be loss vectors in \([0, 1]^n\) for \(n\) experts. Run Hedge with learning rate \(\eta\) from unit weights, that is \(w_1(j) = 1\) and \(w_{t+1}(j) = w_t(j) e^{-\eta \ell_t(j)}\), and let \(x_t(j) = w_t(j) / \sum_k w_t(k)\) be the distribution played in round \(t\). Then for every expert \(i\),

\[(1 - e^{-\eta}) \sum_{t=1}^T \sum_j x_t(j) \ell_t(j) \le \eta \sum_{t=1}^T \ell_t(i) + \log n.\]

For \(\eta > 0\), writing \(L\) for the algorithm's loss and \(L_i\) for expert \(i\)'s loss, this is the bound \(L \le (\log n + \eta L_i) / (1 - e^{-\eta})\) of Freund and Schapire (after Littlestone and Warmuth).

theorem algLoss_le {η : ℝ} (ls : List (Fin n → ℝ)) (hb : Bounded ls) (i : Fin n) :
    (1 - exp (-η)) * algLoss η ls (fun _ => 1) ≤ η * expertLoss i ls + log n

Uses 7

Statement usesLosses in the unit interval · Loss of the Hedge algorithm · Total loss of an expert

Proof usesTotal weight of the Hedge experts · Weight decay over a Hedge run · Hedge weights after a sequence of rounds · Closed form of the Hedge weights

21 fully proved

The second-order bound

DefinitionWeighted second moment of a Hedge round#✓fully proved

For weights \(w\) and losses \(\ell\) on \(n\) experts, the round's weighted second moment is \(\left(\sum_i w_i \ell_i^2\right) / W\), where \(W = \sum_i w_i\) is the total weight; that is, \(\sum_i x_i \ell_i^2\) for the played distribution \(x = w / W\).

noncomputable def roundSq (w ℓ : Fin n → ℝ) : ℝ := (∑ i, w i * ℓ i ^ 2) / total w

Uses 1 · Used by 4

Statement usesTotal weight of the Hedge experts

Used bySummed second moments of the Hedge losses · The summed second moments split at any round · A round costs weight in proportion to the algorithm's loss, up to a second-order term · Weight decay over a Hedge run, second-order form

DefinitionSummed second moments of the Hedge losses#✓fully proved

Let \(\eta\) be a learning rate, \(w \in \mathbb{R}^n\) initial weights on \(n\) experts and \(\ell_1, \dots, \ell_T \in \mathbb{R}^n\) the losses of \(T\) rounds. Set \(w_1 = w\) and \(w_{t+1}(j) = w_t(j) e^{-\eta \ell_t(j)}\). The summed second moment is \(\sum_{t=1}^T \bigl(\sum_j w_t(j) \ell_t(j)^2\bigr) / \sum_j w_t(j)\), the sum over the rounds of the weighted second moment of that round's losses; a round whose total weight is \(0\) contributes \(0\).

noncomputable def algSq (η : ℝ) : List (Fin n → ℝ) → (Fin n → ℝ) → ℝ
  | [], _ => 0
  | ℓ :: ls, w => roundSq w ℓ + algSq η ls (update η w ℓ)

Uses 2 · Used by 3

Statement usesWeighted second moment of a Hedge round · Hedge weight update

Used byThe second-order Hedge bound · The summed second moments split at any round · Weight decay over a Hedge run, second-order form

DefinitionNonnegative losses#✓fully proved

A finite sequence of loss vectors \(\ell_1, \dots, \ell_T \in \mathbb{R}^n\) on \(n\) experts has nonnegative losses when \(\ell_t(i) \ge 0\) for every round \(t\) and every expert \(i\).

def Nonneg (ls : List (Fin n → ℝ)) : Prop := ∀ ℓ ∈ ls, ∀ i, 0 ≤ ℓ i

Used by 2

Used byThe second-order Hedge bound · Weight decay over a Hedge run, second-order form

TheoremA round costs weight in proportion to the algorithm's loss, up to a second-order term#✓fully proved

Let \(n > 0\), let \(w\) be positive weights on \(n\) experts, let \(\ell\) be nonnegative losses, and let \(\eta \ge 0\). Let \(w'\) be the Hedge update of \(w\) with learning rate \(\eta\), so that \(w'_i = w_i e^{-\eta \ell_i}\), and let \(W\) and \(W'\) be the total weights of \(w\) and \(w'\). Then \(W' \le W \exp(-\eta L + \eta^2 Q)\), where \(L\) is the round's loss and \(Q\) its weighted second moment under the weights \(w\).

theorem total_update_le_sq {η : ℝ} {w ℓ : Fin n → ℝ} (hw : ∀ i, 0 < w i) (hn : 0 < n)
    (hη : 0 ≤ η) (hℓ : ∀ i, 0 ≤ ℓ i) :
    total (update η w ℓ) ≤ total w * exp (-η * roundLoss w ℓ + η ^ 2 * roundSq w ℓ)

Uses 5 · Used by 1

Statement usesLoss of a Hedge round · Weighted second moment of a Hedge round · Total weight of the Hedge experts · Hedge weight update

Proof usesQuadratic upper bound for \(e^{-x}\)

Used byWeight decay over a Hedge run, second-order form

TheoremWeight decay over a Hedge run, second-order form#✓fully proved

Let \(n > 0\) and \(\eta \ge 0\). For every sequence of rounds with nonnegative losses and all positive initial weights \(w\) on \(n\) experts, the total weight after running Hedge with learning rate \(\eta\) from \(w\) is at most \(W \exp(-\eta L + \eta^2 Q)\). Here \(W\) is the total weight of \(w\), \(L\) is the algorithm's total loss over the rounds and \(Q\) is the sum of the rounds' weighted second moments, both for the run from \(w\) with learning rate \(\eta\).

theorem total_weights_le_sq {η : ℝ} (hn : 0 < n) (hη : 0 ≤ η) :
    ∀ (ls : List (Fin n → ℝ)) (w : Fin n → ℝ), (∀ i, 0 < w i) → Nonneg ls →
    total (weights η ls w) ≤ total w * exp (-η * algLoss η ls w + η ^ 2 * algSq η ls w)

Uses 9 · Used by 1

Statement usesNonnegative losses · Loss of the Hedge algorithm · Summed second moments of the Hedge losses · Total weight of the Hedge experts · Hedge weights after a sequence of rounds

Proof usesLoss of a Hedge round · Weighted second moment of a Hedge round · A round costs weight in proportion to the algorithm's loss, up to a second-order term · Hedge weight update

Used byThe second-order Hedge bound

TheoremThe second-order Hedge bound#✓fully proved

Let \(\eta > 0\), and let \(\ell_1, \dots, \ell_T\) be loss vectors in \(\mathbb{R}^n\) for \(n\) experts with \(\ell_t(j) \ge 0\) for all \(t\) and \(j\). Run Hedge with learning rate \(\eta\) from unit weights, that is \(w_1(j) = 1\) and \(w_{t+1}(j) = w_t(j) e^{-\eta \ell_t(j)}\), and let \(x_t(j) = w_t(j) / \sum_k w_t(k)\) be the distribution played in round \(t\). Then for every expert \(i\),

\[\sum_{t=1}^T \sum_j x_t(j) \ell_t(j) \le \sum_{t=1}^T \ell_t(i) + \eta \sum_{t=1}^T \sum_j x_t(j) \ell_t(j)^2 + \frac{\log n}{\eta}.\]

This is Theorem 1.3 of Hazan, Introduction to Online Convex Optimization. Unlike the first-order Hedge loss bound, the losses need not be at most \(1\).

theorem algLoss_le_sq {η : ℝ} (hη : 0 < η) (ls : List (Fin n → ℝ)) (hb : Nonneg ls)
    (i : Fin n) :
    algLoss η ls (fun _ => 1) ≤ expertLoss i ls + η * algSq η ls (fun _ => 1) + log n / η

Uses 8

Statement usesNonnegative losses · Loss of the Hedge algorithm · Summed second moments of the Hedge losses · Total loss of an expert

Proof usesTotal weight of the Hedge experts · Weight decay over a Hedge run, second-order form · Hedge weights after a sequence of rounds · Closed form of the Hedge weights

Splitting a run

TheoremA Hedge run splits at any round#✓fully proved

For every learning rate \(\eta\), sequences of rounds \(\lambda\) and \(\lambda'\), and initial weights \(w\), the weights after running Hedge on the rounds of \(\lambda\) followed by those of \(\lambda'\), starting from \(w\), equal the weights after running it on \(\lambda'\) starting from the weights reached after \(\lambda\) from \(w\).

theorem weights_append (η : ℝ) : ∀ (ls ls' : List (Fin n → ℝ)) (w : Fin n → ℝ),
    weights η (ls ++ ls') w = weights η ls' (weights η ls w)

Uses 2

Statement usesHedge weights after a sequence of rounds

Proof usesHedge weight update

TheoremThe Hedge loss splits at any round#✓fully proved

Fix a learning rate \(\eta\) and \(n\) experts. For a finite sequence \(\sigma\) of loss vectors in \(\mathbb{R}^n\) and weights \(w \in \mathbb{R}^n\), write \(L(\sigma, w)\) for the algorithm's total loss over \(\sigma\) started from \(w\), and \(W(\sigma, w)\) for the weights after the rounds of \(\sigma\) started from \(w\). Then for all such sequences \(\sigma, \sigma'\) and all weights \(w\), the loss over the concatenation \(\sigma\sigma'\) satisfies \(L(\sigma\sigma', w) = L(\sigma, w) + L(\sigma', W(\sigma, w))\).

theorem algLoss_append (η : ℝ) : ∀ (ls ls' : List (Fin n → ℝ)) (w : Fin n → ℝ),
    algLoss η (ls ++ ls') w = algLoss η ls w + algLoss η ls' (weights η ls w)

Uses 4

Statement usesLoss of the Hedge algorithm · Hedge weights after a sequence of rounds

Proof usesLoss of a Hedge round · Hedge weight update

TheoremThe summed second moments split at any round#✓fully proved

Fix a learning rate \(\eta\) and \(n\) experts. For a finite sequence \(\sigma\) of loss vectors in \(\mathbb{R}^n\) and weights \(w \in \mathbb{R}^n\), write \(Q(\sigma, w)\) for the sum over the rounds of \(\sigma\) of the weighted second moments of the losses, started from \(w\), and \(W(\sigma, w)\) for the weights after the rounds of \(\sigma\) started from \(w\). Then for all such sequences \(\sigma, \sigma'\) and all weights \(w\), \(Q(\sigma\sigma', w) = Q(\sigma, w) + Q(\sigma', W(\sigma, w))\).

theorem algSq_append (η : ℝ) : ∀ (ls ls' : List (Fin n → ℝ)) (w : Fin n → ℝ),
    algSq η (ls ++ ls') w = algSq η ls w + algSq η ls' (weights η ls w)

Uses 4

Statement usesSummed second moments of the Hedge losses · Hedge weights after a sequence of rounds

Proof usesWeighted second moment of a Hedge round · Hedge weight update

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.