The Gaussian is a positive-definite function

The Gaussian a ↦ exp (-c‖a‖²) on a real inner-product space V is continuous, and its subtraction kernel (a, b) ↦ exp (-c‖a - b‖²) is positive definite, for every c ≥ 0. This supplies the positive-definiteness half of the Gaussian acceptance example requested in Part C of the OneParameterSemigroups roadmap in TauCetiRoadmap ("positive-definite functions and Bochner's theorem"); the representing-measure half is supplied by TauCeti.bochner in TauCeti/Analysis/Bochner/BochnerTheorem.lean.

The positive-definiteness is not proved from scratch: Mathlib's ProbabilityTheory.charFun_stdGaussian computes the characteristic function of the standard Gaussian measure on V to be t ↦ exp (-‖t‖²/2), and TauCeti.posSemidef_charFun (the finite-measure Fourier-transform correspondence) already records that a characteristic function has a positive-definite kernel. Rescaling the argument by √(2c) turns exp (-‖·‖²/2) into exp (-c‖·‖²). The standard Gaussian measure needs a finite-dimensional space, but the kernel form transfers to an arbitrary real inner-product space: positive definiteness constrains only finite families of points, and those span a finite-dimensional subspace on which the norm — hence the kernel — restricts. The function form then follows on that same generality through isPositiveDefinite_iff_posSemidef_sub.

Main declarations

• TauCeti.charFun_stdGaussian_sqrt_smul: on a finite-dimensional space, charFun (stdGaussian V) (√(2c) • a) = exp (-c‖a‖²).
• TauCeti.isPositiveDefinite_cexp_neg_mul_sq_norm: on any real inner-product space, a ↦ exp (-c‖a‖²) is positive definite for c ≥ 0 under the negation involution.
• TauCeti.posSemidef_cexp_neg_mul_sq_norm: the involution-free kernel form, (a, b) ↦ exp (-c‖a - b‖²) is a positive-definite kernel on any real inner-product space.
• TauCeti.continuous_cexp_neg_mul_sq_norm: a ↦ exp (-c‖a‖²) is continuous.
• TauCeti.tendsto_cexp_neg_mul_sq_norm: exp (-c‖a‖²) → 1 as c → 0.
• TauCeti.integrable_cexp_neg_mul_sq_norm: a ↦ exp (-c‖a‖²) is integrable for c > 0.
• TauCeti.isPositiveDefinite_cexp_neg_sq_norm: the positive-definiteness half of the Gaussian acceptance example (c = 1), a ↦ exp (-‖a‖²).
• TauCeti.posSemidef_cexp_neg_sq_norm: the involution-free kernel form of the c = 1 acceptance example, (a, b) ↦ exp (-‖a - b‖²).

References

• W. Rudin, Fourier Analysis on Groups (1962) — Bochner's theorem and positive-definite functions.
• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Chapter 3.

The Gaussian factor

theorem TauCeti.continuous_cexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] (c : ℝ) : Continuous fun (a : V) => Complex.exp (-↑(c * ‖a‖ ^ 2))

The Gaussian a ↦ exp (-c‖a‖²) is continuous on V for every real c.

theorem TauCeti.tendsto_cexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] (a : V) : Filter.Tendsto (fun (c : ℝ) => Complex.exp (-↑(c * ‖a‖ ^ 2))) (nhds 0) (nhds 1)

The Gaussian factor exp (-c‖a‖²) tends to 1 as the width parameter c tends to 0. This is the pointwise convergence underlying Gaussian regularization.

The finite-dimensional case

theorem TauCeti.integrable_cexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {c : ℝ} (hc : 0 < c) : MeasureTheory.Integrable (fun (a : V) => Complex.exp (-↑(c * ‖a‖ ^ 2))) MeasureTheory.volume

The Gaussian a ↦ exp (-c‖a‖²) is integrable on V for every c > 0.

theorem TauCeti.charFun_stdGaussian_sqrt_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {c : ℝ} (hc : 0 ≤ c) (a : V) : MeasureTheory.charFun (ProbabilityTheory.stdGaussian V) (√(2 * c) • a) = Complex.exp (-↑(c * ‖a‖ ^ 2))

The characteristic function of the standard Gaussian measure on V, with its argument rescaled by √(2c), is the Gaussian a ↦ exp (-c‖a‖²).

Positive definiteness on an arbitrary inner-product space

theorem TauCeti.posSemidef_cexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {c : ℝ} (hc : 0 ≤ c) : Matrix.PosSemidef fun (a b : V) => Complex.exp (-↑(c * ‖a - b‖ ^ 2))

The translation-invariant kernel attached to the Gaussian, (a, b) ↦ exp (-c‖a - b‖²), is positive definite for every c ≥ 0, on any real inner-product space. This is the kernel form of isPositiveDefinite_cexp_neg_mul_sq_norm, avoiding any explicit choice of involution on the domain.

Positive definiteness constrains only finite families of points, and any finite family spans a finite-dimensional subspace on which the kernel restricts to the Gaussian kernel of that subspace; so the statement follows from the finite-dimensional case, where the Gaussian is the characteristic function of the standard Gaussian measure.

theorem TauCeti.isPositiveDefinite_cexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [StarAddMonoid V] (hstar : ∀ (x : V), star x = -x) {c : ℝ} (hc : 0 ≤ c) : IsPositiveDefinite fun (a : V) => Complex.exp (-↑(c * ‖a‖ ^ 2))

The Gaussian a ↦ exp (-c‖a‖²) on a real inner-product space is positive definite for every c ≥ 0, under the negation involution a⋆ = -a. This is the function form of posSemidef_cexp_neg_mul_sq_norm.

theorem TauCeti.isPositiveDefinite_cexp_neg_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [StarAddMonoid V] (hstar : ∀ (x : V), star x = -x) : IsPositiveDefinite fun (a : V) => Complex.exp (-↑(‖a‖ ^ 2))

The positive-definiteness half of the Gaussian acceptance example (c = 1): a ↦ exp (-‖a‖²) is positive definite under the negation involution.

theorem TauCeti.posSemidef_cexp_neg_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : Matrix.PosSemidef fun (a b : V) => Complex.exp (-↑(‖a - b‖ ^ 2))

The involution-free kernel form of the Gaussian acceptance example (c = 1): (a, b) ↦ exp (-‖a - b‖²) is a positive-definite kernel. Unlike isPositiveDefinite_cexp_neg_sq_norm, this requires no choice of involution on V.