Lean module · Foundations
BanditRLProof.MathlibWrappers
# Mathlib-backed finite bookkeeping wrappers This module is the first intentional Mathlib interop layer. The dependency-light lemmas remain in `BanditRLProof.LeafLemmas`; this file only bridges those local recursive definitions to Mathlib-facing finite containers.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCCountLemmas, BanditRLProof.Algorithms.ETCEmpiricalMean, BanditRLProof.Algorithms.ETCSumRewardsDiff, BanditRLProof.ConditionalRewardLawSource, BanditRLProof.MeasurableLocalQuantities, BanditRLProof.MeasurableRegret, BanditRLProof.PullCountDecomposition, BanditRLProof.RealMeanRegretPullCount, BanditRLProof.RegretDecomposition
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.pullCount_eq_finset_filter_card
Compiled
The recursive pull count equals the cardinality of the matching arm times in `Finset.range t`. This is the first Mathlib-backed wrapper leaf. It is intentionally kept separate from the dependency-light `List.range` bridge.
theorem pullCount_eq_finset_filter_card : pullCount action a t = ((Finset.range t).filter (fun s : Nat => action s = a)).card
theorem
BanditRLProof.sumRewards_eq_finset_filter_sum
Compiled
The recursive selected reward sum equals the Mathlib finite sum over selected time points in `Finset.range t`. The local recursive definition only needs weak `0` and `+` operations. This Mathlib-facing wrapper strengthens the algebra contract to `AddCommMonoid` because `Finset.sum` is commutative and the insertion proof swaps summand order.
theorem sumRewards_eq_finset_filter_sum : sumRewards action reward a t = ((Finset.range t).filter (fun s : Nat => action s = a)).sum (fun s : Nat => reward s)
theorem
BanditRLProof.pseudoRegret_eq_finset_sum
Compiled
The recursive pseudo-regret equals the Mathlib finite sum of selected gaps over `Finset.range t`. This is the Rat-valued finite-sum wrapper. It deliberately comes before the generic reward-sum wrapper because `Finset.sum` only needs the Mathlib `AddCommMonoid Rat` instance supplied by the Rat algebra imports.
theorem pseudoRegret_eq_finset_sum : pseudoRegret model action t = (Finset.range t).sum (fun s : Nat => model.gap (action s))