Positive-definite functions on an additive commutative group

On an additive commutative group G the classical positive-definiteness condition for F : G → ℂ reads ∑_{i,j} cᵢ · conj(cⱼ) · F(aᵢ - aⱼ) ≥ 0: the involution is negation, so the kernel is the translation-invariant K(a, b) = F(a - b). Mathlib's star on a real vector space is the identity, not negation, so the generic involutive predicate TauCeti.IsPositiveDefinite does not express this condition for the canonical instances on ℝ or on a Euclidean space. This file supplies the subtraction-form predicate TauCeti.IsPositiveDefiniteSub that does, and connects it to the generic theory.

The connection runs through the type synonym TauCeti.WithNegStar G, a copy of G carrying the negation involution star a = -a as a genuine StarAddMonoid instance. Installing that involution on G itself would clash with Mathlib's star conventions, so it is installed on the synonym instead, and TauCeti.isPositiveDefiniteSub_iff_isPositiveDefinite transports statements across. The synonym is public: a generic lemma with no transfer lemma here can still be applied to fun a : WithNegStar G => F (WithNegStar.ofNegStar a).

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Objects, which asks for IsPositiveDefinite to be defined generically and then instantiated on a finite-dimensional real inner-product space with the involution a⋆ = -a, and the API to develop items (closure properties, the value bounds at the origin, continuity at 0 implying uniform continuity, the PD-function ↔ PD-kernel equivalence F(a - b), and normalization) at that instantiation. It is the predicate in which Bochner's theorem is stated, in TauCeti/Analysis/Bochner/BochnerTheorem.lean.

Main declarations

• TauCeti.WithNegStar: the type synonym carrying the negation involution.
• TauCeti.IsPositiveDefiniteSub: the subtraction-form positive-definiteness predicate.
• TauCeti.isPositiveDefiniteSub_iff_forall_sum_nonneg: the defining finite-family condition.
• TauCeti.isPositiveDefiniteSub_iff_isPositiveDefinite: the transfer to the generic predicate.
• TauCeti.isPositiveDefiniteSub_iff_posSemidef: the PD-function ↔ PD-kernel equivalence.
• TauCeti.isPositiveDefinite_iff_isPositiveDefiniteSub: agreement with the generic predicate on a group whose own involution is negation.
• TauCeti.IsPositiveDefiniteSub.map_zero_nonneg, map_zero_re_nonneg, map_zero_eq_ofReal_re, map_neg, conj_symm, normSq_le, norm_apply_le_map_zero_re: values at and around the origin.
• TauCeti.IsPositiveDefiniteSub.add, const_mul, real_smul, mul, sum, prod, TauCeti.isPositiveDefiniteSub_const: closure properties.
• TauCeti.IsPositiveDefiniteSub.comp_addMonoidHom, comp_smul, comp_neg: pullbacks.
• TauCeti.IsPositiveDefiniteSub.of_tendsto: pointwise limits.
• TauCeti.IsPositiveDefiniteSub.normalize: normalization to value 1 at the origin.
• TauCeti.IsPositiveDefiniteSub.uniformContinuous_of_continuousAt_zero: continuity at 0 implies uniform continuity.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Chapter 3.
• W. Rudin, Fourier Analysis on Groups (1962), §1.4.

The negation involution

def TauCeti.WithNegStar (G : Type u_1) : Type u_1

WithNegStar G is a type synonym for an additive commutative group G, carrying the negation involution star a = -a.

Mathlib pins no negation StarAddMonoid instance on an additive group — on a real vector space star is the identity — so the involution used by classical positive definiteness is installed on this synonym rather than on G itself.

Equations

• TauCeti.WithNegStar G = G

@[instance_reducible]

instance TauCeti.WithNegStar.instAddCommGroup {G : Type u_1} [AddCommGroup G] : AddCommGroup (WithNegStar G)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.WithNegStar.instStar {G : Type u_1} [AddCommGroup G] : Star (WithNegStar G)

