BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLaw

The reward shift selected from the finite observed pair history available before round `t`.

noncomputable def finiteArmIIDHistoryAdaptiveRewardShiftAt {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (t : Nat) (trajectory : (k : Nat) -> Fin K × Real) (arm : Fin K) : Real

The realized predictable shift of a fixed arm is measurable on the full trajectory space.

theorem measurable_finiteArmIIDHistoryAdaptiveRewardShiftAt {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (t : Nat) (arm : Fin K) : Measurable (fun trajectory : (k : Nat) -> Fin K × Real => finiteArmIIDHistoryAdaptiveRewardShiftAt source t trajectory arm)

The realized shift retains the deterministic envelope supplied by the history-adaptive source.

theorem abs_finiteArmIIDHistoryAdaptiveRewardShiftAt_le {K : Nat} (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (t : Nat) (trajectory : (k : Nat) -> Fin K × Real) (arm : Fin K) : |finiteArmIIDHistoryAdaptiveRewardShiftAt source t trajectory arm| <= source.envelope t arm

The actual/reference predictable loss-gap deviation is controlled by the two shifts realized on the observed history, before replacing them by their deterministic envelopes.

theorem abs_historyAdaptiveCorruptedPredictableLossDiff_sub_baseLossDiff_le_actualShift {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)| <= |finiteArmIIDHistoryAdaptiveRewardShiftAt source t sample.2 arm| + |finiteArmIIDHistoryAdaptiveRewardShiftAt source t sample.2 best|

Probability-weighted realized history-adaptive deviation is integrable under every finite trajectory measure.

theorem integrable_sampledScheduledHalfTsallisProbability_mul_historyAdaptiveRewardShiftDeviation {Env : Type*} {K : Nat} [MeasurableSpace Env] (mu : Measure (Env × ((k : Nat) -> Fin K × Real))) [IsFiniteMeasure mu] (arms : Finset (Fin K)) (harms : arms.Nonempty) (eta : Nat -> Real) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (t : Nat) (best arm : Fin K) (harm : arm ∈ arms) : Integrable (fun sample => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample arm * (|finiteArmIIDHistoryAdaptiveRewardShiftAt source t sample.2 arm| + |finiteArmIIDHistoryAdaptiveRewardShiftAt source t sample.2 best|)) mu

Expected corruption weighted by the generated policy's conditional selection probability for each affected suboptimal arm, using the realized history-adaptive shifts.

noncomputable def finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (mu : Measure ((Nat -> Fin K -> Rat) × ((k : Nat) -> Fin K × Real))) : Real

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

theorem finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget_eq {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (mu : Measure ((Nat -> Fin K -> Rat) × ((k : Nat) -> Fin K × Real))) : finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget model horizon source mu = (Finset.range (horizon + 1)).sum (fun t => ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => integral mu (fun sample => sampledScheduledHalfTsallisProbabilityAtTime (Finset.univ : Finset (Fin K)) ⟨model.bestArm, Finset.mem_univ model.bestArm⟩ sampledScheduledHalfTsallisSqrtSchedule t sample arm * (|finiteArmIIDHistoryAdaptiveRewardShiftAt source t sample.2 arm| + |finiteArmIIDHistoryAdaptiveRewardShiftAt source t sample.2 model.bestArm|))))

The policy-weighted realized corruption budget is nonnegative.

theorem finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget_nonneg {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (mu : Measure ((Nat -> Fin K -> Rat) × ((k : Nat) -> Fin K × Real))) : 0 <= finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget model horizon source mu

The expected realized budget never exceeds the source's deterministic all-round envelope budget.

theorem finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget_le {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (mu : Measure ((Nat -> Fin K -> Rat) × ((k : Nat) -> Fin K × Real))) [IsProbabilityMeasure mu] : finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudget model horizon source mu <= finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon source

The finite-arm IID history-adaptive model satisfies self-bounding with the exact policy-weighted realized corruption budget.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLaw_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)

The square-root schedule gives logarithmic regret with the exact expected realized history-adaptive corruption budget.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLawRegret_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)

The generated-law specialization of the expected realized corruption budget, packaged without exposing the trajectory measure to callers.

noncomputable def finiteArmIIDHistoryAdaptiveExpectedRewardCorruptionBudgetForLaw {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (horizon : Nat) : Real

The coefficient-aware refined window evaluated at the generated policy's expected realized history-adaptive corruption.

noncomputable def finiteArmIIDHistoryAdaptiveExpectedRefinedCorruptionWindow {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (horizon : Nat) : Prop

Refined local regret using the policy-weighted realized corruption budget. The compact window discharges the low-level scalar tuning inequalities.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLawRegret_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 : finiteArmIIDHistoryAdaptiveExpectedRefinedCorruptionWindow model armLaw source horizon) : letI : Nonempty (Fin K)

Total regret envelope using the refined expected-corruption expression when there is a suboptimal arm and the compact window holds, and the logarithmic expected-corruption expression otherwise.

noncomputable def finiteArmIIDHistoryAdaptiveExpectedCorruptionAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (horizon : Nat) : Real

With one arm there is no suboptimal coordinate and the expected corruption all-regimes envelope reduces to the logarithmic base term.

theorem finiteArmIIDHistoryAdaptiveExpectedCorruptionAllRegimeBound_fin_one (model : FiniteBanditModel 1) (armLaw : Fin 1 -> Measure Rat) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource 1) (horizon : Nat) : finiteArmIIDHistoryAdaptiveExpectedCorruptionAllRegimeBound model armLaw source horizon = 1 + Real.log (((horizon + 1 : Nat) : Real))

Scheduled half-Tsallis regret for every finite-arm IID history-adaptive reward-shift source and finite horizon, using the policy-weighted realized corruption budget in both automatically selected regimes.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLawRegret_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)) (source : FiniteArmIIDHistoryAdaptiveRewardShiftSource K) (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)

Measurable history-arm-gated suboptimal boosts inherit the all-regimes bound with gate-open corruption weighted by conditional selection probability, rather than the full deterministic boost schedule.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDMeasurableHistoryArmGatedSuboptimalBoostExpectedCorruptionRewardLawRegret_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) (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)