Positive-definite functions on [0, ∞) × V

This file records the Berg--Christensen--Ressel semigroup-group positive-definiteness predicate for functions on ℝ≥0 × V. For an additive group V, the intended involution is (t, v) ↦ (t, -v), so the finite quadratic forms use the entries F (tᵢ + tⱼ, vᵢ - vⱼ).

The generic positive-definite-function predicate already captures the finite quadratic-form condition. Here we name its BCR specialization by using the local wrapper BCRPoint V, whose involution is (t, v) ↦ (t, -v), rather than installing a global negation StarAddMonoid instance on every additive group V, which would conflict with Mathlib's ordinary star conventions. The result is the named hypothesis needed for the BCR Laplace--Fourier representation target in the OneParameterSemigroups roadmap.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Objects: the roadmap asks for IsSemigroupGroupPD as the positive-definite predicate on ℝ≥0 × V with involution (t, a)⋆ = (t, -a).

Main declarations

• TauCeti.IsSemigroupGroupPD: the BCR positive-definiteness predicate on ℝ≥0 × V.
• TauCeti.isSemigroupGroupPD_iff_posSemidef: the bridge to the associated positive-definite kernel.
• TauCeti.isSemigroupGroupPD_iff: the finite quadratic-form characterization.
• TauCeti.IsSemigroupGroupPD.conj_symm, diagonal, and origin lemmas: basic consequences of the semigroup-group positive-definiteness condition.
• TauCeti.isSemigroupGroupPD_const_of_nonneg, TauCeti.isSemigroupGroupPD_zero, and TauCeti.isSemigroupGroupPD_one: basic constant examples.
• TauCeti.IsSemigroupGroupPD.add, TauCeti.IsSemigroupGroupPD.mul, and finite sum/prod: closure properties inherited from positive-definite kernels.
• TauCeti.IsSemigroupGroupPD.quadForm_two_nonneg: the 2 × 2 BCR Hermitian sub-form is nonnegative.

References

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

def TauCeti.IsSemigroupGroupPD {V : Type u_1} [AddCommGroup V] (F : NNReal × V → ℂ) : Prop

A function on ℝ≥0 × V is semigroup-group positive definite, in the Berg--Christensen--Ressel sense, if all finite quadratic forms formed using the involution (t, v) ↦ (t, -v) are nonnegative: ∑ᵢⱼ cᵢ conj(cⱼ) F(tᵢ + tⱼ, vᵢ - vⱼ) ≥ 0.

Equations

• TauCeti.IsSemigroupGroupPD F = TauCeti.IsPositiveDefinite fun (p : TauCeti.BCRPoint✝ V) => F (TauCeti.BCRPoint.time✝ p, TauCeti.BCRPoint.point✝ p)

theorem TauCeti.isSemigroupGroupPD_iff_posSemidef {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} : IsSemigroupGroupPD F ↔ Matrix.PosSemidef fun (p q : NNReal × V) => F (p.1 + q.1, p.2 - q.2)

The bridge from semigroup-group positive definiteness to the associated positive-definite kernel.

theorem TauCeti.IsSemigroupGroupPD.posSemidef {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : Matrix.PosSemidef fun (p q : NNReal × V) => F (p.1 + q.1, p.2 - q.2)

The kernel associated to a semigroup-group positive-definite function is positive definite.

theorem TauCeti.IsSemigroupGroupPD.of_posSemidef {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : Matrix.PosSemidef fun (p q : NNReal × V) => F (p.1 + q.1, p.2 - q.2)) : IsSemigroupGroupPD F

Build a semigroup-group positive-definite function from the associated positive-definite kernel.

theorem TauCeti.isSemigroupGroupPD_const_of_nonneg {V : Type u_1} [AddCommGroup V] {k : ℂ} (hk : 0 ≤ k) : IsSemigroupGroupPD fun (x : NNReal × V) => k

A nonnegative complex constant is semigroup-group positive definite.

theorem TauCeti.isSemigroupGroupPD_zero {V : Type u_1} [AddCommGroup V] : IsSemigroupGroupPD fun (x : NNReal × V) => 0

The zero function is semigroup-group positive definite.

theorem TauCeti.isSemigroupGroupPD_one {V : Type u_1} [AddCommGroup V] : IsSemigroupGroupPD fun (x : NNReal × V) => 1

The constant-one function is semigroup-group positive definite.

theorem TauCeti.isSemigroupGroupPD_iff {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} : IsSemigroupGroupPD F ↔ (∀ (p q : NNReal × V), (starRingEnd ℂ) (F (p.1 + q.1, p.2 - q.2)) = F (q.1 + p.1, q.2 - p.2)) ∧ ∀ {ι : Type u_2} [inst : Fintype ι] (c : ι → ℂ) (p : ι → NNReal × V), 0 ≤ ∑ i : ι, ∑ j : ι, c i * (starRingEnd ℂ) (c j) * F ((p i).1 + (p j).1, (p i).2 - (p j).2)

The finite quadratic-form characterization of semigroup-group positive definiteness.

theorem TauCeti.IsSemigroupGroupPD.sum_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) {ι : Type u_2} [Fintype ι] (c : ι → ℂ) (p : ι → NNReal × V) : 0 ≤ ∑ i : ι, ∑ j : ι, c i * (starRingEnd ℂ) (c j) * F ((p i).1 + (p j).1, (p i).2 - (p j).2)

Positive-definiteness holds for arbitrary finite BCR families: for every finite family of scalars c and points p, the quadratic form ∑ i, ∑ j, c i * conj (c j) * F ((p i).1 + (p j).1, (p i).2 - (p j).2) is nonnegative.

