OAI/NumberTheory/Ostmann/Preliminaries/OrientedAutocorrelation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Unit changes of the bottom-pair difference

Multiplying the difference by a unit is equivalent to composing the test with that multiplication. Thus the uniform Mellin estimate applies to both difference orientations with its original constant.

  1. theorem OAI.Ostmann.additiveAutocorrelation_const_mul line 20
  2. theorem OAI.Ostmann.additiveAutocorrelation_unit_mul line 33
  3. theorem OAI.Ostmann.characterTwist_unit_mul line 46
  4. theorem OAI.Ostmann.pairAutocorrelation_unit_mul line 58
  5. theorem OAI.Ostmann.uniform_mellin_bound_scaled line 70

    Source documentation

    The uniform estimate for either sign of the bottom-pair difference.

    theorem uniform_mellin_bound_scaled {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (hg : g 0 = 0)
    (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
    (ε : ℝ) (hε : MixedFourierBound g ε)
    (u : (ZMod p)ˣ) (η : MulChar (ZMod p) ℂ) (a : ZMod p) :
    (∑ χ : MulChar (ZMod p) ℂ,
      ‖additiveFourier (fun d => pairAutocorrelation g χ ((u : ZMod p) * d) * χ d * η d) a‖ ^ 2) ≤
      ((p : ℝ) / ((p : ℝ) - 1)) * (ε ^ 4 + Real.sqrt (3 / (p : ℝ))) := by
…

    Mentions: OAI.Ostmann.MixedFourierBound, OAI.Ostmann.additiveFourier, OAI.Ostmann.pairAutocorrelation