BanditRLProof.TsallisScheduledIIDMeanGap

A predictable loss vector obtained by reading one fresh loss state at each time. Joint measurability of `value` is the sole evaluation regularity contract; pointwise bounds make this a valid `[0,1]` loss process.

def iidLossStatePredictableLossVector {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) : Exp3.PredictableLossVector (Nat -> LossState) Action where

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

theorem predictableLossAt_iidLossStatePredictableLossVector {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) (t : Nat) (sample : (Nat -> LossState) × ((k : Nat) -> Action × Real)) (action : Action) : Exp3.predictableLossAt (iidLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one) t sample action = value (sample.1 t) action

Extend a finite loss-state prefix to an infinite stream by a fixed fallback state after the prefix endpoint.

def extendLossStatePrefix {LossState : Type u} (fallback : LossState) (n : Nat) (statePrefix : (i : Finset.Iic n) -> LossState) : Nat -> LossState

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

theorem measurable_extendLossStatePrefix {LossState : Type u} [MeasurableSpace LossState] (fallback : LossState) (n : Nat) : Measurable (extendLossStatePrefix fallback n)

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

theorem extendLossStatePrefix_apply_of_le {LossState : Type u} (fallback : LossState) (n t : Nat) (ht : t <= n) (statePrefix : (i : Finset.Iic n) -> LossState) : extendLossStatePrefix fallback n statePrefix t = statePrefix ⟨t, Finset.mem_Iic.mpr ht⟩

The visible scheduled trajectory prefix generated from an IID loss-state stream is unchanged when the stream is replaced by any other stream with the same finite loss-state prefix.

theorem sampledScheduledHalfTsallisTrajectoryKernel_map_frestrictLe_eq_of_iidLossState_prefix_eq {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (environment₁ environment₂ : Nat -> LossState) (n : Nat) (henvironment : Preorder.frestrictLe n environment₁ = Preorder.frestrictLe n environment₂) : (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector (iidLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one).environment environment₁).map (Preorder.frestrictLe n) = (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector (iidLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one).environment environment₂).map (Preorder.frestrictLe n)

Finite pair-prefix kernel obtained by extending the supplied loss-state prefix and running the canonical scheduled trajectory.

noncomputable def sampledScheduledHalfTsallisIIDPrefixKernel {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Nonempty Action] [DecidableEq Action] (fallback : LossState) (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) (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)

The stationary mean loss gap induced by one coordinate law.

noncomputable def iidLossStateMeanGap {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] (law : Measure LossState) (value : LossState -> Action -> Real) (best action : Action) : Real

Exact remaining trajectory-law obligation for the IID route. At every scheduled successor time, the generated visible pair prefix is a Markov-kernel extension of the corresponding finite loss-state prefix.

def HasScheduledIIDPrefixKernelFactorization {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] (trajectoryKernel : Kernel (Nat -> LossState) ((k : Nat) -> Action × Real)) (horizon : Nat) : Prop

The canonical scheduled half-Tsallis trajectory automatically factors through every finite IID loss-state prefix.

theorem hasScheduledIIDPrefixKernelFactorization_sampledScheduledHalfTsallisTrajectoryKernel {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (fallback : LossState) (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (horizon : Nat) : HasScheduledIIDPrefixKernelFactorization (sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector (iidLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one).environment) horizon

Infinite-product loss states plus finite-prefix factorization produce the independence and global-mean contract consumed by scheduled self-bounding.

theorem hasScheduledIndependentMeanGapLaw_of_iidLossState {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (law : Measure LossState) [IsProbabilityMeasure law] (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) (arms : Finset Action) (best : Action) (horizon : Nat) (trajectoryKernel : Kernel (Nat -> LossState) ((k : Nat) -> Action × Real)) [IsMarkovKernel trajectoryKernel] (hfactor : HasScheduledIIDPrefixKernelFactorization trajectoryKernel horizon) : let prior := Measure.infinitePi (fun _ : Nat => law) let mu := prior ⊗ₘ trajectoryKernel HasScheduledIndependentMeanGapLaw mu arms (iidLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one) best (iidLossStateMeanGap law value best) horizon

The canonical scheduled half-Tsallis trajectory reaches the explicit logarithmic bound for an IID loss-state environment. Its finite-prefix factorization is constructed internally.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_log_iidLossState {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (law : Measure LossState) [IsProbabilityMeasure law] (value : LossState -> Action -> Real) (hvalue : Measurable (fun input : LossState × Action => value input.1 input.2)) (hvalue_nonneg : ∀ state action, 0 <= value state action) (hvalue_le_one : ∀ state action, value state action <= 1) (arms : Finset Action) (harms : arms.Nonempty) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < iidLossStateMeanGap law value best action) (corruption : Real) (hcorruption : 0 <= corruption) : let prior := Measure.infinitePi (fun _ : Nat => law) let loss := iidLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= (1 + Real.log (((horizon + 1 : Nat) : Real))) * (1 + 25 * (arms.erase best).sum (fun action => 1 / iidLossStateMeanGap law value best action)) + corruption