theorem TauCeti.IsSemigroupGroupPD.quadForm_two_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (p q : NNReal × V) (c₀ c₁ : ℂ) : 0 ≤ c₀ * (starRingEnd ℂ) c₀ * F (p.1 + p.1, p.2 - p.2) + c₀ * (starRingEnd ℂ) c₁ * F (p.1 + q.1, p.2 - q.2) + c₁ * (starRingEnd ℂ) c₀ * F (q.1 + p.1, q.2 - p.2) + c₁ * (starRingEnd ℂ) c₁ * F (q.1 + q.1, q.2 - q.2)

The 2 × 2 BCR Hermitian sub-form at two points.

@[simp]

theorem TauCeti.IsSemigroupGroupPD.conj_symm {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (p q : NNReal × V) : (starRingEnd ℂ) (F (p.1 + q.1, p.2 - q.2)) = F (q.1 + p.1, q.2 - p.2)

A semigroup-group positive-definite function is conjugate symmetric for the BCR kernel: conj (F (t + u, v - w)) = F (u + t, w - v).

theorem TauCeti.IsSemigroupGroupPD.diagonal_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) : 0 ≤ F (t + t, 0)

Values of a semigroup-group positive-definite function on the time diagonal (t + t, 0) are real and nonnegative.

@[simp]

theorem TauCeti.IsSemigroupGroupPD.diagonal_im {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) : (F (t + t, 0)).im = 0

Values of a semigroup-group positive-definite function on the time diagonal (t + t, 0) have zero imaginary part.

theorem TauCeti.IsSemigroupGroupPD.diagonal_re_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) : 0 ≤ (F (t + t, 0)).re

The real part of a semigroup-group positive-definite function on the time diagonal (t + t, 0) is nonnegative.

theorem TauCeti.IsSemigroupGroupPD.diagonal_eq_ofReal_re {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) : F (t + t, 0) = ↑(F (t + t, 0)).re

A semigroup-group positive-definite function on the time diagonal (t + t, 0) is equal to its real part, viewed as a complex number.

theorem TauCeti.IsSemigroupGroupPD.map_zero_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : 0 ≤ F (0, 0)

The value of a semigroup-group positive-definite function at (0, 0) is real and nonnegative.

@[simp]

theorem TauCeti.IsSemigroupGroupPD.map_zero_im {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : (F (0, 0)).im = 0

The value of a semigroup-group positive-definite function at (0, 0) has zero imaginary part.

theorem TauCeti.IsSemigroupGroupPD.map_zero_re_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : 0 ≤ (F (0, 0)).re

The real part of the value of a semigroup-group positive-definite function at (0, 0) is nonnegative.

theorem TauCeti.IsSemigroupGroupPD.map_zero_eq_ofReal_re {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : F (0, 0) = ↑(F (0, 0)).re

The value at (0, 0) of a semigroup-group positive-definite function is equal to its real part, viewed as a complex number.

theorem TauCeti.IsSemigroupGroupPD.map_zero_re_pos_of_ne_zero {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (h0 : F (0, 0) ≠ 0) : 0 < (F (0, 0)).re

If a semigroup-group positive-definite function is nonzero at the origin, then the real part of its value at the origin is strictly positive.

theorem TauCeti.IsSemigroupGroupPD.add {V : Type u_1} [AddCommGroup V] {F G : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (hG : IsSemigroupGroupPD G) : IsSemigroupGroupPD fun (x : NNReal × V) => F x + G x

Semigroup-group positive-definite functions are closed under addition.

theorem TauCeti.IsSemigroupGroupPD.const_mul {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {k : ℂ} (hk : 0 ≤ k) (hF : IsSemigroupGroupPD F) : IsSemigroupGroupPD fun (x : NNReal × V) => k * F x

Semigroup-group positive-definite functions are closed under multiplication by a nonnegative complex scalar.

theorem TauCeti.IsSemigroupGroupPD.smul_of_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {r : ℝ} (hr : 0 ≤ r) (hF : IsSemigroupGroupPD F) : IsSemigroupGroupPD fun (x : NNReal × V) => r • F x

Semigroup-group positive-definite functions are closed under multiplication by a nonnegative real scalar.

theorem TauCeti.IsSemigroupGroupPD.mul {V : Type u_1} [AddCommGroup V] {F G : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (hG : IsSemigroupGroupPD G) : IsSemigroupGroupPD fun (x : NNReal × V) => F x * G x

Semigroup-group positive-definite functions are closed under pointwise multiplication (Schur product).

theorem TauCeti.IsSemigroupGroupPD.sum {V : Type u_1} [AddCommGroup V] {ι : Type u_2} {s : Finset ι} {F : ι → NNReal × V → ℂ} (hF : ∀ i ∈ s, IsSemigroupGroupPD (F i)) : IsSemigroupGroupPD fun (x : NNReal × V) => ∑ i ∈ s, F i x

Semigroup-group positive-definite functions are closed under finite sums.

theorem TauCeti.IsSemigroupGroupPD.prod {V : Type u_1} [AddCommGroup V] {ι : Type u_2} {s : Finset ι} {F : ι → NNReal × V → ℂ} (hF : ∀ i ∈ s, IsSemigroupGroupPD (F i)) : IsSemigroupGroupPD fun (x : NNReal × V) => ∏ i ∈ s, F i x

Semigroup-group positive-definite functions are closed under finite products (Schur products).