Time differences of bounded semigroup-group positive-definite functions

This file proves the alternating finite-difference property needed for the existence half of the Berg--Christensen--Ressel representation theorem. If F is bounded and positive definite on the involutive semigroup ℝ≥0 × V, then every iterated time difference built from

(t, v) ↦ F (t, v) - F (t + h, v)

is again positive definite.

The argument uses the canonical Kolmogorov decomposition of the BCR kernel. For any finite linear combination of feature vectors, translating every time coordinate by s gives a vector w s whose Gram function depends only on the sum of the two translation parameters. Its diagonal values form a bounded nonnegative log-convex sequence along any arithmetic progression. Such a sequence is decreasing, which is exactly positivity of the time difference.

Applying Bochner's theorem to those differences makes the corresponding alternating differences of the spatial Bochner measures positive, the time-regularity input required to assemble the BCR representing measure.

An iterated time difference expands into the alternating binomial sum (t, v) ↦ ∑ k ≤ n, (-1) ^ k (n choose k) F (t + k • h, v), so that sum is positive definite too. Positive definiteness is a statement about quadratic forms, not a pointwise sign: nonnegativity of the values themselves is asserted only along the zero-spatial axis, where it becomes the classical complete monotonicity of t ↦ F (t, 0) in the finite-difference sense. Those one-variable statements are read off the differences built here in TauCeti/Analysis/PositiveDefinite/SemigroupGroup/Time/Axis.lean.

Main declarations

• TauCeti.timeDifference: the one-step alternating time difference, the negative of Mathlib's forward difference fwdDiff applied in the time coordinate.
• TauCeti.listTimeDifference: the alternating difference along a finite list of time steps, and TauCeti.iteratedTimeDifference: its equal-step specialization.
• TauCeti.iteratedTimeDifference_eq_alternating_sum: the binomial expansion of an iterated time difference.
• TauCeti.IsSemigroupGroupPD.timeDifference: a bounded BCR-positive-definite function remains positive definite after subtracting a nonnegative forward time translate.
• TauCeti.IsSemigroupGroupPD.listTimeDifference and TauCeti.IsSemigroupGroupPD.iteratedTimeDifference: every alternating time difference of a bounded BCR-positive-definite function, along arbitrary or repeated steps, is positive definite, and TauCeti.IsSemigroupGroupPD.alternating_sum says the same in binomial form.
• TauCeti.isBounded_range_listTimeDifference and TauCeti.isBounded_range_iteratedTimeDifference: those differences stay bounded, so they can be differenced again.
• TauCeti.continuous_listTimeDifference and TauCeti.continuous_iteratedTimeDifference: those differences stay continuous, so Bochner's theorem applies to each of their time slices.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Theorem 4.1.13 and its bounded-semigroup argument.

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 ("BCR semigroup--Bochner").

def TauCeti.timeDifference {V : Type u} (h : NNReal) (F : NNReal × V → ℂ) : NNReal × V → ℂ

The first alternating time difference with step h: timeDifference h F (t, v) = F (t, v) - F (t + h, v). It is the negative of Mathlib's forward difference fwdDiff applied in the time coordinate.

Equations

• TauCeti.timeDifference h F p = -fwdDiff h (fun (t : NNReal) => F (t, p.2)) p.1

@[simp]

theorem TauCeti.timeDifference_apply {V : Type u} (h : NNReal) (F : NNReal × V → ℂ) (p : NNReal × V) : timeDifference h F p = F p - F (p.1 + h, p.2)

The first time difference evaluated at a point.

@[simp]

theorem TauCeti.timeDifference_zero {V : Type u} (F : NNReal × V → ℂ) : timeDifference 0 F = 0

The time difference with step zero is the zero function.

def TauCeti.listTimeDifference {V : Type u} (l : List NNReal) (F : NNReal × V → ℂ) : NNReal × V → ℂ

The alternating time difference along a finite list of steps, one application of timeDifference per entry of the list.

Equations

• TauCeti.listTimeDifference l F = List.foldr TauCeti.timeDifference F l

@[simp]

theorem TauCeti.listTimeDifference_nil {V : Type u} (F : NNReal × V → ℂ) : listTimeDifference [] F = F

Differencing along no steps at all is the identity.

@[simp]

theorem TauCeti.listTimeDifference_cons {V : Type u} (h : NNReal) (l : List NNReal) (F : NNReal × V → ℂ) : listTimeDifference (h :: l) F = timeDifference h (listTimeDifference l F)

Differencing along h :: l is one further first difference with step h.

def TauCeti.iteratedTimeDifference {V : Type u} (n : ℕ) (h : NNReal) (F : NNReal × V → ℂ) : NNReal × V → ℂ

The n-th alternating time difference, obtained by iterating timeDifference h.

Equations

• TauCeti.iteratedTimeDifference n h F = (TauCeti.timeDifference h)^[n] F

@[simp]

theorem TauCeti.iteratedTimeDifference_zero {V : Type u} (h : NNReal) (F : NNReal × V → ℂ) : iteratedTimeDifference 0 h F = F

