BanditRLProof.HeavyTailFixedTilt

No declaration docstring is present; use the chapter context and exact statement below.

theorem bounded_centered_mgf {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (b v tilt : ℝ) (hXm : Measurable X) (hb : ∀ ω, |X ω| ≤ b) (hmean : (∫ ω, X ω ∂μ) = 0) (hv : (∫ ω, (X ω)^2 ∂μ) ≤ v) (hsmall : |tilt| * b ≤ 1) : Concentration.HasMGFUpperBoundAt X tilt (tilt^2 * v) μ

Shared centering producer for bounded transformed rewards. Both hard truncation and clipping supply their own second-moment proofs to this interface.

theorem bounded_centering_mgf {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : Ω → ℝ) (B v tilt : ℝ) (hYm : Measurable Y) (hbound : ∀ ω, |Y ω| ≤ B) (hv : (∫ ω, (Y ω)^2 ∂μ) ≤ v) (hsmall : |tilt| * (2 * B) ≤ 1) : Concentration.HasMGFUpperBoundAt (fun ω => Y ω - ∫ ω, Y ω ∂μ) tilt (tilt^2 * v) μ

Moment assumptions produce a centered truncated MGF at every admissible tilt. Signed rewards require the factor 2 in the centering range.

theorem truncated_centered_mgf {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (B ε u tilt : ℝ) (hXm : Measurable X) (hB : 0 < B) (hε : ε ≤ 1) (hm : Integrable (fun ω => |X ω| ^ (1 + ε)) μ) (hu : (∫ ω, |X ω| ^ (1 + ε) ∂μ) ≤ u) (hsmall : |tilt| * (2 * B) ≤ 1) : Concentration.HasMGFUpperBoundAt (fun ω => truncate B (X ω) - ∫ ω, truncate B (X ω) ∂μ) tilt (tilt^2 * (u * B^(1-ε))) μ

Independent composition preserves the individual admissible tilt, instead of imposing a range bound on the whole sum.

theorem independent_sum_mgf {Ω ι : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ι → Ω → ℝ) (s : Finset ι) (tilt : ℝ) (budget : ι → ℝ) (hi : iIndepFun X μ) (hm : ∀ i, Measurable (X i)) (h : ∀ i ∈ s, Concentration.HasMGFUpperBoundAt (X i) tilt (budget i) μ) : Concentration.HasMGFUpperBoundAt (∑ i ∈ s, X i) tilt (∑ i ∈ s, budget i) μ

Fixed-prefix one-sided concentration from independent raw-moment data. This is an actual tail producer, before bias assembly and adaptive-count peeling.

theorem truncated_sum_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (B : ℕ → ℝ) (ε u tilt r : ℝ) (n : ℕ) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hB : ∀ i, 0 < B i) (hε : ε ≤ 1) (hm : ∀ i, Integrable (fun ω => |X i ω| ^ (1 + ε)) μ) (hu : ∀ i, (∫ ω, |X i ω| ^ (1 + ε) ∂μ) ≤ u) (ht : 0 ≤ tilt) (hsmall : ∀ i ∈ Finset.range n, |tilt| * (2 * B i) ≤ 1) : μ.real {ω | r ≤ ∑ i ∈ Finset.range n, (truncate (B i) (X i ω) - ∫ ω, truncate (B i) (X i ω) ∂μ)} ≤ Real.exp (-tilt * r + ∑ i ∈ Finset.range n, tilt^2 * (u * (B i)^(1-ε)))