Lean module · EXP3
BanditRLProof.Exp3PredictableRegretAllTime
This module gives every positive prefix of one fixed generated EXP3 process a geometric confidence share and reuses the compiled fixed-horizon pathwise potential, exploration, and comparator assembly. The result is countable outer-measure subadditivity, not a Ville/Doob, mixture, optional-stopping, self-normalized, general Freedman, or tuned horizon-free EXP3 theorem.
Module map
Imports
BanditRLProof.ConcentrationConfidenceSchedule, BanditRLProof.Exp3HighProbabilityRegret
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableRegretGeometricAllTimeBudget
Compiled
The fixed-horizon predictable-regret budget at prefix `n+1`. The outer geometric share is divided by two because the parent total-delta theorem allocates equal shares to its pure-cross and comparator-estimator events.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictableRegretGeometricAllTimeBudgetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sampledPredictableRegretGeometricAllTimeBudget {Action : Type v} (arms : Finset Action) (eta gamma delta : Real) (n : Nat) : Real
def
BanditRLProof.Exp3.sampledPredictableRegretGeometricAllTimeFailureSet
Compiled
Countable predictable-regret failure event over every positive prefix of one generated EXP3 trajectory.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictableRegretGeometricAllTimeFailureSetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sampledPredictableRegretGeometricAllTimeFailureSet {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (comparator : Action) (delta : Real) : Set (Env × ((k : Nat) -> Action × Real))
theorem
BanditRLProof.Exp3.mem_sampledPredictableRegretGeometricAllTimeFailureSet_iff
Compiled
Membership is predictable-regret failure at at least one positive prefix.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.mem_sampledPredictableRegretGeometricAllTimeFailureSet_iffReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem mem_sampledPredictableRegretGeometricAllTimeFailureSet_iff {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (comparator : Action) (delta : Real) (sample : Env × ((k : Nat) -> Action × Real)) : sample ∈ sampledPredictableRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta ↔ ∃ n, sampledPredictableRegretGeometricAllTimeBudget arms eta gamma delta n <= (Finset.range (n + 1)).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range (n + 1)).sum (fun t => predictableLossAt loss t sample comparator)
theorem
BanditRLProof.Exp3.measure_sampledPredictableRegretGeometricAllTimeFailureSet_le
Compiled
On one fixed generated EXP3 process and against one fixed supported comparator, predictable-regret failures over all positive prefixes have outer measure at most the geometric confidence budget.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.measure_sampledPredictableRegretGeometricAllTimeFailureSet_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measure_sampledPredictableRegretGeometricAllTimeFailureSet_le {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) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu (sampledPredictableRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta) <= ENNReal.ofReal delta