Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledIIDHistoryAdaptive
# History-adaptive predictable losses on IID states The loss chosen at a successor round may inspect the complete pre-action pair history. It may inspect the fresh IID state only through the current state coordinate. This coordinate-locality contract is exactly what is needed for the canonical visible trajectory to factor through every finite state prefix.
Module map
Imports
BanditRLProof.TsallisScheduledIIDMeanGap
Imported by
BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLaw
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.Tsallis.HasIIDStateCoordinateLocality
Compiled
A predictable loss family reads state coordinate `0` initially and state coordinate `n + 1` after a history of length `n + 1`. The successor value may otherwise depend arbitrarily and measurably on that pre-action history.
structure HasIIDStateCoordinateLocality {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] (loss : Exp3.PredictableLossVector (Nat -> LossState) Action) : Prop where
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisTrajectoryKernel_map_frestrictLe_eq_of_iidStateCoordinateLocality_prefix_eq
Compiled
Equal IID state prefixes generate equal visible trajectory prefixes for a history-adaptive coordinate-local predictable loss family.
theorem sampledScheduledHalfTsallisTrajectoryKernel_map_frestrictLe_eq_of_iidStateCoordinateLocality_prefix_eq {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (loss : Exp3.PredictableLossVector (Nat -> LossState) Action) (hlocal : HasIIDStateCoordinateLocality loss) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (environment1 environment2 : Nat -> LossState) (n : Nat) (henvironment : Preorder.frestrictLe n environment1 = Preorder.frestrictLe n environment2) : (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment environment1).map (Preorder.frestrictLe n) = (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment environment2).map (Preorder.frestrictLe n)
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisIIDHistoryAdaptivePrefixKernel
Compiled
Finite visible-prefix kernel induced by a coordinate-local predictable loss family on an IID state trace.
noncomputable def sampledScheduledHalfTsallisIIDHistoryAdaptivePrefixKernel {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Nonempty Action] [DecidableEq Action] (fallback : LossState) (loss : Exp3.PredictableLossVector (Nat -> LossState) Action) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Kernel ((i : Finset.Iic n) -> LossState) (History.FinitePairHistory Action Real n)
theorem
BanditRLProof.Tsallis.hasScheduledIIDPrefixKernelFactorization_sampledScheduledHalfTsallisHistoryAdaptiveTrajectoryKernel
Compiled
The canonical scheduled trajectory of a history-adaptive coordinate-local loss family factors through every finite IID state prefix.
theorem hasScheduledIIDPrefixKernelFactorization_sampledScheduledHalfTsallisHistoryAdaptiveTrajectoryKernel {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (fallback : LossState) (loss : Exp3.PredictableLossVector (Nat -> LossState) Action) (hlocal : HasIIDStateCoordinateLocality loss) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (horizon : Nat) : HasScheduledIIDPrefixKernelFactorization (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment) horizon