OAI/NumberTheory/CubicMoment/Angular/AngularHeckeFromFourier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete angular analytic package constructed from the finite Gauss Fourier identity and its norm, via the proved harmonic Poisson formula.

  1. lemma OAI.CubicFirstMoment.angularHecke_from_finiteFourier line 11