Coarse-graining support: Support.Probability.IndependentSums.Rosenthal.BennettKernel

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.IndependentSums.bennettKernel_le_rpow {p r : ℝ} (hp : 0 ≤ p) (hr : 0 ≤ r) : r ^ (p - 1) * Real.exp (-(p * bennettBeta (r ^ 2))) ≤ r ^ (p - 1)

The Bennett kernel is pointwise dominated by the pure power r^(p-1) on the nonnegative half-line.

theorem HCPolySupport.IndependentSums.bennettKernel_le_rpowTail {p r : ℝ} (hp : 2 ≤ p) (hr : Real.exp 2 ≤ r) : r ^ (p - 1) * Real.exp (-(p * bennettBeta (r ^ 2))) ≤ r ^ (-p / 2 - 1)

Beyond the large-scale Bennett threshold exp 2, the Rosenthal kernel is dominated by the integrable tail power r^(-p/2 - 1).

noncomputable def HCPolySupport.IndependentSums.rosenthalBennettIntegralConst : ℝ

A universal bound for the Bennett kernel integral appearing in the tail-integration step of Rosenthal's inequality.

Equations

• HCPolySupport.IndependentSums.rosenthalBennettIntegralConst = 4 * Real.exp 2

theorem HCPolySupport.IndependentSums.rosenthal_bennett_kernel_integral_le {p : ℝ} (hp : 2 ≤ p) : p * ∫ (r : ℝ) in Set.Ioi 0, r ^ (p - 1) * Real.exp (-(p * bennettBeta (r ^ 2))) ≤ rosenthalBennettIntegralConst ^ p

theorem HCPolySupport.IndependentSums.integrableOn_rosenthal_bennett_kernel {p : ℝ} (hp : 2 ≤ p) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ (p - 1) * Real.exp (-(p * bennettBeta (r ^ 2)))) (Set.Ioi 0) MeasureTheory.volume

The universal Bennett kernel appearing in the Rosenthal proof is integrable on (0, ∞).

theorem HCPolySupport.IndependentSums.rosenthal_bennett_scaled_integral_le {p sigmaSq : ℝ} (hp : 2 ≤ p) (hSigma_pos : 0 < sigmaSq) : p * ∫ (t : ℝ) in Set.Ioi 0, t ^ (p - 1) * Real.exp (-(p * bennettBeta (t ^ 2 / (p * sigmaSq)))) ≤ (rosenthalBennettIntegralConst * (√p * √sigmaSq)) ^ p

After the moment-adapted truncation choice, the Bennett tail integral at variance scale σ² is exactly a scaled copy of the universal Bennett kernel integral.

theorem HCPolySupport.IndependentSums.integrableOn_rosenthal_bennett_scaled_kernel {p sigmaSq : ℝ} (hp : 2 ≤ p) (hSigma_pos : 0 < sigmaSq) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (p - 1) * Real.exp (-(p * bennettBeta (t ^ 2 / (p * sigmaSq))))) (Set.Ioi 0) MeasureTheory.volume

The Bennett kernel at variance scale σ² is integrable on (0, ∞).

theorem HCPolySupport.IndependentSums.lintegral_rpow_sup'_abs_eq_scaled_tail {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 0 < p) (h_meas : ∀ (i : ι), Measurable (X i)) : ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {ω : Ω | t / p < s.sup' hs fun (i : ι) => |X i ω|} * ENNReal.ofReal (t ^ (p - 1)) = ENNReal.ofReal (p ^ p) * ∫⁻ (ω : Ω), ENNReal.ofReal ((s.sup' hs fun (i : ι) => |X i ω|) ^ p) ∂μ

Layer cake for the Rosenthal maximum term: applying the standard L^p tail formula to the scaled maximum p M gives the exact p^p E[M^p] contribution.

noncomputable def HCPolySupport.IndependentSums.bennettOptimalLambda (v y t : ℝ) : ℝ

The optimizing Chernoff parameter in the Bennett exponent.

Equations

• HCPolySupport.IndependentSums.bennettOptimalLambda v y t = Real.log (1 + t * y / v) / y