ProductAnnulusCircle

ProductAnnulusCircle

Orbitwise circle inequalities lifted to a fixed product annulus. Scaffolding notes: ScaffoldingNotes/Circle/product_annulus_circle.md.

theorem Hermite1DimdLEAN.rhoPointwise (a u v : ℂ) : rho a u ≤ rho a v + ‖u - v‖

Reverse-triangle comparison for modulus defects.

theorem Hermite1DimdLEAN.rhoPointwiseSq (a u v : ℂ) : rho a u ^ 2 ≤ 2 * rho a v ^ 2 + 2 * ‖u - v‖ ^ 2

Quadratic defect comparison derived from rhoPointwise.

theorem Hermite1DimdLEAN.productAnnulusEstimate {d : ℕ} (hd : 1 ≤ d) (κ : MultiIndex d) (M : ℕ) (j : MultiIndex d) (G : FiniteHermiteSum d) (horth : hermiteInnerNu κ G = 0) : annulusMass j (evalHermiteSum κ (localPart j M G)) ≤ productAnnulusConstantSq d M * defectAnnulusMass κ j (evalHermiteSum κ (localPart j M G))

Annulus-local circle estimate for the local window.