Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsity
# Sparse realized EXP3 regret with two pathwise variance budgets Outside the explicit sparsity-failure event, the mixed-square predictable variance is bounded by `(1 / (gamma / K)) * (S * T)` and the exact selected-loss predictable variance is bounded by `S * T`. Four confidence events receive `delta / 4`, and the common sparsity-failure set is charged exactly once.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsity, BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedDoublePredictableVarianceHighProbabilityRegret
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.sampledPredictableSparseRealizedVarianceBudget
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableSparseRealizedVarianceBudget (horizon sparsity : Nat) : Real
theorem
BanditRLProof.Exp3.sampledPredictableRealizedVarianceSum_le_sparseRealizedVarianceBudget_or_mem_sparsityFailure
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedVarianceSum_le_sparseRealizedVarianceBudget_or_mem_sparsityFailure {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) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) (sample : Env × ((k : Nat) → Action × Real)) : (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) ≤ sampledPredictableSparseRealizedVarianceBudget horizon sparsity ∨ sample ∈ sampledPredictableSparsityFailure arms loss horizon sparsity
def
BanditRLProof.Exp3.sampledPredictableDoubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegretBudget
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableDoubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_doubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegret_tail_off_sparsityFailure
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictable_doubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegret_tail_off_sparsityFailure {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 sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu ({sample | sampledPredictableDoubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegretBudget arms eta gamma horizon sparsity delta ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} \ sampledPredictableSparsityFailure arms loss horizon sparsity) ≤ ENNReal.ofReal delta
theorem
BanditRLProof.Exp3.sampledPredictable_doubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegret_tail
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictable_doubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegret_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 sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableDoubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegretBudget arms eta gamma horizon sparsity delta ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} ≤ ENNReal.ofReal delta + mu (sampledPredictableSparsityFailure arms loss horizon sparsity)
theorem
BanditRLProof.Exp3.sampledPredictable_doubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegret_tail_of_sparsityFailure_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictable_doubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegret_tail_of_sparsityFailure_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) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) (hfailure : (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment) (sampledPredictableSparsityFailure arms loss horizon sparsity) ≤ ENNReal.ofReal epsilon) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableDoubleVarianceProbabilisticSparseLossRealizedHighProbabilityRegretBudget arms eta gamma horizon sparsity delta ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} ≤ ENNReal.ofReal delta + ENNReal.ofReal epsilon