MomentBoostedChernoff

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Internal finite-family Chernoff reduction for moment-boosted tails

This module is a deterministic probability component of the p > 2 branch for e.kl.bounds.large; it is not a source-facing stream theorem. It turns the strengthened one-sided tail and an independently verified second moment into the exact finite-sum truncation estimate used by the later coloring transport. The key tilted-tail bound is supplied by MomentBoostedTruncation.lean, whose fixed base is independent of sigma.

The argument is a direct use of the local truncated-MGF and independent-sum A. No generic gammaTriangleConst is invoked.

theorem Algsuperdiff.Section3.Provider.Stream.measureReal_upperTailEvent_finset_sum_le_momentBoosted {Omega : Type u_1} {iota : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : iota → Omega → ℝ} {s : Finset iota} {a sigma l L C2 : ℝ} (h_indep : ProbabilityTheory.iIndepFun X mu) (h_meas : ∀ (i : iota), Measurable (X i)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) mu) (h_sq : ∀ i ∈ s, MeasureTheory.Integrable (fun (omega : Omega) => |X i omega| ^ 2) mu) (h_mean : ∀ i ∈ s, ∫ (omega : Omega), X i omega ∂mu = 0) (h_second : ∀ i ∈ s, ∫ (omega : Omega), |X i omega| ^ 2 ∂mu ≤ C2) (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) (X i) 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hlL : l ≤ momentBoostedKernelCoeff sigma * L ^ (sigma - 1)) : mu.real (HCPolySupport.IndependentSums.upperTailEvent (fun (omega : Omega) => ∑ i ∈ s, X i omega) a) ≤ Real.exp (-l * a + ↑s.card * (l ^ 2 * (C2 / 2 + Real.exp 1 / 2 + 48 ^ (2 / sigma) / 2))) + ↑s.card * (momentBoostedGammaSigma sigma L)⁻¹

Internal finite-family Chernoff estimate for centered unit-scale moment-boosted variables. The result deliberately remains at the explicit truncation stage; cutoff optimization and coloring are separate lemmas.