Positive-definite functions on an involutive additive monoid

A complex-valued function F on an additive monoid M equipped with an involution star (an AddMonoid with a StarAddMonoid structure) is positive definite when, for every finite family (cᵢ, aᵢ) of scalars cᵢ : ℂ and points aᵢ : M, the Hermitian form ∑_{i,j} cᵢ · conj(cⱼ) · F(aᵢ + aⱼ⋆) is a nonnegative real number. The involution aⱼ⋆ inside the argument is what makes this the right notion on an involutive semigroup (Berg–Christensen– Ressel): on a finite-dimensional real inner-product space with a⋆ = -a it specialises to the classical translation-invariant positive-definiteness ∑ cᵢ conj(cⱼ) F(aᵢ - aⱼ) ≥ 0, and on the product monoid ℝ≥0 × V it produces the BCR involution (t, a)⋆ = (t, -a).

This file introduces the predicate TauCeti.IsPositiveDefinite at this general level and develops its basic algebraic API: the value at 0 is real and nonnegative, the function is conjugate symmetric in the involution, it satisfies the Cauchy–Schwarz inequality coming from the 2 × 2 sub-form, and the class is closed under sums and nonnegative complex scalar multiples, with the Schur pointwise product closure and nonnegative constants as examples.

This is the Objects and first API to develop slice of Part C of the OneParameterSemigroups roadmap in TauCetiRoadmap: "positive-definite functions and Bochner's theorem". Mathlib has related APIs for positive-semidefinite matrices, bilinear and linear maps, and RKHS kernels, but not for positive-definite functions on an involutive monoid, so the predicate and its API are built here. The continuity theory and Bochner's representation theorem are later milestones.

Main declarations

• TauCeti.IsPositiveDefinite: the positive-definiteness predicate for F : M → ℂ.
• TauCeti.IsPositiveDefinite.sum_nonneg: nonnegativity for arbitrary finite families.
• TauCeti.IsPositiveDefinite.quadForm_two_nonneg: nonnegativity of the 2 × 2 sub-form.
• TauCeti.IsPositiveDefinite.map_zero_nonneg: 0 ≤ F 0.
• TauCeti.IsPositiveDefinite.map_zero_im: (F 0).im = 0.
• TauCeti.IsPositiveDefinite.map_zero_re_nonneg: 0 ≤ (F 0).re.
• TauCeti.IsPositiveDefinite.map_zero_eq_ofReal_re: F 0 = ((F 0).re : ℂ).
• TauCeti.IsPositiveDefinite.map_zero_re_pos_of_ne_zero: if F 0 ≠ 0, then 0 < (F 0).re.
• TauCeti.IsPositiveDefinite.conj_symm: conj (F (b + a⋆)) = F (a + b⋆).
• TauCeti.IsPositiveDefinite.normSq_le: the Cauchy–Schwarz inequality ‖F (a + b⋆)‖² ≤ (F (a + a⋆)).re * (F (b + b⋆)).re.
• TauCeti.IsPositiveDefinite.norm_apply_le_map_zero_re_of_add_star_eq_zero: ‖F a‖ ≤ (F 0).re when a + star a = 0, with the additive-group corollary TauCeti.IsPositiveDefinite.norm_apply_le_map_zero_re_of_star_eq_neg for star a = -a.
• TauCeti.IsPositiveDefinite.apply_eq_zero_of_map_zero_re_eq_zero: (F 0).re = 0 forces F to vanish identically.
• TauCeti.IsPositiveDefinite.posSemidef: a positive-definite function gives the positive-definite kernel fun a b => F (a + star b).
• TauCeti.IsPositiveDefinite.of_posSemidef: conversely, if the kernel fun a b => F (a + star b) is positive definite then F is positive definite.
• TauCeti.IsPositiveDefinite.add, TauCeti.IsPositiveDefinite.sum, TauCeti.IsPositiveDefinite.const_mul, TauCeti.IsPositiveDefinite.mul, TauCeti.IsPositiveDefinite.prod, TauCeti.isPositiveDefinite_const: closure properties and examples.

