Documentation

Expdb.Fourier.L2Integral

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.

The exponential sum #

source
noncomputable def Expdb.expSum {ι : Type u_1} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (t : ℝ) :
ℂ

The exponential sum with coefficients a and frequencies ξ, evaluated at t.

Equations
Instances For
    source
    theorem Expdb.expSum_continuous {ι : Type u_1} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) :
    Continuous (expSum a ξ)

    An exponential sum is continuous in its evaluation point.

    Local L² bound #

    Smoothing identity #

    Decay of the smoothing error #

    Integrated smoothing-error bound #

    L² integral estimate lemma #

    source
    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.

    source
    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‖².

    source
    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.