Lean module · Foundations
BanditRLProof.HeavyTailClippedScheduled
The actual algorithm's scheduled radius, produced from raw moments.
Module map
Imports
BanditRLProof.HeavyTailTuning, BanditRLProof.HeavyTailClippedConfidence
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.scheduled_clipped_mean_tail
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.scheduled_clipped_mean_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem scheduled_clipped_mean_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u mean : ℝ) (t n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω| ^ (1 + ε)) μ) (hu : ∀ i, (∫ ω, |X i ω| ^ (1 + ε) ∂μ) ≤ u) : μ.real {ω | confidenceRadius ε u t n ≤ |(∑ s ∈ Finset.range n, clip (sampleThreshold ε u t s) (X s ω)) / n - mean|} ≤ 2 * Real.exp (-confidenceLog t)
theorem
BanditRLProof.HeavyTail.scheduled_adaptive_clipped_mean_tail
Compiled
Union over deterministic prefix sizes. The adaptive count is never asserted IID.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.scheduled_adaptive_clipped_mean_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem scheduled_adaptive_clipped_mean_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (count : Ω → ℕ) (ε u mean : ℝ) (t : ℕ) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω| ^ (1 + ε)) μ) (hu : ∀ i, (∫ ω, |X i ω| ^ (1 + ε) ∂μ) ≤ u) : μ.real {ω | 0 < count ω ∧ count ω ≤ t ∧ confidenceRadius ε u t (count ω) ≤ |(∑ s ∈ Finset.range (count ω), clip (sampleThreshold ε u t s) (X s ω)) / count ω - mean|} ≤ t * (2 * Real.exp (-confidenceLog t))