Time slices of semigroup-group positive-definite functions

A Berg--Christensen--Ressel positive-definite function on ℝ≥0 × V is positive definite in the spatial variable at every fixed time. Indeed, to test the kernel (v, w) ↦ F (t, v - w), apply the BCR kernel to the family of points (t / 2, v).

This file records that fixed-time-slice API in kernel form, together with the predicate form for the fixed-time slice. These lemmas are prerequisites for the BCR representation milestone in the OneParameterSemigroups roadmap: later proofs can apply the spatial Bochner theorem to each time slice before handling the remaining Laplace/semigroup structure.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 ("BCR semigroup--Bochner"), specifically the reduction of a bounded continuous positive-definite function on [0,∞) × V to spatial positive-definite functions.

Main declarations

• TauCeti.IsSemigroupGroupPD.posSemidef_timeSlice: the fixed-time spatial kernel is positive definite.
• TauCeti.IsSemigroupGroupPD.timeSlice_conj_symm and diagonal lemmas: basic symmetry and real-nonnegative diagonal facts for fixed-time slices.
• TauCeti.IsSemigroupGroupPD.timeSlice_sum_nonneg: the fixed-time spatial quadratic form is nonnegative for arbitrary finite families.
• TauCeti.IsSemigroupGroupPD.timeSlice_normSq_le: the fixed-time spatial Cauchy--Schwarz estimate.
• TauCeti.IsSemigroupGroupPD.norm_apply_le_timeSlice_diagonal_re: the direct fixed-time bound ‖F (t, v)‖ ≤ (F (t, 0)).re.
• TauCeti.IsSemigroupGroupPD.timeSlice_eq_zero_of_timeSlice_diagonal_eq_zero: a zero fixed-time diagonal value kills the whole fixed-time spatial slice.
• TauCeti.IsSemigroupGroupPD.timeSlice_isPositiveDefinite and TauCeti.IsSemigroupGroupPD.isPositiveDefiniteSub_timeSlice: the predicate forms, for the negation involution and in the subtraction form Bochner's theorem uses.
• TauCeti.IsSemigroupGroupPD.posSemidef_timeSlice_and_continuous: packages the fixed-time positive-definite kernel with continuity of the fixed-time slice.

References

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

theorem TauCeti.IsSemigroupGroupPD.posSemidef_timeSlice {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) : Matrix.PosSemidef fun (v w : V) => F (t, v - w)

At every fixed time t, a semigroup-group positive-definite function gives the spatial positive-definite kernel (v, w) ↦ F (t, v - w).

@[simp]

theorem TauCeti.IsSemigroupGroupPD.timeSlice_conj_symm {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) (v w : V) : (starRingEnd ℂ) (F (t, v - w)) = F (t, w - v)

Fixed-time slices are conjugate-symmetric in the spatial variable: conj (F (t, v - w)) = F (t, w - v).

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

The diagonal value F (t, 0) of a fixed-time slice is real and nonnegative.

@[simp]

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

The diagonal value F (t, 0) of a fixed-time slice has zero imaginary part.

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

The real part of the diagonal value F (t, 0) of a fixed-time slice is nonnegative.

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

The diagonal value F (t, 0) of a fixed-time slice is equal to its real part, viewed as a complex number.

theorem TauCeti.IsSemigroupGroupPD.timeSlice_sum_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) {ι : Type u_2} [Fintype ι] (v : ι → V) (x : ι → ℂ) : 0 ≤ ∑ i : ι, ∑ j : ι, (starRingEnd ℂ) (x i) * x j * F (t, v i - v j)

The fixed-time spatial quadratic form is nonnegative for arbitrary finite families.

theorem TauCeti.IsSemigroupGroupPD.timeSlice_normSq_le {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) (v w : V) : RCLike.normSq (F (t, v - w)) ≤ RCLike.re (F (t, 0)) * RCLike.re (F (t, 0))

The fixed-time spatial Cauchy--Schwarz bound for the kernel entry F (t, v - w).

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

At a fixed time, a semigroup-group positive-definite function is bounded by the real part of its zero-spatial value.

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

If the fixed-time diagonal value is zero, then the whole fixed-time spatial slice is zero.

theorem TauCeti.IsSemigroupGroupPD.norm_apply_le_one_of_timeSlice_diagonal_eq_one {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) {t : NNReal} (ht : F (t, 0) = 1) (v : V) : ‖F (t, v)‖ ≤ 1

Normalized fixed-time slices are bounded by 1.

theorem TauCeti.IsSemigroupGroupPD.timeSlice_isPositiveDefinite {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} [StarAddMonoid V] (hF : IsSemigroupGroupPD F) (hstar : ∀ (v : V), star v = -v) (t : NNReal) : IsPositiveDefinite fun (v : V) => F (t, v)

If the spatial type is equipped with the negation involution, then each fixed-time slice is a positive-definite function in the generic IsPositiveDefinite sense.

theorem TauCeti.IsSemigroupGroupPD.isPositiveDefiniteSub_timeSlice {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (t : NNReal) : IsPositiveDefiniteSub fun (v : V) => F (t, v)

Each fixed-time slice is positive definite in the subtraction form, the predicate that Bochner's theorem on a finite-dimensional real inner-product space takes as its hypothesis.

theorem TauCeti.IsSemigroupGroupPD.posSemidef_timeSlice_and_continuous {V : Type u_1} [AddCommGroup V] [TopologicalSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (t : NNReal) : (Matrix.PosSemidef fun (v w : V) => F (t, v - w)) ∧ Continuous fun (v : V) => F (t, v)

Package the positive-definite kernel on a fixed-time slice with continuity of the one-variable fixed-time slice.