Lean module · Foundations
BanditRLProof.HeavyTailUnshiftedMGF
Centering after the exponential bound preserves the raw-variable tilt range. This uses a raw second moment, not the variance of the centered variable.
Module map
Imports
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.exp_le_one_add_self_add_three_quarters_sq
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.exp_le_one_add_self_add_three_quarters_sqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exp_le_one_add_self_add_three_quarters_sq {x : ℝ} (hx : |x| ≤ 1) : Real.exp x ≤ 1 + x + (3/4 : ℝ)*x^2
theorem
BanditRLProof.HeavyTail.bounded_centering_mgf_unshifted_sharp
Compiled
Sharper raw-second-moment MGF at the unchanged full raw-variable tilt.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.bounded_centering_mgf_unshifted_sharpReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bounded_centering_mgf_unshifted_sharp {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : Ω → ℝ) (B v tilt : ℝ) (hYm : Measurable Y) (hbound : ∀ ω, |Y ω| ≤ B) (hv : (∫ ω, (Y ω)^2 ∂μ) ≤ v) (hsmall : |tilt| * B ≤ 1) : Concentration.HasMGFUpperBoundAt (fun ω => Y ω - ∫ ω, Y ω ∂μ) tilt ((3/4 : ℝ)*tilt^2 * v) μ
theorem
BanditRLProof.HeavyTail.bounded_centering_mgf_unshifted
Compiled
Compatibility weakening of the sharper raw-second-moment producer.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.bounded_centering_mgf_unshiftedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bounded_centering_mgf_unshifted {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : Ω → ℝ) (B v tilt : ℝ) (hYm : Measurable Y) (hbound : ∀ ω, |Y ω| ≤ B) (hv : (∫ ω, (Y ω)^2 ∂μ) ≤ v) (hsmall : |tilt| * B ≤ 1) : Concentration.HasMGFUpperBoundAt (fun ω => Y ω - ∫ ω, Y ω ∂μ) tilt (tilt^2 * v) μ