BanditRLProof.TsallisFiniteArmIIDMeasurableHistoryArmGatedSuboptimalBoostRegret

A history-adaptive corruption source with an arbitrary initial arm gate and arbitrary measurable finite-pair-history-and-arm successor gates. The best arm is never shifted.

noncomputable def measurableHistoryArmGatedSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (initialGate : Set (Fin K)) (gate : (n : Nat) -> Set (History.FinitePairHistory (Fin K) Real n × Fin K)) (hgate : forall n, MeasurableSet (gate n)) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) : FiniteArmIIDHistoryAdaptiveRewardShiftSource K where

The measurable history-arm gate does not enlarge the deterministic envelope, whose budget is exactly the underlying time-varying schedule.

theorem finiteArmIIDHistoryAdaptiveRewardCorruptionBudget_measurableHistoryArmGatedSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (initialGate : Set (Fin K)) (gate : (n : Nat) -> Set (History.FinitePairHistory (Fin K) Real n × Fin K)) (hgate : forall n, MeasurableSet (gate n)) (horizon : Nat) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) : finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon (measurableHistoryArmGatedSuboptimalRewardBoostSource model initialGate gate hgate boost hboost) = finiteArmIIDTimeVaryingSuboptimalBoostBudget model horizon boost

The named time-varying refined regime supplies the compact window for an arbitrary measurable history-arm-gated source with the same envelope.

theorem finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow_measurableHistoryArmGatedSuboptimalRewardBoostSource_of_refinedRegime {K : Nat} (model : FiniteBanditModel K) (initialGate : Set (Fin K)) (gate : (n : Nat) -> Set (History.FinitePairHistory (Fin K) Real n × Fin K)) (hgate : forall n, MeasurableSet (gate n)) (horizon : Nat) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) (hregime : finiteArmIIDTimeVaryingSuboptimalBoostRefinedRegime model horizon boost) : finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow model horizon (measurableHistoryArmGatedSuboptimalRewardBoostSource model initialGate gate hgate boost hboost)

Scheduled half-Tsallis regret for every initial arm gate and measurable predictable successor gate on the complete finite pair history and candidate arm. The theorem covers every finite horizon and selects the refined or logarithmic branch internally.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDMeasurableHistoryArmGatedSuboptimalBoostRewardLawRegret_le_allRegimes {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (initialGate : Set (Fin K)) (gate : (n : Nat) -> Set (History.FinitePairHistory (Fin K) Real n × Fin K)) (hgate : forall n, MeasurableSet (gate n)) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) (hsuboptimal : ((Finset.univ : Finset (Fin K)).erase model.bestArm).Nonempty) (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)