BanditRLProof.TsallisScheduledExpectedRegret

Predictable importance-weighted loss using the scheduled probability at the same actual trajectory time.

noncomputable def sampledScheduledHalfTsallisPredictableEstimatedLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action -> Real

Predictable environment regret of the scheduled generated probabilities against a fixed comparator through the inclusive terminal time.

noncomputable def sampledScheduledHalfTsallisPredictableEnvironmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Finite-horizon scheduled regret after replacing stored rewards by the predictable importance-weighted loss vectors.

noncomputable def sampledScheduledHalfTsallisPredictableEstimatedRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

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

theorem measurable_sampledScheduledHalfTsallisProbabilityAtTime {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample candidate)

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

theorem measurable_sampledScheduledHalfTsallisPredictableEstimatedLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledScheduledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample candidate)

Deterministic predictable feedback identifies each stored-reward scheduled estimator with its predictable counterpart almost surely.

theorem sampledScheduledHalfTsallisObservedEstimatedLossAt_eq_predictable_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (fun sample => sampledScheduledHalfTsallisObservedEstimatedLossAt arms harms eta t sample) =ᵐ[mu] (fun sample => sampledScheduledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)

At each scheduled time, the mixed and comparator-weighted predictable IW estimators are integrable and have their corresponding environment first moments.

theorem sampledScheduledHalfTsallisPredictableEstimatedLossAt_first_moments {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (t : Nat) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (Integrable (fun sample => FTRL.linearLoss arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample) (sampledScheduledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) mu ∧ Integrable (fun sample => FTRL.linearLoss arms q (sampledScheduledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) mu) ∧ ((integral mu (fun sample => FTRL.linearLoss arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample) (sampledScheduledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) = integral mu (fun sample => FTRL.linearLoss arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample) (Exp3.predictableLossAt loss t sample))) ∧ (integral mu (fun sample => FTRL.linearLoss arms q (sampledScheduledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) = integral mu (fun sample => FTRL.linearLoss arms q (Exp3.predictableLossAt loss t sample))))

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

theorem finiteSimplex_sampledScheduledHalfTsallisProbabilityAtTime {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : FTRL.finiteSimplex arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample)

Current scheduled mixed predictable loss and a fixed-comparator predictable loss are integrable at every actual time.

theorem integrable_sampledScheduledHalfTsallisPredictableLinearLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (t : Nat) : Integrable (fun sample => FTRL.linearLoss arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample) (Exp3.predictableLossAt loss t sample)) mu ∧ Integrable (fun sample => FTRL.linearLoss arms q (Exp3.predictableLossAt loss t sample)) mu

Predictable scheduled estimated regret is integrable and has exactly the same finite-horizon integral as predictable environment regret.

theorem integral_sampledScheduledHalfTsallisPredictableEstimatedRegret_eq_environmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon : Nat) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (sampledScheduledHalfTsallisPredictableEstimatedRegret arms harms eta loss q horizon) mu ∧ Integrable (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) mu ∧ integral mu (sampledScheduledHalfTsallisPredictableEstimatedRegret arms harms eta loss q horizon) = integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon)

Observed scheduled estimated regret agrees almost surely with the predictable-estimator version over every finite horizon.

theorem sampledScheduledHalfTsallisEstimatedRegret_eq_predictable_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (horizon : Nat) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment sampledScheduledHalfTsallisEstimatedRegret arms harms eta q horizon =ᵐ[mu] sampledScheduledHalfTsallisPredictableEstimatedRegret arms harms eta loss q horizon

Observed scheduled IW regret is integrable and has exactly the predictable environment-regret integral.

theorem integral_sampledScheduledHalfTsallisEstimatedRegret_eq_environmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon : Nat) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (sampledScheduledHalfTsallisEstimatedRegret arms harms eta q horizon) mu ∧ Integrable (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) mu ∧ integral mu (sampledScheduledHalfTsallisEstimatedRegret arms harms eta q horizon) = integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon)

Observed scheduled IW regret is integrable and has exactly the predictable environment-regret integral. -/ theorem integral_sampledScheduledHalfTsallisEstimatedRegret_eq_environmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon : Nat) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (sampledScheduledHalfTsallisEstimatedRegret arms harms eta q horizon) mu ∧ Integrable (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) mu ∧ integral mu (sampledScheduledHalfTsallisEstimatedRegret arms harms eta q horizon) = integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) := by dsimp only let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment have hpredictable := integral_sampledScheduledHalfTsallisPredictableEstimatedRegret_eq_environmentRegret prior arms harms eta loss q hq horizon dsimp only at hpredictable have hae := sampledScheduledHalfTsallisEstimatedRegret_eq_predictable_ae prior arms harms eta loss q horizon dsimp only at hae have hobserved : Integrable (sampledScheduledHalfTsallisEstimatedRegret arms harms eta q horizon) mu := hpredictable.1.congr hae.symm exact ⟨hobserved, hpredictable.2.1, (integral_congr_ae hae).trans hpredictable.2.2⟩ /-! The theorem below is the generated-trajectory scheduled regret endpoint of this module. The rate schedule is only required to be positive on the finite horizon and nonincreasing between included rounds. Each stability term uses the refined branch when its local rate is at most `1 / 2`, and the compiled constant-one fallback otherwise.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_allRateBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (heta : forall t, t <= horizon -> 0 < eta t) (hetaMono : forall t, t < horizon -> eta (t + 1) <= eta t) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) <= integral mu (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)) + halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (eta 0)) / eta horizon - 1 / eta horizon