Also read in: Online Learning Book. This is the same chapter and the same Lean nodes.

Teaching chapter 07 of 10 · Canonical route compiled

7. EXP3 and adversarial concentration

The scoped canonical generated EXP3 route compiles from exponential-weight potentials and importance-weighted conditional moments through horizon-tuned expected and best-arm high-probability endpoints, plus a distinct fixed-process all-positive-prefix realized-regret event and a sparse-loss extension.

How to read the status. It describes this page's canonical local Lean route, not completion of the cited textbook chapter or every extension listed below.

Orientation

Who should read this. Read Foundations first; later sections use the Probability layer heavily.

Learning goals

Connect the one-step exponential-potential inequality to deterministic Hedge regret.
See why positive exploration makes importance-weighted estimators legal.
Track predictable variance, realized deviation, comparator regret, and sparsity failures into explicit probability events.

Textbook crosswalk

Read the mathematics before the Lean interface

The Book Map is a curated formalization curriculum anchored in Bandit Algorithms, not a chapter-for-chapter reproduction of one book. Visible page labels use the numbered pages of its free online edition; source buttons use the PDF viewer's physical page index, which includes front matter and can therefore be larger. Companion papers cover algorithm-specific results.

Primary spine · free online edition

Bandit Algorithms

Tor Lattimore and Csaba Szepesvári

Location: Ch. 11–12
Pages: online pp. 148–172

Open at the cited pages

algorithm · ordered flow

EXP3 with importance-weighted losses

Read top to bottom: each step supplies the state or proof fact used by the next one.

Turn weights into probabilities
Normalize positive arm weights into the current sampling law.
Sample an arm
Draw the current action from that probability vector.
Estimate all losses
Use the observed loss divided by its sampling probability for the selected arm; use zero for the others.
Update exponentially
Downweight arms according to their estimated cumulative losses.
Separate guarantees
Expected, fixed-horizon tail, all-time, and sparse-loss results use distinct concentration interfaces.

Algorithm · explicit conventions

EXP3 importance-weighted update

The loop names the sampling law, the one-coordinate unbiased loss estimate, and the exponential update used by the potential argument.

Sampling, estimation, and weight update. Formula renderer unavailable; readable fallback: Normalize positive weights, sample an arm, divide the observed loss by that arm's probability, and exponentially downweight each arm by its estimated loss.\[p_t(a)=\frac{w_t(a)}{\sum_b w_t(b)},\qquad \widehat\ell_t(a)=\frac{\ell_t(A_t)\mathbf 1\{A_t=a\}}{p_t(a)},\qquad w_{t+1}(a)=w_t(a)e^{-\eta\widehat\ell_t(a)}.\]

input: k arms, horizon n, learning rate η; initialize w_1(a) = 1
for t = 1,…,n:
    normalize weights into the sampling law p_t
    sample A_t ~ p_t and observe only loss ℓ_t(A_t)
    set ℓ̂_t(a) = ℓ_t(A_t) 1{A_t=a} / p_t(a) for every arm
    update w_{t+1}(a) = w_t(a) exp(-η ℓ̂_t(a))

Source/Lean boundary. The displayed equations are the textbook core. BanditRLlib's generated predictable route makes positive support and any exploration mixture explicit, and its expected, fixed-window, all-prefix, realized, and sparse-loss guarantees remain separate theorems with separate confidence contracts.

Worked example · follow one decision

One EXP3 update from a single observed loss

Start with two equal weights, learning rate η = 0.25, and suppose the sampled second arm incurs loss 0.8. The update shows why dividing by the sampling probability is both necessary and noisy.

Sample from equal weights
Both arms initially have the same probability; this particular history samples arm 2.
Worked example step 1. Formula renderer unavailable; readable fallback: Both initial weights are one, both probabilities are one half, and arm 2 is sampled with observed loss 0.8.\[w_1=(1,1),\qquad p_1=\left(\frac12,\frac12\right),\qquad A_1=2,\quad \ell_1(A_1)=0.8.\]
Reconstruct an unbiased loss coordinate
Only arm 2 is observed. Dividing by its probability produces a larger estimate whose conditional expectation equals the hidden loss coordinate.
Worked example step 2. Formula renderer unavailable; readable fallback: The estimated loss is zero for arm 1 and 1.6 for arm 2 because the observed 0.8 is divided by probability one half.\[\widehat\ell_1(1)=0,\qquad \widehat\ell_1(2)=\frac{0.8}{1/2}=1.6.\]
Downweight the observed loss
The exponential update lowers arm 2's weight, so arm 1 becomes more likely at the next round without assigning arm 2 zero probability.
Worked example step 3. Formula renderer unavailable; readable fallback: The next weights are approximately 1 and 0.6703, so arm 1 receives probability about 0.599.\[w_2=(1,e^{-0.4})\approx(1,0.6703),\qquad p_2(1)=\frac1{1+e^{-0.4}}\approx0.599.\]

