BanditRLProof.TsallisFiniteArmIIDCorruptedRewardLaw

Projection of a real value to the unit interval.

noncomputable def clippedUnitReal (value : Real) : Real

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

theorem clippedUnitReal_mem_Icc (value : Real) : clippedUnitReal value ∈ Set.Icc (0 : Real) 1

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

theorem clippedUnitReal_eq_of_mem_Icc (value : Real) (hvalue : value ∈ Set.Icc (0 : Real) 1) : clippedUnitReal value = value

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

theorem abs_clippedUnitReal_add_sub_self_le (value shift : Real) (hvalue : value ∈ Set.Icc (0 : Real) 1) : |clippedUnitReal (value + shift) - value| <= |shift|

Reward after a stationary arm-dependent shift and unit-interval clipping.

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

Selected loss associated with the stationary corrupted reward vector.

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

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

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

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

theorem finiteArmIIDStationaryCorruptedRewardVectorLoss_nonneg {K : Nat} (rewardShift : Fin K -> Real) (state : Fin K -> Rat) (arm : Fin K) : 0 <= finiteArmIIDStationaryCorruptedRewardVectorLoss rewardShift state arm

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

theorem finiteArmIIDStationaryCorruptedRewardVectorLoss_le_one {K : Nat} (rewardShift : Fin K -> Real) (state : Fin K -> Rat) (arm : Fin K) : finiteArmIIDStationaryCorruptedRewardVectorLoss rewardShift state arm <= 1

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

theorem abs_finiteArmIIDStationaryCorruptedReward_sub_base_le {K : Nat} (rewardShift : Fin K -> Real) (state : Fin K -> Rat) (arm : Fin K) : |finiteArmIIDStationaryCorruptedReward rewardShift state arm - clippedUnitReward (state arm)| <= |rewardShift arm|

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

theorem abs_stationaryCorruptedLossDiff_sub_baseLossDiff_le {K : Nat} (rewardShift : Fin K -> Real) (state : Fin K -> Rat) (best arm : Fin K) : |(finiteArmIIDStationaryCorruptedRewardVectorLoss rewardShift state arm - finiteArmIIDStationaryCorruptedRewardVectorLoss rewardShift state best) - (finiteArmIIDRewardVectorLoss state arm - finiteArmIIDRewardVectorLoss state best)| <= |rewardShift arm| + |rewardShift best|

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

theorem integrable_iidLossStateDiff {LossState Action : Type*} [MeasurableSpace LossState] [MeasurableSpace Action] (law : Measure LossState) [IsFiniteMeasure law] (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : forall state action, 0 <= value state action) (hvalue_le_one : forall state action, value state action <= 1) (best arm : Action) : Integrable (fun state => value state arm - value state best) law

The actual stationary-corrupted IID loss gap remains within the two affected arm shifts of the uncorrupted finite-bandit model gap.

theorem abs_iidLossStateMeanGap_stationaryCorrupted_sub_modelGap_le {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)) (rewardShift : Fin K -> Real) (arm : Fin K) : |iidLossStateMeanGap (finiteArmIIDRewardVectorLaw armLaw) (finiteArmIIDStationaryCorruptedRewardVectorLoss rewardShift) model.bestArm arm - ((model.gap arm : Rat) : Real)| <= |rewardShift arm| + |rewardShift model.bestArm|

Total baseline-gap perturbation allowance through the inclusive horizon.

noncomputable def scheduledGapDeviationBudget {Action : Type*} [DecidableEq Action] (arms : Finset Action) (best : Action) (horizon : Nat) (deviation : Action -> Real) : Real

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

theorem scheduledGapDeviationBudget_eq {Action : Type*} [DecidableEq Action] (arms : Finset Action) (best : Action) (horizon : Nat) (deviation : Action -> Real) : scheduledGapDeviationBudget arms best horizon deviation = (((horizon + 1 : Nat) : Real)) * (arms.erase best).sum deviation

An expected law for perturbed gaps yields the baseline-gap self-bound with the accumulated coordinatewise gap-deviation budget.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_perturbedExpectedGapLaw {Env Action : Type*} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (baseGap actualGap deviation : Action -> Real) (hactualGapLaw : HasScheduledExpectedGapLaw mu arms harms eta loss best actualGap horizon) (hdeviation : forall action, action ∈ arms.erase best -> |actualGap action - baseGap action| <= deviation action) : (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => baseGap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - scheduledGapDeviationBudget arms best horizon deviation <= integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon)

Explicit corruption budget for a stationary arm-dependent reward shift.

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

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

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

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

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

Scheduled half-Tsallis logarithmic regret for an IID finite-arm reward model with a fixed clipped reward shift. The additive corruption term is derived from `rewardShift`; it is not a free theorem parameter.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDStationaryCorruptedRewardLawRegret_le_log {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)) (rewardShift : Fin K -> Real) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) : letI : Nonempty (Fin K)