BanditRLProof.HeavyTailConfidence

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

theorem exists_variance_tilt (V b L : ℝ) (hV : 0 ≤ V) (hb : 0 < b) (hL : 0 ≤ L) : ∃ t : ℝ, 0 ≤ t ∧ t * b ≤ 1 ∧ -t * (2 * Real.sqrt (V * L) + b * L) + t^2 * V ≤ -L

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

theorem neg_mgf {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) (t v : ℝ) (h : Concentration.HasMGFUpperBoundAt X (-t) v μ) : Concentration.HasMGFUpperBoundAt (fun ω => -X ω) t v μ

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

theorem fixed_mgf_abs_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (V b L : ℝ) (hV : 0 ≤ V) (hb : 0 < b) (hL : 0 ≤ L) (h : ∀ t : ℝ, |t| * b ≤ 1 → Concentration.HasMGFUpperBoundAt X t (t^2 * V) μ) : μ.real {ω | 2 * Real.sqrt (V * L) + b * L ≤ |X ω|} ≤ 2 * Real.exp (-L)

Two-sided centered sum, with variance budget and maximum increment bound derived from the raw moments and deterministic truncation thresholds.

theorem truncated_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ε : ε ≤ 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, (truncate (B i) (X i ω) - ∫ ω, truncate (B i) (X i ω) ∂μ)|} ≤ 2 * Real.exp (-L)

Shared bias-plus-fluctuation assembly for independent transformed estimators. The truncation and clipping producers discharge both premises separately.

theorem sum_mean_tail_of_centered {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : ℕ → Ω → ℝ) (mean bias fluctuation δ : ℝ) (n : ℕ) (hbias : |∑ i ∈ Finset.range n, ((∫ ω, Y i ω ∂μ) - mean)| ≤ bias) (htail : μ.real {ω | fluctuation ≤ |∑ i ∈ Finset.range n, (Y i ω - ∫ ω, Y i ω ∂μ)|} ≤ δ) : μ.real {ω | bias + fluctuation ≤ |(∑ i ∈ Finset.range n, Y i ω) - n*mean|} ≤ δ

The bias is produced from the same raw moment hypotheses as the fluctuation. The common mean is a distributional assumption, not a confidence assumption.

theorem truncated_sum_mean_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (B : ℕ → ℝ) (ε u b L mean : ℝ) (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) ≤ |(∑ i ∈ Finset.range n, truncate (B i) (X i ω)) - n * mean|} ≤ 2 * Real.exp (-L)

Fixed positive sample-size confidence for the actual truncated empirical mean.

theorem truncated_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 ≤ |(∑ i ∈ Finset.range n, truncate (B i) (X i ω)) / n - mean|} ≤ 2 * Real.exp (-L)