Lean module · Foundations
BanditRLProof.MathlibWrappers
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.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.pullCount_eq_finset_filter_cardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.sumRewards_eq_finset_filter_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.pseudoRegret_eq_finset_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem pseudoRegret_eq_finset_sum : pseudoRegret model action t = (Finset.range t).sum (fun s : Nat => model.gap (action s))