OAI/NumberTheory/JointDickman/Probability/RationalGeometricKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The geometric kernel at reduced rational frequencies

  1. lemma OAI.JointDickman.cyclic_kernel_as_real_phase line 10
  2. theorem OAI.JointDickman.rational_geometric_kernel_sum line 26

    Source documentation

    A complete period has only one quadratic peak. All nonzero frequencies together cost O(Nq), and the same estimate controls an arbitrary prefix.

    theorem rational_geometric_kernel_sum {q : ℕ} [NeZero q]
    (N L : ℕ) (u : (ZMod q)ˣ) :
    (∑ h ∈ Icc 1 L, geometricSquareKernel N (((u:ZMod q).val:ℝ)/q*h)) ≤
      (N:ℝ)^2*(L:ℝ)/q + (N:ℝ)*((L:ℝ)+2*q) := by
…

    Mentions: OAI.JointDickman.geometricSquareKernel

  3. lemma OAI.JointDickman.cyclic_kernel_coprime_numerator line 33
  4. theorem OAI.JointDickman.rational_geometric_kernel_sum_coprime line 51