OAI/NumberTheory/JointDickman/Probability/RamanujanResidueFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact residue factor in the small-major-arc kernel

  1. theorem OAI.JointDickman.ramanujanSum_crt line 11
  2. theorem OAI.JointDickman.ramanujanSum_parseval line 25
  3. theorem OAI.JointDickman.ramanujanSum_coprime_norm line 30
  4. theorem OAI.JointDickman.coprime_residue_count line 35
  5. theorem OAI.JointDickman.crt_coprime_frequency line 47
  6. theorem OAI.JointDickman.ramanujan_restricted_parseval line 60

    Source documentation

    Unnormalized version of manuscript (40).

    theorem ramanujan_restricted_parseval {j q : ℕ} [NeZero j] [NeZero q]
    [NeZero (j*q)] (hcop : j.Coprime q) (hq : Squarefree q) :
    (∑ h : ZMod (j*q), if h.val.Coprime q then ‖ramanujanSum (j*q) h‖^2 else 0) =
      (j : ℝ)*j.totient*q.totient := by
…

    Mentions: OAI.JointDickman.ramanujanSum

  7. theorem OAI.JointDickman.ramanujan_residue_factor line 84

    Source documentation

    The exact normalized frequency factor, including the vanishing non-coprime case.

    theorem ramanujan_residue_factor {j q : ℕ} [NeZero j] [NeZero q] [NeZero (j*q)]
    (hq : Squarefree q) :
    (∑ h : ZMod (j*q), if h.val.Coprime q then
      ‖ramanujanSum (j*q) h‖^2 / ((j*q).totient : ℝ)^2 else 0) =
      if j.Coprime q then (j : ℝ)/(j.totient*q.totient) else 0 := by
…

    Mentions: OAI.JointDickman.ramanujanSum