AdaBoost

DefinitionWeighted training error#✓fully proved

For labels \(y\), weights \(D\) and predictions \(h\) on \(m\) training points, the weighted training error of \(h\) under \(D\) is \(\sum_{i : h(i) \ne y(i)} D(i)\), the total weight of the points that \(h\) misclassifies.

noncomputable def err (y : Fin m → Bool) (D : Fin m → ℝ) (h : Fin m → Bool) : ℝ :=
  ∑ i, if h i = y i then 0 else D i

Used by 9

Used byUnrolling the weights · Weighted error of an AdaBoost round · Normalizer of a boosting round · The normalizer of a round is \(2\sqrt{\varepsilon(1 - \varepsilon)}\) · AdaBoost reweighting · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error · The weak-learning assumption

DefinitionAdaBoost's hypothesis weight#✓fully proved

A weak hypothesis with weighted error \(\varepsilon \in \mathbb{R}\) gets the weight \(\alpha(\varepsilon) = \frac{1}{2} \log \frac{1 - \varepsilon}{\varepsilon}\).

noncomputable def alpha (ε : ℝ) : ℝ := log ((1 - ε) / ε) / 2

Used by 8

Used byUnrolling the weights · Normalizer of a boosting round · The normalizer of a round is \(2\sqrt{\varepsilon(1 - \varepsilon)}\) · AdaBoost reweighting · AdaBoost's combined score · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error

DefinitionNormalizer of a boosting round#✓fully proved

For labels \(y\), weights \(D\) and predictions \(h\) on \(m\) training points, let \(\varepsilon\) be the weighted training error of \(h\) under \(D\) and \(\alpha = \alpha(\varepsilon)\) the hypothesis weight. The normalizer of the round is

\[Z = \sum_i D(i) \exp(-\alpha\, y_i h_i),\]

where the label \(y_i\) and the prediction \(h_i\) are read as \(\pm 1\).

noncomputable def normalizer (y : Fin m → Bool) (D : Fin m → ℝ) (h : Fin m → Bool) : ℝ :=
  ∑ i, D i * exp (-(alpha (err y D h)) * ((sign (y i) : ℝ) * sign (h i)))

Uses 3 · Used by 7

Statement usesAdaBoost's hypothesis weight · Weighted training error · Sign of a Boolean label

Used byUnrolling the weights · The normalizer of a round is \(2\sqrt{\varepsilon(1 - \varepsilon)}\) · AdaBoost reweighting · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error · Normalizer of an AdaBoost round

DefinitionAdaBoost reweighting#✓fully proved

For labels \(y\), weights \(D\) and predictions \(h\) on \(m\) training points, let \(\varepsilon\) be the weighted training error of \(h\) under \(D\), \(\alpha = \alpha(\varepsilon)\) the hypothesis weight and \(Z\) the normalizer of the round. The reweighted weight of point \(i\) is

