Evaluation of Pontryagin characters

Evaluation at a fixed monoid element is continuous on the Pontryagin dual. Its complex-valued form is integrable against every finite measure. These lemmas supply the integrands for Fourier–Stieltjes transforms, and apply to arbitrary monoids with a topology.

theorem TauCeti.PontryaginDual.continuous_coe_eval_const {G : Type u_1} [Monoid G] [TopologicalSpace G] (g : G) : Continuous fun (χ : PontryaginDual G) => ↑(χ g)

Complex-valued evaluation of a Pontryagin character at a fixed monoid element is continuous.

theorem TauCeti.PontryaginDual.integrable_coe_eval {G : Type u_1} [Monoid G] [TopologicalSpace G] [MeasurableSpace (PontryaginDual G)] [OpensMeasurableSpace (PontryaginDual G)] {μ : MeasureTheory.Measure (PontryaginDual G)} [MeasureTheory.IsFiniteMeasure μ] (g : G) : MeasureTheory.Integrable (fun (χ : PontryaginDual G) => ↑(χ g)) μ

Complex-valued evaluation of a Pontryagin character is integrable against a finite measure.