Pontryagin characters are positive-definite atoms #
A continuous character of a topological abelian group becomes a continuous function on the
additive group after transporting G to Multiplicative G. This file proves that every such
character is a continuous subtraction-positive-definite function. The character-level fact is
an atomic input for Fourier analysis on locally compact abelian groups; it does not assert a
measure-representation or Pontryagin-duality theorem.
Main declarations #
PontryaginDual.isPositiveDefiniteSub: a continuous Pontryagin character is a continuous positive-definite function in the additive subtraction form.
theorem
PontryaginDual.isPositiveDefiniteSub
{G : Type u_1}
[AddCommGroup G]
[TopologicalSpace G]
(χ : PontryaginDual (Multiplicative G))
:
(Continuous fun (g : G) => ↑(χ (Multiplicative.ofAdd g))) ∧ TauCeti.IsPositiveDefiniteSub fun (g : G) => ↑(χ (Multiplicative.ofAdd g))
Precomposing a Pontryagin character with Multiplicative.ofAdd gives a continuous function in
subtraction-positive-definite form.