The spatial Bochner measures 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. Freezing the time variable leaves the continuous positive-definite function F (t, ·) on V, so Bochner's theorem produces a finite measure bochnerMeasure (F (t, ·)) on V. The Berg--Christensen--Ressel representation F (t, a) = ∫ (p, q), exp (-t p) * exp (-2πi⟪a, q⟫) ∂μ prescribes exactly these measures as the spatial slices of μ (TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq), so the existence half of the representation is the problem of realizing the family t ↦ bochnerMeasure (F (t, ·)) as the Laplace-weighted slices of a single measure on ℝ≥0 × V.

This file develops the time regularity of that family, which is what a Bernstein-type argument consumes. The input is the alternating time-difference positivity of Time/Difference.lean: for every step h, the function (t, v) ↦ F (t, v) - F (t + h, v) is again bounded, continuous and positive definite. Bochner's theorem is additive, so the Bochner measure of a time slice splits as the Bochner measure of that difference plus the Bochner measure of the translated slice. Three consequences follow.

• The family decreases in time, so each slab mass t ↦ (bochnerMeasure (F (t, ·))).real B is antitone and bounded by (F (0, 0)).re.
• Each slab mass is continuous: a decrease of the mass of B between two times is dominated by the decrease of the total mass, which is the continuous function t ↦ (F (t, 0)).re.
• Every mixed alternating difference of a slab mass is nonnegative, since it is again the mass of B under the Bochner measure of the corresponding list time difference of F.

Together the last two say that each slab mass is a bounded continuous function on [0,∞) all of whose alternating finite differences have the sign (-1)ⁿ, the hypothesis of the Hausdorff--Bernstein--Widder theorem in its difference form. The reverse reading is already available for a function that is represented (TauCeti.RepresentsLaplaceFourier.representsLaplace_bochnerMeasure).

Main declarations

• TauCeti.bochnerMeasure_timeSlice_eq_add: the Bochner measure of a time slice splits as the Bochner measure of a time difference plus the Bochner measure of the translated slice.
• TauCeti.bochnerMeasure_timeSlice_antitone and TauCeti.bochnerMeasure_timeSlice_real_antitone: the family of Bochner measures, and each of its slab masses, decrease in time.
• TauCeti.bochnerMeasure_timeSlice_absolutelyContinuous and TauCeti.withDensity_rnDeriv_bochnerMeasure_timeSlice: consequently every member of the family is absolutely continuous with respect to the one at time 0, and is recovered from it by a Radon--Nikodym derivative.
• TauCeti.bochnerMeasure_timeSlice_real_univ, TauCeti.bochnerMeasure_timeSlice_real_le and TauCeti.isBounded_range_bochnerMeasure_timeSlice_real: the total mass is (F (t, 0)).re, and every slab mass is bounded by (F (0, 0)).re, hence has bounded range.
• TauCeti.sub_bochnerMeasure_timeSlice_real_le_sub_timeAxis_re and TauCeti.continuous_bochnerMeasure_timeSlice_real: a slab mass drops by at most the drop of the total mass, so it is a continuous function of the time.
• TauCeti.bochnerMeasure_timeSlice_real_listTimeDifference: every mixed forward difference of a slab mass is the mass of the corresponding list time difference of F, up to its alternating sign.
• TauCeti.isDifferenceCompletelyMonotone_bochnerMeasure_timeSlice_real: after extending time from ℝ≥0 to ℝ by Real.toNNReal, every slab mass is completely monotone in the finite-difference sense.

References

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

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

theorem TauCeti.bochnerMeasure_timeSlice_eq_add {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 h : NNReal) : (bochnerMeasure fun (a : V) => F (t, a)) = (bochnerMeasure fun (a : V) => timeDifference h F (t, a)) + bochnerMeasure fun (a : V) => F (t + h, a)

Splitting a time slice along a time difference. For a bounded continuous Berg--Christensen--Ressel positive-definite function F, the Bochner measure of the slice at time t is the Bochner measure of the slice of the time difference F (·, ·) - F (· + h, ·) plus the Bochner measure of the slice at time t + h. This is Bochner additivity applied to the decomposition F (t, a) = (F (t, a) - F (t + h, a)) + F (t + h, a), both summands being continuous positive-definite functions on V.

theorem TauCeti.bochnerMeasure_timeSlice_antitone {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)) : Antitone fun (t : NNReal) => bochnerMeasure fun (a : V) => F (t, a)

