L² integral estimate

This module formalizes the L² integral estimate from the blueprint's Basic Fourier estimates chapter (l2-chapter). It proves both the blueprint's equality with a bounded error coefficient and the corresponding absolute-error bound.

A normalized smooth bump

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

L² integral estimate lemma

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

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² integral estimate: for a 1 / N-separated family, the integral differs from T * ∑ r, ‖a r‖² by at most a universal constant times N * ∑ r, ‖a r‖².

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

A long enough interval contains a point where a separated exponential sum has at least half of its mean-square mass.