BanditRLProof.TsallisFiniteArmIndependentDriftingMeanDynamicRegret

Predictable environment regret against a deterministic comparator that may change with the round.

noncomputable def sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (comparator : Nat -> Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Moving-comparator regret is fixed-comparator regret plus the cumulative loss advantage of the moving comparator over the fixed arm.

theorem sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_eq_fixed_add {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (comparator : Nat -> Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta loss comparator horizon sample = sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon sample + (Finset.range (horizon + 1)).sum (fun t => Exp3.predictableLossAt loss t sample best - Exp3.predictableLossAt loss t sample (comparator t))

An actual-mean maximizing arm at round `t`. The finite action space is nonempty because it comes from a `FiniteBanditModel`.

noncomputable def finiteArmIndependentBestArmAt {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) : Fin K

The selected dynamic arm maximizes the actual roundwise reward mean.

theorem finiteArmIndependentRewardMean_le_bestArmAt {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : finiteArmIndependentRewardMean armLaw t arm <= finiteArmIndependentRewardMean armLaw t (finiteArmIndependentBestArmAt model armLaw t)

Extra envelope budget needed to move from the fixed model comparator to the actual-mean maximizing arm at every included round.

noncomputable def finiteArmIndependentDynamicComparatorPenalty {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) (meanDeviation : Nat -> Fin K -> Real) : Real

With one arm the dynamic comparator cannot move, so its extra penalty is zero.

theorem finiteArmIndependentDynamicComparatorPenalty_fin_one (model : FiniteBanditModel 1) (armLaw : Nat -> Fin 1 -> Measure Rat) (horizon : Nat) (meanDeviation : Nat -> Fin 1 -> Real) : finiteArmIndependentDynamicComparatorPenalty model armLaw horizon meanDeviation = 0

The actual-mean advantage of any arm over the fixed baseline best arm is controlled by the two corresponding mean-deviation envelopes.

theorem finiteArmIndependentRewardMean_sub_bestArm_le_meanDeviation {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (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) : finiteArmIndependentRewardMean armLaw t arm - finiteArmIndependentRewardMean armLaw t model.bestArm <= meanDeviation t arm + meanDeviation t model.bestArm

For the concrete independent nonidentical generated law, integrated moving-comparator regret is fixed-baseline regret plus the exact cumulative actual-mean advantage of the comparator.

theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentMovingComparatorRewardLawRegret_eq_fixed_add_meanAdvantage {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) (comparator : Nat -> Fin K) (horizon : Nat) : letI : Nonempty (Fin K)

Dynamic all-regimes bound: fixed-baseline all-regimes regret plus the explicit envelope cost of following the actual-mean maximizing arm.

noncomputable def finiteArmIndependentDriftingMeanDynamicAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) (meanDeviation : Nat -> Fin K -> Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem finiteArmIndependentDriftingMeanDynamicAllRegimeBound_fin_one (model : FiniteBanditModel 1) (armLaw : Nat -> Fin 1 -> Measure Rat) (horizon : Nat) (meanDeviation : Nat -> Fin 1 -> Real) : finiteArmIndependentDriftingMeanDynamicAllRegimeBound model armLaw horizon meanDeviation = 1 + Real.log (((horizon + 1 : Nat) : Real))

Generated scheduled half-Tsallis dynamic regret against the arm with the largest actual reward mean at each round. No caller supplies the dynamic comparator, a refined-window proof, or a nonempty-suboptimal-arm proof.

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)