OAI/NumberTheory/JointDickman/Analysis/SquarefreeCharacterDischarge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Discharge of the squarefree character estimate

For the two exponents used in the manuscript, uniform logarithmic cancellation follows from the classical Siegel bound, the character Euler product, a regular Perron contour, and bounded-coefficient unsmoothing.

  1. theorem OAI.JointDickman.squarefreeCharacterSum_norm_le_cutoff line 14
  2. theorem OAI.JointDickman.squarefreeCharacterSum_all_cutoffs line 25
  3. theorem OAI.JointDickman.squarefreeCharacterEstimateInput line 58

    Source documentation

    Uniform logarithmic cancellation for squarefree character sums.

    theorem squarefreeCharacterEstimateInput : PublishedInputs.SquarefreeCharacterEstimateInput := by
…

    Mentions: OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput