Documentation

TauCeti.Analysis.Bochner.Fourier.Nonneg

Nonnegativity of the Fourier transform of a positive-definite function #

For a continuous, integrable function F : V → ℂ on a finite-dimensional real inner-product space whose subtraction kernel (a, b) ↦ F (a - b) is positive definite, the Fourier transform 𝓕 F is real and nonnegative: its real part is nonnegative at every frequency and its imaginary part vanishes. This is the analytic half of Bochner's theorem.

The real-part nonnegativity is proved by Fejér ball averaging. For a fixed frequency ξ, the twisted function ψ = fourierAtom ξ * F is still positive definite (Schur product with the Fourier atom kernel), continuous, and integrable, and 𝓕 F ξ = ∫ ψ. For R > 0 the averaged double integral J_R = vol(B_R)⁻¹ ∬_{B_R × B_R} ψ (x - y) has nonnegative real part because it is a limit of positive-definite double sums (simple-function approximation of the identity), while Fubini rewrites J_R = ∫ ψ · overlapRatio R whose dominated limit as R → ∞ is ∫ ψ.

Building on this, the Fourier transform of such a function is itself integrable: testing against a shrinking family of Gaussians and using the Parseval/Fubini identity bounds ∫ (𝓕 F) · exp (-t‖·‖²) by (F 0).re uniformly in t, and Fatou's lemma passes to the limit.

Adapted (Apache 2.0) from the Bochner–Minlos formalization by Michael R. Douglas (https://github.com/mrdouglasny/bochner, revision 08eb302), source files Bochner/FejerPD.lean and Bochner/Main.lean; the arguments are ported with the positive-definiteness hypotheses restated through Matrix.PosSemidef.

Main declarations #

References #

A simple-function expansion for integrals of compositions #

Consequences of positive definiteness for a subtraction kernel #

Step A: the positive-definite double integral has nonnegative real part #

The Fejér overlap ratio #

Step B: the Fubini identity for the Fejér average #

Step C: the integral of a positive-definite function has nonnegative real part #

The main theorems #

source
theorem TauCeti.fourier_re_nonneg_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (hcont : Continuous F) (ξ : V) :
0 ≤ (FourierTransform.fourier F ξ).re

The Fourier transform of a continuous integrable positive-definite function on a finite-dimensional real inner-product space has nonnegative real part.

Rudin, Fourier Analysis on Groups, Theorem 1.4.3; Folland, A Course in Abstract Harmonic Analysis, §4.2, Lemma 4.8.

source
theorem TauCeti.fourier_im_eq_zero_of_map_neg_eq_conj {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hsymm : ∀ (v : V), F (-v) = (starRingEnd ℂ) (F v)) (_hint : MeasureTheory.Integrable F MeasureTheory.volume) (ξ : V) :
(FourierTransform.fourier F ξ).im = 0

The Fourier transform of an integrable function whose subtraction kernel is positive definite, on a finite-dimensional real inner-product space, has vanishing imaginary part — by Hermitian symmetry and the negation invariance of Haar measure.

The argument never uses _hint, and the statement is provable without it: each step — Real.fourier_eq, integral_conj, integral_neg_eq_self — is an equality that survives a divergent integral, both sides then being the default value 0. So requiring integrability is a deliberate design choice, not a proof obligation. Without it 𝓕 F is that default value rather than the Fourier transform, so on a non-integrable conjugate-symmetric function such as F = 1 the conclusion degenerates to (0 : ℂ).im = 0; keeping those vacuous instances out of the public API is worth the strength given up. Hence the hypothesis is bound as _hint.

Not a @[simp] lemma: neither side condition is dischargeable by simp's discharger, so the rule would be tried against every (𝓕 _ _).im and never fire.

source
theorem TauCeti.fourier_eq_re_of_map_neg_eq_conj {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hsymm : ∀ (v : V), F (-v) = (starRingEnd ℂ) (F v)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (ξ : V) :
FourierTransform.fourier F ξ = ↑(FourierTransform.fourier F ξ).re

The Fourier transform of an integrable conjugate-symmetric function on a finite-dimensional real inner-product space is real: it equals the coercion of its own real part.

As in fourier_im_eq_zero_of_map_neg_eq_conj, hint is a design choice rather than a proof obligation — it is used only to discharge that lemma, which is itself provable without it. It is required here so that the conclusion cannot be read off a divergent integral's default value.

source
theorem TauCeti.fourier_im_eq_zero_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (ξ : V) :
(FourierTransform.fourier F ξ).im = 0

The positive-definite specialization of fourier_im_eq_zero_of_map_neg_eq_conj: a function with positive-definite subtraction kernel is conjugate-symmetric.

source
theorem TauCeti.fourier_eq_re_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (ξ : V) :
FourierTransform.fourier F ξ = ↑(FourierTransform.fourier F ξ).re

The positive-definite specialization of fourier_eq_re_of_map_neg_eq_conj.

Integrability of the Fourier transform of a positive-definite function #

source
theorem TauCeti.integrable_fourier_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (hcont : Continuous F) :
MeasureTheory.Integrable (FourierTransform.fourier F) MeasureTheory.volume

The Fourier transform of a continuous integrable positive-definite function is integrable.

Testing 𝓕 F against the Gaussians exp (-‖·‖²/(n+1)) gives integrals uniformly bounded by (F 0).re, and Fatou's lemma passes the bound to ∫⁻ ‖𝓕 F‖ₑ. Folland, A Course in Abstract Harmonic Analysis, §4.2.

The inverse transform #

The inverse Fourier transform 𝓕⁻ F = 𝓕 F ∘ (-·) is the density of the representing measure of Bochner's theorem, so nonnegativity, realness and integrability are recorded for it too.

source
theorem TauCeti.fourierInv_re_nonneg_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (hcont : Continuous F) (ξ : V) :
0 ≤ (FourierTransformInv.fourierInv F ξ).re

The inverse Fourier transform of a continuous integrable positive-definite function has nonnegative real part.

source
theorem TauCeti.fourierInv_eq_re_of_map_neg_eq_conj {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hsymm : ∀ (v : V), F (-v) = (starRingEnd ℂ) (F v)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (ξ : V) :
FourierTransformInv.fourierInv F ξ = ↑(FourierTransformInv.fourierInv F ξ).re

The inverse Fourier transform of an integrable conjugate-symmetric function is real: it equals the coercion of its own real part. As in fourier_im_eq_zero_of_map_neg_eq_conj, hint is a design choice rather than a proof obligation: it keeps the statement from being read off the default value of a divergent integral.

source
theorem TauCeti.fourierInv_eq_re_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (ξ : V) :
FourierTransformInv.fourierInv F ξ = ↑(FourierTransformInv.fourierInv F ξ).re

The positive-definite specialization of fourierInv_eq_re_of_map_neg_eq_conj.

source
theorem TauCeti.integrable_fourierInv_of_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (hcont : Continuous F) :
MeasureTheory.Integrable (FourierTransformInv.fourierInv F) MeasureTheory.volume

The inverse Fourier transform of a continuous integrable positive-definite function is integrable.

source
theorem TauCeti.measurable_ofReal_re_fourierInv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hint : MeasureTheory.Integrable F MeasureTheory.volume) :
Measurable fun (ξ : V) => ENNReal.ofReal (FourierTransformInv.fourierInv F ξ).re

The ℝ≥0∞-valued density (𝓕⁻ F).re of the Bochner representing measure is measurable whenever F is integrable.