Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteArmIndependentPathVariationDynamicRegret
# Path-variation dynamic regret for independent nonidentical reward laws This module derives the mean-deviation envelope used by the compiled drifting-mean dynamic-regret theorem from the actual reward-mean path. The only model-alignment premise is equality of the actual and baseline means at round zero.
Module map
Imports
BanditRLProof.TsallisFiniteArmIndependentDriftingMeanDynamicRegret
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIndependentMeanSwitchCountDynamicRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.finiteArmIndependentCumulativeMeanPathVariation
Compiled
Cumulative absolute variation of one arm's actual reward mean before round `t`.
noncomputable def finiteArmIndependentCumulativeMeanPathVariation {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : Real
theorem
BanditRLProof.Tsallis.finiteArmIndependentCumulativeMeanPathVariation_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteArmIndependentCumulativeMeanPathVariation_zero {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (arm : Fin K) : finiteArmIndependentCumulativeMeanPathVariation armLaw 0 arm = 0
theorem
BanditRLProof.Tsallis.abs_finiteArmIndependentRewardMean_sub_zero_le_cumulativeMeanPathVariation
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem abs_finiteArmIndependentRewardMean_sub_zero_le_cumulativeMeanPathVariation {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : |finiteArmIndependentRewardMean armLaw t arm - finiteArmIndependentRewardMean armLaw 0 arm| <= finiteArmIndependentCumulativeMeanPathVariation armLaw t arm
theorem
BanditRLProof.Tsallis.abs_finiteArmIndependentRewardMean_sub_model_le_cumulativeMeanPathVariation
Compiled
Initial mean matching turns cumulative actual-mean path variation into the all-time model-deviation envelope required by the drifting-mean theorem.
theorem abs_finiteArmIndependentRewardMean_sub_model_le_cumulativeMeanPathVariation {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hinitialMean : forall arm, finiteArmIndependentRewardMean armLaw 0 arm = ((model.mean arm : Rat) : Real)) (t : Nat) (arm : Fin K) : |finiteArmIndependentRewardMean armLaw t arm - ((model.mean arm : Rat) : Real)| <= finiteArmIndependentCumulativeMeanPathVariation armLaw t arm
def
BanditRLProof.Tsallis.finiteArmIndependentPathVariationDynamicAllRegimeBound
Compiled
The compiled dynamic all-regimes bound specialized to the law-derived cumulative population-mean path-variation envelope.
noncomputable def finiteArmIndependentPathVariationDynamicAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : Real
theorem
BanditRLProof.Tsallis.finiteArmIndependentPathVariationDynamicAllRegimeBound_fin_one
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteArmIndependentPathVariationDynamicAllRegimeBound_fin_one (model : FiniteBanditModel 1) (armLaw : Nat -> Fin 1 -> Measure Rat) (horizon : Nat) : finiteArmIndependentPathVariationDynamicAllRegimeBound model armLaw horizon = 1 + Real.log (((horizon + 1 : Nat) : Real))
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentPathVariationDynamicRegret_le_allRegimes
Compiled
Generated expected predictable-environment dynamic regret with the all-time deviation envelope derived from the reward laws' population-mean path variation. No caller supplies a deviation envelope or the moving comparator. This retains one cumulative prefix envelope at every included time; it is not a horizon-compressed or minimax-sharp standard `V_T` bound.
theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentPathVariationDynamicRegret_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) (hinitialMean : forall arm, finiteArmIndependentRewardMean armLaw 0 arm = ((model.mean arm : Rat) : Real)) (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)