noncomputable def BandlimitedBound.fourierTransformRd (d : ℕ) (f : EuclideanSpace ℝ (Fin d) → ℂ) : EuclideanSpace ℝ (Fin d) → ℂ

The Fourier transform f̂ on ℝ^d (Euclidean space), defined via VectorFourier.fourierIntegral using the standard character and inner product.

def BandlimitedBound.HasFourierSupportIn {d : ℕ} (g : EuclideanSpace ℝ (Fin d) → ℂ) (S : Set (EuclideanSpace ℝ (Fin d))) : Prop

g has Fourier support contained in S, i.e. supp ĝ ⊆ S.

structure BandlimitedBound.IsApproxIdentityMajorant {d : ℕ} (ψ : EuclideanSpace ℝ (Fin d) → ℝ) (r : ℝ) : Prop

A non-negative integrable majorant ψ at scale r > 0, used as an approximate identity in the bandlimited bound.

• nonneg (x : EuclideanSpace ℝ (Fin d)) : 0 ≤ ψ x
• integrable : MeasureTheory.Integrable ψ MeasureTheory.volume
• pos_scale : 0 < r

theorem BandlimitedBound.exists_convolution_repr (d : ℕ) (r : ℝ) (hr : 0 < r) (g : EuclideanSpace ℝ (Fin d) → ℂ) (hg : HasFourierSupportIn g (Metric.ball 0 (1 / r))) : ∃ (η : EuclideanSpace ℝ (Fin d) → ℂ), MeasureTheory.Integrable (fun (y : EuclideanSpace ℝ (Fin d)) => ‖η y‖) MeasureTheory.volume ∧ 0 < ∫ (y : EuclideanSpace ℝ (Fin d)), ‖η y‖ ∧ (∀ (x : EuclideanSpace ℝ (Fin d)), g x = ∫ (y : EuclideanSpace ℝ (Fin d)), g y * η (x - y)) ∧ (∀ (x : EuclideanSpace ℝ (Fin d)), MeasureTheory.MemLp (fun (y : EuclideanSpace ℝ (Fin d)) => ‖g y‖ * √‖η (x - y)‖) (ENNReal.ofReal 2) MeasureTheory.volume) ∧ (∀ (x : EuclideanSpace ℝ (Fin d)), MeasureTheory.MemLp (fun (y : EuclideanSpace ℝ (Fin d)) => √‖η (x - y)‖) (ENNReal.ofReal 2) MeasureTheory.volume) ∧ ∀ (x : EuclideanSpace ℝ (Fin d)), ∫ (y : EuclideanSpace ℝ (Fin d)), ‖η (x - y)‖ = ∫ (y : EuclideanSpace ℝ (Fin d)), ‖η y‖

If supp ĝ ⊆ B(0, 1/r), then g admits a convolution representation g(x) = ∫ g(y) η(x − y) dy for some integrable η, with the auxiliary L² integrability properties needed to apply Hölder's inequality.

theorem BandlimitedBound.sq_norm_le_convolution_approx_identity (d : ℕ) (r : ℝ) (hr : 0 < r) (g : EuclideanSpace ℝ (Fin d) → ℂ) (hg : HasFourierSupportIn g (Metric.ball 0 (1 / r))) : ∃ (C : ℝ) (_ : 0 < C) (ψ : EuclideanSpace ℝ (Fin d) → ℝ) (_ : IsApproxIdentityMajorant ψ r), ∀ (x : EuclideanSpace ℝ (Fin d)), ‖g x‖ ^ 2 ≤ C * MeasureTheory.convolution (fun (y : EuclideanSpace ℝ (Fin d)) => ‖g y‖ ^ 2) ψ (ContinuousLinearMap.mul ℝ ℝ) MeasureTheory.volume x

Bandlimited bound (Lemma, "Fourier method in Euclidean space"). If supp ĝ ⊆ B_{1/r}, then |g(x)|² ≲ (|g|² ∗ ψ_r)(x) for some non-negative approximate identity ψ_r at scale r. This is the key estimate that turns a Fourier support hypothesis into a pointwise inequality controlling |g|² by its convolution against a mollifier.