Lean module · Foundations
BanditRLProof.Algorithms.HeavyTailSourceRegret
Complete corrected expected-regret bound for the unchanged source policy. The rejected printed coefficient remains a separate finite-counterexample obligation.
Module map
Imports
BanditRLProof.Algorithms.HeavyTailSourceExpectedCount, BanditRLProof.Algorithms.HeavyTailRegret
Imported by
BanditRLProof, BanditRLProof.Algorithms.HeavyTailSourceCounterexample
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_expected_regret
Compiled
Raw moments produce the entire causal algorithm-to-expected-pseudo-regret chain.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Heavy-tailed bandits
Canonical node identity
declaration:BanditRLProof.HeavyTail.SourcePolicy.robust_expected_regretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_expected_regret (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (ε u : ℝ) (T : ℕ) (hε0 : 0 < ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hm : ∀ a, Integrable (fun x : ℝ => |x|^(1+ε)) (ν a)) (hu : ∀ a, (∫ x, |x|^(1+ε) ∂ν a) ≤ u) : (∫ stream, realMeanRegret (realKernelMean ν) (robustAction hK ε u stream) T ∂UCB.armStreamMeasure ν) ≤ ∑ arm ∈ Finset.univ.filter (fun arm : Fin K => 0 < realMeanGap (realKernelMean ν) arm), realMeanGap (realKernelMean ν) arm * (gapBudget ε u (realMeanGap (realKernelMean ν) arm) T + 5)
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_regret_integrable
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.HeavyTail.SourcePolicy.robust_regret_integrableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_regret_integrable (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (ε u : ℝ) (T : ℕ) : Integrable (fun stream => realMeanRegret (realKernelMean ν) (robustAction hK ε u stream) T) (UCB.armStreamMeasure ν)