Lean module · Foundations
BanditRLProof.PullCountDecomposition
This module contains deterministic count identities that consume the Mathlib-backed Finset.range wrappers. It stays below the probability and algorithm-specific layers.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Algorithms.HeavyTailSourceCounterexample, BanditRLProof.Algorithms.MOSSRegret, BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoStarvation, BanditRLProof.Algorithms.ThompsonClippedUCBScore
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.finset_sum_pullCount_eq_time
Compiled
The pull counts over a finite action space partition the time horizon. This is the deterministic `PULLCOUNT-SUM-TIME` leaf. It consumes the compiled `pullCount` Finset wrapper and Mathlib's finite fiber-cardinality theorem.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.finset_sum_pullCount_eq_timeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finset_sum_pullCount_eq_time : (Finset.univ : Finset Action).sum (fun a : Action => pullCount action a t) = t
theorem
BanditRLProof.finset_sum_comp_pullCount
Compiled
Reindex a sum over action times by arm and the arm's prior pull count. At a time `s`, the value `pullCount action (action s) s` is the zero-based index of that pull among occurrences of the selected arm. This is the local Mathlib-backed counterpart of LML's `sum_comp_pullCount` bookkeeping lemma.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.finset_sum_comp_pullCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finset_sum_comp_pullCount {R : Type v} [AddCommMonoid R] (f : Nat -> R) : ∑ s ∈ Finset.range t, f (pullCount action (action s) s) = ∑ a : Action, ∑ j ∈ Finset.range (pullCount action a t), f j