BasisLocalization

theorem HermitekLEAN.phi0_localization (k : ℕ) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ∀ (j : ℕ), annulusIntegralSq (phi0 k) j ≤ C * Real.exp (-c * posPart (↑j - ↑(k + 5)) ^ 2)

Localization of the lowest vector Phi k 0.

theorem HermitekLEAN.single_basis_localization (k : ℕ) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ∀ (n j : ℕ), 1 ≤ n → annulusIntegralSq (Phi k n) j ≤ C * Real.exp (-c * posPart (|↑j - √↑n| - ↑(k + 4)) ^ 2)

Single-basis localization near the annulus |z| ~ sqrt n.