BlockDecomposition

Def 5.1: Frequency blocks

I_ℓ = { n : ℕ | ℓ² ≤ n ∧ n < (ℓ+1)² } for ℓ ≥ 1. Note: |I_ℓ| = 2ℓ + 1.

def FockSPR.freqBlock (ℓ : ℕ) : Finset ℕ

The frequency block I_ℓ = [ℓ², (ℓ+1)² − 1].

Equations

• FockSPR.freqBlock ℓ = Finset.Icc (ℓ ^ 2) ((ℓ + 1) ^ 2 - 1)

Def 5.2: Block polynomials

U_ℓ(z) = ∑_{n ∈ I_ℓ, n ≤ D} a_n z^n.

def FockSPR.blockPoly {D : ℕ} (a : Fin D → ℂ) (ℓ : ℕ) (z : ℂ) : ℂ

The block polynomial: restriction of U to frequencies in I_ℓ.

Equations

• FockSPR.blockPoly a ℓ z = ∑ k : Fin D, if ↑k + 1 ∈ FockSPR.freqBlock ℓ then a k * z ^ (↑k + 1) else 0

Def 5.3: Maximum block index

Λ = ⌊√D⌋.

def FockSPR.maxBlockIndex (D : ℕ) : ℕ

Λ = Nat.sqrt D — the index of the last complete block.

Equations

• FockSPR.maxBlockIndex D = D.sqrt

Def 5.4: Local and remainder pieces

For fixed M ≥ 1 and j : ℕ: V_j = ∑_{ℓ : max(1,j−M) ≤ ℓ ≤ min(Λ,j+M)} U_ℓ R_j = U − V_j

def FockSPR.localPoly {D : ℕ} (a : Fin D → ℂ) (M j : ℕ) (z : ℂ) : ℂ

The local polynomial around annulus j, collecting blocks within distance M.

Equations

• FockSPR.localPoly a M j z = ∑ ℓ ∈ Finset.Icc (max 1 (j - M)) (min (FockSPR.maxBlockIndex D) (j + M)), FockSPR.blockPoly a ℓ z

def FockSPR.remainderPoly {D : ℕ} (a : Fin D → ℂ) (M j : ℕ) (z : ℂ) : ℂ

The remainder polynomial: R_j = U − V_j.

Equations

• FockSPR.remainderPoly a M j z = FockSPR.polyEval a z - FockSPR.localPoly a M j z

Helper lemmas

theorem FockSPR.freqBlock_card (ℓ : ℕ) : (freqBlock ℓ).card = 2 * ℓ + 1

The cardinality of freqBlock ℓ is 2ℓ + 1.

Fourier analysis helpers

Theorem 5.1: Blocks are frequency-disjoint

For ℓ₁ ≠ ℓ₂ with ℓ₁, ℓ₂ ≥ 1: I_{ℓ₁} ∩ I_{ℓ₂} = ∅.

theorem FockSPR.blocks_disjoint {ℓ₁ ℓ₂ : ℕ} (h₁ : 1 ≤ ℓ₁) (h₂ : 1 ≤ ℓ₂) (hne : ℓ₁ ≠ ℓ₂) : Disjoint (freqBlock ℓ₁) (freqBlock ℓ₂)

Theorem 5.2: Blocks partition {1, …, D}

Every n ∈ {1, …, D} belongs to exactly one block I_ℓ.

theorem FockSPR.blocks_cover (D n : ℕ) (hn : 1 ≤ n) (_hnD : n ≤ D) : ∃ (ℓ : ℕ), 1 ≤ ℓ ∧ n ∈ freqBlock ℓ

Theorem 5.3: Fock norm decomposes

fockNormSq(U) = ∑_{ℓ=1}^Λ fockNormSq(U_ℓ) (up to tail).

Proof: The blocks are frequency-disjoint, and fockNormSq is a sum over frequencies.

theorem FockSPR.fockNorm_decomposes {D : ℕ} (a : Fin D → ℂ) : fockNormSq a = ∑ ℓ ∈ Finset.Icc 1 (maxBlockIndex D), ∑ k : Fin D, if ↑k + 1 ∈ freqBlock ℓ then ‖a k‖ ^ 2 * ↑(↑k + 1).factorial else 0

Theorem 5.4: Orthogonality on circles

For ℓ₁ ≠ ℓ₂, r ≥ 0: ∫ U_{ℓ₁}(r e^{it}) * conj(U_{ℓ₂}(r e^{it})) d(haar)(t) = 0

Proof: Disjoint frequency supports ⟹ orthogonality of exponentials.

theorem FockSPR.blocks_orthogonal_circle {D : ℕ} (a : Fin D → ℂ) {ℓ₁ ℓ₂ : ℕ} (_h₁ : 1 ≤ ℓ₁) (_h₂ : 1 ≤ ℓ₂) (hne : ℓ₁ ≠ ℓ₂) (r : ℝ) (_hr : 0 ≤ r) : ∫ (t : AddCircle T), blockPoly a ℓ₁ (↑r * (fourier 1) t) * (starRingEnd ℂ) (blockPoly a ℓ₂ (↑r * (fourier 1) t)) ∂AddCircle.haarAddCircle = 0

Theorem 5.5: Frequency support of V_j

For j ≥ M + 1:

• Frequency support of V_j ⊆ [(j−M)², (j+M+1)²).
• All frequencies ≥ 1.
• Number of frequencies: L_j = (2M+1)(2j+1).

For 0 ≤ j ≤ M:

• Frequency support ⊆ [1, (j+M+1)²).
• Number of frequencies ≤ (j+M+1)² − 1.

theorem FockSPR.freq_support_localPoly_lower {ℓ M j : ℕ} (_hM : 1 ≤ M) (hj : M + 1 ≤ j) (n : ℕ) : n ∈ freqBlock ℓ → ℓ ∈ Finset.Icc (max 1 (j - M)) (j + M) → (j - M) ^ 2 ≤ n

Frequencies of V_j are all ≥ (j−M)² when j ≥ M + 1.

theorem FockSPR.freq_count_localPoly {M j : ℕ} (hM : 1 ≤ M) (hj : M + 1 ≤ j) : ∑ ℓ ∈ Finset.Icc (max 1 (j - M)) (j + M), (freqBlock ℓ).card = (2 * M + 1) * (2 * j + 1)

The number of frequencies in V_j for j ≥ M + 1 is (2M+1)(2j+1).

Theorem 5.6: Monomial peak localization

For n ∈ I_ℓ with ℓ ≥ 1: ℓ < √(n + 1/2) < ℓ + 1 i.e., r_n = √(n + 1/2) ∈ (ℓ, ℓ+1).

Proof: n ≥ ℓ² gives n + 1/2 > ℓ², so √(n+1/2) > ℓ. n < (ℓ+1)² gives n + 1/2 < (ℓ+1)², so √(n+1/2) < ℓ+1.

theorem FockSPR.monomial_peak_localization {n ℓ : ℕ} (hℓ : 1 ≤ ℓ) (hn : n ∈ freqBlock ℓ) : ↑ℓ < √(↑n + 1 / 2) ∧ √(↑n + 1 / 2) < ↑ℓ + 1