OAI/NumberTheory/JointDickman/Analysis/MellinShortComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal weights in a short interval

Replacing the counting weight by x/n costs at most (H+1)/x in a one-bounded short average. This is the elementary bridge to logarithmic windows; the bound is uniform in the coefficients.

  1. def OAI.JointDickman.reciprocalShortAverage line 14
  2. theorem OAI.JointDickman.mellin_short_interval_card_le line 17
  3. theorem OAI.JointDickman.short_average_reciprocal_error line 28

    Source documentation

    The reciprocal-weight normalization has a vanishing error whenever H/x and 1/x tend to zero.

    theorem short_average_reciprocal_error (f : ArithmeticFunction ℂ)
    (hf : ∀ n, ‖f n‖ ≤ 1) {x H : ℝ} (hx : 0 < x) (hH : 0 < H) :
    ‖complexShortAverage f H x - reciprocalShortAverage f H x‖ ≤ (H + 1) / x := by
…

    Mentions: OAI.JointDickman.reciprocalShortAverage