Documentation

Expdb.Fourier.Bump

A normalized smooth bump and its Fourier transform #

This module collects the concrete bump function used in the proof of the L² integral estimate of the blueprint's Basic Fourier estimates chapter (l2-chapter), together with its Fourier transform and the orthonormal family formed by its translates.

The bump bump is a fixed smooth, nonnegative, compactly supported function with ‖bump‖_{L²} = 1 and support in [-1/4, 1/4]. Its translates by 1-separated shifts are therefore orthonormal, which is what the L² estimate uses.

These declarations are auxiliary to Expdb.Fourier.L2Integral and are collected in the namespace Expdb.L2Bump.

A normalized smooth bump #

noncomputable def Expdb.L2Bump.rawBump :

Equations

Expdb.L2Bump.rawBump = { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := Expdb.L2Bump.rawBump._proof_1, rIn_lt_rOut := Expdb.L2Bump.rawBump._proof_2 }

Instances For

noncomputable def Expdb.L2Bump.rawL2 :

Equations

Expdb.L2Bump.rawL2 = ∫ (x : ℝ), ↑Expdb.L2Bump.rawBump x ^ 2

Instances For

noncomputable def Expdb.L2Bump.bump (x : ℝ) :

Equations

Expdb.L2Bump.bump x = ↑Expdb.L2Bump.rawBump x / √Expdb.L2Bump.rawL2

Instances For

theorem Expdb.L2Bump.bump_smooth :

ContDiff ℝ (↑⊤) bump

theorem Expdb.L2Bump.bump_hasCompactSupport :

HasCompactSupport bump

theorem Expdb.L2Bump.bump_supp (x : ℝ) (hx : bump x ≠ 0) :

|x| ≤ 1 / 4

theorem Expdb.L2Bump.bump_nonneg (x : ℝ) :

theorem Expdb.L2Bump.bump_l2norm :

∫ (x : ℝ), bump x ^ 2 = 1

noncomputable def Expdb.L2Bump.bumpFourier (u : ℝ) :

Equations

Expdb.L2Bump.bumpFourier u = ∫ (x : ℝ), ↑(Expdb.L2Bump.bump x) * ↑(Real.fourierChar (-(x * u)))

Instances For

theorem Expdb.L2Bump.bump_integrable :

MeasureTheory.Integrable bump MeasureTheory.volume

Plancherel and decay of the bump's Fourier transform #

theorem Expdb.L2Bump.bumpFourier_continuous :

Continuous bumpFourier

theorem Expdb.L2Bump.bumpFourier_l2 :

∫ (u : ℝ), ‖bumpFourier u‖ ^ 2 = 1

theorem Expdb.L2Bump.bumpFourier_sq_integrable :

MeasureTheory.Integrable (fun (u : ℝ) => ‖bumpFourier u‖ ^ 2) MeasureTheory.volume

theorem Expdb.L2Bump.bumpFourier_decay (K : ℕ) :

∃ (C : ℝ), 0 < C ∧ ∀ (u : ℝ), ‖bumpFourier u‖ ≤ C * (1 + |u|) ^ (-↑K)

theorem Expdb.L2Bump.bumpFourier_lower_bound :

∃ (c : ℝ) (δ : ℝ), 0 < c ∧ 0 < δ ∧ ∀ (u : ℝ), |u| ≤ δ → c ≤ ‖bumpFourier u‖ ^ 2

Weighted Plancherel identity #

noncomputable def Expdb.L2Bump.bumpShift (w : ℝ) :

SchwartzMap ℝ ℂ

Equations

Expdb.L2Bump.bumpShift w = ⋯.toSchwartzMap ⋯

Instances For

theorem Expdb.L2Bump.bumpShift_apply (w x : ℝ) :

(bumpShift w) x = ↑(bump (x + w))

theorem Expdb.L2Bump.fourier_bumpShift (w u : ℝ) :

FourierTransform.fourier (⇑(bumpShift w)) u = ↑(Real.fourierChar (w * u)) * bumpFourier u

theorem Expdb.L2Bump.bumpShift_orthonormal {ι : Type u_1} [Finite ι] (ξ : ι → ℝ) (N : ℝ) (hN : 0 < N) (hsep : IsSeparatedFamily (1 / N) ξ) :

Orthonormal ℂ fun (r : ι) => (bumpShift (N * ξ r)).toLp 2 MeasureTheory.volume