The time axis of semigroup-group positive-definite functions

A Berg--Christensen--Ressel positive-definite function on ℝ≥0 × V restricts along the zero-spatial axis to a positive-definite function of time. At the kernel level, this says that (t, u) ↦ F (t + u, 0) is positive definite, obtained from the BCR kernel by pulling back along t ↦ (t, 0).

This is the companion to the fixed-time spatial-slice API. It is a small prerequisite for the BCR semigroup--Bochner representation milestone in the OneParameterSemigroups roadmap: later proofs can separate the spatial Bochner slices from the remaining one-dimensional time-axis structure. When the spatial variable is trivial, this is the positive-definiteness statement left before the Bernstein/Laplace component of BCR.

Reading the alternating time differences of TauCeti.timeDifference on the axis v = 0 gives the regularity of that one-dimensional function: it is antitone and all of its iterated forward differences carry the sign (-1)ⁿ, which is complete monotonicity in the finite-difference sense. Those statements are the generic TauCeti.IsPositiveDefinite theory of TauCeti/Analysis/PositiveDefinite/Function/Difference.lean, applied to the positive-definite function t ↦ F (t, 0) on ℝ≥0 with its trivial involution and evaluated at the norm point t / 2 + star (t / 2) = t. Accordingly they assume only that the time axis is bounded, ‖F (t, 0)‖ ≤ C, rather than that F is bounded on all of ℝ≥0 × V.

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

Main declarations

• TauCeti.IsSemigroupGroupPD.posSemidef_timeAxis: the kernel (t, u) ↦ F (t + u, 0) is positive definite.
• TauCeti.IsSemigroupGroupPD.timeAxis_conj_symm: conjugate symmetry for the time-axis kernel. The existing fixed-time-slice diagonal lemmas give the real/nonnegative facts for F (t, 0).
• TauCeti.IsSemigroupGroupPD.timeAxis_sum_nonneg: the finite quadratic-form restatement.
• TauCeti.IsSemigroupGroupPD.timeAxis_isPositiveDefinite: the one-variable predicate form for t ↦ F (t, 0) using the trivial involution on ℝ≥0.
• TauCeti.IsSemigroupGroupPD.timeAxis_normSq_le: the time-axis Cauchy--Schwarz estimate.
• TauCeti.IsSemigroupGroupPD.posSemidef_timeAxis_and_continuous: packages the kernel result with continuity of the zero-spatial slice.
• TauCeti.iteratedTimeDifference_timeAxis_re: the time-axis value of an iterated time difference of F is, up to the sign (-1)ⁿ, an iterated forward difference of t ↦ (F (t, 0)).re.
• TauCeti.IsSemigroupGroupPD.timeAxis_alternating_sum_nonneg, TauCeti.IsSemigroupGroupPD.timeAxis_alternating_sum_re_nonneg, TauCeti.IsSemigroupGroupPD.timeAxis_iteratedTimeDifference_nonneg and TauCeti.IsSemigroupGroupPD.neg_one_pow_mul_fwdDiff_timeAxis_re_nonneg: a bounded time axis t ↦ F (t, 0) is completely monotone in the finite-difference sense, in the order of ℂ, for real parts, and in binomial-sum and forward-difference form.
• TauCeti.IsSemigroupGroupPD.timeAxis_sub_nonneg and TauCeti.IsSemigroupGroupPD.timeAxis_re_antitone: a bounded time axis is nonincreasing.

References

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

theorem TauCeti.iteratedTimeDifference_timeAxis_re {V : Type u_1} [Zero V] {F : NNReal × V → ℂ} (n : ℕ) (h t : NNReal) : (iteratedTimeDifference n h F (t, 0)).re = (-1) ^ n * (fwdDiff h)^[n] (fun (s : NNReal) => (F (s, 0)).re) t

The n-th iterated forward difference of the time-axis function t ↦ (F (t, 0)).re, with the sign (-1)ⁿ, is the time-axis value of the n-th iterated time difference of F.

theorem TauCeti.IsSemigroupGroupPD.posSemidef_timeAxis {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) : Matrix.PosSemidef fun (t u : NNReal) => F (t + u, 0)

The zero-spatial time-axis kernel of a semigroup-group positive-definite function is positive definite: (t, u) ↦ F (t + u, 0).

@[simp]

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