Takeaway. Importance weighting repairs the missing feedback in expectation, while its enlarged squared magnitude creates the variance term that the EXP3 proof must pay for.

Scope. This is one deterministic arithmetic trace conditional on a sampled action. It is not an adversarial-regret experiment and does not merge the expected, fixed-window, all-prefix, or realized-regret theorem contracts.

Proof bridge · source to Lean

How one bandit observation becomes an adversarial regret guarantee

EXP3 couples an unbiased importance-weighted estimator with the exponential-weights potential. The proof must pay explicitly for the estimator's second moment.

Recover every coordinate in expectation
Although only the selected loss is observed, positive sampling probability makes the importance-weighted estimate conditionally unbiased.
Step 1 equation. Formula renderer unavailable; readable fallback: Given the past, the importance-weighted estimated loss of each arm has expectation equal to that arm's actual loss.\[\mathbb E_t[\widehat\ell_t(a)]=\ell_t(a).\]
Compare exponential potentials
The log change of total weight compares the algorithm's estimated loss with any fixed arm, leaving a learning-rate times second-moment penalty.
Step 2 equation. Formula renderer unavailable; readable fallback: Estimated regret is at most log k over eta plus eta over two times the accumulated estimated-loss second moment.\[\sum_t\langle p_t,\widehat\ell_t\rangle-\sum_t\widehat\ell_t(a)\le\frac{\log k}{\eta}+\frac{\eta}{2}\sum_t\langle p_t,\widehat\ell_t^2\rangle.\]
Pay for bandit noise
Importance weighting inflates individual observations, but averaging under the sampling law bounds the conditional second-moment contribution by the number of arms.
Step 3 equation. Formula renderer unavailable; readable fallback: The conditional expected weighted squared estimate is at most the number of arms.\[\mathbb E_t\langle p_t,\widehat\ell_t^2\rangle\le k.\]
Balance the two costs
Choosing the learning rate so that the initial-complexity and variance terms match yields the square-root expected-regret rate.
Step 4 equation. Formula renderer unavailable; readable fallback: With the balanced learning rate, expected regret is at most the square root of two n k log k.\[\eta=\sqrt{\frac{2\log k}{nk}}\quad\Longrightarrow\quad R_n\le\sqrt{2nk\log k}.\]

Reading boundary. The bridge follows the textbook expected-regret argument. BanditRLlib's fixed-window, all-prefix, realized, and sparse-loss extensions have additional hypotheses and are intentionally not collapsed into this one card.

Source theorem · faithful restatement

Theorem 11.2 (EXP3 expected regret)

Original at online p. 156 ↗

Importance weighting makes the bandit observation unbiased, while exponential weights controls the resulting estimated-loss regret.

Model: An adversarial k-armed bandit with a fixed reward table x in [0,1]^(n×k).
Assumptions: The policy is the textbook EXP3 construction and compares with the best fixed arm in hindsight.
Algorithm parameters: Horizon n, arm count k, and learning rate η = √(2 log k/(nk)).
Regret notion: Expected adversarial pseudo-regret R_n against the best fixed arm.
Guarantee: R_n ≤ √(2nk log k).

Source mathematical statement. Formula renderer unavailable; readable fallback: With the textbook learning rate, EXP3 has expected adversarial regret at most the square root of two times horizon, arm count, and log arm count.\[\eta=\sqrt{\frac{2\log k}{nk}}\quad\Longrightarrow\quad R_n\le\sqrt{2nk\log k}.\]

BanditRLlib relationship. The local generated predictable process uses its own tuning constants and also compiles separate fixed-horizon, all-time, realized-regret, and sparse-loss extensions.

The mathematical content is restated in this site's notation; wording is ours. See online p. 156 in the linked source for the original statement and full assumptions.

Natural-language and Lean side by side

The mathematical readings are explanatory summaries. The exact generated Lean statement and its source link remain authoritative for hypotheses, types, constants, and indexing.

A curated route through definitions, key bridges, and canonical terminals stays visible. 4 additional dependency, extension, or research-frontier notes are grouped below.

Mathematics ↔ Lean

Pathwise exponential-weights regret

