Gaussian regularization of positive-definite functions

The Gaussian regularization φ_ε = φ · exp (-ε‖·‖²) of a positive-definite function φ on a real inner-product space is again positive definite (a Schur product with the Gaussian kernel) and converges to φ pointwise as ε → 0. On a finite-dimensional space and for ε > 0 it is integrable whenever φ is bounded and almost-everywhere strongly measurable — in particular whenever φ has a positive-definite subtraction kernel and is continuous. This is the approximation device of the second step of Bochner's theorem: it replaces a bounded positive-definite function by an integrable one to which Fourier inversion applies.

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

Main declarations

• TauCeti.gaussianRegularize: the Gaussian regularization φ_ε = φ · exp (-ε‖·‖²).
• TauCeti.posSemidef_gaussianRegularize: φ_ε has a positive-definite subtraction kernel whenever φ does.
• TauCeti.gaussianRegularize_apply_zero: regularization preserves the value at the origin.
• TauCeti.continuous_gaussianRegularize, TauCeti.integrable_gaussianRegularize, TauCeti.tendsto_gaussianRegularize: the basic analytic facts about φ_ε.

References

• W. Rudin, Fourier Analysis on Groups (1962), §1.4.
• G. B. Folland, A Course in Abstract Harmonic Analysis, §4.2.
• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part C (Bochner milestone).

The Gaussian regularization and its elementary properties

noncomputable def TauCeti.gaussianRegularize {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (ε : ℝ) : V → ℂ

The Gaussian regularization φ_ε = φ · exp (-ε‖·‖²) of a function φ. For ε > 0 and bounded φ — in particular when φ has a positive-definite subtraction kernel — it decays like a Gaussian, and as ε → 0⁺ it recovers φ pointwise.

Equations

• TauCeti.gaussianRegularize φ ε x = φ x * Complex.exp (-↑(ε * ‖x‖ ^ 2))

@[simp]

theorem TauCeti.gaussianRegularize_apply {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (ε : ℝ) (x : V) : gaussianRegularize φ ε x = φ x * Complex.exp (-↑(ε * ‖x‖ ^ 2))

The defining formula of the Gaussian regularization.

theorem TauCeti.gaussianRegularize_apply_zero {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (ε : ℝ) : gaussianRegularize φ ε 0 = φ 0

The Gaussian regularization preserves the value at the origin: the Gaussian factor is 1 there. This is what makes the regularized representing measures probability measures.

Not a @[simp] lemma: simp already proves it through gaussianRegularize_apply, and the simpNF linter reports the tagged form as a duplicate.

theorem TauCeti.continuous_gaussianRegularize {V : Type u_1} [NormedAddCommGroup V] {φ : V → ℂ} (hcont : Continuous φ) (ε : ℝ) : Continuous (gaussianRegularize φ ε)

The Gaussian regularization is continuous when φ is.

theorem TauCeti.tendsto_gaussianRegularize {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (x : V) : Filter.Tendsto (fun (ε : ℝ) => gaussianRegularize φ ε x) (nhds 0) (nhds (φ x))

The Gaussian regularization converges to φ pointwise as ε → 0.

Positive definiteness of the regularization

theorem TauCeti.posSemidef_gaussianRegularize {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {φ : V → ℂ} (hpd : Matrix.PosSemidef fun (a b : V) => φ (a - b)) {ε : ℝ} (hε : 0 ≤ ε) : Matrix.PosSemidef fun (a b : V) => gaussianRegularize φ ε (a - b)

The Gaussian regularization of a function with positive-definite subtraction kernel again has a positive-definite subtraction kernel: it is the Schur product of the original kernel with the Gaussian kernel (a, b) ↦ exp (-ε‖a - b‖²).

Integrability of the regularization

theorem TauCeti.integrable_gaussianRegularize {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {φ : V → ℂ} {C : ℝ} (hb : ∀ (x : V), ‖φ x‖ ≤ C) (hm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (gaussianRegularize φ ε) MeasureTheory.volume

The Gaussian regularization of a bounded a.e. strongly measurable function is integrable for every ε > 0: the Gaussian factor is integrable and dominates. In particular this applies to a continuous function with positive-definite subtraction kernel, which is bounded by (φ 0).re.