Normalizing semigroup-group positive-definite functions

This file records the standard normalization step for Berg--Christensen--Ressel semigroup-group positive-definite functions on ℝ≥0 × V: if F (0, 0) ≠ 0, then multiplying F by the reciprocal of the nonnegative real number (F (0, 0)).re gives a semigroup-group positive-definite function with value 1 at the origin.

The generic positive-definite-function normalization API applies to the internal involutive monoid used to define TauCeti.IsSemigroupGroupPD, but that wrapper is intentionally private. This file exposes the corresponding public API directly on functions ℝ≥0 × V → ℂ. It is a small prerequisite for the BCR semigroup--Bochner representation milestone, where one separates normalization from the independent boundedness and continuity hypotheses.

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

Main declarations

• TauCeti.IsSemigroupGroupPD.normalize: the normalized function remains semigroup-group positive definite.
• TauCeti.IsSemigroupGroupPD.normalize_apply_zero: the normalized function has value 1 at (0, 0).
• TauCeti.IsSemigroupGroupPD.normalize_continuous: normalization preserves continuity.
• TauCeti.IsSemigroupGroupPD.norm_normalize_apply_le_one_of_norm_le_map_zero_re: a bounded BCR function becomes bounded by 1 after normalization.

References

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

theorem TauCeti.IsSemigroupGroupPD.normalize {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : IsSemigroupGroupPD fun (p : NNReal × V) => (↑(F (0, 0)).re)⁻¹ * F p

Multiplying a semigroup-group positive-definite function by the reciprocal of its real value at the origin preserves semigroup-group positive-definiteness. If F (0, 0) = 0, this is the zero scaling; the separate normalize_apply_zero lemma records the useful nonzero case.

@[simp]

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

The normalized semigroup-group positive-definite function has value 1 at the origin.

theorem TauCeti.IsSemigroupGroupPD.normalize_map_zero {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (h0 : F (0, 0) ≠ 0) : (fun (p : NNReal × V) => (↑(F (0, 0)).re)⁻¹ * F p) (0, 0) = 1

A normalized semigroup-group positive-definite function has origin value 1, stated as the map-zero lemma for the normalized function.

theorem TauCeti.IsSemigroupGroupPD.normalize_apply_of_map_zero_eq_one {V : Type u_1} [Zero V] {F : NNReal × V → ℂ} (hF0 : F (0, 0) = 1) (p : NNReal × V) : (↑(F (0, 0)).re)⁻¹ * F p = F p

If a semigroup-group positive-definite function is already normalized at the origin, the explicit normalization leaves it unchanged pointwise.

theorem TauCeti.IsSemigroupGroupPD.normalize_continuous {V : Type u_1} [Zero V] {F : NNReal × V → ℂ} [TopologicalSpace V] (hFcont : Continuous F) : Continuous fun (p : NNReal × V) => (↑(F (0, 0)).re)⁻¹ * F p

Normalization preserves continuity.

theorem TauCeti.IsSemigroupGroupPD.normalize_and_continuous {V : Type u_1} [AddCommGroup V] [TopologicalSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) : (IsSemigroupGroupPD fun (p : NNReal × V) => (↑(F (0, 0)).re)⁻¹ * F p) ∧ Continuous fun (p : NNReal × V) => (↑(F (0, 0)).re)⁻¹ * F p

Package normalization with continuity preservation.

theorem TauCeti.IsSemigroupGroupPD.norm_normalize_apply_le_one_of_norm_le_map_zero_re {V : Type u_1} [Zero V] {F : NNReal × V → ℂ} (hbound : ∀ (p : NNReal × V), ‖F p‖ ≤ (F (0, 0)).re) (p : NNReal × V) : ‖(↑(F (0, 0)).re)⁻¹ * F p‖ ≤ 1

A function bounded by its origin value becomes bounded by 1 after normalization. This keeps the boundedness hypothesis separate, as in the BCR representation theorem.

theorem TauCeti.IsSemigroupGroupPD.norm_normalize_apply_le_one_of_norm_le_one_of_map_zero_eq_one {V : Type u_1} [Zero V] {F : NNReal × V → ℂ} (hF0 : F (0, 0) = 1) (hbound : ∀ (p : NNReal × V), ‖F p‖ ≤ 1) (p : NNReal × V) : ‖(↑(F (0, 0)).re)⁻¹ * F p‖ ≤ 1

If a semigroup-group positive-definite function is already bounded by 1 and normalized at the origin, then applying the explicit normalization preserves the same bound.