Lean module · EXP3
BanditRLProof.Exp3RealizedPredictableVarianceTail
# Predictable-variance tail for realized EXP3 loss This module iterates the exact selected-loss variance-compensated conditional MGF along the generated trajectory. It yields a Bernstein-shaped upper tail for realized-minus-predictable selected loss jointly with a pathwise budget on the cumulative selected-loss predictable variance.
Module map
Imports
BanditRLProof.Exp3RealizedPredictableVariance
Imported by
BanditRLProof.Exp3MixedSquarePredictableVarianceRealizedDoublePredictableVarianceHighProbabilityRegret, BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedDoublePredictableVarianceHighProbabilityRegret, BanditRLProof.Exp3RealizedPredictableVarianceAllTime, BanditRLProof.Exp3RealizedPredictableVarianceMaximal
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableRealizedCompensatedProcess
Compiled
Shifted exact-variance compensated realized-loss process.
noncomputable def sampledPredictableRealizedCompensatedProcess {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma tilt : Real) (loss : PredictableLossVector Env Action) : Nat → Env × ((k : Nat) → Action × Real) → Real
theorem
BanditRLProof.Exp3.sampledPredictableRealizedCompensatedProcess_stronglyAdapted
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedCompensatedProcess_stronglyAdapted {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma tilt : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableRealizedCompensatedProcess arms eta gamma tilt loss)
theorem
BanditRLProof.Exp3.sampledPredictableRealizedCompensatedProcess_sum_range_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedCompensatedProcess_sum_range_succ {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma tilt : Real) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : (Finset.range (horizon + 1)).sum (fun i => sampledPredictableRealizedCompensatedProcess arms eta gamma tilt loss i sample) = tilt * (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample) - tilt ^ 2 * (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample)
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_sum_tail_predictableVariance_fixedTilt
Compiled
Fixed-tilt upper tail retaining the random cumulative selected-loss predictable variance.
theorem sampledPredictableRealizedDeviation_sum_tail_predictableVariance_fixedTilt {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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (tilt : Real) (htilt_nonneg : 0 ≤ tilt) (htilt_le_one : tilt ≤ 1) (threshold varianceBudget : Real) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | threshold ≤ (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample) ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ ENNReal.ofReal (Real.exp (-tilt * threshold + tilt ^ 2 * varianceBudget))
def
BanditRLProof.Exp3.sampledRealizedPredictableVarianceRadius
Compiled
Bernstein radius for realized selected-loss deviation under a pathwise predictable-variance budget.
noncomputable def sampledRealizedPredictableVarianceRadius (varianceBudget delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_sum_tail_predictableVariance_delta
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviation_sum_tail_predictableVariance_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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | sampledRealizedPredictableVarianceRadius varianceBudget delta ≤ (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample) ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ ENNReal.ofReal delta