Lean module · EXP3
BanditRLProof.Exp3ExplorationBias
# Exploration bias for concrete sampled EXP3 This module compares the pure exponential-weights distribution `q_t` used by the Hedge potential with the exploration-mixed sampling distribution `p_t = (1 - gamma) q_t + gamma / |arms|`. The final finite-horizon theorem gives both inequalities needed before the almost-sure Hedge bound can be integrated: actual predictable loss is at most pure-distribution predictable loss plus `gamma` per round, and the pure estimator square is controlled by the actual probability-mixed estimator square with factor `1 / (1 - gamma)`.
Module map
Imports
BanditRLProof.Exp3PredictableHedge
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Exp3.distribution_le_sampledTrajectoryProbabilityAt_div_one_sub_gamma
Compiled
A pure Hedge coordinate is at most the corresponding explored probability divided by `1 - gamma`.
theorem distribution_le_sampledTrajectoryProbabilityAt_div_one_sub_gamma {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_lt_one : gamma < 1) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (action : Action) : distribution arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t action <= sampledTrajectoryProbabilityAt arms eta gamma t sample action / (1 - gamma)
theorem
BanditRLProof.Exp3.mixedSquaredLoss_sampledTrajectoryObservedLoss_le_inv_one_sub_gamma
Compiled
The pure-Hedge estimator square is bounded by the explored-probability mixed square with the standard `1 / (1 - gamma)` factor.
theorem mixedSquaredLoss_sampledTrajectoryObservedLoss_le_inv_one_sub_gamma {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_lt_one : gamma < 1) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : mixedSquaredLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t <= (1 / (1 - gamma)) * observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample
theorem
BanditRLProof.Exp3.sampledTrajectoryPredictableMixedLoss_le_pure_add_gamma
Compiled
Exploration changes one predictable `[0,1]` mixed loss by at most `gamma` relative to the pure Hedge distribution.
theorem sampledTrajectoryPredictableMixedLoss_le_pure_add_gamma {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : arms.sum (fun action => sampledTrajectoryProbabilityAt arms eta gamma t sample action * predictableLossAt loss t sample action) <= arms.sum (fun action => distribution arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t action * predictableLossAt loss t sample action) + gamma
theorem
BanditRLProof.Exp3.sampledTrajectory_finiteHorizon_explorationBias_secondMoment
Compiled
Finite-horizon exploration bias and second-moment comparison on one concrete sampled trajectory.
theorem sampledTrajectory_finiteHorizon_explorationBias_secondMoment {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : ((Finset.range horizon).sum (fun t => arms.sum (fun action => sampledTrajectoryProbabilityAt arms eta gamma t sample action * predictableLossAt loss t sample action)) <= (Finset.range horizon).sum (fun t => arms.sum (fun action => distribution arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t action * predictableLossAt loss t sample action)) + gamma * (horizon : Real)) ∧ ((Finset.range horizon).sum (fun t => mixedSquaredLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t) <= (1 / (1 - gamma)) * (Finset.range horizon).sum (fun t => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample))