Lean module · Foundations
BanditRLProof.Algorithms.CUCBRegretTail
Exact cumulative source tail and signed regret reduction to the actual under-sampled charge weight. The refined gap integral remains separate.
Module map
Imports
BanditRLProof.Algorithms.CUCBRegretDecomposition
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_sufficientIndicator_le
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_sufficientIndicator_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_sufficientIndicator_le (H n : ℕ) (hH : n+1≤H) : (∫Y, S.sufficientIndicator H n Y ∂cucbTrajectory S.oracle M.environment) ≤ (2+(if M.globalMinTrigger<1 then 1 else 0))*(m:ℝ)/((n:ℝ)+1)^2
theorem
BanditRLProof.CUCB.SourceModel.sum_inverse_square_le
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.sum_inverse_square_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_inverse_square_le (H : ℕ) : (∑n∈Finset.range H, (((n:ℝ)+1)^2)⁻¹)≤Real.pi^2/6
theorem
BanditRLProof.CUCB.SourceModel.sum_expected_sufficientIndicator_le
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.sum_expected_sufficientIndicator_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_expected_sufficientIndicator_le (H : ℕ) : (∑n∈Finset.range H, ∫Y, S.sufficientIndicator H n Y ∂cucbTrajectory S.oracle M.environment) ≤ (2+(if M.globalMinTrigger<1 then 1 else 0))*(m:ℝ)*(Real.pi^2/6)
theorem
BanditRLProof.CUCB.SourceModel.approximationRegret_le_underSampled_add_source_tail
Compiled
The original signed regret, with the oracle-failure credit cancelled and all sufficiently sampled rounds summed with the exact source constant.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.approximationRegret_le_underSampled_add_source_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem approximationRegret_le_underSampled_add_source_tail (H : ℕ) : S.approximationRegret 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) + (2+(if M.globalMinTrigger<1 then 1 else 0))*(m:ℝ)* maxPositiveGap S.score M.trueInput S.alpha*Real.pi^2/6