Finite Poisson Summation

Abstract

Finite Poisson summation on an arbitrary additive subgroup of a positive cyclic group.

Theorem 1.1 (Finite Poisson summation on a cyclic subgroup).

$$\forall x2\in \mathrm{AddSubgroup}\left(\mathrm{ZMod}\left(\cdot \right)\right),\forall x3\in \left(\forall x3\in \mathrm{ZMod}\left(\cdot \right),\mathrm{Complex}\right),\mathrm{sum}\left(\mathrm{univ},\forall x4\in \mathrm{Type},x3\left(\mathrm{val}\left(x4\right)\right)\right)=\mathrm{divide}\left(\mathrm{cast}\left(\mathrm{card}\left(\mathrm{Subtype}\left(\mathrm{ZMod}\left(\cdot \right),\forall x4\in \mathrm{Type},x2\in x4\right)\right)\right),\mathrm{cast}\left(\cdot \right)\right)\cdot \mathrm{sum}\left(\mathrm{univ},\forall x4\in \mathrm{Type},x3\left(\mathrm{val}\left(x4\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Fourier/FinitePoisson.finite_poisson_summation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The annihilator is defined explicitly by triviality of the standard character on H. Its identification with the complete character group of the quotient supplies both character orthogonality and the cardinal identity |H||H-perp| = m. Expanding the pinned ZMod discrete Fourier transform and exchanging the two finite sums then yields the stated normalization without assuming either identity.

Theorem 1.2 (The even subgroup has an explicit Poisson witness).

$$H=\{0,2\},f(x)=1_{x=0}\Rightarrow \sum _{h\in H}f(h)=1=\frac{|H|}{4}\sum _{k\in H^{\perp }}\hat{f}(k).$$

Proof. Machine-checked in Lean as D5/S3/Fourier/FinitePoisson.finite_poisson_mod_four_even_delta (✓ std3). ∎

Source. Repository-derived.

Commentary.

Kernel-reduced membership checks prove that 2 belongs to H while 1 does not. The branch witnesses then prove 2 belongs to the annihilator and 1 does not; character orthogonality evaluates to 2 at x = 2 and to 0 at x = 1. For the delta function at zero, both sides of Poisson summation reduce to the explicit value 1.

References

• Truth anchor: D5/S3/Fourier/FinitePoisson.finite_poisson_mod_four_even_delta
• Truth anchor: D5/S3/Fourier/FinitePoisson.finite_poisson_summation