The zero-spatial Berg--Christensen--Ressel theorem

When the spatial inner-product space in the Berg--Christensen--Ressel representation is the zero space PUnit, its Laplace--Fourier transform has no Fourier factor and is just a Laplace transform. This file makes that specialization precise at both the measure and theorem levels.

The measurable equivalence ℝ≥0 × PUnit ≃ᵐ ℝ≥0 identifies finite representing measures. Under this equivalence, TauCeti.RepresentsLaplaceFourier for the function (t, _) ↦ f t is exactly TauCeti.RepresentsLaplace for f. Consequently the bounded, continuous positive-definite condition in the BCR theorem is equivalent to complete monotonicity on the closed half-line. Thus the zero-spatial case of BCR is precisely the Hausdorff--Bernstein--Widder theorem, including uniqueness of the representing measure.

Main declarations

• TauCeti.laplaceFourierTransform_map_prodPUnit_symm: transporting a measure from ℝ≥0 to ℝ≥0 × PUnit turns its Laplace--Fourier transform into its Laplace transform.
• TauCeti.representsLaplaceFourier_map_prodPUnit_symm_iff: the corresponding equivalence of representation predicates.
• TauCeti.bcr_zero_spatial_iff_hausdorff_bernstein_widder: the BCR hypotheses with zero spatial variable are equivalent to complete monotonicity.
• TauCeti.eq_map_prodPUnit_symm_bernsteinMeasure: the unique BCR representing measure in the zero-spatial case is the transported Bernstein measure.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Theorem 4.1.13.
• D. V. Widder, The Laplace Transform, Chapter IV.

@[simp]

theorem TauCeti.laplaceFourierTransform_map_prodPUnit_symm (μ : MeasureTheory.Measure NNReal) (t : NNReal) (u : PUnit.{1}) : laplaceFourierTransform (MeasureTheory.Measure.map (⇑MeasurableEquiv.prodPUnit.symm) μ) (t, u) = ↑(laplaceTransform μ ↑t)

The Laplace--Fourier transform of a measure transported to ℝ≥0 × PUnit is its ordinary Laplace transform, viewed in ℂ.

theorem TauCeti.representsLaplaceFourier_map_prodPUnit_symm_iff (μ : MeasureTheory.Measure NNReal) (f : ℝ → ℝ) : (RepresentsLaplaceFourier (MeasureTheory.Measure.map (⇑MeasurableEquiv.prodPUnit.symm) μ) fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)) ↔ RepresentsLaplace μ f

In zero spatial dimension, Laplace--Fourier representation of (t, _) ↦ f t by the transported measure is exactly ordinary Laplace representation of f.

@[simp]

theorem TauCeti.representsLaplaceFourier_zero_spatial_iff (μ : MeasureTheory.Measure (NNReal × PUnit.{1})) (f : ℝ → ℝ) : (RepresentsLaplaceFourier μ fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)) ↔ RepresentsLaplace (MeasureTheory.Measure.map (⇑MeasurableEquiv.prodPUnit) μ) f

A measure on ℝ≥0 × PUnit represents a zero-spatial function if and only if its time marginal gives the corresponding Laplace representation.

theorem TauCeti.bcr_zero_spatial_iff_hausdorff_bernstein_widder (f : ℝ → ℝ) : (IsSemigroupGroupPD fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)) ∧ (Continuous fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)) ∧ Bornology.IsBounded (Set.range fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)) ↔ IsContinuousCompletelyMonotoneOnIoi f

The zero-spatial BCR theorem is the Hausdorff--Bernstein--Widder theorem.

For a real function f, the bounded, continuous positive-definite condition on (t, _) ↦ f t : ℝ≥0 × PUnit → ℂ holds exactly when f is continuous on [0, ∞) and completely monotone on (0, ∞).

theorem TauCeti.representsLaplaceFourier_map_prodPUnit_symm_bernsteinMeasure {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : RepresentsLaplaceFourier (MeasureTheory.Measure.map (⇑MeasurableEquiv.prodPUnit.symm) (bernsteinMeasure f)) fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)

In zero spatial dimension, the transported Bernstein measure represents a function that is continuous on [0, ∞) and completely monotone on (0, ∞).

theorem TauCeti.eq_map_prodPUnit_symm_bernsteinMeasure {f : ℝ → ℝ} (μ : MeasureTheory.Measure (NNReal × PUnit.{1})) (hμ : RepresentsLaplaceFourier μ fun (x : NNReal × PUnit.{1}) => ↑(f ↑x.1)) : μ = MeasureTheory.Measure.map (⇑MeasurableEquiv.prodPUnit.symm) (bernsteinMeasure f)

Any zero-spatial BCR representing measure is the transported Bernstein measure.