Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteArmIndependentGlobalMeanSwitchCountCompressedDynamicRegret
# Horizon-compressed global mean-switch-count dynamic regret This module replaces every time-indexed global prefix count in the logarithmic dynamic-regret route by the single terminal count at `horizon`. The resulting bound is explicit and finite-sum free in its nonstationarity term, but remains linear rather than minimax-sharp.
Module map
Imports
BanditRLProof.TsallisFiniteArmIndependentGlobalMeanSwitchCountDynamicRegret
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIndependentSingleSwitchComparatorObstruction
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Tsallis.finiteArmIndependentCumulativeGlobalMeanSwitchCount_nonneg
Compiled
The global population-mean switch count is nonnegative.
theorem finiteArmIndependentCumulativeGlobalMeanSwitchCount_nonneg {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) : 0 <= finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t
theorem
BanditRLProof.Tsallis.finiteArmIndependentCumulativeGlobalMeanSwitchCount_mono
Compiled
Enlarging the prefix cannot decrease the global switch count.
theorem finiteArmIndependentCumulativeGlobalMeanSwitchCount_mono {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) {t u : Nat} (htu : t <= u) : finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t <= finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw u
theorem
BanditRLProof.Tsallis.finiteArmIndependentMeanDeviationBudget_globalMeanSwitchCount_le
Compiled
The fixed-comparator mean-deviation budget at the global prefix envelope is bounded by the terminal count times horizon mass and suboptimal-arm cardinality.
theorem finiteArmIndependentMeanDeviationBudget_globalMeanSwitchCount_le {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : finiteArmIndependentMeanDeviationBudget model horizon (fun t _ => finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t) <= 2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real)) * finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw horizon
theorem
BanditRLProof.Tsallis.finiteArmIndependentDynamicComparatorPenalty_globalMeanSwitchCount_le
Compiled
The moving-comparator penalty at the global prefix envelope is bounded by the same terminal-count expression as the fixed-comparator deviation budget. The erased-arm cardinality makes the bound exactly zero for `Fin 1`.
theorem finiteArmIndependentDynamicComparatorPenalty_globalMeanSwitchCount_le {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : finiteArmIndependentDynamicComparatorPenalty model armLaw horizon (fun t _ => finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t) <= 2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real)) * finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw horizon
theorem
BanditRLProof.Tsallis.finiteArmIndependentGlobalMeanSwitchCount_totalBudget_le
Compiled
One terminal global switch count controls both the fixed-comparator mean-deviation budget and the moving-comparator penalty.
theorem finiteArmIndependentGlobalMeanSwitchCount_totalBudget_le {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : finiteArmIndependentMeanDeviationBudget model horizon (fun t _ => finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t) + finiteArmIndependentDynamicComparatorPenalty model armLaw horizon (fun t _ => finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t) <= 4 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real)) * finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw horizon
def
BanditRLProof.Tsallis.finiteArmIndependentGlobalMeanSwitchCountHorizonCompressedLogDynamicBound
Compiled
Explicit logarithmic dynamic-regret bound with a single terminal global population-mean switch count.
noncomputable def finiteArmIndependentGlobalMeanSwitchCountHorizonCompressedLogDynamicBound {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : Real
theorem
BanditRLProof.Tsallis.finiteArmIndependentGlobalMeanSwitchCountHorizonCompressedLogDynamicBound_fin_one
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteArmIndependentGlobalMeanSwitchCountHorizonCompressedLogDynamicBound_fin_one (model : FiniteBanditModel 1) (armLaw : Nat -> Fin 1 -> Measure Rat) (horizon : Nat) : finiteArmIndependentGlobalMeanSwitchCountHorizonCompressedLogDynamicBound model armLaw horizon = 1 + Real.log (((horizon + 1 : Nat) : Real))
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentGlobalMeanSwitchCountHorizonCompressedDynamicRegret_le_log
Compiled
Generated expected predictable-environment dynamic regret with all time-indexed population-mean switch envelopes compressed into the terminal global count. This is a linear horizon-level compression, not a minimax switch-rate theorem.
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)