The Bochner measures of the time slices decrease in time. Each step forward in time removes the Bochner measure of the corresponding time difference, which is a measure.

theorem TauCeti.bochnerMeasure_timeSlice_real_antitone {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)) (B : Set V) : Antitone fun (t : NNReal) => (bochnerMeasure fun (a : V) => F (t, a)).real B

The mass a fixed measurable set receives from the Bochner measures of the time slices decreases in time.

theorem TauCeti.bochnerMeasure_timeSlice_absolutelyContinuous {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) : (bochnerMeasure fun (a : V) => F (t, a)).AbsolutelyContinuous (bochnerMeasure fun (a : V) => F (0, a))

The spatial Bochner measures are absolutely continuous with respect to the one at time 0. They decrease in time, and the time-0 measure dominates them all.

theorem TauCeti.withDensity_rnDeriv_bochnerMeasure_timeSlice {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) : (bochnerMeasure fun (a : V) => F (0, a)).withDensity ((bochnerMeasure fun (a : V) => F (t, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a))) = bochnerMeasure fun (a : V) => F (t, a)

The spatial Bochner measure at time t is the time-0 one weighted by a Radon--Nikodym derivative. These derivatives are the densities that the existence half of the Berg--Christensen--Ressel representation must realize.

theorem TauCeti.bochnerMeasure_timeSlice_real_univ {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (t : NNReal) : (bochnerMeasure fun (a : V) => F (t, a)).real Set.univ = (F (t, 0)).re

The total mass of the Bochner measure of the time slice at t is (F (t, 0)).re.

theorem TauCeti.bochnerMeasure_timeSlice_real_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)) (B : Set V) (t : NNReal) : (bochnerMeasure fun (a : V) => F (t, a)).real B ≤ (F (0, 0)).re

Every slab mass of the family of Bochner measures is bounded by (F (0, 0)).re.

theorem TauCeti.isBounded_range_bochnerMeasure_timeSlice_real {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)) (B : Set V) : Bornology.IsBounded (Set.range fun (t : NNReal) => (bochnerMeasure fun (a : V) => F (t, a)).real B)

The slab masses form a bounded family. Every value of the slab mass lies in the interval [0, (F (0, 0)).re], so its range is bounded; this is the boundedness hypothesis of the Hausdorff--Bernstein--Widder theorem.

theorem TauCeti.sub_bochnerMeasure_timeSlice_real_le_sub_timeAxis_re {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)) {B : Set V} (hB : MeasurableSet B) {t s : NNReal} (hts : t ≤ s) : (bochnerMeasure fun (a : V) => F (t, a)).real B - (bochnerMeasure fun (a : V) => F (s, a)).real B ≤ (F (t, 0)).re - (F (s, 0)).re

The slab masses lose no more than the total mass. Between two times the mass of a measurable set B drops by at most the drop of the total mass, because the mass of Bᶜ also drops.

theorem TauCeti.continuous_bochnerMeasure_timeSlice_real {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)) {B : Set V} (hB : MeasurableSet B) : Continuous fun (t : NNReal) => (bochnerMeasure fun (a : V) => F (t, a)).real B

The slab masses are continuous in time. The variation of the mass of B is dominated by the variation of the total mass t ↦ (F (t, 0)).re, which is continuous because F is.

theorem TauCeti.bochnerMeasure_timeSlice_real_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)) (B : Set V) (l : List NNReal) (t : NNReal) : (bochnerMeasure fun (a : V) => listTimeDifference l F (t, a)).real B = (-1) ^ l.length * fwdDiffList l (fun (s : NNReal) => (bochnerMeasure fun (a : V) => F (s, a)).real B) t

Mixed forward differences of a slab mass are slab masses. The mixed forward difference along l of t ↦ (bochnerMeasure (F (t, ·))).real B, corrected by the sign (-1)^|l|, is the mass of B under the Bochner measure of the corresponding list time difference of F.

theorem TauCeti.isDifferenceCompletelyMonotone_bochnerMeasure_timeSlice_real {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)) (B : Set V) : IsDifferenceCompletelyMonotone fun (t : ℝ) => (bochnerMeasure fun (a : V) => F (t.toNNReal, a)).real B

Spatial Bochner slice masses are completely monotone in the finite-difference sense. After extending the time parameter from ℝ≥0 to ℝ by Real.toNNReal, every slab mass has nonnegative alternating mixed forward differences on [0, ∞).