Lean module · Foundations
BanditRLProof.Algorithms.CUCBRefinedRegret
The full refined integral approximation-regret endpoint, with the disclosed normalized analysis-counter repair and the unchanged source CUCB learner.
Module map
Imports
BanditRLProof.Algorithms.CUCBUnderCountIntegral, BanditRLProof.Algorithms.CUCBRegretTail
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.SourceModel.expected_underSampledGap_le_refined
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.CUCB.SourceModel.expected_underSampledGap_le_refinedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_underSampledGap_le_refined (H : ℕ) (hH : 1≤H) : (∑n∈Finset.range H, ∫Y : ℕ → Round A m, S.underSampledGap H (S.chargeData.counters (fun t => (Y t).1) n) (Y n).1 ∂cucbTrajectory S.oracle M.environment) ≤ (∑i:Fin m, S.armRefinedTerm H i)+(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.theorem_one_refined_regret
Compiled
Chen et al. JMLR 2016 Theorem 1, with the documented normalized charge repair. The per-arm gap family is derived from actual bad actions and possible triggers; an empty family contributes zero. No performance/count premise is assumed.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.theorem_one_refined_regretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem theorem_one_refined_regret (H : ℕ) (hH : 1≤H) : S.approximationRegret H ≤ (∑i:Fin m, S.armRefinedTerm H i)+ (1+(2+(if M.globalMinTrigger<1 then 1 else 0))*Real.pi^2/6)* (m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.armRefinedTerm_eq_zero_of_no_bad
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.CUCB.SourceModel.armRefinedTerm_eq_zero_of_no_badReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem armRefinedTerm_eq_zero_of_no_bad (H : ℕ) (h : ∀a, S.gap a≤0) (i : Fin m) : S.armRefinedTerm H i=0
theorem
BanditRLProof.CUCB.SourceModel.approximationRegret_nonpos_of_no_bad
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.CUCB.SourceModel.approximationRegret_nonpos_of_no_badReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem approximationRegret_nonpos_of_no_bad (H : ℕ) (h : ∀a, S.gap a≤0) : S.approximationRegret H≤0