BanditRLProof.TsallisScheduledIIDTimeVaryingMeanGap

A predictable loss vector whose fresh-state evaluator may vary by round.

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

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

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

Equal state prefixes generate equal visible trajectory prefixes for a time-varying fresh-state evaluator.

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

Finite visible-prefix kernel for a time-varying fresh-state evaluator.

noncomputable def sampledScheduledHalfTsallisIIDTimeVaryingPrefixKernel {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Nonempty Action] [DecidableEq Action] (fallback : LossState) (value : Nat -> LossState -> Action -> Real) (hvalue : ∀ t, Measurable (fun input : LossState × Action => value t input.1 input.2)) (hvalue_nonneg : ∀ t state action, 0 <= value t state action) (hvalue_le_one : ∀ t state action, value t 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 canonical trajectory factors through every finite IID state prefix even when the deterministic evaluator varies with time.

theorem hasScheduledIIDPrefixKernelFactorization_sampledScheduledHalfTsallisTimeVaryingTrajectoryKernel {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (fallback : LossState) (value : Nat -> LossState -> Action -> Real) (hvalue : ∀ t, Measurable (fun input : LossState × Action => value t input.1 input.2)) (hvalue_nonneg : ∀ t state action, 0 <= value t state action) (hvalue_le_one : ∀ t state action, value t 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 (iidTimeVaryingLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one).environment) horizon

Mean loss gap of the round-`t` evaluator under its coordinate law.

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

Mean loss gap of the round-`t` evaluator under the common coordinate law.

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

Independent, potentially nonidentically distributed coordinates plus prefix factorization produce the time-varying independence and global-mean contract.

theorem hasScheduledTimeVaryingIndependentMeanGapLaw_of_independentLossState {LossState : Type u} {Action : Type v} [MeasurableSpace LossState] [StandardBorelSpace LossState] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (law : Nat -> Measure LossState) [∀ t, IsProbabilityMeasure (law t)] (value : Nat -> LossState -> Action -> Real) (hvalue : ∀ t, Measurable (fun input : LossState × Action => value t input.1 input.2)) (hvalue_nonneg : ∀ t state action, 0 <= value t state action) (hvalue_le_one : ∀ t state action, value t 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 law let mu := prior ⊗ₘ trajectoryKernel HasScheduledTimeVaryingIndependentMeanGapLaw mu arms (iidTimeVaryingLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one) best (fun t action => independentLossStateTimeVaryingMeanGap law value t best action) horizon

IID coordinates are the constant-law specialization of the independent coordinate producer.

theorem hasScheduledTimeVaryingIndependentMeanGapLaw_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 : Nat -> LossState -> Action -> Real) (hvalue : ∀ t, Measurable (fun input : LossState × Action => value t input.1 input.2)) (hvalue_nonneg : ∀ t state action, 0 <= value t state action) (hvalue_le_one : ∀ t state action, value t 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 HasScheduledTimeVaryingIndependentMeanGapLaw mu arms (iidTimeVaryingLossStatePredictableLossVector value hvalue hvalue_nonneg hvalue_le_one) best (fun t action => iidLossStateTimeVaryingMeanGap law value t best action) horizon