8. Tsallis-FTRL, corruption, and nonstationarity

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.

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

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

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.

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

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)

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.

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

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)

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.

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

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)

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.

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

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)

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.

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

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

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.

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

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)