Lean module · EXP3
BanditRLProof.Exp3RealizedDeviationTail
# Finite-horizon realized EXP3 concentration This module shifts the generated predictable realized-deviation process by one time step so that its deterministic zero initial value and every actual round fit Mathlib's conditional sub-Gaussian sum theorem. The resulting public theorem bounds the full finite-horizon realized-minus-exploration-mixed loss sum under a probability environment prior.
Module map
Imports
BanditRLProof.Exp3RealizedConcentration
Imported by
BanditRLProof, BanditRLProof.Exp3ComparatorConfidence, BanditRLProof.Exp3RealizedConfidence
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Exp3.sampledPredictableSelectedDeviation_zero_hasCondSubgaussianMGF
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableSelectedDeviation_zero_hasCondSubgaussianMGF {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) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ProbabilityTheory.HasCondSubgaussianMGF ((inferInstance : MeasurableSpace Env).comap (fun sample : Env × ((k : Nat) -> Action × Real) => sample.1)) measurable_fst.comap_le (sampledTrajectorySelectedDeviationAt arms eta gamma loss 0) (Concentration.intervalVarianceProxy 0 1) mu
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_zero_hasCondSubgaussianMGF
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviation_zero_hasCondSubgaussianMGF {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) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ProbabilityTheory.HasCondSubgaussianMGF ((inferInstance : MeasurableSpace Env).comap (fun sample : Env × ((k : Nat) -> Action × Real) => sample.1)) measurable_fst.comap_le (sampledTrajectoryRealizedDeviationAt arms eta gamma loss 0) (Concentration.intervalVarianceProxy 0 1) mu
def
BanditRLProof.Exp3.sampledPredictableDeviationFiltration
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def sampledPredictableDeviationFiltration (Env : Type u) (Action : Type v) [MeasurableSpace Env] [MeasurableSpace Action] : Filtration Nat (inferInstance : MeasurableSpace (Env × ((k : Nat) -> Action × Real))) where
theorem
BanditRLProof.Exp3.sampledPredictableDeviationFiltration_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableDeviationFiltration_zero (Env : Type u) (Action : Type v) [MeasurableSpace Env] [MeasurableSpace Action] : sampledPredictableDeviationFiltration Env Action 0 = (inferInstance : MeasurableSpace Env).comap (fun sample : Env × ((k : Nat) -> Action × Real) => sample.1)
theorem
BanditRLProof.Exp3.sampledPredictableDeviationFiltration_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableDeviationFiltration_succ (Env : Type u) (Action : Type v) [MeasurableSpace Env] [MeasurableSpace Action] (i : Nat) : sampledPredictableDeviationFiltration Env Action (i + 1) = (inferInstance : MeasurableSpace (Env × History.FinitePairHistory Action Real i)).comap (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe i sample.2))
def
BanditRLProof.Exp3.sampledPredictableRealizedDeviationProcess
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableRealizedDeviationProcess {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) : Nat -> Env × ((k : Nat) -> Action × Real) -> Real | 0, _sample => 0 | i + 1, sample => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample noncomputable def sampledPredictableRealizedDeviationProxy : Nat -> NNReal | 0 => 0 | _i + 1 => Concentration.intervalVarianceProxy 0 1 theorem sampledPredictableRealizedDeviationProcess_stronglyAdapted {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) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableRealizedDeviationProcess arms eta gamma loss)
def
BanditRLProof.Exp3.sampledPredictableRealizedDeviationProxy
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableRealizedDeviationProxy : Nat -> NNReal | 0 => 0 | _i + 1 => Concentration.intervalVarianceProxy 0 1 theorem sampledPredictableRealizedDeviationProcess_stronglyAdapted {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) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableRealizedDeviationProcess arms eta gamma loss)
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviationProcess_stronglyAdapted
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviationProcess_stronglyAdapted {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) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableRealizedDeviationProcess arms eta gamma loss)
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviationProcess_sum_range_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviationProcess_sum_range_succ {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : (Finset.range (horizon + 1)).sum (fun i => sampledPredictableRealizedDeviationProcess arms eta gamma loss i sample) = (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample)
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviationProxy_sum_range_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviationProxy_sum_range_succ (horizon : Nat) : (Finset.range (horizon + 1)).sum sampledPredictableRealizedDeviationProxy = (horizon : NNReal) * Concentration.intervalVarianceProxy 0 1
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_sum_tail_ennreal
Compiled
Finite-horizon one-sided concentration for the realized predictable EXP3 deviation from its exploration-mixed conditional mean.
theorem sampledPredictableRealizedDeviation_sum_tail_ennreal {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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) {eps : Real} (heps : 0 <= eps) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment mu {sample | eps <= (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((((horizon : NNReal) * Concentration.intervalVarianceProxy 0 1 : NNReal)) : Real))))