ProductAnnulusLocalization

ProductAnnulusLocalization

Finite block-localization scaffold for product annuli and coefficient windows.

theorem DimdPolyLEAN.annulusMassPartition {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (J : ℕ) (H : Pkappa d kappa) : lowAnnulusMass J (ofPkappa kappa H) + highAnnulusMass J (ofPkappa kappa H) = ‖H‖ ^ 2

theorem DimdPolyLEAN.lowAnnulusProjection {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (J : ℕ) : ∃ (E : Finset (Idx d)) (rho : ℝ), 0 < rho ∧ ∀ {H : Pkappa d kappa}, ‖H‖ = 1 → ∑ alpha ∈ E, ‖coeffPkappa H alpha‖ ^ 2 ≤ rho → lowAnnulusMass J (ofPkappa kappa H) ≤ 1 / 4