The fibrewise spatial densities of a Berg--Christensen--Ressel positive-definite function

Let F be a bounded continuous positive-definite function on the involutive semigroup ℝ≥0 × V, with V a finite-dimensional real inner-product space. Its spatial Bochner measures bochnerMeasure (F (t, ·)) decrease in time, so each of them has a Radon--Nikodym derivative against the one at time 0 (TauCeti.withDensity_rnDeriv_bochnerMeasure_timeSlice). The existence half of the Berg--Christensen--Ressel representation is exactly the problem of realizing that family of densities as a family of fibrewise Laplace transforms (TauCeti.exists_representsLaplaceFourier_iff_exists_timeKernel), which is a Bernstein problem in the time variable at almost every spatial frequency.

This file supplies the input of that Bernstein problem. Two obstacles have to be cleared.

• A Radon--Nikodym derivative is defined only up to a null set, so the alternating time differences of the densities can only be controlled at countably many times at once, whereas complete monotonicity quantifies over all real times. The countable version is TauCeti.toReal_rnDeriv_bochnerMeasure_timeSlice_listTimeDifference: the density of the Bochner measure of a list time difference of F is, almost everywhere, the corresponding mixed forward difference of the densities, and it is nonnegative because it is a density.
• The version of the density that is used must be right-continuous in time, since TauCeti.isDifferenceCompletelyMonotone_of_forall_rat upgrades rational data to real data only for a right-continuous function. TauCeti.timeSliceDensity is that version: the supremum of the Radon--Nikodym derivatives over rational times r > t. Being a supremum over a shrinking family of rational times it is antitone and right-continuous for every spatial frequency, with no null set attached, and it agrees almost everywhere with the Radon--Nikodym derivative at each fixed time (TauCeti.timeSliceDensity_ae_eq_rnDeriv) because the total masses are continuous in time.

The conclusion is TauCeti.ae_isContinuousCompletelyMonotoneOnIoi_timeSliceDensity: almost every fibre of TauCeti.timeSliceDensity is a completely monotone function of time, hence a Laplace transform.

Main declarations

• TauCeti.bochnerMeasure_timeSlice_listTimeDifference_le: the Bochner measure of a list time difference is dominated by the Bochner measure of the time slice it differences.
• TauCeti.toReal_rnDeriv_bochnerMeasure_timeSlice_listTimeDifference: mixed forward differences of the densities are themselves densities, almost everywhere.
• TauCeti.timeSliceDensity: the right-continuous version of the family of densities.
• TauCeti.timeSliceDensity_ae_eq_rnDeriv: it is a Radon--Nikodym derivative at every fixed time.
• TauCeti.ae_isDifferenceCompletelyMonotone_timeSliceDensity and TauCeti.ae_isContinuousCompletelyMonotoneOnIoi_timeSliceDensity: almost every fibre is completely monotone in time.
• TauCeti.ae_timeSliceDensity_zero_eq_one: almost every fibre is normalized at time 0.

References

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

Time differences of the spatial Bochner measures

theorem TauCeti.bochnerMeasure_timeSlice_listTimeDifference_le {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) (l : List NNReal) (t : NNReal) : (bochnerMeasure fun (a : V) => listTimeDifference l F (t, a)) ≤ bochnerMeasure fun (a : V) => F (t, a)

A list time difference has a smaller Bochner measure than the slice it differences. Each further first difference splits the Bochner measure of the previous one into two summands (TauCeti.bochnerMeasure_timeSlice_eq_add), and a summand of measures is dominated by their sum.

theorem TauCeti.rnDeriv_bochnerMeasure_timeSlice_ae_le {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) {t s : NNReal} (hts : t ≤ s) : (bochnerMeasure fun (a : V) => F (s, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a)) ≤ᵐ[bochnerMeasure fun (a : V) => F (0, a)] (bochnerMeasure fun (a : V) => F (t, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a))

The densities decrease in time, almost everywhere against the time-0 Bochner measure: the earlier spatial measure is the later one plus the Bochner measure of the time difference between them.

theorem TauCeti.toReal_rnDeriv_bochnerMeasure_timeSlice_listTimeDifference {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) (l : List NNReal) (t : NNReal) : ∀ᵐ (q : V) ∂bochnerMeasure fun (a : V) => F (0, a), ((bochnerMeasure fun (a : V) => listTimeDifference l F (t, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a)) q).toReal = (-1) ^ l.length * fwdDiffList (List.map (fun (h : NNReal) => ↑h) l) (fun (s : ℝ) => ((bochnerMeasure fun (a : V) => F (s.toNNReal, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a)) q).toReal) ↑t

Mixed forward differences of the densities are densities. The Radon--Nikodym derivative of the Bochner measure of a list time difference of F is, almost everywhere, the corresponding mixed forward difference of the Radon--Nikodym derivatives of the time slices. Since the left-hand side is a density it is nonnegative, which is the sign condition of the Hausdorff--Bernstein--Widder theorem at the times involved.

The right-continuous version of the densities

