Lean module · Probability layer
BanditRLProof.BoundedRewardKernelLaw
# Centered laws for bounded context-dependent reward kernels This module constructs the one-step centered reward-kernel contract directly from pointwise MGF witnesses or common almost-sure bounds. It is independent of any bandit algorithm or trajectory construction.
Module map
Imports
BanditRLProof.ConcentrationSubGaussian, BanditRLProof.RewardKernel
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBContextDependentBoundedRewardKernel, BanditRLProof.Algorithms.UCBContextDependentSubGaussianRewardKernel, BanditRLProof.FiniteArmRewardKernelLaw
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.intervalVarianceProxy_pos_of_lt
Compiled
A nondegenerate interval has a strictly positive Hoeffding proxy.
theorem intervalVarianceProxy_pos_of_lt {lo hi : Real} (hlohi : lo < hi) : 0 < ((intervalVarianceProxy lo hi : NNReal) : Real)
def
BanditRLProof.RewardKernel.centeredRewardKernelLaw_of_hasSubgaussianMGF
Compiled
Exact pointwise means and centered sub-Gaussian MGF witnesses form a centered law for an arbitrary context/action Markov reward kernel.
noncomputable def centeredRewardKernelLaw_of_hasSubgaussianMGF {Context Action : Type} [MeasurableSpace Context] [MeasurableSpace Action] (rewardKernel : MarkovRewardKernel (Context × Action) Rat) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (hmean : forall context arm, integral (selectedMeasure rewardKernel context arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((mean context arm : Rat) : Real)) (hsubG : forall context arm, HasSubgaussianMGF (fun reward : Rat => (((reward - mean context arm : Rat) : Real))) (varianceProxy context arm) (selectedMeasure rewardKernel context arm)) : CenteredRewardKernelLaw rewardKernel mean varianceProxy where
def
BanditRLProof.RewardKernel.boundedCenteredRewardKernelLaw
Compiled
Common almost-sure reward bounds and exact pointwise means form a centered law for an arbitrary context/action Markov reward kernel.
noncomputable def boundedCenteredRewardKernelLaw {Context Action : Type} [MeasurableSpace Context] [MeasurableSpace Action] (rewardKernel : MarkovRewardKernel (Context × Action) Rat) (mean : Context -> Action -> Rat) (lo hi : Real) (hmeas : forall context arm, AEMeasurable (fun reward : Rat => ((reward : Rat) : Real)) (selectedMeasure rewardKernel context arm)) (hbound : forall context arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi ((reward : Rat) : Real)) (ae (selectedMeasure rewardKernel context arm))) (hmean : forall context arm, integral (selectedMeasure rewardKernel context arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((mean context arm : Rat) : Real)) : CenteredRewardKernelLaw rewardKernel mean (fun _ _ => Concentration.intervalVarianceProxy lo hi)