Lean declarationBanditRLProof.Exp3.hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss_of_nonneg

Compiled

Plain-English statement. For nonnegative estimated losses, exponential weights has pathwise regret at most a log-cardinality term divided by the learning rate plus the learning rate times the mixed squared loss.

Mathematical reading. Formula renderer unavailable; readable fallback: For nonnegative estimated losses, exponential weights has pathwise regret at most a log-cardinality term divided by the learning rate plus the learning rate times the mixed squared loss.\(\sum_t\langle p_t,\hat\ell_t\rangle-\sum_t\hat\ell_t(a)\le\frac{\log K}{\eta}+\eta\sum_t\langle p_t,\hat\ell_t^2\rangle.\)

Intuition: The log potential can neither fall below the comparator weight nor rise faster than the second-order exponential bound permits.
Why it is needed: This deterministic theorem is the algorithmic core reused by expected and high-probability EXP3 consumers.
Place in the proof: It sits between the potential algebra and probability-specific moment transport.

Proof and Lean reading notes

Proof idea: Bound each exponential update by a quadratic inequality, telescope the log normalizer, and compare the final normalizer with one fixed arm's weight.
Lean reading notes: The theorem is pathwise and does not itself mention a probability measure. Unbiasedness and integrability enter later.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss_of_nonneg {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (loss : Nat -> Action -> Real) (T : Nat) (hloss : forall t, t < T -> forall a, a ∈ arms -> 0 <= loss t a) (comparator : Action) (hcomparator : comparator ∈ arms) : (Finset.range T).sum (fun t => mixedLoss arms eta loss t) - cumulativeLoss loss T comparator <= Real.log arms.card / eta + eta * (Finset.range T).sum (fun t => mixedSquaredLoss arms eta loss t)

Open in the declaration catalog Open source at line 283

Mathematics ↔ Lean

Expected regret for the generated EXP3 process

Lean declarationBanditRLProof.Exp3.sampledPredictable_expectedRegret_le_four_mul_sqrt

Compiled

Plain-English statement. With the repository's tuned learning and exploration rates, the generated predictable EXP3 process has expected regret bounded by an explicit square-root expression.

Mathematical reading. Formula renderer unavailable; readable fallback: With the repository's tuned learning and exploration rates, the generated predictable EXP3 process has expected regret bounded by an explicit square-root expression.\(\mathbb E R_T\le4\sqrt{KT\log K}\) in the theorem's normalized finite-arm setting.

Intuition: The tuning balances the potential term, second-moment term, and the price of forced exploration.
Why it is needed: It demonstrates a complete expected-regret route from the generated adaptive trajectory, not only a deterministic Hedge inequality.
Place in the proof: This is the clean expected endpoint before the later Bernstein and sparsity-sensitive high-probability branches.

Proof and Lean reading notes

Proof idea: Combine the Hedge theorem with conditional importance-weighted moment identities and exploration-bias control, then optimize the scalar parameters.
Lean reading notes: The exact constant and off-by-one horizon convention are governed by the displayed Lean statement. The schematic formula summarizes the leading shape only.
Teaching dependencies: BanditRLProof.Exp3.hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss_of_nonneg

Exact Lean statement

theorem sampledPredictable_expectedRegret_le_four_mul_sqrt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon_pos : 0 < horizon) (hscale : 4 * (arms.card : Real) * Real.log arms.card <= (horizon : Real)) (comparator : Action) (hcomparator : comparator ∈ arms) : let K := (arms.card : Real) let T := (horizon : Real) let gamma := tunedExplorationRate K T let eta := tunedLearningRate K T let mu := prior ⊗ₘ tunedPredictableTrajectoryKernel arms harms hcard_two loss horizon hhorizon_pos hscale integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) <= 4 * Real.sqrt (K * T * Real.log K)

Open in the declaration catalog Open source at line 181

Mathematics ↔ Lean

Finite-horizon Bernstein realized-regret tail

Lean declarationBanditRLProof.Exp3.sampledPredictable_allHorizonBernsteinSquareBestArmRealizedRegret_tail

Compiled

Plain-English statement. At any supplied positive horizon, the generated EXP3 process with the theorem's Bernstein-square tuning has a realized-regret tail against the best supported arm obtained by a finite comparator union.

Mathematical reading. Formula renderer unavailable; readable fallback: At any supplied positive horizon, the generated EXP3 process with the theorem's Bernstein-square tuning has a realized-regret tail against the best supported arm obtained by a finite comparator union.\(\Pr\{R_T^{\mathrm{real}}(a_T^\star)\ge b(K,T,\delta)\}\le\delta.\)