noncomputable def TauCeti.timeSliceDensity {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) (t : NNReal) (q : V) : ENNReal

The right-continuous spatial density of a function on ℝ≥0 × V at time t: the supremum, over rational times r > t, of the Radon--Nikodym derivative of the spatial Bochner measure at time r against the one at time 0.

Taking the supremum over rational times to the right of t costs nothing at a fixed time — the family of Radon--Nikodym derivatives decreases in time and the total masses are continuous, so TauCeti.timeSliceDensity_ae_eq_rnDeriv identifies this with the Radon--Nikodym derivative itself — while it buys antitonicity and right-continuity in time at every point of V, with no null set attached. That is what makes a fibrewise Bernstein argument possible.

Equations

• TauCeti.timeSliceDensity F t q = ⨆ (r : { r : ℚ≥0 // t < ↑r }), (TauCeti.bochnerMeasure fun (a : V) => F (↑↑r, a)).rnDeriv (TauCeti.bochnerMeasure fun (a : V) => F (0, a)) q

theorem TauCeti.rnDeriv_le_timeSliceDensity {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) {t : NNReal} {r : ℚ≥0} (hr : t < ↑r) (q : V) : (bochnerMeasure fun (a : V) => F (↑r, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a)) q ≤ timeSliceDensity F t q

Each Radon--Nikodym derivative at a rational time to the right of t is dominated by the right-continuous density at t.

theorem TauCeti.timeSliceDensity_antitone {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) (q : V) : Antitone fun (t : NNReal) => timeSliceDensity F t q

The right-continuous density decreases in time, at every point.

theorem TauCeti.measurable_timeSliceDensity {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) (t : NNReal) : Measurable (timeSliceDensity F t)

theorem TauCeti.timeSliceDensity_le_rnDeriv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) (t : NNReal) : timeSliceDensity F t ≤ᵐ[bochnerMeasure fun (a : V) => F (0, a)] (bochnerMeasure fun (a : V) => F (t, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a))

The right-continuous density is dominated by the Radon--Nikodym derivative at the same time.

theorem TauCeti.timeSliceDensity_ae_eq_rnDeriv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) (t : NNReal) : timeSliceDensity F t =ᵐ[bochnerMeasure fun (a : V) => F (0, a)] (bochnerMeasure fun (a : V) => F (t, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a))

The right-continuous density is a Radon--Nikodym derivative at every fixed time. The supremum over rational times to the right loses no mass, because the total mass t ↦ (F (t, 0)).re is continuous.

theorem TauCeti.ae_timeSliceDensity_zero_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) : ∀ᵐ (q : V) ∂bochnerMeasure fun (a : V) => F (0, a), timeSliceDensity F 0 q = 1

Almost every fibre of the right-continuous density is normalized at time 0.

theorem TauCeti.tendsto_timeSliceDensity_nhdsGT {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) (t : NNReal) (q : V) : Filter.Tendsto (fun (s : NNReal) => timeSliceDensity F s q) (nhdsWithin t (Set.Ioi t)) (nhds (timeSliceDensity F t q))

The right-continuous density is right-continuous in time. No null set is involved: the supremum defining it runs over the rational times to the right of t, so it is both antitone and its own right limit.

theorem TauCeti.tendsto_toReal_timeSliceDensity_nhdsGT {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) {q : V} {u : ℝ} (hq : timeSliceDensity F u.toNNReal q ≠ ⊤) (hu : 0 ≤ u) : Filter.Tendsto (fun (s : ℝ) => (timeSliceDensity F s.toNNReal q).toReal) (nhdsWithin u (Set.Ioi u)) (nhds (timeSliceDensity F u.toNNReal q).toReal)

The real-valued time profile of a fibre, reparametrized by a real time, is right-continuous at every nonnegative time where its value is finite.

Complete monotonicity of the fibres

theorem TauCeti.ae_isDifferenceCompletelyMonotone_timeSliceDensity {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) : ∀ᵐ (q : V) ∂bochnerMeasure fun (a : V) => F (0, a), IsDifferenceCompletelyMonotone fun (s : ℝ) => (timeSliceDensity F s.toNNReal q).toReal

Almost every fibre of the right-continuous density is completely monotone in the finite-difference sense. The mixed forward differences at rational data are densities of the Bochner measures of the corresponding list time differences of F, hence nonnegative; rational data suffice because the fibres are right-continuous (TauCeti.isDifferenceCompletelyMonotone_of_forall_rat).

theorem TauCeti.ae_isContinuousCompletelyMonotoneOnIoi_timeSliceDensity {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) : ∀ᵐ (q : V) ∂bochnerMeasure fun (a : V) => F (0, a), IsContinuousCompletelyMonotoneOnIoi fun (s : ℝ) => (timeSliceDensity F s.toNNReal q).toReal

Almost every fibre of the right-continuous density is a completely monotone function of time. This is the hypothesis of TauCeti.bernsteinMeasureKernel, so almost every fibre carries a Bernstein representing measure on ℝ≥0.