BanditRLProof.TsallisFiniteArmIIDTimeVaryingCorruptedRewardLaw

Reward after a deterministic time-indexed arm shift and clipping.

noncomputable def finiteArmIIDTimeVaryingCorruptedReward {K : Nat} (rewardShift : Nat -> Fin K -> Real) (t : Nat) (state : Fin K -> Rat) (arm : Fin K) : Real

Loss vector induced by the time-indexed clipped reward.

noncomputable def finiteArmIIDTimeVaryingCorruptedRewardVectorLoss {K : Nat} (rewardShift : Nat -> Fin K -> Real) (t : Nat) (state : Fin K -> Rat) (arm : Fin K) : Real

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

theorem measurable_finiteArmIIDTimeVaryingCorruptedRewardVectorLoss {K : Nat} (rewardShift : Nat -> Fin K -> Real) (t : Nat) : Measurable (fun input : (Fin K -> Rat) × Fin K => finiteArmIIDTimeVaryingCorruptedRewardVectorLoss rewardShift t input.1 input.2)

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

theorem finiteArmIIDTimeVaryingCorruptedRewardVectorLoss_nonneg {K : Nat} (rewardShift : Nat -> Fin K -> Real) (t : Nat) (state : Fin K -> Rat) (arm : Fin K) : 0 <= finiteArmIIDTimeVaryingCorruptedRewardVectorLoss rewardShift t state arm

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

theorem finiteArmIIDTimeVaryingCorruptedRewardVectorLoss_le_one {K : Nat} (rewardShift : Nat -> Fin K -> Real) (t : Nat) (state : Fin K -> Rat) (arm : Fin K) : finiteArmIIDTimeVaryingCorruptedRewardVectorLoss rewardShift t state arm <= 1

The actual mean gap at round `t` differs from the baseline model gap by at most the two affected arm shifts.

theorem abs_iidLossStateTimeVaryingMeanGap_corrupted_sub_modelGap_le {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : ∀ arm, IsProbabilityMeasure (armLaw arm)) (hbound : ∀ arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : ∀ arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (rewardShift : Nat -> Fin K -> Real) (t : Nat) (arm : Fin K) : |iidLossStateTimeVaryingMeanGap (finiteArmIIDRewardVectorLaw armLaw) (finiteArmIIDTimeVaryingCorruptedRewardVectorLoss rewardShift) t model.bestArm arm - ((model.gap arm : Rat) : Real)| <= |rewardShift t arm| + |rewardShift t model.bestArm|

Explicit accumulated budget of a time-indexed oblivious reward-shift schedule through the inclusive horizon.

noncomputable def finiteArmIIDTimeVaryingRewardCorruptionBudget {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (rewardShift : Nat -> Fin K -> Real) : Real

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

theorem finiteArmIIDTimeVaryingRewardCorruptionBudget_eq {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (rewardShift : Nat -> Fin K -> Real) : finiteArmIIDTimeVaryingRewardCorruptionBudget model horizon rewardShift = (Finset.range (horizon + 1)).sum (fun t => ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => |rewardShift t arm| + |rewardShift t model.bestArm|))

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

theorem finiteArmIIDTimeVaryingRewardCorruptionBudget_zero {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) : finiteArmIIDTimeVaryingRewardCorruptionBudget model horizon (fun _ _ => 0) = 0

A constant shift schedule recovers the stationary corruption budget.

theorem finiteArmIIDTimeVaryingRewardCorruptionBudget_const_eq_stationary {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (rewardShift : Fin K -> Real) : finiteArmIIDTimeVaryingRewardCorruptionBudget model horizon (fun _ => rewardShift) = finiteArmIIDStationaryRewardCorruptionBudget model horizon rewardShift

Scheduled half-Tsallis logarithmic regret under an explicit deterministic time-indexed reward-shift schedule. The additive allowance is derived from the schedule and is not a free corruption parameter.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDTimeVaryingCorruptedRewardLawRegret_le_log {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : ∀ arm, IsProbabilityMeasure (armLaw arm)) (hbound : ∀ arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : ∀ arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (rewardShift : Nat -> Fin K -> Real) (hgapPos : ∀ arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) : letI : Nonempty (Fin K)