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

Teaching chapter 08 of 10 · Canonical route compiled

8. Tsallis-FTRL, corruption, and nonstationarity

The scoped canonical half-Tsallis FTRL route compiles from finite-simplex minimizers and one-step stability through a measurable scheduled generated trajectory, score alignment, expected self-bounding, and a finite-arm IID bounded reward-law logarithmic regret terminal; corruption and nonstationary routes remain labelled extensions.

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. This is one of the longest routes; read EXP3 and the Probability layer first.

Learning goals

Separate deterministic FTRL stability from stochastic law transport.
Use expected action probabilities and gap self-bounds to obtain logarithmic or corruption-sensitive regret.
Follow the now-compiled generated oracle-restart law while preserving its full-information change-point assumption.

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. 28 (FTRL and mirror-descent foundation)
Pages: online pp. 327–344

Open at the cited pages

Algorithm-specific companion

Tsallis-INF: An Optimal Algorithm for Stochastic and Adversarial Bandits

Julian Zimmert and Yevgeny Seldin

Location: Algorithm 1 and Theorem 1
Pages: paper pp. 7–13

Open at the cited pages

algorithm · ordered flow

Half-Tsallis FTRL update

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

Estimate bandit losses
Construct an importance-weighted or reduced-variance estimate from the selected arm.
Accumulate the estimate
Add the new estimate to the running loss vector.
Regularize with half-Tsallis entropy
Choose the next distribution by minimizing estimated loss plus the scheduled Tsallis potential.
Sample and adapt
Draw the next arm and update the learning-rate schedule; specialized theorems then add self-bounding, corruption, drift, or restart assumptions.

Algorithm · explicit conventions

Half-Tsallis FTRL / Tsallis-INF core

This compact route shows where the regularizer, loss estimator, and round-dependent learning rate meet; estimator-specific corrections remain explicit.

Regularized decision and bandit estimate. Formula renderer unavailable; readable fallback: Choose the simplex distribution minimizing cumulative estimated loss plus the scheduled half-Tsallis regularizer, then form the stated bandit loss estimate from the sampled arm.\[p_t\in\operatorname*{arg\,min}_{p\in\Delta_K}\left\{\langle\widehat L_{t-1},p\rangle+\Psi_t(p)\right\},\qquad \widehat\ell_t(a)=\frac{\ell_t(A_t)\mathbf 1\{A_t=a\}}{p_t(a)}.\]

input: K arms, half-Tsallis regularizer Ψ_t, schedule η_t, estimator variant
initialize cumulative estimated loss L̂_0 = 0
for t = 1,…,T:
    choose p_t by the regularized FTRL minimization over the simplex
    sample A_t ~ p_t; observe the selected loss and form the declared estimator ℓ̂_t
    set L̂_t = L̂_{t-1} + ℓ̂_t and advance the learning-rate schedule

Source/Lean boundary. The source paper distinguishes importance-weighted and reduced-variance estimators. BanditRLlib compiles a scheduled half-Tsallis route plus IID, corrupted, drifting, and oracle-restart consumers; these source-aligned local theorems do not claim every paper-sharp regime verbatim.

Worked example · follow one decision

See estimator noise and gap credit in one round

At one two-arm round, suppose the FTRL distribution is p = (0.25, 0.75), arm 1 is sampled, and its observed loss is 0.5. The arithmetic exposes the two quantities that the regularizer must reconcile.

Importance-weight the observed coordinate
Only arm 1 is observed, so its loss is divided by the probability with which it was sampled.
Worked example step 1. Formula renderer unavailable; readable fallback: Arm 1 is sampled with probability 0.25 and loss 0.5, producing estimated loss vector (2, 0).\[A_t=1,\quad \ell_t(A_t)=0.5,\qquad \widehat\ell_t=(0.5/0.25,0)=(2,0).\]
Notice the rare-arm variance cost
A small sampling probability makes the realized estimate large; its conditional second moment carries the inverse-probability geometry.
Worked example step 2. Formula renderer unavailable; readable fallback: The conditional second moment of arm 1's importance-weighted estimate is 0.25 divided by 0.25, which equals 1.\[\mathbb E_t[\widehat\ell_t(1)^2]=\frac{0.5^2}{0.25}=1.\]
Compare the stochastic gap credit
If arm 2 is optimal and arm 1 has mean-loss gap 0.2, the same probability mass contributes a smaller but structured self-bounding term.
Worked example step 3. Formula renderer unavailable; readable fallback: With gap 0.2, sampling arm 1 with probability 0.25 contributes instantaneous expected gap cost 0.05.\[\Delta_1p_t(1)=0.2\cdot0.25=0.05.\]

