Lean module · Probability layer
BanditRLProof.FiniteContextVarianceProxy
# Uniform variance proxies over finite context-action families This module computes one common `NNReal` proxy for a finite context space and finite arm set. It is independent of any particular bandit algorithm.
Module map
Imports
BanditRLProof.FiniteArmRewardKernelLaw
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBContextDependentSubGaussianRewardKernel
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Concentration.finiteContextArmVarianceProxy
Compiled
The largest variance proxy over a finite context-action family.
noncomputable def finiteContextArmVarianceProxy {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) : NNReal
theorem
BanditRLProof.Concentration.varianceProxy_le_finiteContextArmVarianceProxy
Compiled
Every context-action proxy is bounded by the finite-family maximum.
theorem varianceProxy_le_finiteContextArmVarianceProxy {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) (context : Context) (arm : Fin K) : varianceProxy context arm <= finiteContextArmVarianceProxy varianceProxy
theorem
BanditRLProof.Concentration.finiteContextArmVarianceProxy_pos_of_exists
Compiled
A positive member makes the finite context-action maximum positive.
theorem finiteContextArmVarianceProxy_pos_of_exists {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) (hpos : exists context arm, 0 < ((varianceProxy context arm : NNReal) : Real)) : 0 < ((finiteContextArmVarianceProxy varianceProxy : NNReal) : Real)
def
BanditRLProof.Concentration.finiteContextArmPositiveVarianceProxy
Compiled
The finite context-action maximum padded by one. This gives algorithms that require a strictly positive tuning parameter a uniform proxy even when every genuine variance proxy is zero.
noncomputable def finiteContextArmPositiveVarianceProxy {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) : NNReal
theorem
BanditRLProof.Concentration.varianceProxy_le_finiteContextArmPositiveVarianceProxy
Compiled
Every genuine proxy is bounded by the positive padded proxy.
theorem varianceProxy_le_finiteContextArmPositiveVarianceProxy {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) (context : Context) (arm : Fin K) : varianceProxy context arm <= finiteContextArmPositiveVarianceProxy varianceProxy
theorem
BanditRLProof.Concentration.finiteContextArmPositiveVarianceProxy_pos
Compiled
The padded finite context-action proxy is always strictly positive.
theorem finiteContextArmPositiveVarianceProxy_pos {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) : 0 < ((finiteContextArmPositiveVarianceProxy varianceProxy : NNReal) : Real)