Lean module · Foundations
BanditRLProof.PullCountDecomposition
# Pull-count decompositions over finite action spaces 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.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.
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.
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