Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRewardLaw
# Finite-arm independent reward laws with drifting means Each round may use a different probability law for every arm. The roundwise arm means may drift from a fixed finite-bandit model, with a deterministic coordinatewise deviation envelope. The resulting regret theorem charges the induced two-arm gap deviation explicitly.
Module map
Imports
BanditRLProof.TsallisFiniteArmIndependentRewardLaw
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRefinedRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.finiteArmIndependentRewardMean
Compiled
The actual mean reward of arm `arm` at round `t`.
noncomputable def finiteArmIndependentRewardMean {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : Real
theorem
BanditRLProof.Tsallis.independentLossStateTimeVaryingMeanGap_finiteArmIndependentRewardVectorLoss_eq_mean_sub
Compiled
Under the unit-support contract, the roundwise product-law loss gap is the difference between the actual mean rewards of the best and selected arms.
theorem independentLossStateTimeVaryingMeanGap_finiteArmIndependentRewardVectorLoss_eq_mean_sub {K : Nat} (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) (t : Nat) (best arm : Fin K) : independentLossStateTimeVaryingMeanGap (finiteArmIndependentRewardVectorLaw armLaw) (fun _ => finiteArmIIDRewardVectorLoss) t best arm = finiteArmIndependentRewardMean armLaw t best - finiteArmIndependentRewardMean armLaw t arm
theorem
BanditRLProof.Tsallis.abs_independentLossStateTimeVaryingMeanGap_sub_modelGap_le
Compiled
The actual loss gap stays within the sum of the two supplied arm-mean deviation envelopes from the fixed model gap.
theorem abs_independentLossStateTimeVaryingMeanGap_sub_modelGap_le {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) (t : Nat) (arm : Fin K) (harm : arm ≠ model.bestArm) : |independentLossStateTimeVaryingMeanGap (finiteArmIndependentRewardVectorLaw armLaw) (fun _ => finiteArmIIDRewardVectorLoss) t model.bestArm arm - ((model.gap arm : Rat) : Real)| <= meanDeviation t arm + meanDeviation t model.bestArm
def
BanditRLProof.Tsallis.finiteArmIndependentMeanDeviationBudget
Compiled
Explicit accumulated gap-deviation budget induced by armwise drifting means through the inclusive horizon.
noncomputable def finiteArmIndependentMeanDeviationBudget {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (meanDeviation : Nat -> Fin K -> Real) : Real
theorem
BanditRLProof.Tsallis.finiteArmIndependentMeanDeviationBudget_eq
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteArmIndependentMeanDeviationBudget_eq {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (meanDeviation : Nat -> Fin K -> Real) : finiteArmIndependentMeanDeviationBudget model horizon meanDeviation = (Finset.range (horizon + 1)).sum (fun t => ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => meanDeviation t arm + meanDeviation t model.bestArm))
theorem
BanditRLProof.Tsallis.finiteArmIndependentMeanDeviationBudget_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteArmIndependentMeanDeviationBudget_zero {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) : finiteArmIndependentMeanDeviationBudget model horizon (fun _ _ => 0) = 0
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLaw_hasSelfBounding
Compiled
Independent nonidentical reward laws with an armwise mean-deviation envelope supply the terminal self-bound consumed by both logarithmic and refined square-root schedule routes.
theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLaw_hasSelfBounding {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) (horizon : Nat) : letI : Nonempty (Fin K)
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLawRegret_le_log
Compiled
Generated scheduled half-Tsallis logarithmic regret against the fixed baseline comparator `model.bestArm` for independent, nonidentical finite-arm reward laws whose means drift within an explicit coordinatewise envelope. This is a static-comparator theorem, not dynamic regret against each round's best actual mean.
theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLawRegret_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) (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)) (horizon : Nat) : letI : Nonempty (Fin K)