Equations

• TauCeti.WithNegStar.instStar = { star := fun (a : TauCeti.WithNegStar G) => -a }

@[simp]

theorem TauCeti.WithNegStar.star_eq_neg {G : Type u_1} [AddCommGroup G] (a : WithNegStar G) : star a = -a

@[instance_reducible]

instance TauCeti.WithNegStar.instStarAddMonoid {G : Type u_1} [AddCommGroup G] : StarAddMonoid (WithNegStar G)

Equations

• TauCeti.WithNegStar.instStarAddMonoid = { toStar := TauCeti.WithNegStar.instStar, star_involutive := ⋯, star_add := ⋯ }

def TauCeti.WithNegStar.toNegStar {G : Type u_1} [AddCommGroup G] : G ≃+ WithNegStar G

The identity additive equivalence from G to its negation-involution copy.

Equations

• TauCeti.WithNegStar.toNegStar = AddEquiv.refl G

def TauCeti.WithNegStar.ofNegStar {G : Type u_1} [AddCommGroup G] : WithNegStar G ≃+ G

The identity additive equivalence from the negation-involution copy of G back to G.

Equations

• TauCeti.WithNegStar.ofNegStar = TauCeti.WithNegStar.toNegStar.symm

@[simp]

theorem TauCeti.WithNegStar.ofNegStar_toNegStar {G : Type u_1} [AddCommGroup G] (a : G) : ofNegStar (toNegStar a) = a

@[simp]

theorem TauCeti.WithNegStar.toNegStar_ofNegStar {G : Type u_1} [AddCommGroup G] (a : WithNegStar G) : toNegStar (ofNegStar a) = a

@[instance_reducible]

instance TauCeti.WithNegStar.instSeminormedAddCommGroup {G : Type u_1} [SeminormedAddCommGroup G] : SeminormedAddCommGroup (WithNegStar G)

Equations

• One or more equations did not get rendered due to their size.

The subtraction-form predicate

def TauCeti.IsPositiveDefiniteSub {G : Type u_1} [AddCommGroup G] (F : G → ℂ) : Prop

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

This is the classical translation-invariant condition, the one Bochner's theorem is stated in. It is TauCeti.IsPositiveDefinite for the negation involution; see TauCeti.isPositiveDefiniteSub_iff_isPositiveDefinite.

Equations

• TauCeti.IsPositiveDefiniteSub F = ∀ (n : ℕ) (c : Fin n → ℂ) (v : Fin n → G), 0 ≤ ∑ i : Fin n, ∑ j : Fin n, c i * (starRingEnd ℂ) (c j) * F (v i - v j)

theorem TauCeti.isPositiveDefiniteSub_iff_forall_sum_nonneg {G : Type u_1} [AddCommGroup G] {F : G → ℂ} : IsPositiveDefiniteSub F ↔ ∀ (n : ℕ) (c : Fin n → ℂ) (v : Fin n → G), 0 ≤ ∑ i : Fin n, ∑ j : Fin n, c i * (starRingEnd ℂ) (c j) * F (v i - v j)

The defining finite-family characterization, for building a positive-definite function directly from the quadratic-form condition.

theorem TauCeti.isPositiveDefiniteSub_iff_isPositiveDefinite {G : Type u_1} [AddCommGroup G] {F : G → ℂ} : IsPositiveDefiniteSub F ↔ IsPositiveDefinite fun (a : WithNegStar G) => F (WithNegStar.ofNegStar a)

Subtraction-form positive definiteness is the generic involutive predicate for the negation involution, read on the type synonym TauCeti.WithNegStar.

