Lean module · EXP3
BanditRLProof.Exp3PredictableHedge
# Almost-sure Hedge control for predictable sampled EXP3 This module discharges the pathwise nonnegative-feedback premise of `Exp3SampledHedge` from the generated predictable `[0,1]` reward law. It first aggregates the time-zero and successor reward identifications into one finite-horizon almost-sure event, then applies the concrete pathwise Hedge bound on that event. The endpoint remains an almost-sure inequality. Integrating it and comparing the pure Hedge distribution with the exploration-mixed sampling distribution are separate downstream steps.
Module map
Imports
BanditRLProof.Exp3SampledHedge
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.sampledPredictableTrajectoryMeasure_reward_nonneg_ae
Compiled
Every observed scalar reward is nonnegative almost surely under the generated predictable sampled-EXP3 trajectory law.
theorem sampledPredictableTrajectoryMeasure_reward_nonneg_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, 0 <= (sample.2 t).2
theorem
BanditRLProof.Exp3.sampledPredictableTrajectoryMeasure_finiteHorizon_reward_nonneg_ae
Compiled
One common almost-sure event supplies reward nonnegativity at every time strictly before a finite horizon.
theorem sampledPredictableTrajectoryMeasure_finiteHorizon_reward_nonneg_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) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, ∀ t, t < horizon -> 0 <= (sample.2 t).2
theorem
BanditRLProof.Exp3.sampledPredictableTrajectoryMeasure_hedge_regret_le_ae
Compiled
The concrete finite-horizon Hedge inequality holds almost surely on the generated predictable sampled-EXP3 trajectory.
theorem sampledPredictableTrajectoryMeasure_hedge_regret_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) (heta : 0 < eta) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, (Finset.range horizon).sum (fun t => mixedLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t) - cumulativeLoss (sampledTrajectoryObservedLoss arms eta gamma sample) horizon comparator <= Real.log arms.card / eta + eta * (Finset.range horizon).sum (fun t => mixedSquaredLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t)
theorem
BanditRLProof.Exp3.sampledPredictableScoreHedge_ae
Compiled
The same almost-sure inequality with the comparator cumulative estimator exposed as the inclusive concrete sampled history score.
theorem sampledPredictableScoreHedge_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) (heta : 0 < eta) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (n : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, (Finset.range (n + 1)).sum (fun t => mixedLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t) - sampledHistoryScore arms eta gamma n (Preorder.frestrictLe n sample.2) comparator <= Real.log arms.card / eta + eta * (Finset.range (n + 1)).sum (fun t => mixedSquaredLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t)