OAI/NumberTheory/JointDickman/Counting/ShortLengthComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Varying the short length on a fixed interval of origins

  1. lemma OAI.JointDickman.norm_short_sum_le line 9
  2. lemma OAI.JointDickman.norm_short_sum_length_difference line 18
  3. lemma OAI.JointDickman.norm_shortAverage_le_two line 36
  4. theorem OAI.JointDickman.shortAverage_length_difference line 44

    Source documentation

    Nearby lengths have uniformly close normalized averages.

    theorem shortAverage_length_difference (f : ArithmeticFunction ℂ) (hf : ∀ n, ‖f n‖ ≤ 1)
    {x H K : ℝ} (hx : 0 ≤ x) (hH : 1 ≤ H) (hHK : H ≤ K) :
    ‖complexShortAverage f H x - complexShortAverage f K x‖ ≤
      3 * (K - H + 1) / H := by
…