Lean module · Foundations
BanditRLProof.HeavyTailClippedMoments
Clean clipping bias and second moments, produced from raw moments.
Module map
Imports
BanditRLProof.HeavyTailClipping, BanditRLProof.HeavyTailFixedTilt
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.clip_eq_self
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.clip_eq_selfReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem clip_eq_self (B x : ℝ) (hx : |x| ≤ B) : clip B x = x
theorem
BanditRLProof.HeavyTail.abs_clip_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.HeavyTail.abs_clip_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem abs_clip_le (B x : ℝ) (hB : 0 ≤ B) : |clip B x| ≤ B
theorem
BanditRLProof.HeavyTail.abs_clip_le_abs
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.abs_clip_le_absReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem abs_clip_le_abs (B x : ℝ) (hB : 0 ≤ B) : |clip B x| ≤ |x|
theorem
BanditRLProof.HeavyTail.abs_sub_clip_le_truncate
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.abs_sub_clip_le_truncateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem abs_sub_clip_le_truncate (B x : ℝ) (hB : 0 ≤ B) : |x - clip B x| ≤ |x - truncate B x|
theorem
BanditRLProof.HeavyTail.abs_sub_clip_moment_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.HeavyTail.abs_sub_clip_moment_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem abs_sub_clip_moment_le (B x ε : ℝ) (hB : 0 < B) (hε : 0 ≤ ε) : |x - clip B x| ≤ |x|^(1+ε) / B^ε
theorem
BanditRLProof.HeavyTail.sq_clip_moment_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.HeavyTail.sq_clip_moment_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sq_clip_moment_le (B x ε : ℝ) (hB : 0 < B) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) : (clip B x)^2 ≤ |x|^(1+ε) * B^(1-ε)
theorem
BanditRLProof.HeavyTail.measurable_clip
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.measurable_clipReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_clip (B : ℝ) : Measurable (clip B)
theorem
BanditRLProof.HeavyTail.integral_clip_bias_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.HeavyTail.integral_clip_bias_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_clip_bias_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (B ε u : ℝ) (hB : 0 < B) (hε : 0 ≤ ε) (hXm : Measurable X) (hX : Integrable X μ) (hm : Integrable (fun ω => |X ω|^(1+ε)) μ) (hu : (∫ ω, |X ω|^(1+ε) ∂μ) ≤ u) : |(∫ ω, X ω ∂μ) - ∫ ω, clip B (X ω) ∂μ| ≤ u/B^ε
theorem
BanditRLProof.HeavyTail.integral_sq_clip_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.HeavyTail.integral_sq_clip_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_sq_clip_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) (B ε u : ℝ) (hB : 0 < B) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hXm : Measurable X) (hm : Integrable (fun ω => |X ω|^(1+ε)) μ) (hu : (∫ ω, |X ω|^(1+ε) ∂μ) ≤ u) : (∫ ω, (clip B (X ω))^2 ∂μ) ≤ u*B^(1-ε)