Uniqueness of Fourier--Stieltjes measures on a Pontryagin dual #
On a Polish Pontryagin dual, a finite measure is determined by the integrals of the evaluation characters. Equivalently, the Fourier--Stieltjes transform of a finite measure on the dual is injective. On the dual of an arbitrary locally compact abelian group, where the dual need be neither metrizable nor second countable, the same holds for finite inner regular measures. These are the uniqueness halves of Bochner's theorem for locally compact abelian groups.
The proof packages finite linear combinations of evaluation characters as a star subalgebra of
bounded continuous functions. Evaluation characters separate points of the dual simply because
two continuous homomorphisms that agree at every group element are equal. Mathlib's extension
theorem for finite measures on Polish spaces, or its inner regular counterpart
TauCeti.MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_innerRegular on locally
compact Hausdorff spaces, then promotes equality of the character integrals to equality of the
measures.
The construction of evalMonoidHom, evalAlgHom and evalPoly, together with the proofs that
evalPoly is closed under star and separates points, is adapted from Jakob Stiefel's
charMonoidHom, charAlgHom, charPoly, star_mem_range_charAlgHom and
separatesPoints_charPoly in Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar, which
treats characters of the form v ↦ e (L v w) on a real vector space.
Main declarations #
PontryaginDual.evalBoundedContinuous: evaluation at a group element, bundled as a bounded continuous function on the dual.PontryaginDual.evalPoly: the star subalgebra of finite linear combinations of evaluation characters.MeasureTheory.FiniteMeasure.ext_of_forall_pontryaginMeasureTransform_eq: finite measures on a Polish dual with the same Fourier--Stieltjes transform are equal.MeasureTheory.FiniteMeasure.ext_of_forall_pontryaginMeasureTransform_eq_of_innerRegular: finite inner regular measures on the dual of a locally compact abelian group with the same Fourier--Stieltjes transform are equal.
References #
- W. Rudin, Fourier Analysis on Groups, Chapter 1.
- J. Stiefel,
Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar, Mathlib.
Evaluation at g, as a bounded continuous complex-valued function on the Pontryagin dual.
Its values lie on the unit circle, so its norm is bounded by one.
Equations
- PontryaginDual.evalBoundedContinuous g = BoundedContinuousFunction.ofNormedAddCommGroup (fun (χ : PontryaginDual (Multiplicative G)) => ↑(χ (Multiplicative.ofAdd g))) ⋯ 1 ⋯
Instances For
Evaluation of evalBoundedContinuous at a character.
Evaluation at zero is the constant function one.
Evaluation turns addition in the original group into pointwise multiplication.
Evaluation at the negative of a group element is the pointwise star of evaluation there.
Evaluation as a monoid homomorphism from the multiplicative copy of the original group.
Equations
- PontryaginDual.evalMonoidHom = { toFun := fun (g : Multiplicative G) => PontryaginDual.evalBoundedContinuous (Multiplicative.toAdd g), map_one' := ⋯, map_mul' := ⋯ }
Instances For
Evaluation of evalMonoidHom at a character.
The algebra homomorphism sending a formal finite linear combination of group elements to the corresponding finite linear combination of evaluation characters.
Equations
Instances For
Evaluation of evalAlgHom is the corresponding finite linear combination of characters.
The range of evalAlgHom is closed under pointwise complex conjugation.
The star subalgebra of bounded continuous functions generated by evaluation characters.
Equations
- PontryaginDual.evalPoly = { toSubalgebra := PontryaginDual.evalAlgHom.range, star_mem' := ⋯ }
Instances For
The underlying subalgebra of evalPoly is the range of evalAlgHom.
Membership in evalPoly means being a finite linear combination of evaluation
characters.
Every evaluation character belongs to evalPoly.
The evaluation-character algebra separates points of the Pontryagin dual.
Two finite measures on the dual with the same Fourier--Stieltjes transform integrate every finite linear combination of evaluation characters equally.
Uniqueness of Fourier--Stieltjes measures on a Polish Pontryagin dual. Two finite measures on the dual are equal when their transforms agree on every element of the original group.
The Fourier--Stieltjes transform is injective on finite measures on a Polish Pontryagin dual.
Uniqueness of inner regular Fourier--Stieltjes measures. On the Pontryagin dual of a locally compact abelian group, two finite inner regular measures are equal when their transforms agree on every element of the group. No countability or metrizability is assumed.
The Fourier--Stieltjes transform is injective on finite inner regular measures on the Pontryagin dual of a locally compact abelian group.