OAI/NumberTheory/JointDickman/Probability/CyclicKernelPartialSums.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Partial sums of nonzero rational frequencies

  1. lemma OAI.JointDickman.cyclicGeometricKernel_zero line 10
  2. theorem OAI.JointDickman.cyclic_kernel_nonzero_partial_bound line 15

    Source documentation

    The nonzero frequencies in any initial segment contribute only O(N(L+q)).

    theorem cyclic_kernel_nonzero_partial_bound {q : ℕ} [NeZero q]
    (N L : ℕ) (u : (ZMod q)ˣ) :
    (∑ n ∈ Icc 1 L, if q ∣ n then 0 else
      cyclicGeometricKernel N ((n:ZMod q)*(u:ZMod q))) ≤
      (N:ℝ)*((L:ℝ)+2*q) := by
…

    Mentions: OAI.JointDickman.cyclicGeometricKernel