Laplace--Fourier atoms for semigroup-group positive-definite functions

This file records the atomic positive-definite functions that appear inside the Berg--Christensen--Ressel Laplace--Fourier representation. For a nonnegative Laplace parameter p : ℝ≥0 and a spatial frequency q : V, the separated function

(t, v) ↦ exp (-t p) * exp (-2πi ⟪v, q⟫)

is semigroup-group positive definite on ℝ≥0 × V, and is continuous when V is topological. The proof is just the rank-one-kernel calculation for each factor, followed by the existing separated-product constructor.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 ("BCR semigroup--Bochner"): the representing integrand in the target theorem is a finite-measure mixture of these atoms.

Main declarations

• TauCeti.posSemidef_laplaceAtom: the time kernel (t, u) ↦ exp (-(t + u) p) is positive definite.
• TauCeti.isSemigroupGroupPD_laplaceFourierAtom: the separated BCR atom is positive definite.
• TauCeti.isSemigroupGroupPD_laplaceFourierAtom_and_continuous: the same result packaged with continuity.

References

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

noncomputable def TauCeti.laplaceAtom (p t : NNReal) : ℂ

The Laplace atom at p : ℝ≥0, as a complex-valued function on nonnegative time.

Equations

• TauCeti.laplaceAtom p t = ↑(Real.exp (-↑t * ↑p))

@[simp]

theorem TauCeti.laplaceAtom_def (p t : NNReal) : laplaceAtom p t = ↑(Real.exp (-↑t * ↑p))

The definitional exponential form of a Laplace atom.

theorem TauCeti.laplaceAtom_comm (p t : NNReal) : laplaceAtom p t = laplaceAtom t p

The Laplace atom is symmetric in its two nonnegative arguments: the frequency and the time enter exp (-t p) in the same way.

theorem TauCeti.laplaceAtom_add (p t u : NNReal) : laplaceAtom p (t + u) = (starRingEnd ℂ) (laplaceAtom p t) * laplaceAtom p u

Laplace atoms turn time addition into a rank-one positive-definite kernel.

theorem TauCeti.posSemidef_laplaceAtom (p : NNReal) : Matrix.PosSemidef fun (t u : NNReal) => laplaceAtom p (t + u)

The time kernel supplied by a Laplace atom is positive definite.

theorem TauCeti.continuous_laplaceAtom (p : NNReal) : Continuous (laplaceAtom p)

Laplace atoms are continuous in the nonnegative time variable.

theorem TauCeti.isSemigroupGroupPD_laplaceFourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (p : NNReal) (q : V) : IsSemigroupGroupPD fun (x : NNReal × V) => laplaceAtom p x.1 * fourierAtom q x.2

The separated Laplace--Fourier atom is semigroup-group positive definite.

theorem TauCeti.isSemigroupGroupPD_laplaceFourierAtom_and_continuous {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (p : NNReal) (q : V) : (IsSemigroupGroupPD fun (x : NNReal × V) => laplaceAtom p x.1 * fourierAtom q x.2) ∧ Continuous fun (x : NNReal × V) => laplaceAtom p x.1 * fourierAtom q x.2

The separated Laplace--Fourier atom is semigroup-group positive definite and continuous.