BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLaw

A predictable reward-shift process and its deterministic envelope.

structure FiniteArmIIDHistoryAdaptiveRewardShiftSource (K : Nat) where

Projection to the real unit interval is measurable.

theorem measurable_clippedUnitReal : Measurable clippedUnitReal

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

theorem measurable_finiteArmIIDHistoryAdaptiveCorruptedRewardLoss_initial {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) : Measurable (fun input : (Nat -> (Fin K -> Rat)) × Fin K => finiteArmIIDStationaryCorruptedRewardVectorLoss source.initial (input.1 0) input.2)

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

theorem measurable_finiteArmIIDHistoryAdaptiveCorruptedRewardLoss_successor {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (n : Nat) : Measurable (fun input : (Nat -> (Fin K -> Rat)) × (History.FinitePairHistory (Fin K) Real n × Fin K) => finiteArmIIDStationaryCorruptedRewardVectorLoss (source.successor n input.2.1) (input.1 (n + 1)) input.2.2)

Predictable clipped loss generated by a history-adaptive reward shift.

noncomputable def finiteArmIIDHistoryAdaptiveCorruptedRewardLoss {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) : Exp3.PredictableLossVector (Nat -> (Fin K -> Rat)) (Fin K) where

The concrete history-adaptive loss reads no future IID state coordinate.

theorem finiteArmIIDHistoryAdaptiveCorruptedRewardLoss_hasIIDStateCoordinateLocality {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) : HasIIDStateCoordinateLocality (finiteArmIIDHistoryAdaptiveCorruptedRewardLoss source)

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

theorem predictableLossAt_finiteArmIIDHistoryAdaptiveCorruptedRewardLoss_zero {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (sample : (Nat -> (Fin K -> Rat)) × ((k : Nat) -> Fin K × Real)) (arm : Fin K) : Exp3.predictableLossAt (finiteArmIIDHistoryAdaptiveCorruptedRewardLoss source) 0 sample arm = finiteArmIIDStationaryCorruptedRewardVectorLoss source.initial (sample.1 0) arm

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

theorem predictableLossAt_finiteArmIIDHistoryAdaptiveCorruptedRewardLoss_succ {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (n : Nat) (sample : (Nat -> (Fin K -> Rat)) × ((k : Nat) -> Fin K × Real)) (arm : Fin K) : Exp3.predictableLossAt (finiteArmIIDHistoryAdaptiveCorruptedRewardLoss source) (n + 1) sample arm = finiteArmIIDStationaryCorruptedRewardVectorLoss (source.successor n (Preorder.frestrictLe n sample.2)) (sample.1 (n + 1)) arm

Pointwise actual/reference gap deviation under the source envelope.

theorem abs_historyAdaptiveCorruptedPredictableLossDiff_sub_baseLossDiff_le {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (t : Nat) (sample : (Nat -> (Fin K -> Rat)) × ((k : Nat) -> Fin K × Real)) (best arm : Fin K) : |(Exp3.predictableLossAt (finiteArmIIDHistoryAdaptiveCorruptedRewardLoss source) t sample arm - Exp3.predictableLossAt (finiteArmIIDHistoryAdaptiveCorruptedRewardLoss source) t sample best) - (Exp3.predictableLossAt (iidLossStatePredictableLossVector finiteArmIIDRewardVectorLoss measurable_finiteArmIIDRewardVectorLoss finiteArmIIDRewardVectorLoss_nonneg finiteArmIIDRewardVectorLoss_le_one) t sample arm - Exp3.predictableLossAt (iidLossStatePredictableLossVector finiteArmIIDRewardVectorLoss measurable_finiteArmIIDRewardVectorLoss finiteArmIIDRewardVectorLoss_nonneg finiteArmIIDRewardVectorLoss_le_one) t sample best)| <= source.envelope t arm + source.envelope t best

Explicit deterministic envelope budget for predictable corruption.

noncomputable def finiteArmIIDHistoryAdaptiveRewardCorruptionBudget {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) : Real

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

theorem finiteArmIIDHistoryAdaptiveRewardCorruptionBudget_eq {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) : finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon source = (Finset.range (horizon + 1)).sum (fun t => ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => source.envelope t arm + source.envelope t model.bestArm))

The uncorrupted predictable shift source.

def zeroFiniteArmIIDHistoryAdaptiveRewardShiftSource (K : Nat) : FiniteArmIIDHistoryAdaptiveRewardShiftSource K where

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

theorem finiteArmIIDHistoryAdaptiveRewardCorruptionBudget_zero {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) : finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon (zeroFiniteArmIIDHistoryAdaptiveRewardShiftSource K) = 0

The actual history-adaptive canonical trajectory has the IID-prefix factorization needed to reuse the uncorrupted reference gap law.

theorem hasScheduledIIDPrefixKernelFactorization_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveTrajectoryKernel {K : Nat} [Nonempty (Fin K)] (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (arms : Finset (Fin K)) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (horizon : Nat) : HasScheduledIIDPrefixKernelFactorization (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector (finiteArmIIDHistoryAdaptiveCorruptedRewardLoss source).environment) horizon

Scheduled half-Tsallis logarithmic regret under a measurable predictable history-adaptive reward shift. The additive allowance is the deterministic envelope budget packaged by `source`, not a free theorem parameter.

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