LeakageEstimate

Private helpers

Private Lemma: Distance bound

For n ∈ I_ℓ and integer j ≥ 0: dist(√(n + 1/2), [j, j+1]) ≥ (|j − ℓ| − 1)₊

Proof: Since r_n ∈ (ℓ, ℓ+1) (Theorem 5.6):

• j ≥ ℓ + 1: dist = j − r_n > j − (ℓ+1) = |j−ℓ| − 1.
• j ≤ ℓ − 1: dist = r_n − (j+1) > ℓ − (j+1) = |j−ℓ| − 1.
• j = ℓ: r_n ∈ (j, j+1) ⊂ [j,j+1], so dist = 0 = (0−1)₊ = 0.

Theorem 5.7: Block-to-annulus leakage (single block)

For ℓ ≥ 1, j ≥ 0, and a : Fin D → ℂ defining U_ℓ:

(1/π) ∫_{j ≤ |z| < j+1} |U_ℓ(z)|² exp(−|z|²) dm ≤ exp(1/4) · exp(−(max(|j−ℓ|−1, 0))²) · fockNormSq(U_ℓ)

Proof:

1. Circle orthogonality (Thm 5.4): decompose into radial integrals.
2. Corollary 2.10: bound each radial integral.
3. Theorem 5.6: locate r_n in (ℓ, ℓ+1), bound distance.
4. Sum over n ∈ I_ℓ.

theorem FockSPR.block_annulus_leakage {D : ℕ} (a : Fin D → ℂ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (j : ℕ) : 2 * ∫ (r : ℝ) in ↑j..↑j + 1, r * Real.exp (-r ^ 2) * ∫ (t : AddCircle T), ‖blockPoly a ℓ (↑r * (fourier 1) t)‖ ^ 2 ∂AddCircle.haarAddCircle ≤ Real.exp (1 / 4) * Real.exp (-↑(max (↑j - ↑ℓ - 1) 0) ^ 2) * ∑ k : Fin D, if ↑k + 1 ∈ freqBlock ℓ then ‖a k‖ ^ 2 * ↑(↑k + 1).factorial else 0

Theorem 5.8: Total leakage bound

For M ≥ 2:

∑_j ∫_{A_j} |R_j|² dμ ≤ η_M · fockNormSq(U)

where η_M := 2 exp(1/4) ∑_{m ≥ M} exp(−m²).

Proof:

1. Orthogonality on annuli: ∫_{A_j} |R_j|² dμ = ∑_{|ℓ−j|>M} ∫_{A_j} |U_ℓ|² dμ.
2. Apply Theorem 5.7 to each term.
3. Swap order of summation (Tonelli): ∑_j ∑_{|ℓ−j|>M} … ≤ ∑_ℓ fockNormSq(U_ℓ) · ….
4. Inner sum: ∑_{|j−ℓ|>M} exp(−(|j−ℓ|−1)²) ≤ 2 ∑_{m≥M} exp(−m²).
5. Hence total ≤ η_M · fockNormSq(U).

noncomputable def FockSPR.etaCoeff (M bound : ℕ) : ℝ

The leakage coefficient η_M = 2 exp(1/4) ∑_{m ≥ M}^∞ exp(−m²).

Equations

• FockSPR.etaCoeff M bound = 2 * Real.exp (1 / 4) * ∑ m ∈ Finset.Icc M bound, Real.exp (-↑m ^ 2)

Helper: symmetric block_annulus_leakage

Helper: remainder ≤ far blocks (annulus level)

This combines two steps:

1. Circle Parseval: ‖R_j(r·ζ)‖²_{L²} = ∑_{k not near} ‖a_k‖² r^{2(k+1)}
2. Block grouping: ∑{k not near} ≤ ∑{far ℓ} ∑{k∈I_ℓ} = ∑{far ℓ} ‖U_ℓ(r·ζ)‖² (using blocks_cover and blocks_disjoint) These give a pointwise (in r) bound on the circle norm. The annulus-level bound follows by integrating against r exp(-r²) ≥ 0 and exchanging sum and integral (finite sum of continuous functions).

Helper: inner sum bound

Main theorem

theorem FockSPR.total_leakage_bound {D : ℕ} (a : Fin D → ℂ) {M : ℕ} (hM : 2 ≤ M) (ε : ℝ) : ε > 0 → ∃ (bound : ℕ), ∀ J ≥ bound, ∑ j ∈ Finset.range J, 2 * ∫ (r : ℝ) in ↑j..↑j + 1, r * Real.exp (-r ^ 2) * ∫ (t : AddCircle T), ‖remainderPoly a M j (↑r * (fourier 1) t)‖ ^ 2 ∂AddCircle.haarAddCircle ≤ (etaCoeff M J + ε) * fockNormSq a

Theorem 5.9: Explicit bound for η₅

η₅ < 4 × 10⁻¹¹

Proof: Bound exp(1/4) < 13/10, exp(-25) < 14/10¹², exp(-36) < 1/10¹⁴. Split the sum at m = 5, bound the tail by 95 · exp(-36).

theorem FockSPR.eta_5_bound : etaCoeff 5 100 < 4 / 10 ^ 11