BanditRLProof.TsallisFiniteArmIIDHorizonHistoryAdaptiveExpectedCorruptedRewardLaw

Predictable reward shifts and deterministic envelope witnesses needed only for rounds `0, ..., horizon`. Successor data are indexed by `Fin horizon`, so no measurability or boundedness contract is requested after the final round.

structure FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource (K horizon : Nat) where

Successor shift obtained by extending a horizon-local source by zero.

noncomputable def finiteArmIIDHorizonHistoryAdaptiveRewardShiftSuccessor {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Real

Deterministic envelope obtained by extending a horizon-local envelope by zero after its final successor round.

noncomputable def finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (t : Nat) (arm : Fin K) : Real

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

theorem finiteArmIIDHorizonHistoryAdaptiveRewardShiftSuccessor_of_lt {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : n < horizon) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : finiteArmIIDHorizonHistoryAdaptiveRewardShiftSuccessor source n history arm = source.successor ⟨n, hn⟩ history arm

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

theorem finiteArmIIDHorizonHistoryAdaptiveRewardShiftSuccessor_of_le {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : horizon <= n) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : finiteArmIIDHorizonHistoryAdaptiveRewardShiftSuccessor source n history arm = 0

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

theorem finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope_zero {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (arm : Fin K) : finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope source 0 arm = source.initialEnvelope arm

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

theorem finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope_succ_of_lt {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : n < horizon) (arm : Fin K) : finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope source (Nat.succ n) arm = source.successorEnvelope ⟨n, hn⟩ arm

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

theorem finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope_succ_of_le {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : horizon <= n) (arm : Fin K) : finiteArmIIDHorizonHistoryAdaptiveRewardShiftEnvelope source (Nat.succ n) arm = 0

Zero extension of a horizon-local source to the all-time source interface. The supplied simp lemmas show that the extension is unchanged on every round used by the target horizon; it introduces no post-horizon regularity obligation.

noncomputable def FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) : FiniteArmIIDHistoryAdaptiveRewardShiftSource K where

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

theorem FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime_initial {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (arm : Fin K) : source.toAllTime.initial arm = source.initial arm

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

theorem FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime_successor_of_lt {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : n < horizon) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : source.toAllTime.successor n history arm = source.successor ⟨n, hn⟩ history arm

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

theorem FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime_successor_of_le {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : horizon <= n) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : source.toAllTime.successor n history arm = 0

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

theorem FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime_envelope_zero {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (arm : Fin K) : source.toAllTime.envelope 0 arm = source.initialEnvelope arm

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

theorem FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime_envelope_succ_of_lt {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : n < horizon) (arm : Fin K) : source.toAllTime.envelope (Nat.succ n) arm = source.successorEnvelope ⟨n, hn⟩ arm

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

theorem FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource.toAllTime_envelope_succ_of_le {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (n : Nat) (hn : horizon <= n) (arm : Fin K) : source.toAllTime.envelope (Nat.succ n) arm = 0

Predictable clipped loss attached to the zero extension of a horizon-local reward-shift source.

noncomputable def finiteArmIIDHorizonHistoryAdaptiveCorruptedRewardLoss {K horizon : Nat} (source : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon)

Exact generated-policy expected-corruption budget of a horizon-local source. Only rounds through `horizon` occur in the finite sum.

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

All-regimes expected-corruption envelope for a horizon-local source.

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

Scheduled half-Tsallis regret under a finite-arm IID reward law and a history-adaptive reward-shift source whose regularity contract stops at the target horizon. The conclusion uses the exact generated-policy expected corruption and internally selects the refined or logarithmic branch.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDHorizonHistoryAdaptiveExpectedCorruptedRewardLawRegret_le_allRegimes {K horizon : 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 : FiniteArmIIDHorizonHistoryAdaptiveRewardShiftSource K horizon) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (hgapLeOne : forall arm, arm ≠ model.bestArm -> ((model.gap arm : Rat) : Real) <= 1) : letI : Nonempty (Fin K)