Documentation

TauCeti.Analysis.PositiveDefinite.SemigroupGroup.FourierLaplace.Transform

The Laplace--Fourier transform of a measure on ℝ≥0 × V #

For a finite-dimensional real inner product space V, the Berg--Christensen--Ressel representation writes a bounded continuous positive-definite function on the involutive semigroup ℝ≥0 × V as the Laplace--Fourier transform

F (t, a) = ∫ (p, q), exp (-t p) * exp (-2πi⟪a, q⟫) ∂μ

of a finite measure μ on ℝ≥0 × V. This file defines that transform for an arbitrary V — no finite-dimensionality is needed to write it down — through the atoms of TauCeti.Analysis.PositiveDefinite.SemigroupGroup.FourierLaplace.Basic, and packages the predicate that a finite measure represents a given function this way. It is the material both halves of the representation theorem share: the uniqueness half (TauCeti.Analysis.PositiveDefinite.SemigroupGroup.FourierLaplace.Uniqueness) and the existence half, which consumes Bochner's theorem on V.

Main declarations #

References #

The Laplace--Fourier atoms of a fixed evaluation point #

source
theorem TauCeti.norm_laplaceAtom_mul_fourierAtom_le_one {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] (t p : NNReal) (a q : V) :
‖laplaceAtom t p * fourierAtom a q‖ ≤ 1

The Laplace--Fourier atoms are bounded by 1 in norm: the Laplace factor is at most 1 because both parameters are nonnegative, and the Fourier factor is unimodular.

The Laplace--Fourier transform of a measure #

