Positive-definite transforms of measures on a Pontryagin dual

Integration of characters against a finite positive measure gives a positive-definite function on an additive topological group. This is the positivity part of the measure-to-function direction of Bochner representation on locally compact abelian groups.

theorem MeasureTheory.FiniteMeasure.isPositiveDefiniteSub_pontryaginMeasureTransform {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [OpensMeasurableSpace (PontryaginDual (Multiplicative G))] (μ : FiniteMeasure (PontryaginDual (Multiplicative G))) : TauCeti.IsPositiveDefiniteSub μ.pontryaginMeasureTransform

The transform of a finite positive measure on the dual is positive definite.

theorem MeasureTheory.FiniteMeasure.norm_pontryaginMeasureTransform_le {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [OpensMeasurableSpace (PontryaginDual (Multiplicative G))] (μ : FiniteMeasure (PontryaginDual (Multiplicative G))) (g : G) : ‖μ.pontryaginMeasureTransform g‖ ≤ (↑μ).real Set.univ

The absolute value of a measure transform is bounded by the measure's total mass.