Lean module · EXP3
BanditRLProof.Exp3RealizedConcentration
# EXP3 realized-loss concentration This module identifies the successor action law inside `condExpKernel` without requiring a countable ambient action type. It then freezes the predictable environment/history coordinates and applies the bounded centered Hoeffding MGF bound to the selected and realized one-step loss deviations.
Module map
Imports
BanditRLProof.Exp3RealizedRegret, BanditRLProof.ConditionalExpectationReward, BanditRLProof.ConcentrationSubGaussian
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Exp3.condExpKernel_map_eq_finiteActionMeasure_of_condDistrib_ae_eq
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem condExpKernel_map_eq_finiteActionMeasure_of_condDistrib_ae_eq {Omega : Type u} {Condition : Type v} {Action : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [mCondition : MeasurableSpace Condition] [mAction : MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (X : Omega -> Action) (Y : Omega -> Condition) (hX : @Measurable Omega Action mOmega mAction X) (hY : @Measurable Omega Condition mOmega mCondition Y) (arms : Finset Action) (prob : Condition -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (hcond : Filter.EventuallyEq (ae (mu.map Y)) (condDistrib X Y mu) (finiteActionKernel arms prob source)) : Filter.Eventually (fun omega => @Measure.map Omega Action mOmega mAction X (@condExpKernel Omega mOmega _ mu _ (mCondition.comap Y) omega) = finiteActionMeasure arms (prob (Y omega))) (ae (mu.trim hY.comap_le))
def
BanditRLProof.Exp3.sampledTrajectorySelectedDeviationAt
Compiled
Selected predictable loss minus its exploration-mixed conditional mean.
noncomputable def sampledTrajectorySelectedDeviationAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real
theorem
BanditRLProof.Exp3.measurable_sampledTrajectorySelectedDeviationAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_sampledTrajectorySelectedDeviationAt {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) (t : Nat) : Measurable (sampledTrajectorySelectedDeviationAt arms eta gamma loss t)
theorem
BanditRLProof.Exp3.sampledPredictableSelectedDeviation_succ_hasCondSubgaussianMGF
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableSelectedDeviation_succ_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) (n : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment let history := fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2) ProbabilityTheory.HasCondSubgaussianMGF ((inferInstance : MeasurableSpace (Env × History.FinitePairHistory Action Real n)).comap history) (measurable_fst.prodMk ((Preorder.measurable_frestrictLe n).comp measurable_snd)).comap_le (sampledTrajectorySelectedDeviationAt arms eta gamma loss (n + 1)) (Concentration.intervalVarianceProxy 0 1) mu
def
BanditRLProof.Exp3.sampledTrajectoryRealizedDeviationAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledTrajectoryRealizedDeviationAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_succ_hasCondSubgaussianMGF
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviation_succ_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) (n : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment let history := fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2) ProbabilityTheory.HasCondSubgaussianMGF ((inferInstance : MeasurableSpace (Env × History.FinitePairHistory Action Real n)).comap history) (measurable_fst.prodMk ((Preorder.measurable_frestrictLe n).comp measurable_snd)).comap_le (sampledTrajectoryRealizedDeviationAt arms eta gamma loss (n + 1)) (Concentration.intervalVarianceProxy 0 1) mu