Takeaway. The estimator creates an inverse-probability noise charge, while stochastic gaps price suboptimal probability mass. Half-Tsallis curvature is useful because its stability geometry can connect these two scales.

Scope. This is a one-round calculation, not a derivation of Tsallis-INF or a compiled general curvature-noise-gap calculus. The theorem cards below remain authoritative for schedules, estimators, constants, and regimes.

Proof bridge · source to Lean

Where curvature, estimator noise, and stochastic gaps meet

Tsallis-INF is useful as a reading lens because its guarantee is assembled from three interacting ingredients rather than from the regularizer alone.

Let curvature control stability
Schematically, the FTRL regularizer determines how much the chosen distribution can move when one more estimated loss vector is added.
Step 1 equation. Formula renderer unavailable; readable fallback: One-step FTRL stability is controlled by the regularizer's local inverse curvature.\[\operatorname{stab}_t\lesssim\left\langle\widehat\ell_t,(\nabla^2\Psi_t)^{-1}\widehat\ell_t\right\rangle.\]
Match curvature to bandit noise
The estimator contributes probability-dependent variance, so the useful curvature is the one that absorbs the same rare-arm geometry.
Step 2 equation. Formula renderer unavailable; readable fallback: The estimated loss second moment grows like the squared loss divided by the arm's sampling probability.\[\mathbb E_t[\widehat\ell_t(a)^2]\asymp\frac{\ell_t(a)^2}{p_t(a)}.\]
Add stochastic self-bounding when available
In an IID gap model, expected regret also lower-bounds the probability mass assigned to suboptimal arms; this can repay part of the stability cost.
Step 3 equation. Formula renderer unavailable; readable fallback: Stochastic regret equals the sum over rounds and suboptimal arms of gap times expected sampling probability.\[Reg_T=\sum_{t=1}^{T}\sum_{a\ne a^\star}\Delta_a\,\mathbb E[p_t(a)].\]
Choose the regime-specific consumer
The adversarial analysis keeps the stability charge, while stochastic, corrupted, drifting, and restart results add distinct assumptions to sharpen or reorganize it.
Step 4 equation. Formula renderer unavailable; readable fallback: Curvature, estimator noise, and a stated self-bounding or drift contract combine only within a particular regret theorem.\[\begin{gathered}\mathcal C+\mathcal V-\mathcal G\Longrightarrow Reg_T\text{ bound},\\ \mathcal C=\text{curvature},\quad\mathcal V=\text{noise},\quad\mathcal G=\text{gap credit}.\end{gathered}\]

Reading boundary. This motif is a teaching organization of existing proof routes, not a compiled general curvature-noise-gap calculus. The source theorem cards and each Lean declaration remain authoritative for which coupling has actually been proved.

Source theorem · faithful restatement

Zimmert–Seldin, Theorem 1 (adversarial regime)

Original at paper p. 9 ↗

The half-Tsallis regularizer is designed to retain adversarial robustness while adapting sharply to stochastic self-bounding structure.

Model: Any adversarial K-armed bandit problem in the paper's loss-based protocol.
Assumptions: Tsallis-INF uses α = 1/2, symmetric regularization, and either the importance-weighted or reduced-variance estimator specified in the paper.
Algorithm parameters: Horizon T, arm count K, and schedule η_t = 2/√t for IW or 4/√t for RV.
Regret notion: Adversarial pseudo-regret Reg_T.
Guarantee: The IW route gives 4√(KT)+1; the RV route gives 2√(KT)+10K log T+16.

