High-contrast homogenization: Provider.Window.PsiShellFinite

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

theorem HCPolySupport.IndependentSums.lintegral_Ioc_pow_le_shell_sum (f : ℝ → ENNReal) {B : ℝ} (hB : 1 ≤ B) (n : ℕ) : ∫⁻ (t : ℝ) in Set.Ioc 1 (B ^ n), f t ≤ ∑ j ∈ Finset.range n, ∫⁻ (t : ℝ) in Set.Ioc (B ^ j) (B ^ (j + 1)), f t

theorem HCPolySupport.IndependentSums.lintegral_finite_psi_shells_le {Ψ : ℝ → ℝ} {B : ℝ} (n : ℕ) (hB : 2 ≤ B) (hΨ : HasPsiGrowth Ψ B) (hAdmissible : AdmissiblePsi Ψ) : ∑ j ∈ Finset.range n, ∫⁻ (t : ℝ) in Set.Ioc (B ^ j) (B ^ (j + 1)), ENNReal.ofReal (t ^ (↑n - 1) / Ψ t) ≤ ENNReal.ofReal (B ^ natTriangular (n + 1))

The shells below B^n sum to one triangular growth factor.