source
noncomputable def TauCeti.laplaceFourierTransform {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (x : NNReal × V) :
ℂ

The Laplace--Fourier transform of a measure on ℝ≥0 × V, evaluated at a point x = (t, a) of the involutive semigroup ℝ≥0 × V:

(t, a) ↦ ∫ (p, q), exp (-t p) * exp (-2πi⟪a, q⟫) ∂μ.

The integrand is the separated Laplace--Fourier atom of TauCeti.isSemigroupGroupPD_laplaceFourierAtom. Nothing here relates the measurable structure on V to its topology, so the integral need not converge; integrability of the atoms against a finite measure is TauCeti.integrable_laplaceAtom_mul_fourierAtom, which additionally assumes OpensMeasurableSpace V. For a finite-dimensional V, the Berg--Christensen--Ressel theorem asserts that every bounded continuous semigroup-group positive-definite function on ℝ≥0 × V is the transform of a finite measure.

Equations
Instances For
    source
    theorem TauCeti.laplaceFourierTransform_apply {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (x : NNReal × V) :
    laplaceFourierTransform μ x = ∫ (y : NNReal × V), laplaceAtom x.1 y.1 * fourierAtom x.2 y.2 ∂μ

    The defining formula for laplaceFourierTransform. Not @[simp]: simp should not unfold the abstraction into a raw integral.

    source
    theorem TauCeti.laplaceFourierTransform_apply_exp {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) (a : V) :
    laplaceFourierTransform μ (t, a) = ∫ (y : NNReal × V), ↑(Real.exp (-↑t * ↑y.1)) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑(inner ℝ a y.2)) ∂μ

    The Laplace--Fourier transform in the exponential form used by the Berg--Christensen--Ressel statement: the transform at (t, a) integrates exp (-t p) * exp (-2πi⟪a, q⟫).

    source
    theorem TauCeti.integrable_laplaceAtom_mul_fourierAtom {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] (t : NNReal) (a : V) :
    MeasureTheory.Integrable (fun (y : NNReal × V) => laplaceAtom t y.1 * fourierAtom a y.2) μ

    The integrand of the Laplace--Fourier transform is integrable against a finite measure.

    Values and elementary measure operations #

    source
    @[simp]
    theorem TauCeti.laplaceFourierTransform_zero {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) :
    laplaceFourierTransform μ 0 = ↑(μ.real Set.univ)

    The Laplace--Fourier transform at the identity 0 of ℝ≥0 × V is the total mass: both atoms are 1 there.

    source
    @[simp]
    theorem TauCeti.laplaceFourierTransform_zero_measure {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (x : NNReal × V) :
    laplaceFourierTransform 0 x = 0

    The zero measure has zero Laplace--Fourier transform.

    source
    @[simp]
    theorem TauCeti.laplaceFourierTransform_dirac {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (y x : NNReal × V) :
    laplaceFourierTransform (MeasureTheory.Measure.dirac y) x = laplaceAtom x.1 y.1 * fourierAtom x.2 y.2

    The Laplace--Fourier transform of a Dirac mass is the atom at its point.

    source
    @[simp]
    theorem TauCeti.laplaceFourierTransform_add_measure {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (μ ν : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (x : NNReal × V) :
    laplaceFourierTransform (μ + ν) x = laplaceFourierTransform μ x + laplaceFourierTransform ν x

    The Laplace--Fourier transform is additive in the measure.

    source
    @[simp]
    theorem TauCeti.laplaceFourierTransform_smul_measure {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (c : ENNReal) (x : NNReal × V) :
    laplaceFourierTransform (c • μ) x = c.toReal • laplaceFourierTransform μ x

    Scaling the measure scales its Laplace--Fourier transform.

    The representation predicate #

    source
    def TauCeti.RepresentsLaplaceFourier {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (F : NNReal × V → ℂ) :
    Prop

    A finite measure represents a function on ℝ≥0 × V by its Laplace--Fourier transform. This is the representation asserted by the Berg--Christensen--Ressel theorem.

    Equations
    Instances For
      source
      theorem TauCeti.representsLaplaceFourier_iff {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} :
      RepresentsLaplaceFourier μ F ↔ MeasureTheory.IsFiniteMeasure μ ∧ ∀ (x : NNReal × V), F x = laplaceFourierTransform μ x

      RepresentsLaplaceFourier μ F unfolds to finiteness of μ together with the Laplace--Fourier representation of F.

      source
      theorem TauCeti.RepresentsLaplaceFourier.isFiniteMeasure {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) :
      MeasureTheory.IsFiniteMeasure μ

      A representing measure is finite.

      source
      theorem TauCeti.RepresentsLaplaceFourier.eq_laplaceFourierTransform {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) (x : NNReal × V) :
      F x = laplaceFourierTransform μ x

      A representing measure has the advertised Laplace--Fourier transform.

      source
      theorem TauCeti.RepresentsLaplaceFourier.apply_zero {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) :
      F 0 = ↑(μ.real Set.univ)

      The value of a represented function at the identity of ℝ≥0 × V is the total mass of the representing measure. (Not @[simp]: the left-hand side has a variable head symbol.)

      source
      theorem TauCeti.RepresentsLaplaceFourier.add {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} [OpensMeasurableSpace V] {G : NNReal × V → ℂ} {ν : MeasureTheory.Measure (NNReal × V)} (hF : RepresentsLaplaceFourier μ F) (hG : RepresentsLaplaceFourier ν G) :
      RepresentsLaplaceFourier (μ + ν) (F + G)

      The sum of two representing measures represents the sum of the functions.

      source
      theorem TauCeti.RepresentsLaplaceFourier.smul {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (c : NNReal) (hF : RepresentsLaplaceFourier μ F) :
      RepresentsLaplaceFourier (↑c • μ) fun (x : NNReal × V) => ↑c • F x

      Scaling a representing measure by c : ℝ≥0 represents the scaled function.

      source
      theorem TauCeti.representsLaplaceFourier_zero {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] :
      RepresentsLaplaceFourier 0 0

      The zero measure represents the zero function.

      source
      theorem TauCeti.representsLaplaceFourier_dirac {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (y : NNReal × V) :
      RepresentsLaplaceFourier (MeasureTheory.Measure.dirac y) fun (x : NNReal × V) => laplaceAtom x.1 y.1 * fourierAtom x.2 y.2

      The Dirac mass at y represents the Laplace--Fourier atom of y.