Spatial pullbacks of semigroup-group positive-definite functions

This file records the spatial-coordinate pullback API for Berg--Christensen--Ressel positive-definite functions on ℝ≥0 × V. If F is semigroup-group positive definite and φ : W →+ V is an additive homomorphism, then (t, w) ↦ F (t, φ w) is again semigroup-group positive definite.

This is a small prerequisite for the BCR semigroup--Bochner representation milestone in the OneParameterSemigroups roadmap. The Bochner part is stated on an arbitrary finite-dimensional real inner-product space, so downstream arguments need to transport the spatial variable along additive equivalences and continuous linear maps without unfolding the private BCR wrapper.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, the positive-definite function API item "pullbacks" and Milestone 2 ("BCR semigroup--Bochner").

Main declarations

• TauCeti.IsSemigroupGroupPD.comp_spatial: spatial pullback along an additive homomorphism, stated using Mathlib's homomorphism classes.
• TauCeti.IsSemigroupGroupPD.comp_spatial_comp: composition of spatial pullbacks, stated using Mathlib's homomorphism classes.
• TauCeti.IsSemigroupGroupPD.of_comp_spatial_surjective and TauCeti.IsSemigroupGroupPD.comp_spatial_iff_of_surjective: descent and equivalence for surjective additive homomorphisms.
• TauCeti.IsSemigroupGroupPD.comp_spatial_addEquiv_iff: invariance under a spatial additive equivalence.
• TauCeti.IsSemigroupGroupPD.comp_spatial_continuousLinearMap: the continuous-linear-map form used for real vector spaces.
• TauCeti.IsSemigroupGroupPD.continuous_comp_spatial: spatial pullback preserves continuity along continuous maps.
• TauCeti.IsSemigroupGroupPD.comp_spatial_and_continuous, TauCeti.IsSemigroupGroupPD.comp_spatial_continuousLinearMap_and_continuous: packaged homomorphism-class and continuous-linear forms preserving both positive-definiteness and continuity.

References

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

theorem TauCeti.IsSemigroupGroupPD.comp_spatial {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} {Φ : Type u_4} [FunLike Φ W V] [AddHomClass Φ W V] (hF : IsSemigroupGroupPD F) (φ : Φ) : IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, φ p.2)

Pulling back the spatial coordinate of a semigroup-group positive-definite function along an additive homomorphism preserves semigroup-group positive-definiteness. This is stated for Mathlib's homomorphism classes so it applies to bundled additive homomorphisms, additive equivalences, continuous linear maps, and similar maps.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_addMonoidHom {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (φ : W →+ V) : IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, φ p.2)

The explicit AddMonoidHom form of spatial pullback.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_comp {V : Type u_1} {W : Type u_2} {U : Type u_3} [AddCommGroup V] [AddCommGroup W] [AddCommGroup U] {F : NNReal × V → ℂ} {Φ : Type u_4} {Ψ : Type u_5} [FunLike Φ W V] [AddHomClass Φ W V] [FunLike Ψ U W] [AddHomClass Ψ U W] (hF : IsSemigroupGroupPD F) (φ : Φ) (ψ : Ψ) : IsSemigroupGroupPD fun (p : NNReal × U) => F (p.1, φ (ψ p.2))

Spatial pullbacks compose as expected.

theorem TauCeti.IsSemigroupGroupPD.of_comp_spatial_surjective {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} {Φ : Type u_4} [FunLike Φ W V] [AddHomClass Φ W V] (φ : Φ) (hsurj : Function.Surjective ⇑φ) (hcomp : IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, φ p.2)) : IsSemigroupGroupPD F

Semigroup-group positive-definiteness descends along a surjective spatial additive homomorphism.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_iff_of_surjective {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} {Φ : Type u_4} [FunLike Φ W V] [AddHomClass Φ W V] (φ : Φ) (hsurj : Function.Surjective ⇑φ) : (IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, φ p.2)) ↔ IsSemigroupGroupPD F

Along a surjective spatial additive homomorphism, a function is semigroup-group positive definite if and only if its spatial pullback is.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_addMonoidHom_iff_of_surjective {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} (φ : W →+ V) (hsurj : Function.Surjective ⇑φ) : (IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, φ p.2)) ↔ IsSemigroupGroupPD F

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

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_addEquiv_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} (e : W ≃+ V) : (IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, e p.2)) ↔ IsSemigroupGroupPD F

Semigroup-group positive-definiteness is invariant under precomposition by a spatial additive equivalence.

theorem TauCeti.IsSemigroupGroupPD.continuous_comp_spatial {V : Type u_1} {W : Type u_2} {F : NNReal × V → ℂ} [TopologicalSpace V] [TopologicalSpace W] (hF : Continuous F) (φ : W → V) (hφ : Continuous φ) : Continuous fun (p : NNReal × W) => F (p.1, φ p.2)

If the spatial map is continuous, spatial pullback preserves continuity.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_and_continuous {V : Type u_1} {W : Type u_2} [AddCommGroup V] [AddCommGroup W] {F : NNReal × V → ℂ} [TopologicalSpace V] [TopologicalSpace W] {Φ : Type u_4} [FunLike Φ W V] [AddHomClass Φ W V] (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (φ : Φ) (hφ : Continuous ⇑φ) : (IsSemigroupGroupPD fun (p : NNReal × W) => F (p.1, φ p.2)) ∧ Continuous fun (p : NNReal × W) => F (p.1, φ p.2)

Package spatial pullback of a semigroup-group positive-definite function with continuity of the pulled-back function.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_continuousLinearMap {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {G : NNReal × E → ℂ} (hG : IsSemigroupGroupPD G) (φ : E' →L[ℝ] E) : IsSemigroupGroupPD fun (p : NNReal × E') => G (p.1, φ p.2)

Spatial pullback along a continuous linear map preserves semigroup-group positive-definiteness.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_continuousLinearEquiv_iff {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {G : NNReal × E → ℂ} (e : E' ≃L[ℝ] E) : (IsSemigroupGroupPD fun (p : NNReal × E') => G (p.1, e p.2)) ↔ IsSemigroupGroupPD G

Spatial pullback along a continuous linear equivalence is an equivalence on semigroup-group positive-definiteness.

theorem TauCeti.IsSemigroupGroupPD.comp_spatial_continuousLinearMap_and_continuous {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {G : NNReal × E → ℂ} (hGpd : IsSemigroupGroupPD G) (hGcont : Continuous G) (φ : E' →L[ℝ] E) : (IsSemigroupGroupPD fun (p : NNReal × E') => G (p.1, φ p.2)) ∧ Continuous fun (p : NNReal × E') => G (p.1, φ p.2)

Package spatial pullback along a continuous linear map with preservation of continuity.