UniformMellin.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The uniform Mellin estimate

The positive-difference form of equation src42 follows by combining Mellin Parseval on the diagonal with the reciprocal affine bound.

def OAI.Ostmann.pairAutocorrelation line 19
theorem OAI.Ostmann.mellinDiagonalCoefficient_eq_fourier line 24
theorem OAI.Ostmann.bottomPair_diagonal_norm_bound line 45

theorem OAI.Ostmann.uniform_mellin_bound line 83

Source documentation

Equation src42 with the positive difference convention.

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

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

theorem OAI.Ostmann.uniform_mellin_bound_of_fourier_bound line 95

Source documentation

The mixed Fourier hypothesis gives the paper's explicit epsilon bound.

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

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