Hermitian symmetry and bounds for subtraction kernels

This file records the reality of ψ 0 and symmetry under negation for Hermitian subtraction kernels (a, b) ↦ ψ (a - b). For positive-semidefinite subtraction kernels, the scalar Cauchy--Schwarz estimates from TauCeti.Analysis.Matrix.PosSemidef give nonnegativity of re (ψ 0) and the uniform norm bound ‖ψ z‖ ≤ re (ψ 0). These properties supply the conjugate symmetry and boundedness used in the Fourier analysis of positive-definite functions.

Main declarations

• Matrix.IsHermitian.map_neg_eq_star: a function with Hermitian subtraction kernel satisfies ψ (-v) = star (ψ v).
• Matrix.IsHermitian.map_zero_eq_ofReal_re: for an RCLike-valued function with Hermitian subtraction kernel, the value at 0 is real.
• Matrix.PosSemidef.map_zero_re_nonneg and Matrix.PosSemidef.norm_apply_le_map_zero_re: for an RCLike-valued function with positive-semidefinite subtraction kernel, the real part of its value at 0 is nonnegative and bounds the function uniformly in norm.

References

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

theorem Matrix.IsHermitian.map_neg_eq_star {R : Type u_1} {V : Type u_2} [Star R] [SubNegZeroMonoid V] {ψ : V → R} (h : IsHermitian fun (a b : V) => ψ (a - b)) (v : V) : ψ (-v) = star (ψ v)

A function with Hermitian subtraction kernel satisfies ψ (-v) = star (ψ v).

theorem Matrix.IsHermitian.map_zero_eq_ofReal_re {𝕜 : Type u_1} [RCLike 𝕜] {V : Type u_2} {ψ : V → 𝕜} [SubNegZeroMonoid V] (h : IsHermitian fun (a b : V) => ψ (a - b)) : ψ 0 = ↑(RCLike.re (ψ 0))

The value at 0 of an RCLike-valued function with Hermitian subtraction kernel is real.

theorem Matrix.PosSemidef.map_zero_re_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {V : Type u_2} {ψ : V → 𝕜} [SubNegZeroMonoid V] (hpd : PosSemidef fun (a b : V) => ψ (a - b)) : 0 ≤ RCLike.re (ψ 0)

The value at 0 of a function with positive-semidefinite subtraction kernel has nonnegative real part.

theorem Matrix.PosSemidef.norm_apply_le_map_zero_re {𝕜 : Type u_1} [RCLike 𝕜] {V : Type u_2} {ψ : V → 𝕜} [AddGroup V] (hpd : PosSemidef fun (a b : V) => ψ (a - b)) (z : V) : ‖ψ z‖ ≤ RCLike.re (ψ 0)

A function with positive-semidefinite subtraction kernel is uniformly bounded by the real part of its value at 0.