BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Probability layer

BanditRLProof.FiniteContextVarianceProxy

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

Declarations
6
Placeholders
0

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book

2. Probability, kernels, filtrations, and concentration

Canonical node identitydeclaration:BanditRLProof.Concentration.finiteContextArmVarianceProxy

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def finiteContextArmVarianceProxy {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) : NNReal
Source line 14 Chapter context: Probability layer
theorem BanditRLProof.Concentration.varianceProxy_le_finiteContextArmVarianceProxy Compiled

Every context-action proxy is bounded by the finite-family maximum.

Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book

2. Probability, kernels, filtrations, and concentration

Canonical node identitydeclaration:BanditRLProof.Concentration.varianceProxy_le_finiteContextArmVarianceProxy

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 20 Chapter context: Probability layer
theorem BanditRLProof.Concentration.finiteContextArmVarianceProxy_pos_of_exists Compiled

A positive member makes the finite context-action maximum positive.

Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book

2. Probability, kernels, filtrations, and concentration

Canonical node identitydeclaration:BanditRLProof.Concentration.finiteContextArmVarianceProxy_pos_of_exists

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)
Source line 37 Chapter context: Probability layer
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.

Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book

2. Probability, kernels, filtrations, and concentration

Canonical node identitydeclaration:BanditRLProof.Concentration.finiteContextArmPositiveVarianceProxy

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def finiteContextArmPositiveVarianceProxy {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) : NNReal
Source line 53 Chapter context: Probability layer
theorem BanditRLProof.Concentration.varianceProxy_le_finiteContextArmPositiveVarianceProxy Compiled

Every genuine proxy is bounded by the positive padded proxy.

Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book

2. Probability, kernels, filtrations, and concentration

Canonical node identitydeclaration:BanditRLProof.Concentration.varianceProxy_le_finiteContextArmPositiveVarianceProxy

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 59 Chapter context: Probability layer
theorem BanditRLProof.Concentration.finiteContextArmPositiveVarianceProxy_pos Compiled

The padded finite context-action proxy is always strictly positive.

Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book

2. Probability, kernels, filtrations, and concentration

Canonical node identitydeclaration:BanditRLProof.Concentration.finiteContextArmPositiveVarianceProxy_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem finiteContextArmPositiveVarianceProxy_pos {Context : Type} [Fintype Context] {K : Nat} (varianceProxy : Context -> Fin K -> NNReal) : 0 < ((finiteContextArmPositiveVarianceProxy varianceProxy : NNReal) : Real)
Source line 70 Chapter context: Probability layer