Lean module · Foundations
BanditRLProof.Algorithms.HeavyTailRegret
Conservative robust-UCB expected pseudo-regret endpoint. This is the separately documented repair/adaptation, not the unchanged printed BCL constant theorem. The policy and measure are fixed across horizons. Zero-gap arms contribute zero.
Module map
Imports
BanditRLProof.Algorithms.HeavyTailExpectedCount, BanditRLProof.Algorithms.ETCRealInfinitePiTail, BanditRLProof.RealMeanRegretPullCount
Imported by
BanditRLProof, BanditRLProof.Algorithms.HeavyTailRegretCap, BanditRLProof.Algorithms.HeavyTailSourceRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.integrable_id_of_raw_moment
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.integrable_id_of_raw_momentReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_id_of_raw_moment (μ : Measure ℝ) [IsProbabilityMeasure μ] (ε : ℝ) (hε : 0 ≤ ε) (hm : Integrable (fun x : ℝ => |x|^(1+ε)) μ) : Integrable (fun x : ℝ => x) μ
theorem
BanditRLProof.HeavyTail.robust_expected_regret
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.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 : Fin K, realMeanGap (realKernelMean ν) arm * (gapThreshold ε u (realMeanGap (realKernelMean ν) arm) T + 2)
theorem
BanditRLProof.HeavyTail.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.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 ν)