Lean module · Foundations
BanditRLProof.RegretDecomposition
# Deterministic regret decompositions This module consumes the Mathlib-backed finite bookkeeping wrappers. It should stay deterministic: probability, measurability, and concentration imports belong in later layers.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.ExpectationRegretPullCount, BanditRLProof.RegretCountBounds, BanditRLProof.ScalarPseudoRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount
Compiled
Pseudo-regret decomposes into an arm-indexed sum of each arm gap multiplied by its pull count. This is the deterministic `REGRET-PULLCOUNT` bridge. It consumes the compiled `Finset.range` wrappers instead of reopening the recursive definitions of `pseudoRegret` or `pullCount`.
theorem pseudoRegret_eq_finset_sum_gap_mul_pullCount : pseudoRegret model action t = (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a * (pullCount action a t : Rat))