Documentation

TauCeti.Analysis.Fourier.Pontryagin.Measure

Fourier–Stieltjes transform of measures on a Pontryagin dual #

Integrating character evaluations against a finite positive measure on the Pontryagin dual defines a complex-valued function on the original additive group. The transform records the measure's mass at the identity and respects addition, scaling, and point masses.

source
noncomputable def MeasureTheory.FiniteMeasure.pontryaginMeasureTransform {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] (μ : FiniteMeasure (PontryaginDual (Multiplicative G))) (g : G) :
ℂ

The Fourier–Stieltjes transform of a finite measure on the Pontryagin dual of an additive group.

Equations
Instances For
    source
    theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_apply {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] (μ : FiniteMeasure (PontryaginDual (Multiplicative G))) (g : G) :
    μ.pontryaginMeasureTransform g = ∫ (χ : PontryaginDual (Multiplicative G)), ↑(χ (Multiplicative.ofAdd g)) ∂↑μ

    The transform evaluated at a group element is the integral of character evaluations.

    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_zero {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] (μ : FiniteMeasure (PontryaginDual (Multiplicative G))) :
    μ.pontryaginMeasureTransform 0 = ↑((↑μ).real Set.univ)

    At the identity, the transform records the total mass of the measure.

    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_zero_measure {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] :
    pontryaginMeasureTransform 0 = 0

    The transform of the zero measure vanishes.

    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_smul {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] (c : NNReal) (μ : FiniteMeasure (PontryaginDual (Multiplicative G))) :
    (c • μ).pontryaginMeasureTransform = c • μ.pontryaginMeasureTransform

    The transform commutes with nonnegative scalar multiplication of finite measures.

    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_add {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [OpensMeasurableSpace (PontryaginDual (Multiplicative G))] (μ ν : FiniteMeasure (PontryaginDual (Multiplicative G))) :
    (μ + ν).pontryaginMeasureTransform = μ.pontryaginMeasureTransform + ν.pontryaginMeasureTransform

    The transform commutes with addition of finite measures.

    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_dirac {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [OpensMeasurableSpace (PontryaginDual (Multiplicative G))] (χ : PontryaginDual (Multiplicative G)) (g : G) :
    pontryaginMeasureTransform ⟨Measure.dirac χ, ⋯⟩ g = ↑(χ (Multiplicative.ofAdd g))

    The transform of a point mass is its character.