Lean module · Foundations
BanditRLProof.RegretDecomposition
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`.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))