OAI/NumberTheory/Ostmann/Characters/NormalizedResidueIndicator.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's normalized residue indicators and additive transforms

  1. def OAI.Ostmann.residueDensity line 12
  2. def OAI.Ostmann.residueVariance line 14
  3. def OAI.Ostmann.normalizedResidueIndicator line 17
  4. def OAI.Ostmann.normalizedResidueTransform line 20
  5. theorem OAI.Ostmann.residueVariance_pos line 23
  6. theorem OAI.Ostmann.centeredDensity_sq_sum line 30
  7. theorem OAI.Ostmann.normalizedResidueIndicator_sum line 48
  8. theorem OAI.Ostmann.normalizedResidueIndicator_energy line 53
  9. theorem OAI.Ostmann.normalizedResidueTransform_zero line 61
  10. theorem OAI.Ostmann.normalizedResidueTransform_energy line 66
  11. theorem OAI.Ostmann.normalizedResidueTransform_neg line 71
  12. theorem OAI.Ostmann.normalizedResidueIndicator_norm_le_three line 83

    Source documentation

    On the balanced supports used in the construction, the physical function has a fixed pointwise bound.

    theorem normalizedResidueIndicator_norm_le_three {p : ℕ} [NeZero p]
    (S : Finset (ZMod p)) (hlo : (1 / 3 : ℝ) ≤ residueDensity S)
    (hhi : residueDensity S ≤ 2 / 3) (x : ZMod p) :
    ‖normalizedResidueIndicator S x‖ ≤ 3 := by
…

    Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueIndicator