BanditRLProof.Exp3UniformRegret

Any generated predictable EXP3 process has expected exploration-mixed regret at most the horizon, independently of the learning rate.

theorem sampledPredictable_exploredExpectedRegret_le_horizon {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 gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) <= (horizon : Real)

The same horizon bound for the scalar losses actually generated by the predictable environment.

theorem sampledPredictable_realizedExpectedRegret_le_horizon {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 gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) <= (horizon : Real)

Exploration rate clipped to the range supported uniformly by the compiled expected-regret route.

noncomputable def clippedExplorationRate (K T : Real) : Real

Learning rate paired with `clippedExplorationRate`.

noncomputable def clippedLearningRate (K T : Real) : Real

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

theorem clippedExplorationRate_nonneg (K T : Real) : 0 <= clippedExplorationRate K T

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

theorem clippedExplorationRate_le_half (K T : Real) : clippedExplorationRate K T <= 1 / 2

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

theorem clippedExplorationRate_eq_tuned (K T : Real) (h : tunedExplorationRate K T <= 1 / 2) : clippedExplorationRate K T = tunedExplorationRate K T

Generated predictable EXP3 kernel using the clipped all-horizon rates.

noncomputable def clippedPredictableTrajectoryKernel {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Nonempty Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (loss : PredictableLossVector Env Action) (horizon : Nat) : Kernel Env (Nat -> Action × Real)

Uniform-horizon expected regret for the scalar loss actually generated by predictable EXP3. The minimum records the trivial short-horizon budget and the large-horizon square-root theorem without imposing a regime assumption.

theorem sampledPredictable_clippedRealizedExpectedRegret_le_min {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) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let K := (arms.card : Real) let T := (horizon : Real) let mu := prior ⊗ₘ clippedPredictableTrajectoryKernel arms harms loss horizon integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) <= min T (4 * Real.sqrt (K * T * Real.log K))