OAI/NumberTheory/JointDickman/Counting/CyclicGeometricEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.cyclicGeometricKernel line 12
2. lemma OAI.JointDickman.cyclicGeometricKernel_nonneg line 15
3. lemma OAI.JointDickman.cyclic_geometric_pair line 18
4. lemma OAI.JointDickman.cyclicGeometricKernel_complete line 31
5. lemma OAI.JointDickman.cyclicGeometricKernel_mod line 63
6. theorem OAI.JointDickman.cyclicGeometricKernel_nonzero_sum line 76

   Source documentation

   Excluding zero frequency removes the quadratic peak. The total remaining energy is at most qN, uniformly even when N spans many periods.

   theorem cyclicGeometricKernel_nonzero_sum {q : ℕ} [NeZero q] (N : ℕ) :
       (∑ x ∈ (univ : Finset (ZMod q)).erase 0, cyclicGeometricKernel N x) ≤ (q:ℝ)*N := by
   …

   Mentions: OAI.JointDickman.cyclicGeometricKernel