\[D'(i) = \frac{D(i) \exp(-\alpha\, y_i h_i)}{Z},\]

where the label \(y_i\) and the prediction \(h_i\) are read as \(\pm 1\).

noncomputable def reweight (y : Fin m → Bool) (D : Fin m → ℝ) (h : Fin m → Bool) (i : Fin m) :
    ℝ :=
  D i * exp (-(alpha (err y D h)) * ((sign (y i) : ℝ) * sign (h i))) / normalizer y D h

Uses 4 · Used by 1

Statement usesAdaBoost's hypothesis weight · Weighted training error · Normalizer of a boosting round · Sign of a Boolean label

Used byAdaBoost's weights

TheoremThe normalizer of a round is \(2\sqrt{\varepsilon(1 - \varepsilon)}\)#✓fully proved

Let \(y\) be labels on \(m\) training points, \(D\) real weights on the points with \(\sum_i D(i) = 1\), and \(h\) predictions whose weighted training error \(\varepsilon\) under \(D\) satisfies \(0 < \varepsilon < 1\). Then the normalizer of the round with weights \(D\) and hypothesis \(h\) equals \(2\sqrt{\varepsilon(1 - \varepsilon)}\).

theorem normalizer_eq (y : Fin m → Bool) {D : Fin m → ℝ} (hD : ∑ i, D i = 1)
    (h : Fin m → Bool) (h0 : 0 < err y D h) (h1 : err y D h < 1) :
    normalizer y D h = 2 * sqrt (err y D h * (1 - err y D h))

Uses 4 · Used by 1

Statement usesWeighted training error · Normalizer of a boosting round

Proof usesAdaBoost's hypothesis weight · Sign of a Boolean label

Used byThe Freund–Schapire bound on AdaBoost's training error

TheoremOne round's factor is at most exp (-2 γ²)#✓fully proved

For real numbers \(\varepsilon\) and \(\gamma\) with \(\gamma \ge 0\) and \(\varepsilon \le 1/2 - \gamma\), we have \(2\sqrt{\varepsilon (1 - \varepsilon)} \le e^{-2\gamma^2}\), where the square root of a negative number is taken to be \(0\).

theorem two_mul_sqrt_le_exp {ε γ : ℝ} (hγ : 0 ≤ γ) (hε : ε ≤ 1 / 2 - γ) :
    2 * sqrt (ε * (1 - ε)) ≤ exp (-2 * γ ^ 2)

Used by 1

Used byAdaBoost drives the training error down exponentially

DefinitionAdaBoost's weights#✓fully proved

Given labels \(y\) on \(m\) training points and a weak learner \(\mathrm{wl}\), which maps weights on the points to a hypothesis's predictions on them, AdaBoost's weights \(D_t\) on the points are defined by \(D_0(i) = 1/m\) for every point \(i\), and \(D_{t+1}\) is the reweighting of \(D_t\) by the hypothesis \(\mathrm{wl}(D_t)\).

noncomputable def dist : ℕ → Fin m → ℝ
  | 0 => fun _ => 1 / m
  | t + 1 => reweight y (dist t) (wl (dist t))

Uses 1 · Used by 7

Statement usesAdaBoost reweighting

Used byUnrolling the weights · Weighted error of an AdaBoost round · Weak hypothesis of an AdaBoost round · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error · Normalizer of an AdaBoost round

DefinitionWeak hypothesis of an AdaBoost round#✓fully proved

The weak hypothesis \(h_t\) of round \(t\) is the weak learner's output \(\mathrm{wl}(D_t)\) on the weights \(D_t\) of round \(t\).

noncomputable def hyp (t : ℕ) : Fin m → Bool := wl (dist y wl t)

Uses 1 · Used by 7

Statement usesAdaBoost's weights

Used byUnrolling the weights · Weighted error of an AdaBoost round · AdaBoost's combined score · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error · Normalizer of an AdaBoost round

DefinitionWeighted error of an AdaBoost round#✓fully proved

The weighted error \(\varepsilon_t\) of round \(t\) is the weighted training error of the weak hypothesis \(h_t\) of round \(t\) under the weights \(D_t\) of round \(t\).

noncomputable def eps (t : ℕ) : ℝ := err y (dist y wl t) (hyp y wl t)

Uses 3 · Used by 4

Statement usesAdaBoost's weights · Weighted training error · Weak hypothesis of an AdaBoost round

Used byUnrolling the weights · AdaBoost's combined score · AdaBoost drives the training error down exponentially · The Freund–Schapire bound on AdaBoost's training error

DefinitionNormalizer of an AdaBoost round#✓fully proved

Run AdaBoost on training points with labels \(y\), and read labels and predictions as \(\pm 1\). The normalizer of round \(t\) is \(Z_t = \sum_i D_t(i) \exp(-\alpha_t y_i h_t(i))\), where \(D_t\) are AdaBoost's weights in round \(t\), \(h_t\) is the weak hypothesis of round \(t\), and \(\alpha_t\) is its weight.

noncomputable def zee (t : ℕ) : ℝ := normalizer y (dist y wl t) (hyp y wl t)

Uses 3 · Used by 4

Statement usesAdaBoost's weights · Weak hypothesis of an AdaBoost round · Normalizer of a boosting round

Used byUnrolling the weights · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error

DefinitionAdaBoost's combined score#✓fully proved

After \(T\) rounds, the combined score of training point \(i\) is

\[F_T(i) = \sum_{t < T} \alpha(\varepsilon_t)\, h_t(i),\]

where \(\varepsilon_t\) is the weighted error and \(h_t\) the weak hypothesis of round \(t\), \(\alpha(\varepsilon) = \frac{1}{2} \log \frac{1 - \varepsilon}{\varepsilon}\) is the hypothesis weight, and the prediction \(h_t(i)\) is read as \(\pm 1\). The final classifier is the sign of \(F_T\).

noncomputable def score (T : ℕ) (i : Fin m) : ℝ :=
  ∑ t ∈ Finset.range T, alpha (eps y wl t) * sign (hyp y wl t i)

Uses 4 · Used by 3

Statement usesAdaBoost's hypothesis weight · Weighted error of an AdaBoost round · Weak hypothesis of an AdaBoost round · Sign of a Boolean label

Used byUnrolling the weights · Training error of AdaBoost · The training error is at most the product of the normalizers

DefinitionTraining error of AdaBoost#✓fully proved

Let AdaBoost run on \(m\) training points with labels \(y\), read labels and predictions as \(\pm 1\), and let \(F_T\) be the combined score after \(T\) rounds. The training error after \(T\) rounds is the number of training points \(i\) with \(y_i F_T(i) \le 0\), divided by \(m\); in particular a zero score counts as an error.

noncomputable def trainErr (T : ℕ) : ℝ :=
  (∑ i, if sign (y i) * score y wl T i ≤ 0 then (1 : ℝ) else 0) / m

Uses 2 · Used by 3

Statement usesAdaBoost's combined score · Sign of a Boolean label

Used byAdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error

TheoremUnrolling the weights#✓fully proved

Run AdaBoost with labels \(y\) on \(m > 0\) training points and a weak learner, and let \(D_T\) be the weights on the points after \(T\) rounds, \(Z_t\) the normalizer of round \(t\), and \(F_T\) the combined score after \(T\) rounds. Then for every \(T \in \mathbb{N}\) and every training point \(i\),

\[D_T(i) \cdot m \prod_{t < T} Z_t = \exp(-y_i F_T(i)),\]

where the label \(y_i\) is read as \(\pm 1\).

theorem dist_mul_prod (hm : 0 < m) : ∀ (T : ℕ) (i : Fin m),
    dist y wl T i * (m * ∏ t ∈ Finset.range T, zee y wl t) = exp (-(sign (y i) * score y wl T i))

Uses 9 · Used by 1

Statement usesAdaBoost's weights · AdaBoost's combined score · Normalizer of an AdaBoost round · Sign of a Boolean label

Proof usesAdaBoost's hypothesis weight · Weighted error of an AdaBoost round · Weighted training error · Weak hypothesis of an AdaBoost round · Normalizer of a boosting round

Used byThe training error is at most the product of the normalizers

TheoremThe training error is at most the product of the normalizers#✓fully proved

Let AdaBoost run on \(m > 0\) training points with labels \(y\) and an arbitrary weak learner, and write \(Z_t\) for the normalizer of round \(t\). Then for every number of rounds \(T\), the training error after \(T\) rounds is at most \(\prod_{t < T} Z_t\).

theorem trainErr_le_prod (hm : 0 < m) (T : ℕ) :
    trainErr y wl T ≤ ∏ t ∈ Finset.range T, zee y wl t

Uses 10 · Used by 1

Statement usesTraining error of AdaBoost · Normalizer of an AdaBoost round

Proof usesAdaBoost's hypothesis weight · AdaBoost's weights · Unrolling the weights · Weighted training error · Weak hypothesis of an AdaBoost round · Normalizer of a boosting round · AdaBoost's combined score · Sign of a Boolean label

Used byThe Freund–Schapire bound on AdaBoost's training error

DefinitionThe weak-learning assumption#✓fully proved

A weak learner, which maps weights on the \(m\) training points with labels \(y\) to a hypothesis on those points, has edge \(\gamma\) if for every weighting \(D\) of the training points with \(D_i > 0\) for all \(i\) and \(\sum_i D_i = 1\), the hypothesis it returns on \(D\) has weighted error under \(D\) in the interval \((0, 1/2 - \gamma]\).

def WeakLearner (y : Fin m → Bool) (wl : (Fin m → ℝ) → Fin m → Bool) (γ : ℝ) : Prop :=
  ∀ D : Fin m → ℝ, (∀ i, 0 < D i) → ∑ i, D i = 1 → 0 < err y D (wl D) ∧ err y D (wl D) ≤ 1 / 2 - γ

Uses 1 · Used by 2

Statement usesWeighted training error

Used byAdaBoost drives the training error down exponentially · The Freund–Schapire bound on AdaBoost's training error

TheoremThe Freund–Schapire bound on AdaBoost's training error#✓fully proved

Let AdaBoost run on \(m > 0\) training points with labels \(y\) and a weak learner with edge \(\gamma \ge 0\), that is, one that on every weighting \(D\) of the training points with \(D_i > 0\) for all \(i\) and \(\sum_i D_i = 1\) returns a hypothesis whose weighted error under \(D\) lies in \((0, 1/2 - \gamma]\). Write \(\varepsilon_t\) for the weighted error of the weak hypothesis of round \(t\) under AdaBoost's weights of that round. Then for every number of rounds \(T\), the training error after \(T\) rounds is at most \(\prod_{t < T} 2\sqrt{\varepsilon_t (1 - \varepsilon_t)}\).

theorem trainErr_le_prod_sqrt (hm : 0 < m) {γ : ℝ} (hγ : 0 ≤ γ) (hwl : WeakLearner y wl γ)
    (T : ℕ) :
    trainErr y wl T ≤ ∏ t ∈ Finset.range T, 2 * sqrt (eps y wl t * (1 - eps y wl t))

Uses 12 · Used by 1

Statement usesThe weak-learning assumption · Weighted error of an AdaBoost round · Training error of AdaBoost

Proof usesAdaBoost's hypothesis weight · AdaBoost's weights · Weighted training error · Weak hypothesis of an AdaBoost round · Normalizer of a boosting round · The normalizer of a round is \(2\sqrt{\varepsilon(1 - \varepsilon)}\) · The training error is at most the product of the normalizers · Normalizer of an AdaBoost round · Sign of a Boolean label

Used byAdaBoost drives the training error down exponentially

TheoremAdaBoost drives the training error down exponentially#✓fully proved

Let AdaBoost run on \(m > 0\) training points with labels \(y\) and a weak learner with edge \(\gamma \ge 0\), that is, one that on every weighting \(D\) of the training points with \(D_i > 0\) for all \(i\) and \(\sum_i D_i = 1\) returns a hypothesis whose weighted error under \(D\) lies in \((0, 1/2 - \gamma]\). Then for every number of rounds \(T\), the training error after \(T\) rounds is at most \(e^{-2\gamma^2 T}\).

theorem trainErr_le_exp (hm : 0 < m) {γ : ℝ} (hγ : 0 ≤ γ) (hwl : WeakLearner y wl γ) (T : ℕ) :
    trainErr y wl T ≤ exp (-2 * γ ^ 2 * T)

Uses 12

Statement usesThe weak-learning assumption · Training error of AdaBoost

Proof usesAdaBoost's hypothesis weight · AdaBoost's weights · Weighted error of an AdaBoost round · Weighted training error · Weak hypothesis of an AdaBoost round · Normalizer of a boosting round · The Freund–Schapire bound on AdaBoost's training error · One round's factor is at most exp (-2 γ²) · Normalizer of an AdaBoost round · Sign of a Boolean label

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.