Intuition: First control regret to each supported comparator at confidence delta divided by the number of arms, then union the finite family and choose the best cumulative-loss arm.
Why it is needed: This is the chapter's fixed-window best-arm endpoint and makes comparator aggregation visible rather than silently replacing a fixed-comparator theorem by a minimum.
Place in the proof: It sits above the fixed-comparator Bernstein-square realized tail and beside, not above, the separate fixed-process all-positive-prefix branch.

Proof and Lean reading notes

Proof idea: Set the armwise confidence share, build horizon-dependent eta and gamma, apply the fixed-comparator generated-law tail to every arm, take a finite union, and rewrite the comparator minimum as best supported-arm cumulative loss.
Lean reading notes: The exact statement requires a probability prior, Standard Borel nonempty environment/action, finite nonempty decidable arms with K at least two, predictable unit losses, positive horizon, and 0<delta<=1. The eta, gamma, and trajectory law depend on T. The identifier allHorizon means the theorem can be instantiated at each horizon, not that one fixed policy is simultaneously controlled at all horizons.
Teaching dependencies: BanditRLProof.Exp3.sampledPredictable_allHorizonBernsteinSquareRealizedRegret_tail

Exact Lean statement

theorem sampledPredictable_allHorizonBernsteinSquareBestArmRealizedRegret_tail {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let deltaArm := delta / (arms.card : Real) let gamma := bernsteinSquareClippedExplorationRate (arms.card : Real) (horizon : Real) deltaArm let eta := bernsteinSquareHighProbabilityLearningRate arms gamma horizon deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (bernsteinSquareClippedExplorationRate_pos (arms.card : Real) (horizon : Real) deltaArm (by exact_mod_cast hcard_two) (by exact_mod_cast hhorizon)).le (by exact (bernsteinSquareClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) deltaArm).trans (by norm_num)) loss.environment mu {sample | bernsteinSquareBestArmAllHorizonRegretThreshold arms horizon delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 30

Mathematics ↔ Lean

One all-time failure event for realized EXP3 regret

Lean declarationBanditRLProof.Exp3.measure_sampledRealizedRegretGeometricAllTimeFailureSet_le

Compiled

Plain-English statement. For one generated EXP3 process and one supported comparator, realized selected-loss regret is below the sum of its predictable-regret and sampling-deviation budgets at every positive prefix, except on an event of outer mass at most delta.

Mathematical reading. Formula renderer unavailable; readable fallback: For one generated EXP3 process and one supported comparator, realized selected-loss regret is below the sum of its predictable-regret and sampling-deviation budgets at every positive prefix, except on an event of outer mass at most delta.\(R^{\mathrm{real}}_{n+1}(a)=R^{\mathrm{pred}}_{n+1}(a)+D_{n+1},\qquad \mu(\exists n:\ R^{\mathrm{real}}_{n+1}(a)\ge B^{\mathrm{pred}}_n+B^{\mathrm{dev}}_n)\le\delta.\)

Intuition: Realized regret has two sources: the exponential-weights decision rule can lose against the comparator in predictable loss, and sampled actions can deviate from those predictable losses. If neither component fails, their sum cannot fail.
Why it is needed: This closes the same-process all-positive-prefix realized-regret composition instead of leaving the algorithmic and martingale halves as unrelated confidence statements.
Place in the proof: It is the current fixed-parameter, supported-comparator all-positive-prefix terminal of the EXP3 chapter.

Proof and Lean reading notes

Proof idea: Prove the finite-prefix regret decomposition exactly, allocate delta/2 to each accepted all-time event family, include the combined failure set in their union, apply outer-measure monotonicity and subadditivity, and normalize the two half budgets.
Lean reading notes: The theorem keeps one prior, eta, gamma, loss process, generated trajectory law, and comparator across all prefixes. It does not claim horizon-dependent tuning, best-arm minimization, a sublinear confidence sequence, optional stopping, or ideal EXP3.P.
Teaching dependencies: BanditRLProof.Exp3.sampledTrajectoryRealizedRegret_eq_predictableRegret_add_realizedDeviation, BanditRLProof.Exp3.measure_sampledPredictableRegretGeometricAllTimeFailureSet_le, BanditRLProof.Exp3.measure_sampledRealizedDeviationGeometricAllTimeFailureSet_le

Exact Lean statement

theorem measure_sampledRealizedRegretGeometricAllTimeFailureSet_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu (sampledRealizedRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta) <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 145

Explore 4 additional Lean teaching notes

Mathematics ↔ Lean

For one generated EXP3 trajectory, the event that the selected-loss…

Lean declarationBanditRLProof.Exp3.measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le

Compiled

Plain-English statement. For one generated EXP3 trajectory, the event that the selected-loss deviation crosses its scheduled predictable-variance radius at any positive prefix while that prefix stays within its variance budget has probability at most delta.

Mathematical reading. Formula renderer unavailable; readable fallback: For one generated EXP3 trajectory, the event that the selected-loss deviation crosses its scheduled predictable-variance radius at any positive prefix while that prefix stays within its variance budget has probability at most delta.\(\mu\!\left(\exists n\ge0:\ D_{n+1}\ge r(v_n,\delta/2^{n+1}),\ V_{n+1}\le v_n\right)\le\delta.\)

Intuition: Every positive prefix receives a geometric share of the failure budget. The shares sum exactly to delta, so the countable union of prefix failures remains controlled.
Why it is needed: This supplies an honest all-time event for the realized-versus-predictable EXP3 variance route, while keeping the precise fixed-trajectory and variance-cap assumptions visible.
Place in the proof: It sits above the fixed-prefix exponential tail, the scheduled quadratic union lemma, and the geometric confidence schedule; later regret theorems may consume the resulting all-time event.

Proof and Lean reading notes

Proof idea: Instantiate the generic scheduled-union theorem with unit variance scale and tilt cap, use the generated EXP3 fixed-tilt tail at prefix n+1, and discharge the total budget with the exact ENNReal sum of geometric confidence shares.
Lean reading notes: This is countable outer-measure subadditivity for one generated process. It is not a Ville/Doob maximal inequality, a mixture boundary, optional stopping, a self-normalized theorem, or a general Freedman theorem.
Teaching dependencies: BanditRLProof.Concentration.measure_iUnion_scheduled_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail, BanditRLProof.Concentration.tsum_ofReal_geometricConfidenceShare, BanditRLProof.Exp3.sampledPredictableRealizedDeviation_sum_tail_predictableVariance_fixedTilt

Exact Lean statement

theorem measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (varianceBudget : Nat -> Real) (hvarianceBudget : forall n, 0 < varianceBudget n) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu (sampledPredictableRealizedDeviationAllTimeFailureSet arms eta gamma loss varianceBudget delta) <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 74

Mathematics ↔ Lean

On one generated EXP3 trajectory, realized selected loss minus predictable…

Lean declarationBanditRLProof.Exp3.measure_sampledRealizedDeviationGeometricAllTimeFailureSet_le

Compiled

Plain-English statement. On one generated EXP3 trajectory, realized selected loss minus predictable selected loss stays below its scheduled radius at every positive prefix, except on a failure event of outer mass at most delta.

Mathematical reading. Formula renderer unavailable; readable fallback: On one generated EXP3 trajectory, realized selected loss minus predictable selected loss stays below its scheduled radius at every positive prefix, except on a failure event of outer mass at most delta.\(\mu(\exists n\ge0:\ D_{n+1}\ge r(n+1,\delta/2^{n+1}))\le\delta.\)

Intuition: The selected loss lies in the unit interval, so its one-step centered conditional variance is at most one. Summing that deterministic budget removes the variance-good side condition from the preceding theorem.
Why it is needed: This turns the variance-conditioned all-time deviation statement into the pure realized-versus-predictable deviation event needed by a realized-regret composition.
Place in the proof: It is the second same-process all-positive-prefix node in Chapter 7, above the predictable-variance tail and below the realized-regret terminal.

Proof and Lean reading notes

Proof idea: Prove the centered second moment is at most one, sum the bound through prefix n+1, identify the variance-conditioned event with the pure deviation event under this linear budget, and reuse the accepted geometric all-time tail.
Lean reading notes: The fixed eta, gamma, prior, action type, and predictable loss process are shared by every prefix. This is a countable scheduled-union result, not a Ville/Doob maximal inequality, optional-stopping theorem, or general Freedman boundary.
Teaching dependencies: BanditRLProof.Exp3.selectedLossCenteredSecondMoment_le_one, BanditRLProof.Exp3.sampledPredictableRealizedVariance_sum_le_horizon, BanditRLProof.Exp3.measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le

Exact Lean statement

theorem measure_sampledRealizedDeviationGeometricAllTimeFailureSet_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu (sampledRealizedDeviationGeometricAllTimeFailureSet arms eta gamma loss delta) ≤ ENNReal.ofReal delta

Open in the declaration catalog Open source at line 97

Mathematics ↔ Lean

For one fixed generated EXP3 process and one supported comparator…

Lean declarationBanditRLProof.Exp3.measure_sampledPredictableRegretGeometricAllTimeFailureSet_le

Compiled

Plain-English statement. For one fixed generated EXP3 process and one supported comparator, predictable regret satisfies its scheduled finite-prefix bound simultaneously at every positive prefix outside one geometrically budgeted failure event.

Mathematical reading. Formula renderer unavailable; readable fallback: For one fixed generated EXP3 process and one supported comparator, predictable regret satisfies its scheduled finite-prefix bound simultaneously at every positive prefix outside one geometrically budgeted failure event.\(\mu(\exists n\ge0:\ R^{\mathrm{pred}}_{n+1}(a)\ge B^{\mathrm{pred}}_{n})\le\delta.\)

Intuition: Each finite-prefix potential-and-comparator proof already has a tail bound. Giving prefix n+1 a geometric share makes their countable union affordable without changing the underlying process or comparator.
Why it is needed: Realized regret needs both an algorithmic predictable-regret certificate and a sampling-deviation certificate on the same trajectory. This theorem supplies the first component for every prefix.
Place in the proof: It runs in parallel with the pure realized-deviation node and feeds the Chapter 7 realized-regret terminal.

Proof and Lean reading notes

Proof idea: Specialize the compiled fixed-horizon predictable-regret theorem at n+1, retain its internal two-event confidence split, bound the countable union termwise, and close the total outer budget with the exact geometric ENNReal sum.
Lean reading notes: The comparator must have positive prior support, and eta and gamma stay fixed as n varies. The resulting scheduled budget is not advertised as a horizon-tuned sublinear rate or a best-arm minimum.
Teaching dependencies: BanditRLProof.Exp3.sampledPredictable_highProbabilityRegret_tail_total_delta, BanditRLProof.Concentration.tsum_ofReal_geometricConfidenceShare

Exact Lean statement

theorem measure_sampledPredictableRegretGeometricAllTimeFailureSet_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu (sampledPredictableRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta) <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 70

Mathematics ↔ Lean

Under predictable sparse losses, the probability that best-arm realized…

Lean declarationBanditRLProof.Exp3.sampledPredictable_allHorizonDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_of_sparsityFailure_le

Compiled

Plain-English statement. Under predictable sparse losses, the probability that best-arm realized regret crosses the tuned all-horizon threshold is at most delta plus the supplied sparsity-failure probability.

Mathematical reading. Formula renderer unavailable; readable fallback: Under predictable sparse losses, the probability that best-arm realized regret crosses the tuned all-horizon threshold is at most delta plus the supplied sparsity-failure probability.\(\Pr\{R_T^{\mathrm{real}}\ge b(K,S,T,\delta)\}\le\delta+\varepsilon.\)

Intuition: A variance-sensitive martingale bound handles the regular sparse regime, while a separate event explicitly accounts for violations of the sparsity model.
Why it is needed: Keeping the failure event visible prevents a conditional sparsity assumption from being disguised as an unconditional theorem.
Place in the proof: This is one of the deepest compiled adversarial high-probability endpoints.

Proof and Lean reading notes

Proof idea: Combine double predictable/pathwise variance control, tuned exploration and learning rates, best-arm comparison, an all-horizon tail argument, and monotonicity with the sparsity-failure measure bound.
Lean reading notes: The theorem's let-bound parameters are part of its formal API. The event difference and ENNReal probability arithmetic are visible in the exact statement.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem sampledPredictable_allHorizonDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_of_sparsityFailure_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (by exact_mod_cast hcard_two) (by exact_mod_cast hsparsity) (by exact_mod_cast hhorizon)).le (by exact (doubleVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm).trans (by norm_num)) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal epsilon → mu {sample | doubleVarianceProbabilisticSparseLossBestArmAllHorizonRegretThreshold arms horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta + ENNReal.ofReal epsilon

Open in the declaration catalog Open source at line 275

Maintainer contract

Open the canonical completion definition and blockers

Complete in the canonical adversarial finite-arm scope when the exponential-potential and deterministic Hedge route, positive-support importance weighting, conditional first/second moments, measurable recursive generated trajectory, predictable-loss transport, and exploration bias compile; the same public canary must type (i) the horizon-dependent tuned expected bound, (ii) the horizon-dependent fixed-window best-supported-arm realized tail, (iii) one fixed prior/arms/loss/eta/gamma/comparator process with predictable and realized-deviation parents, exact decomposition, and an all-positive-prefix realized-regret outer-probability terminal, and (iv) the separately labelled sparse/variance-sensitive endpoint with its failure budget explicit.

Remaining blockers

No remaining blocker inside this canonical scope: Tests/BookMapChaptersSevenAndEightCanary.lean gives full-conclusion applications for the tuned expected, per-horizon best-arm, fixed-process all-prefix, and sparse terminals. The items below are explicit extensions rather than hidden chapter requirements.

Chapter implementation status

The compact summary keeps the reading route visible. Open it for source-linked declarations and exact remaining gaps.

Open 7 implementation records7 compiled · 0 partial · 0 blocked · 0 planned

Milestone	Status	Lean declaration	Remaining gap
Tuned expected EXP3 regret	Compiled	`BanditRLProof.Exp3.sampledPredictable_expectedRegret_le_four_mul_sqrt`	—
Per-horizon best-arm realized high-probability EXP3	Compiled	`BanditRLProof.Exp3.sampledPredictable_allHorizonBernsteinSquareBestArmRealizedRegret_tail`	This is not one horizon-free policy with a simultaneous confidence event over all horizons.
All-positive-prefix EXP3 predictable-variance tail	Compiled	`BanditRLProof.Exp3.measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le`	—
All-positive-prefix EXP3 realized-deviation tail	Compiled	`BanditRLProof.Exp3.measure_sampledRealizedDeviationGeometricAllTimeFailureSet_le`	—
All-positive-prefix EXP3 predictable-regret tail	Compiled	`BanditRLProof.Exp3.measure_sampledPredictableRegretGeometricAllTimeFailureSet_le`	—
All-positive-prefix EXP3 realized-regret tail	Compiled	`BanditRLProof.Exp3.sampledTrajectoryRealizedRegret_eq_predictableRegret_add_realizedDeviationBanditRLProof.Exp3.measure_sampledRealizedRegretGeometricAllTimeFailureSet_le`	The process parameters eta and gamma and the comparator are fixed across prefixes. The theorem is not a horizon-varying tuned sublinear all-time guarantee, a best-arm minimum, or an ideal EXP3.P theorem.
Sparse-loss all-horizon high-probability EXP3	Compiled	`BanditRLProof.Exp3.sampledPredictable_allHorizonDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_of_sparsityFailure_le`	—

Open boundaries

The tuned expected and fixed-window best-arm theorems rebuild eta, gamma, and the generated law from the queried horizon; they are not a single horizon-free policy or simultaneous anytime theorem.
The geometric all-prefix theorem instead fixes eta, gamma, prior, arms, loss, and one supported comparator; its scheduled radius is not a tuned sublinear confidence sequence or a best-arm minimum.
Ville/Doob or mixture boundaries, optional stopping, ideal EXP3.P, contextual/delayed EXP3, and one universal theorem subsuming every hypothesis regime remain extensions. The sparse theorem retains its supplied sparsity-failure probability.

All Lean modules in this chapter

Open the complete module list (86 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.Exp3ActionProcess`	14	1	Compiled
`BanditRLProof.Exp3BernsteinAllHorizon`	8	1	Compiled
`BanditRLProof.Exp3BernsteinExplicitTuning`	16	1	Compiled
`BanditRLProof.Exp3BernsteinHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3BernsteinRealizedHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3BernsteinTuning`	12	1	Compiled
`BanditRLProof.Exp3BestArm`	2	1	Compiled
`BanditRLProof.Exp3ComparatorBernstein`	13	2	Compiled
`BanditRLProof.Exp3ComparatorConfidence`	18	1	Compiled
`BanditRLProof.Exp3ConditionalMoments`	9	1	Compiled
`BanditRLProof.Exp3DoubleVarianceSparseBestArmEventualRefinedRegret`	10	1	Compiled
`BanditRLProof.Exp3ExpectedRegret`	11	1	Compiled
`BanditRLProof.Exp3ExplorationBias`	4	1	Compiled
`BanditRLProof.Exp3HedgeRegret`	26	1	Compiled
`BanditRLProof.Exp3HighProbabilityRegret`	6	1	Compiled
`BanditRLProof.Exp3ImportanceWeighted`	12	1	Compiled
`BanditRLProof.Exp3MixedSquareBernstein`	11	3	Compiled
`BanditRLProof.Exp3MixedSquareBernsteinHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3MixedSquareBernsteinRealizedAllHorizon`	3	2	Compiled
`BanditRLProof.Exp3MixedSquareBernsteinRealizedBestArmAllHorizon`	2	2	Compiled
`BanditRLProof.Exp3MixedSquareBernsteinRealizedExplicitTuning`	11	2	Compiled
`BanditRLProof.Exp3MixedSquareBernsteinRealizedHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3MixedSquareBernsteinRealizedTuning`	9	1	Compiled
`BanditRLProof.Exp3MixedSquareConfidence`	24	1	Compiled
`BanditRLProof.Exp3MixedSquareExponentialHighProbabilityRegret`	3	1	Compiled
`BanditRLProof.Exp3MixedSquareExponentialRealizedAllHorizon`	3	2	Compiled
`BanditRLProof.Exp3MixedSquareExponentialRealizedExplicitTuning`	19	2	Compiled
`BanditRLProof.Exp3MixedSquareExponentialRealizedHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3MixedSquareExponentialRealizedTuning`	9	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVariance`	19	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceHighProbabilityRegret`	6	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceLossEnergyRealizedMarkovHighProbabilityRegret`	7	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceRealizedDoublePredictableVarianceHighProbabilityRegret`	2	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceRealizedHighProbabilityRegret`	5	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceRealizedMarkovHighProbabilityRegret`	8	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedDoublePredictableVarianceHighProbabilityRegret`	2	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedMarkovHighProbabilityRegret`	19	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsity`	6	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityAllHorizon`	5	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityBestArmAllHorizon`	4	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityExplicitTuning`	19	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityTuning`	5	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovAESparsityAllHorizon`	1	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovAllHorizon`	3	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovExplicitTuning`	22	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovHighProbabilityRegret`	7	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsity`	8	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityAllHorizon`	4	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityExplicitTuning`	18	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityTuning`	12	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovTuning`	11	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsity`	6	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityAllHorizon`	5	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityBestArmAllHorizon`	6	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityExplicitTuning`	20	2	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityTuning`	11	1	Compiled
`BanditRLProof.Exp3MixedSquarePredictableVarianceTail`	12	1	Compiled
`BanditRLProof.Exp3Potential`	10	0	Compiled
`BanditRLProof.Exp3PredictableAdversary`	8	1	Compiled
`BanditRLProof.Exp3PredictableHedge`	4	1	Compiled
`BanditRLProof.Exp3PredictableIntegration`	22	1	Compiled
`BanditRLProof.Exp3PredictableMoments`	33	2	Compiled
`BanditRLProof.Exp3PredictableRegretAllTime`	4	2	Compiled
`BanditRLProof.Exp3PureBernstein`	12	2	Compiled
`BanditRLProof.Exp3PureConfidence`	25	1	Compiled
`BanditRLProof.Exp3RandomSquareBernsteinRealizedAllHorizon`	3	2	Compiled
`BanditRLProof.Exp3RandomSquareBernsteinRealizedExplicitTuning`	15	2	Compiled
`BanditRLProof.Exp3RandomSquareBernsteinRealizedHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3RandomSquareBernsteinRealizedTuning`	7	2	Compiled
`BanditRLProof.Exp3RandomSquareHighProbabilityRegret`	9	2	Compiled
`BanditRLProof.Exp3RealizedConcentration`	6	3	Compiled
`BanditRLProof.Exp3RealizedConfidence`	6	1	Compiled
`BanditRLProof.Exp3RealizedDeviationAllTime`	7	1	Compiled
`BanditRLProof.Exp3RealizedDeviationTail`	11	1	Compiled
`BanditRLProof.Exp3RealizedHighProbabilityRegret`	3	2	Compiled
`BanditRLProof.Exp3RealizedPredictableVariance`	23	1	Compiled
`BanditRLProof.Exp3RealizedPredictableVarianceAllTime`	4	3	Compiled
`BanditRLProof.Exp3RealizedPredictableVarianceMaximal`	2	2	Compiled
`BanditRLProof.Exp3RealizedPredictableVarianceTail`	6	1	Compiled
`BanditRLProof.Exp3RealizedRegret`	12	1	Compiled
`BanditRLProof.Exp3RealizedRegretAllTime`	6	2	Compiled
`BanditRLProof.Exp3RecursiveTrajectory`	25	2	Compiled
`BanditRLProof.Exp3SampledHedge`	9	1	Compiled
`BanditRLProof.Exp3SampledHistoryScore`	14	1	Compiled
`BanditRLProof.Exp3ScoreRegularity`	20	1	Compiled
`BanditRLProof.Exp3UniformRegret`	9	1	Compiled