BanditRLProof.Exp3ExpectedRegret

Deterministic EXP3 parameter algebra. If `eta = gamma / K`, exploration is at most one half, and `gamma^2 T` covers `K log K`, then the unoptimized budget is at most `4 gamma T`.

theorem expectedRegretBudget_le_four_mul_gamma_mul_horizon (K T logK eta gamma : Real) (hK : 0 < K) (hT : 0 <= T) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (heta : eta = gamma / K) (hlog_budget : K * logK <= gamma ^ 2 * T) : logK / eta + (eta * (1 / (1 - gamma))) * (K * T) + gamma * T <= 4 * gamma * T

Square-root exploration scale used by the tuned corollary.

noncomputable def tunedExplorationRate (K T : Real) : Real

Learning rate paired with `tunedExplorationRate`.

noncomputable def tunedLearningRate (K T : Real) : Real

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

theorem tunedExplorationRate_pos (K T : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < tunedExplorationRate K T

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

theorem tunedExplorationRate_le_half (K T : Real) (hT : 0 < T) (hscale : 4 * K * Real.log K <= T) : tunedExplorationRate K T <= 1 / 2

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

theorem tunedLearningRate_pos (K T : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < tunedLearningRate K T

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

theorem tunedExplorationRate_sq_mul_eq (K T : Real) (hK_one : 1 < K) (hT : 0 < T) : tunedExplorationRate K T ^ 2 * T = K * Real.log K

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

theorem tunedExplorationRate_mul_eq_sqrt_mul (K T : Real) (hK_one : 1 < K) (hT : 0 < T) : tunedExplorationRate K T * T = Real.sqrt (K * T * Real.log K)

The generated predictable EXP3 trajectory has regret at most `4 gamma horizon` when `eta = gamma / |arms|` and the exploration budget dominates `|arms| log |arms|`.

theorem sampledPredictable_expectedRegret_le_four_mul_gamma_mul_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) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (loss : PredictableLossVector Env Action) (horizon : Nat) (hlog_budget : (arms.card : Real) * Real.log arms.card <= gamma ^ 2 * (horizon : Real)) (comparator : Action) (hcomparator : comparator ∈ arms) : let eta := gamma / (arms.card : Real) let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith) 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)) <= 4 * gamma * (horizon : Real)

Generated predictable EXP3 kernel at the square-root exploration and learning rates. The large-horizon hypotheses discharge the kernel's `0 <= gamma <= 1` contract internally.

noncomputable def tunedPredictableTrajectoryKernel {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Nonempty Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon_pos : 0 < horizon) (hscale : 4 * (arms.card : Real) * Real.log arms.card <= (horizon : Real)) : Kernel Env (Nat -> Action × Real)

Tuned generated-trajectory expected predictable-regret bound. Under the large-horizon regime `4 |A| log |A| <= T`, the square-root exploration and learning rates give the classical `sqrt(|A| T log |A|)` scale.

theorem sampledPredictable_expectedRegret_le_four_mul_sqrt {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) (hhorizon_pos : 0 < horizon) (hscale : 4 * (arms.card : Real) * Real.log arms.card <= (horizon : Real)) (comparator : Action) (hcomparator : comparator ∈ arms) : let K := (arms.card : Real) let T := (horizon : Real) let gamma := tunedExplorationRate K T let eta := tunedLearningRate K T let mu := prior ⊗ₘ tunedPredictableTrajectoryKernel arms harms hcard_two loss horizon hhorizon_pos hscale 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)) <= 4 * Real.sqrt (K * T * Real.log K)