Pullbacks of positive-definite functions

This file adds the pullback API for TauCeti.IsPositiveDefinite, the positive-definite function predicate on an involutive additive monoid. A star-preserving additive homomorphism φ : N → M pulls a positive-definite function F : M → ℂ back to the positive-definite function F ∘ φ : N → ℂ; if φ is surjective, positive-definiteness can also be descended from the pullback.

This is part of the OneParameterSemigroups roadmap, Part C, whose positive-definite-function API asks for pullbacks alongside the PD-function/PD-kernel correspondence and the closure properties. The proofs are the finite-family reindexing argument: apply the defining nonnegativity of F to the image family under φ, using preservation of addition and star to identify the Gram entries.

Main declarations

• TauCeti.IsPositiveDefinite.comp: positive-definiteness is preserved by precomposition with any star-preserving additive homomorphism, stated using Mathlib's homomorphism classes.
• TauCeti.IsPositiveDefinite.comp_addMonoidHom: the same statement for an explicit AddMonoidHom plus a star-preservation hypothesis.
• TauCeti.IsPositiveDefinite.comp_smul: rescaling the argument by a scalar preserves positive-definiteness when the involution is negation.
• TauCeti.IsPositiveDefinite.of_comp_surjective and TauCeti.IsPositiveDefinite.comp_iff_of_surjective: descent and equivalence for surjective star-preserving additive homomorphisms.
• TauCeti.IsPositiveDefinite.comp_addEquiv_iff: invariance under a star-preserving additive equivalence.
• TauCeti.IsPositiveDefinite.comp_fst, TauCeti.IsPositiveDefinite.comp_snd, and TauCeti.IsPositiveDefinite.mul_comp_fst_snd: the projection pullbacks and their pointwise product on a product monoid.

References

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

theorem TauCeti.IsPositiveDefinite.comp {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} {Φ : Type u_3} [FunLike Φ N M] [AddHomClass Φ N M] [StarHomClass Φ N M] (hF : IsPositiveDefinite F) (φ : Φ) : IsPositiveDefinite fun (x : N) => F (φ x)

Positive-definiteness is preserved by pullback along a star-preserving additive homomorphism. This is stated for Mathlib's homomorphism classes so it applies to bundled additive homomorphisms, star algebra homomorphisms, and similar maps.

theorem TauCeti.IsPositiveDefinite.comp_addMonoidHom {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} (hF : IsPositiveDefinite F) (φ : N →+ M) (hstar : ∀ (x : N), φ (star x) = star (φ x)) : IsPositiveDefinite fun (x : N) => F (φ x)

The explicit AddMonoidHom form of pullback: a star-preserving additive homomorphism pulls back positive-definite functions to positive-definite functions.

theorem TauCeti.IsPositiveDefinite.comp_smul {G : Type u_3} [AddGroup G] [StarAddMonoid G] {R : Type u_4} [DistribSMul R G] {F : G → ℂ} (hF : IsPositiveDefinite F) (hstar : ∀ (x : G), star x = -x) (r : R) : IsPositiveDefinite fun (x : G) => F (r • x)

Rescaling the argument by a scalar preserves positive-definiteness, whenever the involution on the domain is negation: if F is positive definite then so is x ↦ F (r • x).

theorem TauCeti.IsPositiveDefinite.of_comp_surjective {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} {Φ : Type u_3} [FunLike Φ N M] [AddHomClass Φ N M] (φ : Φ) (hstar : ∀ (x : N), φ (star x) = star (φ x)) (hsurj : Function.Surjective ⇑φ) (hcomp : IsPositiveDefinite fun (x : N) => F (φ x)) : IsPositiveDefinite F

Positive-definiteness descends along a surjective star-preserving additive homomorphism: if F ∘ φ is positive definite and every point of the codomain is in the range of φ, then F is positive definite.

theorem TauCeti.IsPositiveDefinite.comp_iff_of_surjective {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} {Φ : Type u_3} [FunLike Φ N M] [AddHomClass Φ N M] [StarHomClass Φ N M] (φ : Φ) (hsurj : Function.Surjective ⇑φ) : (IsPositiveDefinite fun (x : N) => F (φ x)) ↔ IsPositiveDefinite F

Along a surjective star-preserving additive homomorphism, a function is positive definite if and only if its pullback is positive definite.

theorem TauCeti.IsPositiveDefinite.comp_addMonoidHom_iff_of_surjective {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} (φ : N →+ M) (hstar : ∀ (x : N), φ (star x) = star (φ x)) (hsurj : Function.Surjective ⇑φ) : (IsPositiveDefinite fun (x : N) => F (φ x)) ↔ IsPositiveDefinite F

The explicit AddMonoidHom form of the pullback equivalence for surjective maps.

theorem TauCeti.IsPositiveDefinite.comp_addEquiv_iff {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} (e : N ≃+ M) (hstar : ∀ (x : N), e (star x) = star (e x)) : (IsPositiveDefinite fun (x : N) => F (e x)) ↔ IsPositiveDefinite F

Positive-definiteness is invariant under precomposition with a star-preserving additive equivalence.

theorem TauCeti.IsPositiveDefinite.comp_fst {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} (hF : IsPositiveDefinite F) : IsPositiveDefinite fun (x : M × N) => F x.1

Pulling back a positive-definite function along the first projection from a product preserves positive-definiteness.

theorem TauCeti.IsPositiveDefinite.comp_snd {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {G : N → ℂ} (hG : IsPositiveDefinite G) : IsPositiveDefinite fun (x : M × N) => G x.2

Pulling back a positive-definite function along the second projection from a product preserves positive-definiteness.

theorem TauCeti.IsPositiveDefinite.mul_comp_fst_snd {M : Type u_1} {N : Type u_2} [AddMonoid M] [StarAddMonoid M] [AddMonoid N] [StarAddMonoid N] {F : M → ℂ} {G : N → ℂ} (hF : IsPositiveDefinite F) (hG : IsPositiveDefinite G) : IsPositiveDefinite fun (x : M × N) => F x.1 * G x.2

The product of two positive-definite functions, pulled back from the two factors of a product monoid, is positive definite. This is the basic product-domain construction obtained by combining pullback along projections with the Schur product closure.