OAI/NumberTheory/Ostmann/Quadratic/QuadraticResidueDecomposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact residue-class splitting before the inverse quadratic estimate

  1. theorem OAI.Ostmann.stdAddChar_nat_ratio line 12
  2. theorem OAI.Ostmann.quadratic_phase_integer_part line 20
  3. def OAI.Ostmann.quadraticResidueAmplitude line 33
  4. def OAI.Ostmann.quadraticResidueWave line 37
  5. theorem OAI.Ostmann.quadraticDensityTerm_residue_factor line 42
  6. theorem OAI.Ostmann.quadraticResidueAmplitude_norm line 51
  7. theorem OAI.Ostmann.sum_by_zmod_residues line 56
  8. theorem OAI.Ostmann.quadraticDensitySum_residue_decomposition line 65