The zeroth time difference is the original function.

@[simp]

theorem TauCeti.iteratedTimeDifference_succ {V : Type u} (n : ℕ) (h : NNReal) (F : NNReal × V → ℂ) : iteratedTimeDifference (n + 1) h F = timeDifference h (iteratedTimeDifference n h F)

The successor time difference is one further first difference.

theorem TauCeti.iteratedTimeDifference_eq_listTimeDifference {V : Type u} (n : ℕ) (h : NNReal) (F : NNReal × V → ℂ) : iteratedTimeDifference n h F = listTimeDifference (List.replicate n h) F

Iterating the step h is differencing along the constant list of n copies of h.

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

At a fixed spatial coordinate, the n-th time difference is the alternating n-th forward difference of the one-variable function t ↦ F (t, v). This is the bridge to the generic finite-difference theory of TauCeti/Analysis/PositiveDefinite/Function/Difference.lean.

theorem TauCeti.iteratedTimeDifference_eq_alternating_sum {V : Type u} (n : ℕ) (h : NNReal) (F : NNReal × V → ℂ) : iteratedTimeDifference n h F = fun (p : NNReal × V) => ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (p.1 + k • h, p.2)

The binomial expansion of an iterated time difference. This is the form in which the measure-theoretic half of the Berg--Christensen--Ressel representation slices the differences by time.

theorem TauCeti.isBounded_range_timeDifference {V : Type u} {F : NNReal × V → ℂ} (hbounded : Bornology.IsBounded (Set.range F)) (h : NNReal) : Bornology.IsBounded (Set.range (timeDifference h F))

Boundedness is preserved by taking a first time difference.

theorem TauCeti.isBounded_range_listTimeDifference {V : Type u} {F : NNReal × V → ℂ} (hbounded : Bornology.IsBounded (Set.range F)) (l : List NNReal) : Bornology.IsBounded (Set.range (listTimeDifference l F))

Boundedness is preserved by differencing along any finite list of steps.

theorem TauCeti.isBounded_range_iteratedTimeDifference {V : Type u} {F : NNReal × V → ℂ} (hbounded : Bornology.IsBounded (Set.range F)) (n : ℕ) (h : NNReal) : Bornology.IsBounded (Set.range (iteratedTimeDifference n h F))

Boundedness is preserved by every iterated time difference.

theorem TauCeti.continuous_timeDifference {V : Type u} {F : NNReal × V → ℂ} [TopologicalSpace V] (hF : Continuous F) (h : NNReal) : Continuous (timeDifference h F)

Continuity is preserved by taking a first time difference.

theorem TauCeti.continuous_listTimeDifference {V : Type u} {F : NNReal × V → ℂ} [TopologicalSpace V] (hF : Continuous F) (l : List NNReal) : Continuous (listTimeDifference l F)

Continuity is preserved by differencing along any finite list of steps.

theorem TauCeti.continuous_iteratedTimeDifference {V : Type u} {F : NNReal × V → ℂ} [TopologicalSpace V] (hF : Continuous F) (n : ℕ) (h : NNReal) : Continuous (iteratedTimeDifference n h F)

Continuity is preserved by every iterated time difference.

theorem TauCeti.IsSemigroupGroupPD.timeDifference {V : Type u} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (hbounded : Bornology.IsBounded (Set.range F)) (h : NNReal) : IsSemigroupGroupPD (TauCeti.timeDifference h F)

A bounded BCR-positive-definite function remains positive definite after subtracting a forward time translate. In other words, for every h : ℝ≥0, the first alternating time difference (t, v) ↦ F (t, v) - F (t + h, v) is semigroup-group positive definite.

theorem TauCeti.IsSemigroupGroupPD.listTimeDifference {V : Type u} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (hbounded : Bornology.IsBounded (Set.range F)) (l : List NNReal) : IsSemigroupGroupPD (TauCeti.listTimeDifference l F)

Every alternating time difference along a finite list of steps of a bounded BCR-positive-definite function is again semigroup-group positive definite.

theorem TauCeti.IsSemigroupGroupPD.iteratedTimeDifference {V : Type u} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (hbounded : Bornology.IsBounded (Set.range F)) (n : ℕ) (h : NNReal) : IsSemigroupGroupPD (TauCeti.iteratedTimeDifference n h F)

Every iterated alternating time difference of a bounded BCR-positive-definite function is again semigroup-group positive definite.

theorem TauCeti.IsSemigroupGroupPD.alternating_sum {V : Type u} [AddCommGroup V] {F : NNReal × V → ℂ} (hF : IsSemigroupGroupPD F) (hbounded : Bornology.IsBounded (Set.range F)) (n : ℕ) (h : NNReal) : IsSemigroupGroupPD fun (p : NNReal × V) => ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (p.1 + k • h, p.2)

The alternating iterated time differences, expanded as binomial sums, are semigroup-group positive definite. This is IsSemigroupGroupPD.iteratedTimeDifference with the differencing operator resolved into an explicit alternating sum over an arithmetic progression of times.