BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Probability layer

BanditRLProof.FiniteArmRewardKernelLaw

# Context-independent finite-arm centered reward laws This module packages action-indexed probability laws into the centered reward kernel contract shared by bandit algorithms. It is deliberately independent of ETC, UCB, or any trajectory construction.

Module map

Declarations
12
Placeholders
0

Imports

BanditRLProof.BoundedRewardKernelLaw

Imported by

BanditRLProof, BanditRLProof.Algorithms.UCBArmStreamFiniteArmRewardLaws, BanditRLProof.Algorithms.UCBBoundedFiniteArmRewardLaw, BanditRLProof.Algorithms.UCBFiniteArmSubGaussianRewardLaw, BanditRLProof.Algorithms.UCBFiniteArmSubGaussianSampledAsymptotics, BanditRLProof.FiniteContextVarianceProxy

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.Concentration.finiteArmIntervalVarianceProxy Compiled

The largest Hoeffding proxy among a finite family of armwise intervals.

noncomputable def finiteArmIntervalVarianceProxy {K : Nat} (lo hi : Fin K -> Real) : NNReal
Source line 18 Chapter context: Probability layer
theorem BanditRLProof.Concentration.intervalVarianceProxy_le_finiteArmIntervalVarianceProxy Compiled

Every armwise interval proxy is bounded by the finite-arm maximum proxy.

theorem intervalVarianceProxy_le_finiteArmIntervalVarianceProxy {K : Nat} (lo hi : Fin K -> Real) (arm : Fin K) : intervalVarianceProxy (lo arm) (hi arm) <= finiteArmIntervalVarianceProxy lo hi
Source line 23 Chapter context: Probability layer
theorem BanditRLProof.Concentration.finiteArmIntervalVarianceProxy_pos Compiled

Nondegenerate armwise intervals give a positive finite-arm maximum proxy.

theorem finiteArmIntervalVarianceProxy_pos {K : Nat} (hK : 0 < K) (lo hi : Fin K -> Real) (hlohi : forall arm, lo arm < hi arm) : 0 < ((finiteArmIntervalVarianceProxy lo hi : NNReal) : Real)
Source line 36 Chapter context: Probability layer
def BanditRLProof.Concentration.finiteArmVarianceProxy Compiled

The largest variance proxy in a finite family of arms.

noncomputable def finiteArmVarianceProxy {K : Nat} (varianceProxy : Fin K -> NNReal) : NNReal
Source line 55 Chapter context: Probability layer
theorem BanditRLProof.Concentration.varianceProxy_le_finiteArmVarianceProxy Compiled

Every arm proxy is bounded by the finite-arm maximum proxy.

theorem varianceProxy_le_finiteArmVarianceProxy {K : Nat} (varianceProxy : Fin K -> NNReal) (arm : Fin K) : varianceProxy arm <= finiteArmVarianceProxy varianceProxy
Source line 60 Chapter context: Probability layer
theorem BanditRLProof.Concentration.finiteArmVarianceProxy_pos_of_exists Compiled

A positive member makes the finite-arm maximum proxy positive.

theorem finiteArmVarianceProxy_pos_of_exists {K : Nat} (varianceProxy : Fin K -> NNReal) (hpos : exists arm, 0 < ((varianceProxy arm : NNReal) : Real)) : 0 < ((finiteArmVarianceProxy varianceProxy : NNReal) : Real)
Source line 71 Chapter context: Probability layer
def BanditRLProof.Concentration.finiteArmPositiveVarianceProxy Compiled

The finite-arm maximum padded by one, providing a strictly positive tuning proxy even when all genuine armwise proxies are zero.

noncomputable def finiteArmPositiveVarianceProxy {K : Nat} (varianceProxy : Fin K -> NNReal) : NNReal
Source line 84 Chapter context: Probability layer
theorem BanditRLProof.Concentration.varianceProxy_le_finiteArmPositiveVarianceProxy Compiled

Every armwise proxy is bounded by the positive padded finite-arm proxy.

theorem varianceProxy_le_finiteArmPositiveVarianceProxy {K : Nat} (varianceProxy : Fin K -> NNReal) (arm : Fin K) : varianceProxy arm <= finiteArmPositiveVarianceProxy varianceProxy
Source line 89 Chapter context: Probability layer
theorem BanditRLProof.Concentration.finiteArmPositiveVarianceProxy_pos Compiled

The padded finite-arm proxy is always strictly positive.

theorem finiteArmPositiveVarianceProxy_pos {K : Nat} (varianceProxy : Fin K -> NNReal) : 0 < ((finiteArmPositiveVarianceProxy varianceProxy : NNReal) : Real)
Source line 97 Chapter context: Probability layer
def BanditRLProof.RewardKernel.contextIndependentCenteredRewardKernelLaw_of_hasSubgaussianMGF Compiled

Action-indexed probability laws with exact means and direct centered sub-Gaussian witnesses form a context-independent centered reward-kernel law.

noncomputable def contextIndependentCenteredRewardKernelLaw_of_hasSubgaussianMGF {Context Action : Type} [MeasurableSpace Context] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (armLaw : Action -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (armMean : Action -> Rat) (varianceProxy : Action -> NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((armMean arm : Rat) : Real)) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Rat => (((reward - armMean arm : Rat) : Real))) (varianceProxy arm) (armLaw arm)) : CenteredRewardKernelLaw (contextIndependentOfActionLaws (Context
Source line 112 Chapter context: Probability layer
def BanditRLProof.RewardKernel.contextIndependentBoundedCenteredRewardKernelLaw Compiled

Common almost-sure interval bounds and exact means form a context-independent centered reward-kernel law with the Hoeffding proxy.

noncomputable def contextIndependentBoundedCenteredRewardKernelLaw {Context Action : Type} [MeasurableSpace Context] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (armLaw : Action -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (armMean : Action -> Rat) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => ((reward : Rat) : Real)) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi ((reward : Rat) : Real)) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((armMean arm : Rat) : Real)) : CenteredRewardKernelLaw (contextIndependentOfActionLaws (Context
Source line 162 Chapter context: Probability layer
def BanditRLProof.RewardKernel.contextIndependentArmwiseBoundedCenteredRewardKernelLaw Compiled

Arm-dependent almost-sure interval bounds and exact means form a context-independent centered reward-kernel law with armwise Hoeffding proxies.

noncomputable def contextIndependentArmwiseBoundedCenteredRewardKernelLaw {Context Action : Type} [MeasurableSpace Context] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (armLaw : Action -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (armMean : Action -> Rat) (lo hi : Action -> Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => ((reward : Rat) : Real)) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc (lo arm) (hi arm) ((reward : Rat) : Real)) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((armMean arm : Rat) : Real)) : CenteredRewardKernelLaw (contextIndependentOfActionLaws (Context
Source line 203 Chapter context: Probability layer