BanditRLProof.TsallisFiniteArmIndependentDriftingMeanAllRegimes

Total explicit fixed-comparator bound for independent nonidentical reward laws with drifting means. The refined expression is used exactly inside its coefficient-aware window; the logarithmic explicit-budget expression is used on the complement.

noncomputable def finiteArmIndependentDriftingMeanAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (meanDeviation : Nat -> Fin K -> Real) : Real

With one arm there is no suboptimal coordinate, so the all-regimes envelope reduces to the logarithmic base term.

theorem finiteArmIndependentDriftingMeanAllRegimeBound_fin_one (model : FiniteBanditModel 1) (horizon : Nat) (meanDeviation : Nat -> Fin 1 -> Real) : finiteArmIndependentDriftingMeanAllRegimeBound model horizon meanDeviation = 1 + Real.log (((horizon + 1 : Nat) : Real))

Generated scheduled half-Tsallis regret against the fixed baseline comparator for every deterministic mean-deviation envelope and finite horizon. The theorem automatically selects the compact-window refined branch or the logarithmic fallback and requires no caller window proof. This is not dynamic regret.

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