OAI/NumberTheory/JointDickman/Analysis/MellinLogWindows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.logarithmicWindowAverage line 10
2. theorem OAI.JointDickman.logarithmic_window_width line 14
3. theorem OAI.JointDickman.logarithmicWindowAverage_endpoints line 30

   Source documentation

   The logarithmic interval has exactly the original arithmetic endpoints.

   theorem logarithmicWindowAverage_endpoints (f : ArithmeticFunction ℂ)
       {x H : ℝ} (hx : 0 < x) (hH : 0 < H) :
       logarithmicWindowAverage f (Real.log ((x + H) / x)) (Real.log x) =
         (∑ n ∈ Ioc ⌊x⌋₊ ⌊x + H⌋₊, f n / (n : ℂ)) /
           (Real.log ((x + H) / x) : ℂ) := by
   …

   Mentions: OAI.JointDickman.logarithmicWindowAverage

4. theorem OAI.JointDickman.reciprocalShortAverage_eq_logarithmic line 43

   Source documentation

   Before normalization, the reciprocal short average is the exact logarithmic-window sum, with no endpoint error.

   theorem reciprocalShortAverage_eq_logarithmic (f : ArithmeticFunction ℂ)
       {x H : ℝ} (hx : 0 < x) (hH : 0 < H) :
       reciprocalShortAverage f H x =
         ((x * Real.log ((x + H) / x) / H : ℝ) : ℂ) *
           logarithmicWindowAverage f (Real.log ((x + H) / x)) (Real.log x) := by
   …

   Mentions: OAI.JointDickman.reciprocalShortAverage, OAI.JointDickman.logarithmicWindowAverage

5. theorem OAI.JointDickman.norm_shortAverage_le_logarithmic line 57

   Source documentation

   A hard short average is bounded by its normalized logarithmic window plus the uniform endpoint-scale error.

   theorem norm_shortAverage_le_logarithmic (f : ArithmeticFunction ℂ)
       (hf : ∀ n, ‖f n‖ ≤ 1) {x H : ℝ} (hx : 0 < x) (hH : 0 < H) :
       ‖complexShortAverage f H x‖ ≤
         ‖logarithmicWindowAverage f (Real.log ((x + H) / x)) (Real.log x)‖ +
           (H + 1) / x := by
   …

   Mentions: OAI.JointDickman.logarithmicWindowAverage

6. theorem OAI.JointDickman.shortAverage_sq_le_logarithmic line 84