L² integral estimate

This module formalizes Lemma 3.1 from Chapter 3 of the ANTEDB blueprint. It proves both the blueprint's equality with a bounded error coefficient and the corresponding absolute-error bound.

A normalized smooth bump

Normalization and the exponential sum

Plancherel and decay of the bump's Fourier transform

Weighted Plancherel identity

Local L² bound

Smoothing identity

Decay of the smoothing error

Integrated smoothing-error bound

Lemma 3.1

theorem Expdb.l2_integral_estimate : ∃ (C : ℝ), 0 < C ∧ ∀ {ι : Type u_1} [inst : Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (N : ℝ), 0 < N → IsSeparatedFamily (1 / N) ξ → ∀ (left right T : ℝ), T = right - left → left ≤ right → ∃ (θ : ℝ), |θ| ≤ C ∧ ∫ (t : ℝ) in Set.Icc left right, ‖∑ r : ι, a r * ↑(Real.fourierChar (ξ r * t))‖ ^ 2 = (T + θ * N) * ∑ r : ι, ‖a r‖ ^ 2

Lemma 3.1 (L² integral estimate). If ξ is a finite 1 / N-separated family of real numbers, then over any interval of length T, ∫ |∑ r, a r * 𝐞 (ξ r * t)|² dt = (T + O(N)) * ∑ r, ‖a r‖². The conclusion expresses O(N) as θ * N, with θ bounded by a universal constant.

theorem Expdb.l2_integral_estimate_error : ∃ (C : ℝ), 0 < C ∧ ∀ {ι : Type u_1} [inst : Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (N : ℝ), 0 < N → IsSeparatedFamily (1 / N) ξ → ∀ (left right T : ℝ), T = right - left → left ≤ right → |(∫ (t : ℝ) in Set.Icc left right, ‖∑ r : ι, a r * ↑(Real.fourierChar (ξ r * t))‖ ^ 2) - T * ∑ r : ι, ‖a r‖ ^ 2| ≤ C * N * ∑ r : ι, ‖a r‖ ^ 2

Absolute-error form of the $L^2$ integral estimate.