Lean module · Foundations
BanditRLProof.FiniteGapLayerCake
Finite gap layer-cake identities and a refined integral envelope.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBUnderCountIntegral, BanditRLProof.FiniteGapCutoff
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteGapLayerCake.intervalIntegrable_step
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.intervalIntegrable_stepReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem intervalIntegrable_step (d a b : ℝ) : IntervalIntegrable (fun x : ℝ => if x≤d then (1:ℝ) else 0) volume a b
theorem
BanditRLProof.FiniteGapLayerCake.integral_step
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.integral_stepReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_step {a b d : ℝ} (hd : d∈Set.Icc a b) : (∫x in a..b, if x≤d then (1:ℝ) else 0)=d-a
theorem
BanditRLProof.FiniteGapLayerCake.intervalIntegrable_card
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.intervalIntegrable_cardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem intervalIntegrable_card {ι : Type*} (s : Finset ι) (d : ι → ℝ) (a b : ℝ) : IntervalIntegrable (fun x => ((s.filter (fun t => x≤d t)).card:ℝ)) volume a b
theorem
BanditRLProof.FiniteGapLayerCake.sum_eq_layerCake
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_eq_layerCakeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_eq_layerCake {ι : Type*} (s : Finset ι) (d : ι → ℝ) (a b : ℝ) (hd : ∀t∈s, d t∈Set.Icc a b) : ∑t∈s, d t = a*(s.card:ℝ)+(∫x in a..b, ((s.filter (fun t => x≤d t)).card:ℝ))
theorem
BanditRLProof.FiniteGapLayerCake.sum_le_refined_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_refined_integralReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_le_refined_integral {ι : Type*} (s : Finset ι) (d : ι → ℝ) (a b : ℝ) (ha : 0≤a) (hab : a≤b) (hd : ∀t∈s, d t∈Set.Icc a 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*ell a+(∫x in a..b, ell x)+b