Source mathematical statement. Formula renderer unavailable; readable fallback: The source theorem gives explicit adversarial square-root regret bounds for importance-weighted and reduced-variance Tsallis-INF variants.\[Reg_T\le4\sqrt{KT}+1\quad\text{(importance weighting)},\qquad Reg_T\le2\sqrt{KT}+10K\log T+16\quad\text{(reduced variance)}.\]

BanditRLlib relationship. BanditRLlib proves a scheduled half-Tsallis route and several IID, corrupted, drifting, and oracle-restart consumers. These are source-aligned local theorems, not a claim that every sharp paper regime has been reproduced verbatim.

The mathematical content is restated in this site's notation; wording is ours. See paper p. 9 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. 5 additional dependency, extension, or research-frontier notes are grouped below.

Mathematics ↔ Lean

All-rate stability for scheduled half-Tsallis FTRL

Lean declarationBanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_allRateBound

Compiled

Plain-English statement. On the canonical scheduled half-Tsallis generated trajectory, expected predictable-environment regret to a supported arm is bounded by the integrated all-rate stability budget plus the exact time-varying potential penalty.

Mathematical reading. Formula renderer unavailable; readable fallback: On the canonical scheduled half-Tsallis generated trajectory, expected predictable-environment regret to a supported arm is bounded by the integrated all-rate stability budget plus the exact time-varying potential penalty.\(\mathbb E R_{0:n}(a^\star)\le\mathbb E\sum_{t=0}^{n}B_t^{\mathrm{stab}}+\Psi(p_0)/\eta_n-1/\eta_n.\)

Intuition: The deterministic FTRL decomposition already separates stability from regularizer drift; the generated conditional action law turns its importance-weighted scores into the true predictable loss regret.
Why it is needed: It is the algorithm-and-law bridge between measurable generated sampling and the later stochastic self-bounding/logarithmic consumers.
Place in the proof: It follows scheduled score alignment and all-rate expected stability, and precedes fixed-gap self-bounding and the finite-arm IID reward-law terminal.

Proof and Lean reading notes

Proof idea: Use the same selector and trajectory measure throughout, identify observed and predictable importance-weighted losses almost everywhere, integrate the pathwise stability-plus-penalty inequality, and dominate each stability term by its refined-or-coarse all-rate bound.
Lean reading notes: The signature retains a probability prior, Standard Borel measurable action/environment contracts, finite nonempty decidable arms, one predictable [0,1] loss vector, a supported comparator, a positive schedule through the horizon, and schedule monotonicity. It is expected predictable regret, not a high-probability, realized, or paper-sharp Tsallis-INF theorem.
Teaching dependencies: BanditRLProof.Tsallis.sampledScheduledHalfTsallisEstimatedRegret_pointMass_le_stability_add_penalty, BanditRLProof.Tsallis.integral_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime_le_allRateBound, BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisEstimatedRegret_eq_environmentRegret

Exact Lean statement

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_allRateBound {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) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (heta : forall t, t <= horizon -> 0 < eta t) (hetaMono : forall t, t < horizon -> eta (t + 1) <= eta t) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) <= integral mu (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)) + halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (eta 0)) / eta horizon - 1 / eta horizon

Open in the declaration catalog Open source at line 648

Mathematics ↔ Lean

Logarithmic stochastic regret for half-Tsallis FTRL

Lean declarationBanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIIDRewardLawRegret_le_log

Compiled

Plain-English statement. For independent IID finite-arm reward laws with exact model means and positive non-best gaps, scheduled half-Tsallis FTRL has a logarithmic expected-regret bound in reciprocal gaps.

Mathematical reading. Formula renderer unavailable; readable fallback: For independent IID finite-arm reward laws with exact model means and positive non-best gaps, scheduled half-Tsallis FTRL has a logarithmic expected-regret bound in reciprocal gaps.\(\mathbb E R_T\le(1+\log(T+1))\left(1+25\sum_{a\ne a^\star}\Delta_a^{-1}\right)+C.\)

Intuition: The stochastic gap law makes the algorithm's own action probabilities pay for regret, and the half-Tsallis schedule converts that self-bound into logarithmic growth.
Why it is needed: This is a model-facing stochastic Tsallis endpoint with no caller-supplied trajectory identification.
Place in the proof: It is the canonical Chapter 8 terminal and the base law theorem reused by corruption and nonstationary extensions.

