OAI/NumberTheory/JointDickman/Analysis/ShortMellinComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform approximation of the original short average on a small block

  1. theorem OAI.JointDickman.shortAverage_le_mellinPacket_of_support line 12

    Source documentation

    The coefficients are restricted to the same fixed block for every location of the short interval; all errors are uniform on that block.

    theorem shortAverage_le_mellinPacket_of_support (f : ArithmeticFunction ℂ)
    (hf : ∀ n, ‖f n‖ ≤ 1) {K N : ℕ} {X H ε η x : ℝ}
    (hX : 0 < X) (hH : 1 ≤ H) (hHX : H ≤ X)
    (hη : 0 < η) (hηhalf : η < 1/2)
    (hx : x ∈ Set.Icc X ((1 + ε) * X))
    (hK : K ≤ ⌊X⌋₊) (hN : ⌊(1 + ε) * (X + H)⌋₊ ≤ N) :
    let δ := Real.log ((X + H) / X)
…
  2. theorem OAI.JointDickman.shortAverage_le_mellinPacket line 65