References

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

def TauCeti.IsPositiveDefinite {M : Type u_1} [AddMonoid M] [StarAddMonoid M] (F : M → ℂ) : Prop

A function F : M → ℂ on an involutive additive monoid is positive definite when, for every finite family of scalars c : Fin n → ℂ and points v : Fin n → M, the Hermitian form ∑_{i,j} c i · conj (c j) · F (v i + star (v j)) is a nonnegative real number (using the order on ℂ for which 0 ≤ z means z is real and nonnegative).

Equations

• TauCeti.IsPositiveDefinite F = ∀ (n : ℕ) (c : Fin n → ℂ) (v : Fin n → M), 0 ≤ ∑ i : Fin n, ∑ j : Fin n, c i * (starRingEnd ℂ) (c j) * F (v i + star (v j))

theorem TauCeti.IsPositiveDefinite.sum_nonneg {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) {ι : Type u_2} [Fintype ι] (c : ι → ℂ) (v : ι → M) : 0 ≤ ∑ i : ι, ∑ j : ι, c i * (starRingEnd ℂ) (c j) * F (v i + star (v j))

Positive-definiteness holds for an arbitrary finite index type, not just Fin n: for every finite family of scalars c : ι → ℂ and points v : ι → M, the Hermitian form ∑_{i,j} c i · conj (c j) · F (v i + star (v j)) is a nonnegative real number.

theorem TauCeti.IsPositiveDefinite.quadForm_two_nonneg {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a b : M) (c₀ c₁ : ℂ) : 0 ≤ c₀ * (starRingEnd ℂ) c₀ * F (a + star a) + c₀ * (starRingEnd ℂ) c₁ * F (a + star b) + c₁ * (starRingEnd ℂ) c₀ * F (b + star a) + c₁ * (starRingEnd ℂ) c₁ * F (b + star b)

The 2 × 2 Hermitian sub-form of a positive-definite function at the points a, b with coefficients c₀, c₁ is nonnegative.

theorem TauCeti.IsPositiveDefinite.add_star_self_nonneg {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a : M) : 0 ≤ F (a + star a)

A positive-definite function takes a real, nonnegative value at every "norm point" a + star a.

theorem TauCeti.IsPositiveDefinite.add_star_self_im {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a : M) : (F (a + star a)).im = 0

The value of a positive-definite function at a "norm point" a + star a has zero imaginary part.

theorem TauCeti.IsPositiveDefinite.add_star_self_re_nonneg {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a : M) : 0 ≤ (F (a + star a)).re

The value of a positive-definite function at a "norm point" a + star a has nonnegative real part.

theorem TauCeti.IsPositiveDefinite.map_zero_nonneg {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) : 0 ≤ F 0

The value of a positive-definite function at 0 is real and nonnegative.

@[simp]

theorem TauCeti.IsPositiveDefinite.map_zero_im {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) : (F 0).im = 0

The value of a positive-definite function at 0 has zero imaginary part.

theorem TauCeti.IsPositiveDefinite.map_zero_re_nonneg {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) : 0 ≤ (F 0).re

The real part of the value of a positive-definite function at 0 is nonnegative.

theorem TauCeti.IsPositiveDefinite.map_zero_eq_ofReal_re {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) : F 0 = ↑(F 0).re

The value at the origin of a positive-definite function is equal to the real number (F 0).re, viewed as a complex number.

theorem TauCeti.IsPositiveDefinite.map_zero_re_pos_of_ne_zero {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (h0 : F 0 ≠ 0) : 0 < (F 0).re

If a positive-definite function is nonzero at the origin, then the real part of that value is strictly positive.

@[simp]

theorem TauCeti.IsPositiveDefinite.conj_symm {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a b : M) : (starRingEnd ℂ) (F (b + star a)) = F (a + star b)

A positive-definite function is conjugate symmetric in the involution: conj (F (b + star a)) = F (a + star b).

theorem TauCeti.IsPositiveDefinite.posSemidef {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) : Matrix.PosSemidef fun (a b : M) => F (a + star b)

A positive-definite function F induces the positive-definite kernel K(a, b) = F(a + b⋆). This is the forward half of the function ↔ kernel correspondence.

theorem TauCeti.IsPositiveDefinite.of_posSemidef {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hK : Matrix.PosSemidef fun (a b : M) => F (a + star b)) : IsPositiveDefinite F

If the kernel K(a, b) = F(a + b⋆) is positive definite, then so is the function F. This is the reverse half of the function ↔ kernel correspondence.

theorem TauCeti.IsPositiveDefinite.normSq_le {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a b : M) : Complex.normSq (F (a + star b)) ≤ (F (a + star a)).re * (F (b + star b)).re

The Cauchy–Schwarz inequality for a positive-definite function: the squared norm of an off-diagonal value is bounded by the product of the two diagonal values.

theorem TauCeti.IsPositiveDefinite.norm_apply_le_map_zero_re_of_add_star_eq_zero {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a : M) (ha : a + star a = 0) : ‖F a‖ ≤ (F 0).re

If a + star a = 0, then a positive-definite function is bounded at a by its value at zero.

theorem TauCeti.IsPositiveDefinite.apply_eq_zero_of_map_zero_re_eq_zero {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (h0 : (F 0).re = 0) (a : M) : F a = 0

A positive-definite function with (F 0).re = 0 vanishes identically.

No hypothesis on the point is required, and none on the ambient structure beyond an involutive additive monoid (AddMonoid and StarAddMonoid).

theorem TauCeti.IsPositiveDefinite.norm_apply_le_map_zero_re_of_star_eq_neg {N : Type u_2} [AddGroup N] [StarAddMonoid N] {H : N → ℂ} (hH : IsPositiveDefinite H) (a : N) (hstar_a : star a = -a) : ‖H a‖ ≤ (H 0).re

If the involution negates the point a, then a positive-definite function is bounded at a by its value at zero. In particular this applies on an additive group whose involution is negation.

theorem TauCeti.IsPositiveDefinite.add {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F G : M → ℂ} (hF : IsPositiveDefinite F) (hG : IsPositiveDefinite G) : IsPositiveDefinite fun (x : M) => F x + G x

Positive-definite functions are closed under addition.

theorem TauCeti.IsPositiveDefinite.const_mul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} {k : ℂ} (hk : 0 ≤ k) (hF : IsPositiveDefinite F) : IsPositiveDefinite fun (x : M) => k * F x

Positive-definite functions are closed under multiplication by a nonnegative complex scalar.

theorem TauCeti.IsPositiveDefinite.mul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F G : M → ℂ} (hF : IsPositiveDefinite F) (hG : IsPositiveDefinite G) : IsPositiveDefinite fun (x : M) => F x * G x

Positive-definite functions are closed under pointwise multiplication (Schur product).

theorem TauCeti.isPositiveDefinite_const {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {k : ℂ} (hk : 0 ≤ k) : IsPositiveDefinite fun (x : M) => k

A nonnegative real constant is a positive-definite function.

theorem TauCeti.isPositiveDefinite_zero {M : Type u_1} [AddMonoid M] [StarAddMonoid M] : IsPositiveDefinite fun (x : M) => 0

The zero function is positive definite.

theorem TauCeti.IsPositiveDefinite.sum {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {s : Finset ι} {F : ι → M → ℂ} (hF : ∀ i ∈ s, IsPositiveDefinite (F i)) : IsPositiveDefinite fun (x : M) => ∑ i ∈ s, F i x

Positive-definite functions are closed under finite sums.

theorem TauCeti.IsPositiveDefinite.prod {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {s : Finset ι} {F : ι → M → ℂ} (hF : ∀ i ∈ s, IsPositiveDefinite (F i)) : IsPositiveDefinite fun (x : M) => ∏ i ∈ s, F i x

Positive-definite functions are closed under finite products (Schur product).