Proof and Lean reading notes

Proof idea: Build the infinite IID product of finite reward vectors, use the same measurable scheduled selector and trajectory kernel as the stability theorem, prove exact clipped-reward mean and gap transport, apply fixed-gap self-bounding, and close the square-root schedule by the harmonic/logarithmic optimization.
Lean reading notes: The finite model has positive arm count. Every arm law is a probability measure with a.e. [0,1] support and the exact supplied model mean; every non-best gap is positive. The horizon and nonnegative additive corruption allowance are explicit, and the canonical uncorrupted case sets it to zero. This is expected generated-trajectory regret, not paper-sharp, high-probability, realized, or complete best-of-both-worlds Tsallis-INF.
Teaching dependencies: BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_log_iidLossState, BanditRLProof.Tsallis.iidLossStateMeanGap_finiteArmIIDRewardVectorLoss_eq_gap

Exact Lean statement

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDRewardLawRegret_le_log {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) (corruption : Real) (hcorruption : 0 <= corruption) : letI : Nonempty (Fin K)

Open in the declaration catalog Open source at line 160

Explore 5 additional Lean teaching notes

Mathematics ↔ Lean

For a measurable pre-action-history corruption model controlled in…

Lean declarationBanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLawRegret_le_allRegimes

Compiled

Plain-English statement. For a measurable pre-action-history corruption model controlled in conditional expectation, the theorem automatically selects a refined local or logarithmic regret bound across all regimes.

Mathematical reading. Formula renderer unavailable; readable fallback: For a measurable pre-action-history corruption model controlled in conditional expectation, the theorem automatically selects a refined local or logarithmic regret bound across all regimes.\(\mathbb E R_T\le\begin{cases}\text{refined }\sqrt{CS}\text{ expression},&\text{inside the certified window},\\\text{logarithmic bound}+C,&\text{otherwise.}\end{cases}\)

Intuition: Predictable corruption may react to the past, but not to the current random action. The theorem keeps that information pattern formal and lets the bound adapt to the corruption scale.
Why it is needed: It closes a substantially more realistic corruption route than a fixed deterministic shift.
Place in the proof: This result lies above IID law construction, predictable loss measurability, self-bounding interpolation, and refined scalar optimization.

Proof and Lean reading notes

