High-contrast homogenization: Provider.Window.PsiShellIntegral

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

theorem HCPolySupport.IndependentSums.lintegral_rpow_div_psi_le {Ψ : ℝ → ℝ} {B : ℝ} (n : ℕ) (hB : 2 ≤ B) (hΨ : HasPsiGrowth Ψ B) (hAdmissible : AdmissiblePsi Ψ) : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t ^ (↑n - 1) / Ψ t) ≤ ENNReal.ofReal (2 * (1 + Real.log B) * B ^ natTriangular (n + 1))

The shifted gauge tail has the exact natural-shell integral needed for integer moments.