7. EXP3 and adversarial concentration

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.

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 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.

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)

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.

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 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

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)

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.

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 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

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

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.

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 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

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

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.

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 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

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

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.

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 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

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

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.

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 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

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

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.

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 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.

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