Documentation

LeanPool.HighContrastHomogenization.Provider.Window.PsiShellAlgebra

High-contrast homogenization: Provider.Window.PsiShellAlgebra #

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

source
theorem HCPolySupport.IndependentSums.psi_lower_scaled_pow {Ψ : ℝ → ℝ} {B t : ℝ} (m : ℕ) (hB : 1 ≤ B) (hΨ : HasPsiGrowth Ψ B) (hAdmissible : AdmissiblePsi Ψ) (ht : B ^ m ≤ t) :
B ^ natTriangular m * (t / B ^ m) ^ m ≤ Ψ t

Iterated gauge growth, run backwards from a point above B^m.

source
theorem HCPolySupport.IndependentSums.rpow_div_psi_le {Ψ : ℝ → ℝ} {B t : ℝ} (n m : ℕ) (hB : 1 ≤ B) (hΨ : HasPsiGrowth Ψ B) (hAdmissible : AdmissiblePsi Ψ) (ht : B ^ m ≤ t) :
t ^ (↑n - 1) / Ψ t ≤ B ^ natTriangular (m + 1) * t ^ (↑n - ↑m - 1)

On a region above B^m, degree m growth removes m powers from the shifted moment quotient.