Proof idea: Construct the actual and reference predictable laws on the same trajectory, bound their gap difference in conditional expectation, derive the exact corruption budget, and invoke the all-regimes optimizer.
Lean reading notes: Current-action corruption, latent-law changes, and expectation-only contracts outside the stated filtration remain separate problems.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLawRegret_le_allRegimes {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (hgapLeOne : forall arm, arm ≠ model.bestArm -> ((model.gap arm : Rat) : Real) <= 1) (horizon : Nat) : letI : Nonempty (Fin K)

Open in the declaration catalog Open source at line 729

Mathematics ↔ Lean

For independent nonidentical reward laws with controlled drifting means…

Lean declarationBanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanDynamicRegret_le_allRegimes

Compiled

Plain-English statement. For independent nonidentical reward laws with controlled drifting means, the expected regret to the time-varying best arm is bounded in all regimes.

Mathematical reading. Formula renderer unavailable; readable fallback: For independent nonidentical reward laws with controlled drifting means, the expected regret to the time-varying best arm is bounded in all regimes.\(\mathbb E R_T^{\mathrm{dyn}}\le B_{\mathrm{fixed}}(T,C,S)+\sum_{t\le T}\bigl(\mu_t(a_t^\star)-\mu_t(a^\star)\bigr).\)

Intuition: Dynamic regret splits into what the algorithm loses against one baseline arm and what that baseline arm loses against the moving best arm.
Why it is needed: This is the first compiled moving-comparator theorem in the long Tsallis nonstationarity chain.
Place in the proof: Path-variation and switch-count modules specialize the explicit comparator-advantage term further.

Proof and Lean reading notes

Proof idea: Prove an exact dynamic-to-fixed decomposition, choose the finite actual-mean maximizer at every time, identify expected gaps under the independent law, and bound the comparator advantage using mean-deviation envelopes.
Lean reading notes: The result is expected predictable-environment dynamic regret, not realized sample-path regret or a minimax-sharp variation theorem.
Teaching dependencies: BanditRLProof.FiniteBanditModel

Exact Lean statement

theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanDynamicRegret_le_allRegimes {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (meanDeviation : Nat -> Fin K -> Real) (hmeanDeviation : forall t arm, |finiteArmIndependentRewardMean armLaw t arm - ((model.mean arm : Rat) : Real)| <= meanDeviation t arm) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (hgapLeOne : forall arm, arm ≠ model.bestArm -> ((model.gap arm : Rat) : Real) <= 1) (horizon : Nat) : letI : Nonempty (Fin K)

Open in the declaration catalog Open source at line 330

Mathematics ↔ Lean

The dynamic-regret nonstationarity cost can be compressed to one terminal…

Lean declarationBanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentGlobalMeanSwitchCountHorizonCompressedDynamicRegret_le_log

Compiled

Plain-English statement. The dynamic-regret nonstationarity cost can be compressed to one terminal count of global population-mean change points, with the theorem's explicit coefficient.

Mathematical reading. Formula renderer unavailable; readable fallback: The dynamic-regret nonstationarity cost can be compressed to one terminal count of global population-mean change points, with the theorem's explicit coefficient.\(\mathbb E R_T^{\mathrm{dyn}}\le B_{\log}(T)+4(K-1)(T+1)S_T.\)

Intuition: A single global switch event dominates every armwise mean change, so repeated prefix penalties can be bounded by the terminal global count.
Why it is needed: It replaces a nested time-by-arm deviation sum with a more readable population-level change count.
Place in the proof: This is a compiled but deliberately non-sharp endpoint; the obstruction theorem explains why the present route cannot yield a square-root switch rate by comparison alone.

Proof and Lean reading notes

Proof idea: Prove monotonicity of the global prefix count, dominate fixed-deviation and moving-comparator penalties separately, and add the two coefficient-two bounds.
Lean reading notes: The count excludes the post-horizon transition. The theorem does not claim a minimax switch-rate result.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentGlobalMeanSwitchCountHorizonCompressedDynamicRegret_le_log {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hinitialMean : forall arm, finiteArmIndependentRewardMean armLaw 0 arm = ((model.mean arm : Rat) : Real)) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) : letI : Nonempty (Fin K)

Open in the declaration catalog Open source at line 218

Mathematics ↔ Lean

If each oracle-defined epoch has a fixed-comparator regret certificate…

Lean declarationBanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSwitchCountSqrt

Compiled

Plain-English statement. If each oracle-defined epoch has a fixed-comparator regret certificate, their total moving-comparator regret is bounded by a square-root term depending on the number of switches and the horizon.

Mathematical reading. Formula renderer unavailable; readable fallback: If each oracle-defined epoch has a fixed-comparator regret certificate, their total moving-comparator regret is bounded by a square-root term depending on the number of switches and the horizon.\(R_T^{\mathrm{mov}}\le c\sum_e\sqrt{|I_e|}\le c\sqrt{(S_T+1)(T+1)}.\)

Intuition: Restarting turns a moving comparator into several fixed-comparator problems; Cauchy-Schwarz aggregates their square-root costs.
Why it is needed: It isolates the deterministic assembly reused by the generated change-point restart theorem.
Place in the proof: This theorem is an upstream deterministic parent. The selector, one-trajectory law transport, epoch-local stability, and population-mean change-point consumer now compile downstream.

Proof and Lean reading notes

Proof idea: Partition the inclusive horizon into epoch fibers, rewrite regret exactly as their sum, apply each local certificate, and bound the sum of square roots by Cauchy-Schwarz.
Lean reading notes: This declaration remains conditional on epoch certificates, but the repository now contains a separate generated consumer. Do not read this parent alone as the final endpoint.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSwitchCountSqrt {Env : Type u} {Action : Type v} {Epoch : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] [DecidableEq Epoch] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (epochs : Finset Epoch) (epochOf : Nat -> Epoch) (epochComparator : Epoch -> Action) (horizon switches : Nat) (hEpochOf : ∀ t ∈ Finset.range (horizon + 1), epochOf t ∈ epochs) (hEpochCard : epochs.card <= switches + 1) (coefficient : Real) (hcoefficient : 0 <= coefficient) (sample : Env × ((k : Nat) -> Action × Real)) (hEpochRegret : ∀ epoch ∈ epochs, sampledScheduledHalfTsallisPredictableOracleRestartEpochRegret arms harms eta loss epochOf epochComparator horizon epoch sample <= coefficient * Real.sqrt ((oracleRestartEpochRounds epochOf horizon epoch).card : Real)) : sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta loss (fun t => epochComparator (epochOf t)) horizon sample <= coefficient * Real.sqrt (((switches + 1 : Nat) : Real)) * Real.sqrt (((horizon + 1 : Nat) : Real))

Open in the declaration catalog Open source at line 162

Mathematics ↔ Lean

The generated half-Tsallis policy that restarts after every global…

Lean declarationBanditRLProof.Tsallis.integral_sampledOracleRestartHalfTsallisFiniteArmIndependentGlobalMeanChangeDynamicRegret_le

Compiled

Plain-English statement. The generated half-Tsallis policy that restarts after every global population-mean change has expected dynamic regret bounded by an explicit square-root function of the number of change points and the horizon.

Mathematical reading. Formula renderer unavailable; readable fallback: The generated half-Tsallis policy that restarts after every global population-mean change has expected dynamic regret bounded by an explicit square-root function of the number of change points and the horizon.\(\mathbb E R_T^{\mathrm{dyn}}\le 8\sqrt{K}\,\sqrt{S_T+1}\,\sqrt{T+1}.\)

Intuition: Inside an epoch the population means do not change, so one fixed comparator remains optimal; restarting localizes learning and Cauchy-Schwarz aggregates the epoch costs.
Why it is needed: It closes the former gap between the deterministic restart assembly and a single generated probability law.
Place in the proof: This is the current terminal of the full-information population-mean oracle-restart branch.

Proof and Lean reading notes

Proof idea: Construct the exact change-point schedule, prove its epoch count is the global switch count plus one, show the epoch-start best arm stays mean-optimal, transport the generated local stability certificates, and invoke the compiled restart assembly.
Lean reading notes: The schedule sees population-mean changes. An observable detector with delay and false alarms is a different, still-open random-schedule theorem route.
Teaching dependencies: BanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSwitchCountSqrt

Exact Lean statement

theorem integral_sampledOracleRestartHalfTsallisFiniteArmIndependentGlobalMeanChangeDynamicRegret_le {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : ∀ t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : ∀ t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (horizon : Nat) : letI : Nonempty (Fin K)

Open in the declaration catalog Open source at line 272

Maintainer contract

Open the canonical completion definition and blockers

Complete in the canonical finite-arm scope when half-Tsallis finite-simplex minimizer existence, interiority, uniqueness, and measurability; one-step importance-weighted stability; time-varying potential/penalty algebra; the measurable scheduled selector and recursive generated action law; observed score/probability alignment; initial, successor, all-times, and all-rate expected stability; expected environment-regret transport; fixed-gap self-bounding; square-root-schedule logarithmic optimization; and a concrete finite-arm IID rational reward-law producer all compile. The terminal must use the same let-bound selector, trajectory kernel, and measure, retain probability/a.e.-unit-support/exact-mean/positive-gap contracts, and admit the uncorrupted specialization by setting its explicit nonnegative corruption allowance to zero.

Remaining blockers

No remaining blocker inside this canonical scope: Tests/BookMapChaptersSevenAndEightCanary.lean checks the actual generated selector/action-law/stability chain and concretely instantiates the IID logarithmic terminal with two bounded Dirac reward laws of means 3/4 and 1/4 and a proved positive gap. The items below remain distinct research extensions.

Chapter implementation status

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

Open 4 implementation records4 compiled · 0 partial · 0 blocked · 0 planned

Milestone	Status	Lean declaration	Remaining gap
Finite-arm IID half-Tsallis logarithmic regret	Compiled	`BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIIDRewardLawRegret_le_log`	—
History-adaptive expected-corruption all-regimes bound	Compiled	`BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLawRegret_le_allRegimes`	—
Nonidentical drifting-mean dynamic regret	Compiled	`BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanDynamicRegret_le_allRegimes`	—
Generated oracle-restart switch-count dynamic regret	Compiled	`BanditRLProof.Tsallis.integral_sampledOracleRestartHalfTsallisFiniteArmIndependentGlobalMeanChangeDynamicRegret_le`	—

Open boundaries

Paper-sharp or minimax-optimal Tsallis-INF constants, a complete best-of-both-worlds theorem, and high-probability or realized-regret guarantees are not claimed by the canonical expected-regret terminal.
History-adaptive corruption, drifting laws, dynamic comparators, and the population-mean oracle restart compile as separately labelled extensions; an observed-reward detector still needs random history-dependent scheduling plus delay/false-alarm concentration.
The strict Fin 2 refined-averaged-stability counterexample remains an explicit obstruction; contextual/linear Tsallis-INF and broader adaptive-learning-rate paper routes remain separate.

All Lean modules in this chapter

Open the complete module list (86 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.FTRLOneStep`	6	0	Compiled
`BanditRLProof.TsallisConjugatePotentialFiniteHorizon`	21	4	Compiled
`BanditRLProof.TsallisConjugatePotentialStability`	17	1	Compiled
`BanditRLProof.TsallisConstrainedQuadraticOptimization`	9	1	Compiled
`BanditRLProof.TsallisFTRLConditionalStability`	8	2	Compiled
`BanditRLProof.TsallisFTRLEstimatedEnvironmentRegret`	39	1	Compiled
`BanditRLProof.TsallisFTRLExpectedStability`	6	2	Compiled
`BanditRLProof.TsallisFTRLFiniteHorizonSelection`	5	1	Compiled
`BanditRLProof.TsallisFTRLGeneratedMeasurability`	9	2	Compiled
`BanditRLProof.TsallisFTRLGeneratedRegularity`	9	1	Compiled
`BanditRLProof.TsallisFTRLInteriority`	8	1	Compiled
`BanditRLProof.TsallisFTRLMinimizerExistence`	20	1	Compiled
`BanditRLProof.TsallisFTRLMinimizerMeasurability`	8	1	Compiled
`BanditRLProof.TsallisFTRLMinimizerUniqueness`	4	1	Compiled
`BanditRLProof.TsallisFTRLOneStepStability`	5	2	Compiled
`BanditRLProof.TsallisFTRLRecursiveTrajectory`	27	4	Compiled
`BanditRLProof.TsallisFTRLRegret`	12	1	Compiled
`BanditRLProof.TsallisFTRLStationarity`	19	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDArmDependentSuboptimalBoostRegret`	6	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDCorruptedRewardLaw`	20	2	Compiled
`BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLaw`	15	3	Compiled
`BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLaw`	18	2	Compiled
`BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveRefinedCorruptedRewardLaw`	4	3	Compiled
`BanditRLProof.TsallisFiniteArmIIDHorizonHistoryAdaptiveExpectedCorruptedRewardLaw`	19	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDMeasurableHistoryArmGatedSuboptimalBoostRegret`	4	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDPreviousActionGatedSuboptimalBoostRegret`	4	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDRewardLaw`	14	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDTimeVaryingCorruptedRewardLaw`	11	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDTimeVaryingSuboptimalBoostRegret`	7	1	Compiled
`BanditRLProof.TsallisFiniteArmIIDUniformSuboptimalBoostRefinedRegret`	8	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentDriftingMeanAllRegimes`	3	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentDriftingMeanDynamicRegret`	11	2	Compiled
`BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRefinedRegret`	2	3	Compiled
`BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRewardLaw`	8	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentGlobalMeanSwitchCountCompressedDynamicRegret`	8	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentGlobalMeanSwitchCountDynamicRegret`	9	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentMeanSwitchCountDynamicRegret`	9	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentPathVariationDynamicRegret`	7	1	Compiled
`BanditRLProof.TsallisFiniteArmIndependentRewardLaw`	4	3	Compiled
`BanditRLProof.TsallisFiniteArmIndependentSingleSwitchComparatorObstruction`	21	1	Compiled
`BanditRLProof.TsallisFiniteBanditMeanLoss`	6	2	Compiled
`BanditRLProof.TsallisImportanceWeightedMoment`	4	2	Compiled
`BanditRLProof.TsallisOracleRestartDynamicRegret`	6	1	Compiled
`BanditRLProof.TsallisOracleRestartExpectedRegret`	25	2	Compiled
`BanditRLProof.TsallisOracleRestartExpectedStability`	26	2	Compiled
`BanditRLProof.TsallisOracleRestartGeneratedDynamicRegret`	2	1	Compiled
`BanditRLProof.TsallisOracleRestartGeneratedTrajectory`	22	1	Compiled
`BanditRLProof.TsallisOracleRestartGlobalMeanSwitchCount`	16	2	Compiled
`BanditRLProof.TsallisOracleRestartPredictableRegret`	11	2	Compiled
`BanditRLProof.TsallisOracleRestartRefinedStabilityTuning`	12	5	Compiled
`BanditRLProof.TsallisOracleRestartScoreAlignment`	17	1	Compiled
`BanditRLProof.TsallisRefinedAveragedStabilityObstruction`	30	1	Compiled
`BanditRLProof.TsallisRefinedImportanceWeightedMoment`	9	2	Compiled
`BanditRLProof.TsallisRefinedSuboptimalStability`	6	1	Compiled
`BanditRLProof.TsallisRegularizer`	6	1	Compiled
`BanditRLProof.TsallisScheduledAllRateExpectedStability`	16	1	Compiled
`BanditRLProof.TsallisScheduledAllTimesExpectedStability`	4	1	Compiled
`BanditRLProof.TsallisScheduledConditionalMeanGap`	5	1	Compiled
`BanditRLProof.TsallisScheduledExpectedGapSelfBounding`	5	1	Compiled
`BanditRLProof.TsallisScheduledExpectedRegret`	13	2	Compiled
`BanditRLProof.TsallisScheduledExpectedStability`	19	2	Compiled
`BanditRLProof.TsallisScheduledFixedGapSelfBounding`	6	1	Compiled
`BanditRLProof.TsallisScheduledIIDHistoryAdaptive`	4	1	Compiled
`BanditRLProof.TsallisScheduledIIDMeanGap`	12	4	Compiled
`BanditRLProof.TsallisScheduledIIDTimeVaryingMeanGap`	9	2	Compiled
`BanditRLProof.TsallisScheduledIndependentMeanGap`	4	2	Compiled
`BanditRLProof.TsallisScheduledInitialExpectedStability`	6	1	Compiled
`BanditRLProof.TsallisScheduledRecursiveTrajectory`	13	1	Compiled
`BanditRLProof.TsallisScheduledReferenceGapExpectedDeviationSelfBounding`	1	1	Compiled
`BanditRLProof.TsallisScheduledReferenceGapSelfBounding`	1	1	Compiled
`BanditRLProof.TsallisScheduledRefinedExpectedPenalty`	8	1	Compiled
`BanditRLProof.TsallisScheduledRefinedStabilityPenalty`	7	2	Compiled
`BanditRLProof.TsallisScheduledScoreAlignment`	11	2	Compiled
`BanditRLProof.TsallisScheduledSelfBoundingInterpolation`	2	1	Compiled
`BanditRLProof.TsallisScheduledSelfBoundingOptimization`	5	2	Compiled
`BanditRLProof.TsallisScheduledSuboptimalExpectedBound`	10	2	Compiled
`BanditRLProof.TsallisScheduledTimeVaryingExpectedGap`	9	2	Compiled
`BanditRLProof.TsallisSelfBounding`	14	1	Compiled
`BanditRLProof.TsallisSelfBoundingBetaRoot`	3	1	Compiled
`BanditRLProof.TsallisSqrtScheduleFixedGap`	17	1	Compiled
`BanditRLProof.TsallisSqrtScheduleSelfBoundingOptimization`	7	2	Compiled
`BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedScalar`	14	1	Compiled
`BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedTuning`	6	1	Compiled
`BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedWindow`	2	1	Compiled
`BanditRLProof.TsallisSqrtScheduleSelfBoundingTuning`	7	1	Compiled
`BanditRLProof.TsallisTimeVaryingPenalty`	14	4	Compiled