Continuity of positive-definite functions

This file records the standard continuity upgrade for positive-definite functions on a seminormed additive group with the negation involution. A positive-definite function that is continuous at the origin is uniformly continuous. The file also records the local estimates ‖F x - F y‖² ≤ 2 F(0).re ((F 0).re - (F (x + star y)).re) and ‖F x - F y‖² ≤ 2 F(0).re ‖F (x + star y) - F 0‖ at points satisfying x + star x = 0 and y + star y = 0, together with their specializations to additive groups whose involution is negation.

This advances Part C of the OneParameterSemigroups roadmap, whose positive-definite-function API asks for the basic fact "continuity at 0 ⇒ uniform continuity" before Bochner's theorem.

Main declarations

In the namespace TauCeti.IsPositiveDefinite:

• norm_sub_sq_le_two_mul_map_zero_re_mul_re_sub_of_star_eq_neg: the local real-part continuity estimate.
• norm_sub_sq_le_two_mul_map_zero_re_mul_re_sub_of_add_star_eq_zero: the monoid-level local real-part continuity estimate.
• norm_sub_sq_le_two_mul_map_zero_re_mul_norm_sub_of_star_eq_neg: the local norm-valued continuity estimate.
• norm_sub_sq_le_two_mul_map_zero_re_mul_norm_sub_of_add_star_eq_zero: the monoid-level local norm-valued continuity estimate.
• norm_sub_sq_le_two_mul_map_zero_re_mul_re_sub_of_forall_star_eq_neg and norm_sub_sq_le_two_mul_map_zero_re_mul_norm_sub_of_forall_star_eq_neg: specializations to a globally negating involution.
• uniformContinuous_of_continuousAt_zero_of_forall_star_eq_neg: continuity at 0 implies uniform continuity.

References

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

theorem TauCeti.IsPositiveDefinite.norm_sub_sq_le_two_mul_map_zero_re_mul_re_sub_of_add_star_eq_zero {E : Type u_1} [AddMonoid E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) {x y : E} (hx : x + star x = 0) (hy : y + star y = 0) : ‖F x - F y‖ ^ 2 ≤ 2 * (F 0).re * ((F 0).re - (F (x + star y)).re)

The local monoid-level real-part form of the standard positive-definite continuity estimate.

theorem TauCeti.IsPositiveDefinite.norm_sub_sq_le_two_mul_map_zero_re_mul_norm_sub_of_add_star_eq_zero {E : Type u_1} [AddMonoid E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) {x y : E} (hx : x + star x = 0) (hy : y + star y = 0) : ‖F x - F y‖ ^ 2 ≤ 2 * (F 0).re * ‖F (x + star y) - F 0‖

The local monoid-level norm-valued form of the standard positive-definite continuity estimate.

theorem TauCeti.IsPositiveDefinite.norm_sub_sq_le_two_mul_map_zero_re_mul_re_sub_of_star_eq_neg {E : Type u_1} [AddGroup E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) {x y : E} (hx : star x = -x) (hy : star y = -y) : ‖F x - F y‖ ^ 2 ≤ 2 * (F 0).re * ((F 0).re - (F (x - y)).re)

The local real-part form of the standard positive-definite continuity estimate.

theorem TauCeti.IsPositiveDefinite.norm_sub_sq_le_two_mul_map_zero_re_mul_re_sub_of_forall_star_eq_neg {E : Type u_1} [AddGroup E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) (hstar : ∀ (x : E), star x = -x) (x y : E) : ‖F x - F y‖ ^ 2 ≤ 2 * (F 0).re * ((F 0).re - (F (x - y)).re)

The real-part form of the standard positive-definite continuity estimate under a globally negating involution.

theorem TauCeti.IsPositiveDefinite.norm_sub_sq_le_two_mul_map_zero_re_mul_norm_sub_of_star_eq_neg {E : Type u_1} [AddGroup E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) {x y : E} (hx : star x = -x) (hy : star y = -y) : ‖F x - F y‖ ^ 2 ≤ 2 * (F 0).re * ‖F (x - y) - F 0‖

The local norm-valued form of the standard positive-definite continuity estimate.

theorem TauCeti.IsPositiveDefinite.norm_sub_sq_le_two_mul_map_zero_re_mul_norm_sub_of_forall_star_eq_neg {E : Type u_1} [AddGroup E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) (hstar : ∀ (x : E), star x = -x) (x y : E) : ‖F x - F y‖ ^ 2 ≤ 2 * (F 0).re * ‖F (x - y) - F 0‖

The norm-valued form of the standard positive-definite continuity estimate under a globally negating involution.

theorem TauCeti.IsPositiveDefinite.uniformContinuous_of_continuousAt_zero_of_forall_star_eq_neg {E : Type u_1} [SeminormedAddGroup E] [StarAddMonoid E] {F : E → ℂ} (hF : IsPositiveDefinite F) (hstar : ∀ (x : E), star x = -x) (hcont : ContinuousAt F 0) : UniformContinuous F

A positive-definite function on a seminormed additive group with the negation involution is uniformly continuous as soon as it is continuous at the origin.