The zero-spatial time-axis kernel is conjugate symmetric: conj (F (t + u, 0)) = F (u + t, 0).

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

The finite quadratic form of the zero-spatial time-axis kernel is nonnegative.

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

The zero-spatial time-axis function t ↦ F (t, 0) is positive definite for the trivial involution on ℝ≥0.

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

The time-axis Cauchy--Schwarz estimate for F (t + u, 0).

Alternating differences along the time axis

Reading the alternating time differences of a BCR-positive-definite function on the time axis v = 0 leaves a statement about the real function t ↦ (F (t, 0)).re alone, the case with no spatial variable. Only that axis has to be bounded for this: the statements below are the generic one-variable theory applied to the positive-definite function t ↦ F (t, 0) on ℝ≥0 with its trivial involution, evaluated at the norm point t / 2 + star (t / 2) = t.

theorem TauCeti.IsSemigroupGroupPD.timeAxis_alternating_sum_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {C : ℝ} (n : ℕ) (hF : IsSemigroupGroupPD F) (hbdd : ∀ (t : NNReal), ‖F (t, 0)‖ ≤ C) (h t : NNReal) : 0 ≤ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (t + k • h, 0)

A semigroup-group positive-definite function with bounded time axis is completely monotone along that axis, in the finite-difference sense: all alternating binomial sums of its values along an arithmetic progression of times are nonnegative. This is the form in which the Laplace half of the Berg--Christensen--Ressel representation consumes positive definiteness.

theorem TauCeti.IsSemigroupGroupPD.timeAxis_iteratedTimeDifference_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {C : ℝ} (n : ℕ) (hF : IsSemigroupGroupPD F) (hbdd : ∀ (t : NNReal), ‖F (t, 0)‖ ≤ C) (h t : NNReal) : 0 ≤ TauCeti.iteratedTimeDifference n h F (t, 0)

The iterated time difference of a semigroup-group positive-definite function whose time axis is bounded is nonnegative along the zero-spatial axis. Only the time axis has to be bounded, in contrast with IsSemigroupGroupPD.iteratedTimeDifference.

theorem TauCeti.IsSemigroupGroupPD.timeAxis_alternating_sum_re_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {C : ℝ} (n : ℕ) (hF : IsSemigroupGroupPD F) (hbdd : ∀ (t : NNReal), ‖F (t, 0)‖ ≤ C) (h t : NNReal) : 0 ≤ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (F (t + k • h, 0)).re

The real-part form of IsSemigroupGroupPD.timeAxis_alternating_sum_nonneg: the alternating binomial sums of t ↦ (F (t, 0)).re are nonnegative. This is the shape consumed by the real-valued complete-monotonicity API.

theorem TauCeti.IsSemigroupGroupPD.neg_one_pow_mul_fwdDiff_timeAxis_re_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {C : ℝ} (n : ℕ) (hF : IsSemigroupGroupPD F) (hbdd : ∀ (t : NNReal), ‖F (t, 0)‖ ≤ C) (h t : NNReal) : 0 ≤ (-1) ^ n * (fwdDiff h)^[n] (fun (s : NNReal) => (F (s, 0)).re) t

The time-axis function of a BCR-positive-definite function with bounded time axis has alternating forward differences. Its n-th forward difference with any step has the sign (-1)ⁿ, which is complete monotonicity in the finite-difference sense.

theorem TauCeti.IsSemigroupGroupPD.timeAxis_sub_nonneg {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {C : ℝ} (hF : IsSemigroupGroupPD F) (hbdd : ∀ (t : NNReal), ‖F (t, 0)‖ ≤ C) (h t : NNReal) : 0 ≤ F (t, 0) - F (t + h, 0)

Along the zero-spatial axis, a later value of a semigroup-group positive-definite function with bounded time axis is dominated by an earlier one, in the order of ℂ.

theorem TauCeti.IsSemigroupGroupPD.timeAxis_re_antitone {V : Type u_1} [AddCommGroup V] {F : NNReal × V → ℂ} {C : ℝ} (hF : IsSemigroupGroupPD F) (hbdd : ∀ (t : NNReal), ‖F (t, 0)‖ ≤ C) : Antitone fun (t : NNReal) => (F (t, 0)).re

The time-axis function of a BCR-positive-definite function with bounded time axis decreases: its real part is an antitone function of time.

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

Package the positive-definite zero-spatial time-axis kernel with continuity of the one-variable time-axis slice.