BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveRefinedCorruptedRewardLaw

The history-adaptive finite-arm corruption model supplies the terminal self-bounding contract consumed by the refined square-root schedule route.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLaw_hasSelfBounding {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)) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (horizon : Nat) : letI : Nonempty (Fin K)

Refined local square-root corruption regret for the concrete finite-arm IID history-adaptive reward-shift model. The corruption scalar is the source's deterministic envelope budget, rather than a free theorem parameter.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLawRegret_le_refinedLocalExplicit {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)) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (hsuboptimal : ((Finset.univ : Finset (Fin K)).erase model.bestArm).Nonempty) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) (hcorruption : 0 < finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon source) (hscalarLower : 2 <= (2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2)) (hscalarThresholdOne : (2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2) <= 2 * (((horizon + 1 : Nat) : Real))) (hcorruptionUpper : 2 * (finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon source * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) <= 2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) (hcorruptionLower : 25 * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real)) * (Real.log ((2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2)) + 2) <= finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon source) : letI : Nonempty (Fin K)

The coefficient-aware refined corruption window specialized to the finite-arm IID history-adaptive reward-shift model.

noncomputable def finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) : Prop

A model-facing refined theorem with the low-level scalar inequalities replaced by a compact corruption window. Unit-bounded positive model gaps imply that the reciprocal-gap sum dominates the number of suboptimal arms.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLawRegret_le_refinedLocalExplicit_of_window {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)) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (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) (hwindow : finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow model horizon source) : letI : Nonempty (Fin K)