Bandit Algorithms
Tor Lattimore and Csaba Szepesvári
- Location
- Ch. 2, Ch. 3, and Ch. 5
- Pages
- online pp. 18–42, 46–54, and 74–81
Teaching chapter 02 of 10 · Canonical route compiled
2. Probability, kernels, filtrations, and concentration
Measure-theoretic infrastructure for generated histories, conditional reward laws, martingale differences, posterior kernels, stopping times, and concentration.
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 after Foundations; familiarity with conditional expectation helps but is not required.
Learning goals
- See why policies and history selectors must be measurable maps.
- Separate a marginal reward distribution from a history-conditioned kernel law.
- Track adaptedness, integrability, finite-measure, and variance-proxy assumptions explicitly.
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.
proof flow · ordered flow
A reusable confidence-event route
Read top to bottom: each step supplies the state or proof fact used by the next one.
- Model conditional noise
State a conditional MGF or bounded-reward assumption on the generated history.
- Derive one tail bound
Convert the MGF bound into a deviation probability at a fixed index.
- Allocate confidence
Assign a finite, geometric, or telescoping share δ_i to every arm and time.
- Join the events
Use a union bound to obtain one good event consumed by an algorithm proof.
Source theorem · faithful restatement
Original at online pp. 77–78 ↗Corollary 5.5 (sub-Gaussian tail)
The fixed-index tail estimate is the mathematical atom from which finite and all-time confidence schedules are assembled.
- Model
- A real-valued random variable X on a probability space.
- Assumptions
- X is centered and σ-sub-Gaussian in the moment-generating-function sense; the deviation ε is nonnegative.
- Algorithm parameters
- Sub-Gaussian scale σ and deviation threshold ε.
- Regret notion
- Not a regret theorem; this is a one-sided concentration primitive consumed by later regret proofs.
- Guarantee
- The upper-tail probability is at most exp(-ε²/(2σ²)).
Source mathematical statement. A centered sub-Gaussian variable has an exponentially small upper-tail probability.
BanditRLlib relationship. The local library adds measure, kernel, filtration, conditional-law, finite-index, and countable-all-time adapters needed by generated bandit trajectories.
The mathematical content is restated in this site's notation; wording is ours. See online pp. 77–78 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
Compiled
Measurable policies define legitimate random actions
Lean declarationBandit
Plain-English statement. A policy is an action-valued function of a state together with proof that this function is measurable.
Mathematical reading. A policy is an action-valued function of a state together with proof that this function is measurable.
- Intuition
- An algorithmic formula is not enough for a probability theorem: the selected action must be a legitimate random variable.
- Why it is needed
- Generated trajectories, conditional distributions, filtrations, and expected regret all depend on policy measurability.
- Place in the proof
- This structure is the interface from deterministic state computation to probability-kernel construction.
Proof and Lean reading notes
- Proof idea
- The structure stores the action function and its measurability proof. Composition lemmas then obtain measurable actions from measurable states.
- Lean reading notes
- Measurable spaces are typeclass arguments. The structure makes the regularity contract explicit instead of relying on an informal claim that the policy is well behaved.
- Teaching dependencies
- No direct teaching dependency recorded.
Exact Lean statement
structure MeasurablePolicy (State : Type u) (Action : Type v) [MeasurableSpace State] [MeasurableSpace Action] whereMathematics ↔ Lean
Compiled
Conditional sub-Gaussian rewards on the generated trajectory
Lean declarationBandit
Plain-English statement. On the canonical trajectory generated by a measurable history step-kernel family, the selected centered successor reward has the promised conditional sub-Gaussian MGF.
Mathematical reading. On the canonical trajectory generated by a measurable history step-kernel family, the selected centered successor reward has the promised conditional sub-Gaussian MGF.
- Intuition
- The theorem closes the gap between a one-step kernel law and the random reward actually observed on the recursively generated path.
- Why it is needed
- UCB, ETC, and adversarial high-probability routes need conditional concentration on the same measure that generates the policy history.
- Place in the proof
- It is a reusable law-transport endpoint in the conditional-reward layer.
Proof and Lean reading notes
- Proof idea
- Identify the conditional kernel of the successor reward under trajMeasure, center the selected law by its declared mean, and reuse the kernel-level conditional-MGF contract.
- Lean reading notes
- The long name records the transport path. The exact Lean statement below is the authoritative list of measurable-space, kernel, mean, and proxy hypotheses.
- Teaching dependencies
BanditRLProof.Policy.MeasurablePolicy
Exact Lean statement
theorem historyStepKernelFamily_centeredReward_succ_hasCondSubgaussianMGF_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure Rat) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (defaultAction : Action) (i : Nat) (c : NNReal) (hvariance : forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= c) : let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) mu0 stepKernel let reward : RewardTrace Rat -> RewardTrace Rat := fun trajectory => trajectory let hreward : forall t : Nat, Measurable (fun trajectory : RewardTrace Rat => reward trajectory t)Mathematics ↔ Lean
Compiled
One confidence budget across every arm and time
Lean declarationBandit
Plain-English statement. A geometric budget over all times can be shared equally across every member of one nonempty finite index type while preserving the total outer confidence budget.
Mathematical reading. A geometric budget over all times can be shared equally across every member of one nonempty finite index type while preserving the total outer confidence budget.
- Intuition
- Use a finite union bound across arms or contexts at each time, then a summable geometric schedule across all times.
- Why it is needed
- ETC and UCB confidence arguments repeatedly need simultaneous control over a finite family and more than one horizon; this theorem packages only that reusable bookkeeping step.
- Place in the proof
- It joins the finite outer-union wrapper to the geometric confidence schedule in Chapter 2, before any algorithm-specific tail producer.
Proof and Lean reading notes
- Proof idea
- Apply countable outer-measure subadditivity over time, invoke the compiled equal-share finite-union theorem at each time, compare the ENNReal series termwise, and rewrite the exact geometric total.
- Lean reading notes
- The exact statement assumes only a measurable ambient space, a nonempty Fintype index, nonnegative delta, and the pointwise outer-measure bounds. It does not require event measurability, a probability measure, independence, filtration, or a concentration producer.
- Teaching dependencies
BanditRLProof.ProbabilityUnionBound.measure_biUnion_finset_le_of_uniform,BanditRLProof.Concentration.tsum_ofReal_geometricConfidenceShare
Exact Lean statement
theorem measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare {Omega : Type u} {Idx : Type v} [MeasurableSpace Omega] [Fintype Idx] [Nonempty Idx] (mu : Measure Omega) (bad : Nat -> Idx -> Set Omega) (delta : Real) (hdelta : 0 <= delta) (hbad : forall n i, mu (bad n i) <= ENNReal.ofReal (geometricConfidenceShare delta n / (Fintype.card Idx : Real))) : mu (⋃ n, ⋃ i, bad n i) <= ENNReal.ofReal deltaMathematics ↔ Lean
Compiled
Simultaneous empirical-mean confidence for every arm and horizon
Lean declarationBandit
Plain-English statement. One canonical generated action/reward trajectory satisfies the existing random-pull-count empirical-mean confidence radius simultaneously for every finite arm and every positive successor horizon, outside one geometrically budgeted failure event.
Mathematical reading. One canonical generated action/reward trajectory satisfies the existing random-pull-count empirical-mean confidence radius simultaneously for every finite arm and every positive successor horizon, outside one geometrically budgeted failure event.
- Intuition
- The fixed-arm tail already adapts to the random number of pulls inside a fixed horizon. This theorem keeps the generated law fixed, shares each time budget across all arms, and then sums the geometric schedule over all horizons.
- Why it is needed
- It closes the gap between generic confidence-budget bookkeeping and a real finite-arm trajectory-level empirical-mean event needed by UCB-facing work.
- Place in the proof
- It sits above the canonical random-pull-count tail and finite-index geometric union, and below any UCB score-selection or regret consumer.
Proof and Lean reading notes
- Proof idea
- At each pair (n, arm), instantiate the compiled canonical tail at horizon n+1 and confidence share delta_n divided by the arm count; then apply the accepted finite-index geometric all-time union to the identical trajectory measure.
- Lean reading notes
- The theorem requires a probability initial pair law, measurable generated context/state, a centered reward-kernel law, a global selected-history variance ceiling, stationary per-arm means, and positive sigma2 and delta. It assumes neither event measurability nor delta at most one, and it proves no maximal inequality or UCB regret bound.
- Teaching dependencies
BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_trajMeasure_on_horizon,BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare
Exact Lean statement
theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_geometricAllTime_abs_tail_ennreal_delta_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Fintype Action] [Nonempty Action] [DecidableEq Action] (mu0 : Measure (Prod Action Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (armMean : Action -> Rat) (sigma2 : NNReal) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Action, mean (context i history) arm = armMean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> ContextExplore 4 additional Lean teaching notes
Mathematics ↔ Lean
Compiled
One canonical generated action/reward trajectory satisfies the…
Lean declarationBandit
Plain-English statement. One canonical generated action/reward trajectory satisfies the random-pull-count empirical-mean confidence radius for every finite arm and every positive successor horizon under a telescoping confidence schedule.
Mathematical reading. One canonical generated action/reward trajectory satisfies the random-pull-count empirical-mean confidence radius for every finite arm and every positive successor horizon under a telescoping confidence schedule.
- Intuition
- The shares telescope exactly to delta while their reciprocal grows only polynomially, so logarithmic radii retain logarithmic time growth instead of the linear growth caused by geometric shares.
- Why it is needed
- This supplies the confidence schedule now consumed by the fixed-policy ordinary-UCB route on the canonical Rat trajectory.
- Place in the proof
- It sits above the fixed-horizon random-count tail and directly below the compiled same-source scheduled UCB score, policy, all-horizon count, and finite-time expected-regret consumers.
Proof and Lean reading notes
- Proof idea
- Prove the reciprocal telescope, convert its exact Real HasSum to ENNReal, share each time budget across the finite arm type, instantiate the accepted fixed-horizon tail at n+1, and apply countable outer-measure subadditivity without changing trajMeasure.
- Lean reading notes
- The theorem retains the same probability, measurability, centered-kernel, stationary-mean, variance-ceiling, and positivity contracts as the geometric producer. It adds no independence, event-measurability, optional-stopping, or delta-at-most-one premise.
- Teaching dependencies
BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_trajMeasure_on_horizon,BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_telescopingConfidenceShare
Exact Lean statement
theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Fintype Action] [Nonempty Action] [DecidableEq Action] (mu0 : Measure (Prod Action Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (armMean : Action -> Rat) (sigma2 : NNReal) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Action, mean (context i history) arm = armMean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> ContextMathematics ↔ Lean
Compiled
If the joint law of environment and history is the canonical…
Lean declarationBandit
Plain-English statement. If the joint law of environment and history is the canonical prior-likelihood law, the canonical posterior kernel agrees almost everywhere with the conditional distribution of the environment given history.
Mathematical reading. If the joint law of environment and history is the canonical prior-likelihood law, the canonical posterior kernel agrees almost everywhere with the conditional distribution of the environment given history.
- Intuition
- Bayes' posterior and measure-theoretic conditional distribution are two descriptions of the same object once their joint law is identified.
- Why it is needed
- Thompson sampling needs to replace a reference posterior sampler by the actual conditional environment law along a generated history.
- Place in the proof
- This theorem is the principal posterior-law transport in the Thompson proof DAG.
Proof and Lean reading notes
- Proof idea
- Rewrite the supplied pair pushforward as the canonical joint measure and use Mathlib's posterior/conditional-distribution identity, transporting the almost-everywhere statement along the history marginal.
- Lean reading notes
- The conclusion is kernel equality almost everywhere, not pointwise equality. Standard Borel and finiteness hypotheses make conditional distributions available.
- Teaching dependencies
- No direct teaching dependency recorded.
Exact Lean statement
theorem canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq {Omega : Type*} [MeasurableSpace Omega] [StandardBorelSpace Env] [Nonempty Env] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (hpair : mu.map (fun omega => (env omega, history omega)) = canonicalJointMeasure prior likelihood) : (canonicalPosterior prior likelihood).kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history muMathematics ↔ Lean
Compiled
The partial sums of an adapted integrable successor-indexed…
Lean declarationBandit
Plain-English statement. The partial sums of an adapted integrable successor-indexed martingale-difference sequence form a martingale.
Mathematical reading. The partial sums of an adapted integrable successor-indexed martingale-difference sequence form a martingale.
- Intuition
- Zero conditional drift is exactly the local condition needed for cumulative noise to have no predictable trend.
- Why it is needed
- Concentration and optional-stopping arguments reason about cumulative centered reward, not isolated one-step rewards.
- Place in the proof
- This theorem converts conditional reward-law work into Mathlib's martingale API.
Proof and Lean reading notes
- Proof idea
- Use the witness fields for strong adaptedness, integrability, and zero conditional expectation; unfold the successor partial sum and verify the martingale conditional-expectation equation.
- Lean reading notes
- The packaged witness prevents measurability and integrability assumptions from disappearing inside a tactic proof.
- Teaching dependencies
- No direct teaching dependency recorded.
Exact Lean statement
theorem martingale_partialSumsSucc_of_succMartingaleDifference {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) : Martingale (partialSumsSucc Y) F muMathematics ↔ Lean
Compiled
A countable family of deviation events, each controlled by its own…
Lean declarationBandit
Plain-English statement. A countable family of deviation events, each controlled by its own fixed-MGF quadratic tail and confidence share, has total outer probability at most the supplied overall budget.
Mathematical reading. A countable family of deviation events, each controlled by its own fixed-MGF quadratic tail and confidence share, has total outer probability at most the supplied overall budget.
- Intuition
- Spend a small part of the confidence budget at each index, prove the corresponding one-event tail, and add the possible failures. Countable subadditivity is enough; the events need not form a martingale stopping argument.
- Why it is needed
- Many all-time algorithm statements need one event covering every deterministic prefix. This theorem turns a reusable fixed-index MGF bound into such a scheduled union without overstating it as Ville, Doob, mixture, optional-stopping, or general Freedman theory.
- Place in the proof
- It is the generic probability bridge consumed by the new all-positive-prefix EXP3 predictable-variance theorem.
Proof and Lean reading notes
- Proof idea
- Apply the measure-of-countable-union upper bound, instantiate the optimized one-event quadratic fixed-MGF theorem at every index, compare termwise ENNReal bounds, and finish with the caller's total confidence-budget inequality.
- Lean reading notes
- The conclusion is an outer-measure inequality, so event measurability is not assumed. Positivity of every scale, variance budget, tilt cap, and confidence share is explicit in the signature.
- Teaching dependencies
BanditRLProof.Concentration.measure_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail
Exact Lean statement
theorem measure_iUnion_scheduled_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) (deviation predictableVariance : Nat -> Omega -> Real) (varianceScale varianceBudget tiltCap deltaAt : Nat -> Real) (delta : Real) (hvarianceScale : forall n, 0 < varianceScale n) (hvarianceBudget : forall n, 0 < varianceBudget n) (htiltCap : forall n, 0 < tiltCap n) (hdeltaAt : forall n, 0 < deltaAt n) (hfixed : forall n tilt, 0 <= tilt -> tilt <= tiltCap n -> mu {omega | quadraticFixedMGFScheduledRadius varianceScale varianceBudget tiltCap deltaAt n <= deviation n omega ∧ predictableVariance n omega <= varianceBudget n} <= ENNReal.ofReal (Real.exp (-tilt * quadraticFixedMGFScheduledRadius varianceScale varianceBudget tiltCap deltaAt n + varianceScale n * (tilt ^ 2 * varianceBudget n)))) (hbudget : (∑' n, ENNReal.ofReal (deltaAt n)) <= ENNReal.ofReal delta) : mu (⋃ n, {omega | quadraticFixedMGFScheduledRadius varianceScale varianceBudget tiltCap deltaAt n <= deviation n omega ∧ predictableVariance n omega <= varianceBudget n}) <= ENNReal.ofReal deltaMaintainer contract
Open the canonical completion definition and blockers
Complete within the Book Map scope when the reusable measure, kernel, filtration, conditional-law, finite-time concentration, and finite/countable all-time confidence-budget adapters required by canonical generated ETC and ordinary-UCB routes compile with explicit regularity contracts. The telescoping all-time producer must remain on the same canonical trajectory when consumed by the fixed-policy UCB extension. Self-normalized and RL-specific confidence remain separate chapters or extensions.
Remaining blockers
- No remaining blocker inside the scoped ETC/ordinary-UCB dependency surface: the finite-arm/time event feeds the horizon-indexed family, while the telescoping all-time event now feeds a horizon-free scheduled UCB policy on the same canonical trajectory through all-horizon pull counts and finite-time expected regret.
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 |
|---|---|---|---|
| Sample-index truncated confidence with source radius four | Compiled | — | |
| Generated-history conditional sub-Gaussian reward law | Compiled | — | |
| Finite-index geometric all-time confidence union | Compiled | Each ETC, UCB, or RL consumer must still supply its per-time, per-index tail events and model-specific law assumptions. | |
| Generated finite-arm empirical-mean all-time confidence | Compiled | The ordinary-UCB chapter uses its exact finite-arm/time confidence producer. A fixed-policy anytime UCB consumer for this stronger geometric event remains a separate extension. | |
| Generated finite-arm telescoping all-time empirical-mean confidence | Compiled | — | |
| Probability interfaces used by canonical ETC and ordinary UCB | Compiled | BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_generatedActionPartialTrajectoryPairLawSource_trajMeasureBanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_centeredReward_succ_hasCondSubgaussianMGF_trajMeasureBanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_finiteArmTime_abs_tail_ennreal_delta_trajMeasure | — |
| Countable scheduled quadratic fixed-MGF tail | Compiled | — |
Open boundaries
- The telescoping all-time empirical-mean producer now has an explicit same-source fixed-policy UCB consumer; the geometric producer remains confidence infrastructure rather than the logarithmic scheduled-regret route.
- There is intentionally no single producer for every adaptive environment or every fixed-policy anytime algorithm.
- Self-normalized and RL-specific concentration remain explicit downstream theorem routes rather than one universal wrapper.