DegreeBookkeeping

DegreeBookkeeping

Finite degree intervals and support-width bounds on a fixed annulus. Scaffolding notes: ScaffoldingNotes/Blocks/degree_bookkeeping.md.

theorem Hermite1DimdLEAN.localDegreeInterval {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : (∀ n ∈ localDegreeSet j M G, degreeIntervalLower j M ≤ n ∧ n ≤ degreeIntervalUpper j M) ∧ (localDegreeSet j M G).card ≤ degreeWidth j M

Local degree support lies in an explicit interval.

theorem Hermite1DimdLEAN.degreeIntervalOrder {d : ℕ} (j : MultiIndex d) (M : ℕ) : degreeIntervalLower j M ≤ degreeIntervalUpper j M

Crude bounds on the degree interval in terms of the annulus radius.

theorem Hermite1DimdLEAN.lowAnnulusDegreeWidthBound {d : ℕ} (hd : 1 ≤ d) (j : MultiIndex d) (M : ℕ) (_hj : annulusRadius j < M + 1) : degreeWidth j M ≤ d * (annulusRadius j + M + 1) ^ 2

Low-annulus crude width bound in terms of the annulus radius.

theorem Hermite1DimdLEAN.uniformLowAnnulusWidthBound {d : ℕ} (hd : 1 ≤ d) (j : MultiIndex d) (M : ℕ) (hj : annulusRadius j < degreeThreshold d M) : degreeWidth j M ≤ d * (degreeThreshold d M + M) ^ 2

Uniform low-annulus width bound at the frozen threshold J(d,M).

theorem Hermite1DimdLEAN.highAnnulusDegreeBounds {d : ℕ} (hd : 1 ≤ d) (j : MultiIndex d) (M : ℕ) (hj : M + 1 ≤ annulusRadius j) : (annulusRadius j - M) ^ 2 ≤ degreeIntervalLower j M ∧ degreeWidth j M ≤ d * (2 * M + 1) * (2 * annulusRadius j + 1)

High-annulus crude degree lower/width upper bounds in terms of the annulus radius.

theorem Hermite1DimdLEAN.highFrequencyThreshold {d : ℕ} (hd : 1 ≤ d) (j : MultiIndex d) (M : ℕ) (hj : degreeThreshold d M ≤ annulusRadius j) : 1343 * degreeWidth j M ^ 2 ≤ degreeIntervalLower j M ^ 2

High-frequency threshold needed for the imported band estimate.

theorem Hermite1DimdLEAN.zeroPaddingBand (N L : ℕ) (E : Finset ℕ) (b : ℕ → ℂ) (hE : ∀ n ∈ E, N ≤ n ∧ n < N + L) : ∃ (c : Fin L → ℂ), positiveFrequencyPolynomial E b = bandLimitedPolynomial N L c

Zero-padding turns arbitrary finite support inside a band into a full band.

theorem Hermite1DimdLEAN.zeroFrequencyAbsent {d : ℕ} (κ j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) (horth : hermiteInnerNu κ G = 0) : 0 ∉ localDegreeSet j M G

Orthogonality to ν_κ removes zero from every local degree window.