High-contrast homogenization: Provider.Window.StrongTailMoment

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

theorem HCPolySupport.IndependentSums.lintegral_rpow_le_of_strongPsiTail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {B : ℝ} {W : Ω → ℝ} (N : ℕ) (hN : 1 ≤ N) (hB : 2 ≤ B) (hGrowth : HasPsiGrowth Ψ B) (hAdmissible : AdmissiblePsi Ψ) (hWm : AEMeasurable W μ) (hW0 : ∀ (ω : Ω), 0 ≤ W ω) (htail : ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real {ω : Ω | t < W ω} ≤ (t * Ψ t)⁻¹) : ∫⁻ (ω : Ω), ENNReal.ofReal (W ω ^ ↑N) ∂μ ≤ ENNReal.ofReal (1 + 2 * ↑N * (1 + Real.log B) * B ^ natTriangular N)

An integer moment from a tail with the extra inverse power.