theorem TauCeti.IsPositiveDefiniteSub.isPositiveDefinite {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : IsPositiveDefinite fun (a : WithNegStar G) => F (WithNegStar.ofNegStar a)

The generic involutive predicate attached to a subtraction-form positive-definite function. This is the workhorse for transporting the generic API.

theorem TauCeti.IsPositiveDefiniteSub.sum_nonneg {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) {ι : Type u_2} [Fintype ι] (c : ι → ℂ) (v : ι → G) : 0 ≤ ∑ i : ι, ∑ j : ι, c i * (starRingEnd ℂ) (c j) * F (v i - v j)

Positive-definiteness holds for an arbitrary finite index type, not just Fin n.

theorem TauCeti.IsPositiveDefiniteSub.posSemidef {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : Matrix.PosSemidef fun (a b : G) => F (a - b)

A subtraction-form positive-definite function gives the translation-invariant positive-definite kernel K(a, b) = F (a - b).

theorem TauCeti.IsPositiveDefiniteSub.of_posSemidef {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hK : Matrix.PosSemidef fun (a b : G) => F (a - b)) : IsPositiveDefiniteSub F

A function whose translation-invariant kernel K(a, b) = F (a - b) is positive definite is positive definite.

theorem TauCeti.isPositiveDefiniteSub_iff_posSemidef {G : Type u_1} [AddCommGroup G] {F : G → ℂ} : IsPositiveDefiniteSub F ↔ Matrix.PosSemidef fun (a b : G) => F (a - b)

The PD-function ↔ PD-kernel equivalence in its classical translation-invariant form: F is positive definite if and only if the kernel K(a, b) = F (a - b) is positive definite.

theorem TauCeti.isPositiveDefinite_iff_isPositiveDefiniteSub {G : Type u_1} [AddCommGroup G] {F : G → ℂ} [StarAddMonoid G] (hstar : ∀ (a : G), star a = -a) : IsPositiveDefinite F ↔ IsPositiveDefiniteSub F

On a group whose own involution is negation, the generic involutive predicate and the subtraction-form predicate agree.

Values at and around the origin

theorem TauCeti.IsPositiveDefiniteSub.map_zero_nonneg {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : 0 ≤ F 0

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

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.map_zero_im {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : (F 0).im = 0

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

theorem TauCeti.IsPositiveDefiniteSub.map_zero_re_nonneg {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : 0 ≤ (F 0).re

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

theorem TauCeti.IsPositiveDefiniteSub.map_zero_eq_ofReal_re {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : F 0 = ↑(F 0).re

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

theorem TauCeti.IsPositiveDefiniteSub.map_zero_re_pos_of_ne_zero {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub 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.IsPositiveDefiniteSub.conj_symm {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a b : G) : (starRingEnd ℂ) (F (b - a)) = F (a - b)

A positive-definite function is conjugate symmetric: conj (F (b - a)) = F (a - b).

theorem TauCeti.IsPositiveDefiniteSub.map_neg {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a : G) : F (-a) = (starRingEnd ℂ) (F a)

A positive-definite function satisfies F (-a) = conj (F a).

theorem TauCeti.IsPositiveDefiniteSub.normSq_le {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a b : G) : Complex.normSq (F (a - b)) ≤ (F 0).re * (F 0).re

The Cauchy–Schwarz inequality for a positive-definite function: the squared norm of any value is bounded by the square of the value at the origin.

theorem TauCeti.IsPositiveDefiniteSub.norm_apply_le_map_zero_re {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a : G) : ‖F a‖ ≤ (F 0).re

A positive-definite function is bounded by its value at the origin.

theorem TauCeti.IsPositiveDefiniteSub.apply_eq_zero_of_map_zero_re_eq_zero {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (h0 : (F 0).re = 0) (a : G) : F a = 0

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

Closure properties

theorem TauCeti.IsPositiveDefiniteSub.add {G : Type u_1} [AddCommGroup G] {F H : G → ℂ} (hF : IsPositiveDefiniteSub F) (hH : IsPositiveDefiniteSub H) : IsPositiveDefiniteSub fun (x : G) => F x + H x

Positive-definite functions are closed under addition.

theorem TauCeti.IsPositiveDefiniteSub.const_mul {G : Type u_1} [AddCommGroup G] {F : G → ℂ} {k : ℂ} (hk : 0 ≤ k) (hF : IsPositiveDefiniteSub F) : IsPositiveDefiniteSub fun (x : G) => k * F x

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

theorem TauCeti.IsPositiveDefiniteSub.real_smul {G : Type u_1} [AddCommGroup G] {F : G → ℂ} {r : ℝ} (hr : 0 ≤ r) (hF : IsPositiveDefiniteSub F) : IsPositiveDefiniteSub fun (x : G) => r • F x

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

theorem TauCeti.IsPositiveDefiniteSub.mul {G : Type u_1} [AddCommGroup G] {F H : G → ℂ} (hF : IsPositiveDefiniteSub F) (hH : IsPositiveDefiniteSub H) : IsPositiveDefiniteSub fun (x : G) => F x * H x

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

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

Positive-definite functions are closed under finite sums.

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

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

Pullbacks

theorem TauCeti.IsPositiveDefiniteSub.comp_addMonoidHom {G : Type u_1} [AddCommGroup G] {F : G → ℂ} {N : Type u_2} [AddCommGroup N] (hF : IsPositiveDefiniteSub F) (φ : N →+ G) : IsPositiveDefiniteSub fun (x : N) => F (φ x)

Positive definiteness is preserved by precomposition with an additive homomorphism; no compatibility with an involution is needed, since an additive homomorphism automatically commutes with negation.

theorem TauCeti.IsPositiveDefiniteSub.comp_smul {G : Type u_1} [AddCommGroup G] {F : G → ℂ} {R : Type u_2} [DistribSMul R G] (hF : IsPositiveDefiniteSub F) (r : R) : IsPositiveDefiniteSub fun (x : G) => F (r • x)

Positive definiteness is preserved by rescaling the argument.

theorem TauCeti.IsPositiveDefiniteSub.comp_neg {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : IsPositiveDefiniteSub fun (x : G) => F (-x)

Positive definiteness is preserved by negating the argument.

Limits

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

Positive definiteness is preserved under pointwise limits along a nontrivial filter.

Normalization

theorem TauCeti.IsPositiveDefiniteSub.normalize {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : IsPositiveDefiniteSub fun (x : G) => (↑(F 0).re)⁻¹ * F x

Multiplying a positive-definite function by the reciprocal of its real value at the origin preserves positive definiteness.

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.normalize_apply_zero {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (h0 : F 0 ≠ 0) : (↑(F 0).re)⁻¹ * F 0 = 1

The normalized function has value 1 at the origin.

theorem TauCeti.IsPositiveDefiniteSub.norm_normalize_apply_le_one {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a : G) : ‖(↑(F 0).re)⁻¹ * F a‖ ≤ 1

A normalized positive-definite function is bounded by 1.

Continuity

theorem TauCeti.IsPositiveDefiniteSub.uniformContinuous_of_continuousAt_zero {G : Type u_2} [SeminormedAddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (hcont : ContinuousAt F 0) : UniformContinuous F

A positive-definite function on a seminormed additive commutative group is uniformly continuous as soon as it is continuous at the origin.

theorem TauCeti.IsPositiveDefiniteSub.continuous_of_continuousAt_zero {G : Type u_2} [SeminormedAddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (hcont : ContinuousAt F 0) : Continuous F

A positive-definite function on a seminormed additive commutative group is continuous as soon as it is continuous at the origin.

theorem TauCeti.isPositiveDefiniteSub_const {G : Type u_1} [AddCommGroup G] {k : ℂ} (hk : 0 ≤ k) : IsPositiveDefiniteSub fun (x : G) => k

A nonnegative real constant is a positive-definite function.

theorem TauCeti.isPositiveDefiniteSub_zero {G : Type u_1} [AddCommGroup G] : IsPositiveDefiniteSub fun (x : G) => 0

The zero function is positive definite.