Lean module · EXP3
BanditRLProof.Exp3HighProbabilityRegret
# Generated predictable EXP3 high-probability regret This module completes the finite-horizon high-probability pseudo-regret route for the generated predictable EXP3 trajectory. A pathwise reciprocal-floor bound controls the random estimator-square sum almost surely. The final theorem then combines the sampled Hedge inequality, exploration bias, the pure-Hedge predictable-minus-observed confidence event, and the comparator-estimator confidence event by a two-event union bound. The resulting theorem is valid but uses range-based Hoeffding radii. Their `(|arms| / gamma)^2` per-round proxy is intentionally recorded rather than silently presented as the ideal EXP3.P/Freedman rate.
Module map
Imports
BanditRLProof.Exp3PureConfidence
Imported by
BanditRLProof, BanditRLProof.Exp3BernsteinHighProbabilityRegret, BanditRLProof.Exp3PredictableRegretAllTime, BanditRLProof.Exp3RealizedHighProbabilityRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Exp3.observedMixedSquaredImportanceWeightedLossAt_le_inv_explorationFloor
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem observedMixedSquaredImportanceWeightedLossAt_le_inv_explorationFloor {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (hreward : (sample.2 t).2 ∈ Set.Icc (0 : Real) 1) : observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample <= 1 / (gamma / (arms.card : Real))
theorem
BanditRLProof.Exp3.sampledPredictableTrajectoryMeasure_reward_mem_unitInterval_ae
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableTrajectoryMeasure_reward_mem_unitInterval_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 gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, (sample.2 t).2 ∈ Set.Icc (0 : Real) 1
theorem
BanditRLProof.Exp3.sampledPredictableTrajectoryMeasure_observedMixedSquared_sum_le_ae
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableTrajectoryMeasure_observedMixedSquared_sum_le_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 gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment ∀ᵐ sample ∂mu, (Finset.range horizon).sum (fun t => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample) <= (horizon : Real) * (1 / (gamma / (arms.card : Real)))
def
BanditRLProof.Exp3.sampledPredictableHighProbabilityRegretBudget
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_highProbabilityRegret_tail_delta
Compiled
Generated predictable EXP3 pseudo-regret exceeds the explicit Hedge, exploration, estimator-square, and two confidence-radius budget with probability at most the sum of the pure-q and comparator failure probabilities.
theorem sampledPredictable_highProbabilityRegret_tail_delta {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty 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) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableHighProbabilityRegretBudget arms eta gamma horizon delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta + ENNReal.ofReal delta
theorem
BanditRLProof.Exp3.sampledPredictable_highProbabilityRegret_tail_total_delta
Compiled
Standard total-failure-probability form of the generated predictable EXP3 pseudo-regret bound. Each of the two confidence events receives `delta / 2`, so their union has probability at most `delta`.
theorem sampledPredictable_highProbabilityRegret_tail_total_delta {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty 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) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableHighProbabilityRegretBudget arms eta gamma horizon (delta / 2) <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta