Limits of positive-definite functions

This file derives pointwise- and locally-uniform-limit closure for TauCeti.IsPositiveDefinite, the positive-definite function predicate on an involutive additive monoid, from Mathlib's closedness theorem for the cone of positive-semidefinite matrices.

This is the limit-closure item from Part C of the OneParameterSemigroups roadmap. The result is about positive-definiteness alone for pointwise limits; as the roadmap notes, continuity needs an additional hypothesis. Mathlib's TendstoLocallyUniformly.continuous provides continuity of a locally uniform limit when the approximating functions are frequently continuous, while this file provides the positive-definiteness conclusion.

Main declarations

• TauCeti.IsPositiveDefinite.of_tendsto: filter-level pointwise-limit closure for positive-definite functions.
• TauCeti.IsPositiveDefinite.of_forall_tendsto: the same result when every function in the family is positive definite.
• TauCeti.IsPositiveDefinite.of_seq_tendsto: the sequential atTop specialization.
• TauCeti.IsPositiveDefinite.of_tendstoLocallyUniformly: locally uniform limits of eventually positive-definite functions are positive definite.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Chapter 3.

theorem TauCeti.IsPositiveDefinite.of_tendsto {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → M → ℂ} {G : M → ℂ} (hF : ∀ᶠ (i : ι) in l, IsPositiveDefinite (F i)) (hlim : ∀ (x : M), Filter.Tendsto (fun (i : ι) => F i x) l (nhds (G x))) : IsPositiveDefinite G

Positive-definiteness is preserved under pointwise limits along a nontrivial filter. The hypothesis on positive-definiteness is eventual, so this applies equally to nets that are eventually positive definite.

theorem TauCeti.IsPositiveDefinite.of_forall_tendsto {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → M → ℂ} {G : M → ℂ} (hF : ∀ (i : ι), IsPositiveDefinite (F i)) (hlim : ∀ (x : M), Filter.Tendsto (fun (i : ι) => F i x) l (nhds (G x))) : IsPositiveDefinite G

A pointwise limit of a family of positive-definite functions is positive definite. This is the non-eventual form of TauCeti.IsPositiveDefinite.of_tendsto.

theorem TauCeti.IsPositiveDefinite.of_seq_tendsto {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : ℕ → M → ℂ} {G : M → ℂ} (hF : ∀ᶠ (n : ℕ) in Filter.atTop, IsPositiveDefinite (F n)) (hlim : ∀ (x : M), Filter.Tendsto (fun (n : ℕ) => F n x) Filter.atTop (nhds (G x))) : IsPositiveDefinite G

Sequential pointwise limits of eventually positive-definite functions are positive definite.

theorem TauCeti.IsPositiveDefinite.of_tendstoLocallyUniformly {M : Type u_1} [AddMonoid M] [StarAddMonoid M] [TopologicalSpace M] {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → M → ℂ} {G : M → ℂ} (hF : ∀ᶠ (i : ι) in l, IsPositiveDefinite (F i)) (hlim : TendstoLocallyUniformly F G l) : IsPositiveDefinite G

A locally uniform limit of eventually positive-definite functions is positive definite.

Unlike continuity, positive-definiteness itself only needs pointwise convergence; local uniform convergence is converted to pointwise convergence before applying TauCeti.IsPositiveDefinite.of_tendsto.