Lean module · Foundations
BanditRLProof.FiniteBanditModelInvariants
# Finite-bandit model invariants This module contains model-semantic facts about the local `FiniteBanditModel.bestArm` selector. It stays below regret, expectation, filtrations, kernels, and concentration.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCPairwiseCenteredSubGaussianTail, BanditRLProof.Algorithms.UCBConditionalRewardLawRegret, BanditRLProof.ExpectationPseudoRegretRatBounds, BanditRLProof.RegretCountBounds, BanditRLProof.TsallisFiniteArmIndependentDriftingMeanDynamicRegret, BanditRLProof.TsallisFiniteBanditMeanLoss
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteBanditModel.mean_le_foldl_select
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem mean_le_foldl_select {K : Nat} (mean : Fin K -> Rat) (init : Fin K) : forall l : List (Fin K), (forall a : Fin K, a ∈ l -> mean a <= mean (l.foldl (fun best arm : Fin K => if mean best < mean arm then arm else best) init)) /\ mean init <= mean (l.foldl (fun best arm : Fin K => if mean best < mean arm then arm else best) init) | [] => by simp | arm :: rest => by let select := fun best arm : Fin K => if mean best < mean arm then arm else best let next := select init arm have ih
theorem
BanditRLProof.FiniteBanditModel.mean_le_bestArm_mean
Compiled
The mean of every arm is at most the mean of the model's selected best arm. This is the `FINITE-BANDIT-BESTARM-DOMINATES` model-invariant leaf. It is a semantic fact about the local finite-arm selector only; it does not prove gap nonnegativity or any expectation/concentration statement.
theorem mean_le_bestArm_mean {K : Nat} (model : FiniteBanditModel K) (a : Fin K) : model.mean a <= model.mean model.bestArm
theorem
BanditRLProof.FiniteBanditModel.gap_nonneg
Compiled
Every local model gap is nonnegative. This is the `FINITE-BANDIT-GAP-NONNEG` model-invariant leaf. It consumes only `FiniteBanditModel.mean_le_bestArm_mean` and the local `gap` definition; it does not prove or use any expectation, filtration, or concentration statement.
theorem gap_nonneg {K : Nat} (model : FiniteBanditModel K) (a : Fin K) : (0 : Rat) <= model.gap a
def
BanditRLProof.FiniteBanditModel.maxGap
Compiled
The maximum local arm gap over the finite arm set. This is a deterministic finite-model constant only. It does not introduce probability, expectation, concentration, or algorithmic behavior.
noncomputable def maxGap {K : Nat} (model : FiniteBanditModel K) : Rat
theorem
BanditRLProof.FiniteBanditModel.gap_le_maxGap
Compiled
Every local model gap is bounded by `FiniteBanditModel.maxGap`. This is the finite max-gap adapter used by sharper ETC suffix bounds.
theorem gap_le_maxGap {K : Nat} (model : FiniteBanditModel K) (a : Fin K) : model.gap a <= model.maxGap
theorem
BanditRLProof.FiniteBanditModel.maxGap_nonneg
Compiled
The finite maximum gap is nonnegative.
theorem maxGap_nonneg {K : Nat} (model : FiniteBanditModel K) : (0 : Rat) <= model.maxGap