Lean module · EXP3

BanditRLProof.Exp3RandomSquareHighProbabilityRegret

# Random estimator-square EXP3 high-probability regret The pathwise EXP3 assembly bounds the mixed importance-weighted estimator-square sum by `|arms| * T / gamma`. Its expectation is at most `|arms| * T`. This module turns that expectation bound into a Markov tail and includes the square event beside the two existing Bernstein confidence events. The resulting regret theorem removes the reciprocal exploration factor from the Hedge-square budget, at the honest cost of a `1 / deltaSquare` failure allocation.

Module map

Source: BanditRLProof/Exp3RandomSquareHighProbabilityRegret.lean
Teaching chapter: 7. EXP3 and adversarial concentration
Declarations: 9
Placeholders: 0

Imports

BanditRLProof.Exp3BernsteinHighProbabilityRegret, BanditRLProof.Exp3PredictableIntegration

Imported by

BanditRLProof, BanditRLProof.Exp3MixedSquareConfidence, BanditRLProof.Exp3RandomSquareBernsteinRealizedHighProbabilityRegret

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.Exp3.sampledObservedMixedSquaredSum Compiled

Finite-horizon sum of the probability-mixed squared importance-weighted loss estimates observed on a sampled trajectory.

noncomputable def sampledObservedMixedSquaredSum {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Source line 23 Chapter context: EXP3

theorem BanditRLProof.Exp3.observedMixedSquaredImportanceWeightedLossAt_nonneg Compiled

Each observed mixed estimator square is pointwise nonnegative.

theorem observedMixedSquaredImportanceWeightedLossAt_nonneg {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : 0 <= observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample

Source line 31 Chapter context: EXP3

theorem BanditRLProof.Exp3.sampledObservedMixedSquaredSum_nonneg Compiled

The finite-horizon observed mixed estimator-square sum is pointwise nonnegative.

theorem sampledObservedMixedSquaredSum_nonneg {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : 0 <= sampledObservedMixedSquaredSum arms eta gamma horizon sample

Source line 49 Chapter context: EXP3

theorem BanditRLProof.Exp3.measurable_sampledObservedMixedSquaredSum Compiled

The finite-horizon observed mixed estimator-square sum is measurable.

theorem measurable_sampledObservedMixedSquaredSum {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (horizon : Nat) : Measurable (sampledObservedMixedSquaredSum arms eta gamma horizon : (Env × ((k : Nat) -> Action × Real)) -> Real)

Source line 62 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_sampledPredictableObservedMixedSquaredSum Compiled

The generated finite-horizon observed mixed estimator-square sum is integrable.

theorem integrable_sampledPredictableObservedMixedSquaredSum {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 Integrable (sampledObservedMixedSquaredSum arms eta gamma horizon) mu

Source line 79 Chapter context: EXP3

theorem BanditRLProof.Exp3.sampledPredictableObservedMixedSquared_sum_tail_markov Compiled

Markov tail for the random finite-horizon estimator-square sum. Its threshold is `|arms| * T / deltaSquare`, with no reciprocal exploration-rate factor.

theorem sampledPredictableObservedMixedSquared_sum_tail_markov {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) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (deltaSquare : Real) (hdeltaSquare : 0 < deltaSquare) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | (arms.card : Real) * (horizon : Real) / deltaSquare <= sampledObservedMixedSquaredSum arms eta gamma horizon sample} <= ENNReal.ofReal deltaSquare

Source line 108 Chapter context: EXP3

def BanditRLProof.Exp3.sampledPredictableRandomSquareBernsteinHighProbabilityRegretBudget Compiled

Predictable regret budget with a caller-visible random-square failure allocation and the two variance-sensitive confidence radii.

noncomputable def sampledPredictableRandomSquareBernsteinHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (deltaSquare deltaConfidence : Real) : Real

Source line 184 Chapter context: EXP3

theorem BanditRLProof.Exp3.sampledPredictable_randomSquareBernsteinHighProbabilityRegret_tail Compiled

Generated predictable EXP3 regret with a Markov estimator-square event and the two compiled Bernstein confidence events.

theorem sampledPredictable_randomSquareBernsteinHighProbabilityRegret_tail {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) (deltaSquare deltaConfidence : Real) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableRandomSquareBernsteinHighProbabilityRegretBudget arms eta gamma horizon deltaSquare deltaConfidence <= (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 deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence

Source line 198 Chapter context: EXP3

theorem BanditRLProof.Exp3.sampledPredictable_randomSquareBernsteinHighProbabilityRegret_tail_total_delta Compiled

Total-failure form: the estimator-square event and both Bernstein confidence events each receive `delta / 3`.

theorem sampledPredictable_randomSquareBernsteinHighProbabilityRegret_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 | sampledPredictableRandomSquareBernsteinHighProbabilityRegretBudget arms eta gamma horizon (delta / 3) (delta / 3) <= (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

Source line 359 Chapter context: EXP3