LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exp4 exponential-weights potential inequality

Statement

For any Exp4 run with learning rate $η > 0$ and any fixed expert $m^{*} \in [M]$ , define ${\tilde{L}}_{t, m} = 1 - {\tilde{X}}_{t, m}$ . The following pathwise inequality holds for every realized action sequence:

\sum_{t = 1}^{n} {\tilde{X}}_{t, m^{*}} - \sum_{t = 1}^{n} \sum_{m = 1}^{M} Q_{t, m} {\tilde{X}}_{t, m} \leq \frac{\log M}{η} + \frac{η}{2} \sum_{t = 1}^{n} \sum_{m = 1}^{M} Q_{t, m} {\tilde{L}}_{t, m}^{2} .

Statement references

Exp4 update: the expert weights are updated by normalized exponentials of the estimated rewards.

Nonpositive-axis exponential inequality: the potential proof applies this inequality to the negative estimated losses.

Facts & Assumptions

Given: Integers $n \geq 1$ , $M > 1$ , a learning rate $η > 0$ , and an Exp4 run.

[F1]

Exp4 with unbiased estimated rewards: $Q_{1, m} = 1 / M$ , $Q_{t + 1, m}$ is proportional to $Q_{t, m} \exp (η {\tilde{X}}_{t, m})$ , and ${\tilde{L}}_{t, m} = 1 - {\tilde{X}}_{t, m} \geq 0$ is finite.

[F2]

Second-order exponential upper bound on the nonpositive axis: $\exp (z) \leq 1 + z + z^{2} / 2$ for every real $z \leq 0$ .

[F3]

The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ : $\exp (a + b) = \exp (a) \exp (b)$ for all real $a, b$ .

[F4]

The natural logarithm as the inverse of the exponential function: $\log$ is defined on positive reals as the inverse of $\exp$ .

[F5]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is strictly increasing, $\log 1 = 0$ , and $\log (u / v) = \log u - \log v$ for $u, v > 0$ .

[F6]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log$ is differentiable on $(0, \infty)$ with $\log^{'} (u) = 1 / u$ .

[F7]

Mean value theorem on a closed real interval: for a continuous function on a closed interval differentiable in its interior, some interior point realizes its secant slope as the derivative.

[F8]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $\exp (u) > 0$ for every real $u$ .

Proof

1.1F4F5F6F7caseschoosealgebra

First, for every $s > 0$ , $\log s \leq s - 1$ . If $s = 1$ this is equality by [F5]. If $s > 1$ , apply [F7] to $\log$ on $[1, s]$ ; by [F6] there is $c \in (1, s)$ with $\log s = (s - 1) / c \leq s - 1$ . If $0 < s < 1$ , apply [F7] on $[s, 1]$ to obtain $c \in (s, 1)$ with $- \log s = (1 - s) / c \geq 1 - s$ , again giving $\log s \leq s - 1$ . All intervals lie in $(0, \infty)$ , where [F6] supplies continuity and differentiability.

2.1F1F2F3F5F8step 1.1algebra

Define $W_{1, m} = 1$ , $W_{t + 1, m} = W_{t, m} \exp (η {\tilde{X}}_{t, m})$ , and $Z_{t} = \sum_{m} W_{t, m}$ . The update gives $Q_{t, m} = W_{t, m} / Z_{t}$ . Since ${\tilde{X}}_{t, m} = 1 - {\tilde{L}}_{t, m}$ , [F3] and [F2] give $Z_{t + 1} / Z_{t} = \sum_{m} Q_{t, m} \exp (η {\tilde{X}}_{t, m}) = \exp (η) \sum_{m} Q_{t, m} \exp (- η {\tilde{L}}_{t, m}) \leq \exp (η) S_{t}$ , where $S_{t} = \sum_{m} Q_{t, m} (1 - η {\tilde{L}}_{t, m} + η^{2} {\tilde{L}}_{t, m}^{2} / 2) > 0$ . Positivity follows termwise from $1 - u + u^{2} / 2 = ((u - 1)^{2} + 1) / 2 > 0$ and $Q_{t, m} > 0$ . Applying [F5] and step 1.1 yields $\log (Z_{t + 1} / Z_{t}) \leq η + \log S_{t} \leq η + S_{t} - 1 = η \sum_{m} Q_{t, m} {\tilde{X}}_{t, m} + (η^{2} / 2) \sum_{m} Q_{t, m} {\tilde{L}}_{t, m}^{2}$ .

3.1F1F5step 2.1algebra∎

Summing step 2.1 over $t$ and using [F5] telescopes the left side to $\log (Z_{n + 1} / Z_{1})$ . Since $Z_{1} = M$ and $Z_{n + 1} = \sum_{m} \exp (η \sum_{t = 1}^{n} {\tilde{X}}_{t, m})$ , the fixed expert term gives $\log (Z_{n + 1} / Z_{1}) \geq η \sum_{t = 1}^{n} {\tilde{X}}_{t, m^{*}} - \log M$ . Combining this lower bound with the summed upper bound and dividing by $η > 0$ proves the stated inequality.

Depends on

Used by

Exp4 expected regret against the best fixed expert Theorem

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (standard reference, not scraped)
Peter Auer, Nicolò Cesa-Bianchi, Yoav Freund, and Robert Schapire, The Nonstochastic Multiarmed Bandit Problem (standard reference, not scraped)