Product constructions for semigroup-group positive-definite functions

This file builds Berg--Christensen--Ressel positive-definite functions on ℝ≥0 × V from separate time and spatial factors. If f : ℝ≥0 → ℂ supplies the positive-definite time kernel (t, u) ↦ f (t + u), and g : V → ℂ supplies the positive-definite spatial subtraction kernel (v, w) ↦ g (v - w), then (t, v) ↦ f t * g v is semigroup-group positive definite. We also provide the convenience form where the spatial kernel comes from a positive-definite function for the negation involution on V.

This is a small prerequisite for the BCR semigroup--Bochner representation milestone in TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 ("BCR semigroup--Bochner"). The eventual Laplace--Fourier examples have exactly this separated shape before integration: a time kernel multiplied by a spatial Fourier kernel.

No Mathlib infrastructure is vendored. The proof reuses Tau Ceti's positive-definite function/kernel correspondence together with Mathlib's Matrix.PosSemidef.submatrix and Matrix.PosSemidef.hadamard operations.

Main declarations

• TauCeti.isSemigroupGroupPD_mul_time_spatial: the product of a time positive-definite function and a spatial positive-definite function is BCR positive definite.
• TauCeti.isSemigroupGroupPD_mul_time_spatial_of_kernels: the same construction when the time factor and spatial subtraction factor are supplied as positive-definite kernels.
• TauCeti.continuous_mul_time_spatial: continuity of separated products.
• TauCeti.isSemigroupGroupPD_mul_time_spatial_and_continuous: the packaged positive-definite and continuous form used by BCR-facing examples.

References

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

theorem TauCeti.isSemigroupGroupPD_mul_time_spatial_of_kernels {V : Type u_1} [AddCommGroup V] {f : NNReal → ℂ} {g : V → ℂ} (hf : Matrix.PosSemidef fun (t u : NNReal) => f (t + u)) (hg : Matrix.PosSemidef fun (v w : V) => g (v - w)) : IsSemigroupGroupPD fun (p : NNReal × V) => f p.1 * g p.2

If the time factor gives a positive-definite kernel (t, u) ↦ f (t + u), and the spatial factor gives a positive-definite subtraction kernel (v, w) ↦ g (v - w), then their separated product is semigroup-group positive definite.

theorem TauCeti.isSemigroupGroupPD_mul_time_spatial {V : Type u_1} [AddCommGroup V] [StarAddMonoid V] {f : NNReal → ℂ} {g : V → ℂ} (hf : IsPositiveDefinite f) (hg : IsPositiveDefinite g) (hstar : ∀ (v : V), star v = -v) : IsSemigroupGroupPD fun (p : NNReal × V) => f p.1 * g p.2

A separated product of a time positive-definite function and a spatial positive-definite function is semigroup-group positive definite. The time factor uses Mathlib's trivial involution on ℝ≥0; the spatial factor uses the supplied negation-involution hypothesis.

theorem TauCeti.continuous_mul_time_spatial {V : Type u_1} [TopologicalSpace V] {f : NNReal → ℂ} {g : V → ℂ} (hf : Continuous f) (hg : Continuous g) : Continuous fun (p : NNReal × V) => f p.1 * g p.2

Separated products are continuous when both factors are continuous.

theorem TauCeti.isSemigroupGroupPD_mul_time_spatial_and_continuous {V : Type u_1} [AddCommGroup V] [TopologicalSpace V] {f : NNReal → ℂ} {g : V → ℂ} [StarAddMonoid V] (hfpd : IsPositiveDefinite f) (hgpd : IsPositiveDefinite g) (hstar : ∀ (v : V), star v = -v) (hfcont : Continuous f) (hgcont : Continuous g) : (IsSemigroupGroupPD fun (p : NNReal × V) => f p.1 * g p.2) ∧ Continuous fun (p : NNReal × V) => f p.1 * g p.2

Package the separated-product construction with continuity of the resulting BCR function.

theorem TauCeti.isSemigroupGroupPD_mul_time_spatial_of_kernels_and_continuous {V : Type u_1} [AddCommGroup V] [TopologicalSpace V] {f : NNReal → ℂ} {g : V → ℂ} (hf : Matrix.PosSemidef fun (t u : NNReal) => f (t + u)) (hg : Matrix.PosSemidef fun (v w : V) => g (v - w)) (hfcont : Continuous f) (hgcont : Continuous g) : (IsSemigroupGroupPD fun (p : NNReal × V) => f p.1 * g p.2) ∧ Continuous fun (p : NNReal × V) => f p.1 * g p.2

Kernel-supplied version of the separated-product construction, packaged with continuity.