Lean module · Foundations
BanditRLProof.FiniteGapCutoff
A cutoff layer-cake envelope that pays the baseline once per observation.
Module map
Imports
BanditRLProof.FiniteGapLayerCake
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteGapLayerCake.sum_le_cutoff_integral
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.FiniteGapLayerCake.sum_le_cutoff_integralReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_le_cutoff_integral {ι : Type*} (s : Finset ι) (d : ι → ℝ) (a b : ℝ) (hab : a≤b) (hd : ∀t∈s, d t≤b) (ell : ℝ → ℝ) (hi : IntervalIntegrable ell volume a b) (hc : ∀x∈Set.Icc a b, ((s.filter (fun t => x≤d t)).card:ℝ)≤ell x+1) : ∑t∈s, d t ≤ a*(s.card:ℝ)+(∫x in a..b, ell x)+(b-a)