Lean module · Foundations
BanditRLProof.HeavyTailClippedConfidence
Clean clipped-mean confidence from raw moments, through shared MGF interfaces.
Module map
Imports
BanditRLProof.HeavyTailClippedMoments, BanditRLProof.HeavyTailConfidence, BanditRLProof.HeavyTailTuning
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.clipped_centered_mgf
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.clipped_centered_mgfReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem clipped_centered_mgf {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (B ε u tilt : ℝ) (hXm : Measurable X) (hB : 0 < B) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hm : Integrable (fun ω => |X ω|^(1+ε)) μ) (hu : (∫ ω, |X ω|^(1+ε) ∂μ) ≤ u) (hsmall : |tilt| * (2*B) ≤ 1) : Concentration.HasMGFUpperBoundAt (fun ω => clip B (X ω) - ∫ ω, clip B (X ω) ∂μ) tilt (tilt^2*(u*B^(1-ε))) μ
theorem
BanditRLProof.HeavyTail.clipped_sum_abs_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.clipped_sum_abs_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem clipped_sum_abs_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (B : ℕ → ℝ) (ε u b L : ℝ) (n : ℕ) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hB : ∀ i, 0 < B i) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 ≤ u) (hb : 0 < b) (hL : 0 ≤ L) (hbound : ∀ i ∈ Finset.range n, 2*B i ≤ b) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hu : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 2*Real.sqrt ((∑ i ∈ Finset.range n, u*(B i)^(1-ε))*L)+b*L ≤ |∑ i ∈ Finset.range n, (clip (B i) (X i ω) - ∫ ω, clip (B i) (X i ω) ∂μ)|} ≤ 2*Real.exp (-L)
theorem
BanditRLProof.HeavyTail.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.clipped_mean_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem clipped_mean_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (B : ℕ → ℝ) (ε u b L mean : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hB : ∀ i, 0 < B i) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 ≤ u) (hb : 0 < b) (hL : 0 ≤ L) (hbound : ∀ i ∈ Finset.range n, 2*B i ≤ b) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hu : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | ((∑ i ∈ Finset.range n, u/(B i)^ε) + (2*Real.sqrt ((∑ i ∈ Finset.range n, u*(B i)^(1-ε))*L)+b*L))/n ≤ |prefixMean (fun i => clip (B i) (X i ω)) n - mean|} ≤ 2*Real.exp (-L)