Normalizing positive-definite functions

This file records the standard normalization step for positive-definite functions: if F : M → ℂ is positive definite and F 0 ≠ 0, then multiplying by the reciprocal of the nonnegative real number (F 0).re gives a positive-definite function whose value at the origin is 1.

This is part of the normalization API requested in Part C of the OneParameterSemigroups roadmap ("Positive-definite functions and Bochner's theorem"). Normalized positive-definite functions are the convenient form for characteristic functions and for the later Bochner and GNS/Kolmogorov constructions: after normalization, the general bound ‖F a‖ ≤ (F 0).re becomes the familiar ‖F a‖ ≤ 1.

The file deliberately keeps the hypotheses unbundled. It proves lemmas about the explicit normalized function rather than introducing a new bundled predicate.

Main declarations

• TauCeti.IsPositiveDefinite.normalize: multiplying by ((F 0).re)⁻¹ preserves positive-definiteness.
• TauCeti.IsPositiveDefinite.normalize_apply_zero: the normalized function has value 1 at the origin.
• TauCeti.IsPositiveDefinite.norm_normalize_apply_le_one_of_add_star_eq_zero and TauCeti.IsPositiveDefinite.norm_normalize_apply_le_one_of_star_eq_neg: normalized functions are bounded by 1 on the usual group-like points.

References

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

theorem TauCeti.IsPositiveDefinite.normalize {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) : IsPositiveDefinite fun (x : M) => (↑(F 0).re)⁻¹ * F x

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

@[simp]

theorem TauCeti.IsPositiveDefinite.normalize_apply_zero {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (h0 : F 0 ≠ 0) : (↑(F 0).re)⁻¹ * F 0 = 1

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

theorem TauCeti.IsPositiveDefinite.norm_normalize_apply_le_one_of_add_star_eq_zero {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (a : M) (ha : a + star a = 0) : ‖(↑(F 0).re)⁻¹ * F a‖ ≤ 1

At points satisfying a + star a = 0, the normalized positive-definite function is bounded by 1. When F 0 = 0 the normalizing scalar is 0, so the bound holds trivially.

theorem TauCeti.IsPositiveDefinite.norm_normalize_apply_le_one_of_star_eq_neg {G : Type u_2} [AddGroup G] [StarAddMonoid G] {H : G → ℂ} (hH : IsPositiveDefinite H) (a : G) (hstar_a : star a = -a) : ‖(↑(H 0).re)⁻¹ * H a‖ ≤ 1

Under the negation involution, the normalized positive-definite function is bounded by 1 at every point.

theorem TauCeti.IsPositiveDefinite.norm_normalize_apply_le_one_of_forall_star_eq_neg {G : Type u_2} [AddGroup G] [StarAddMonoid G] {H : G → ℂ} (hH : IsPositiveDefinite H) (hstar : ∀ (a : G), star a = -a) (a : G) : ‖(↑(H 0).re)⁻¹ * H a‖ ≤ 1

If the involution is negation everywhere, the normalized positive-definite function is uniformly bounded by 1.