OAI/NumberTheory/JointDickman/Analysis/ShortMellinDyadicEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.shortAverage_dyadic_energy line 11

   Source documentation

   The spectral bound is needed only on subintervals of the coefficient range [X,4X]. The number of blocks is fixed before the short length grows.

   theorem shortAverage_dyadic_energy (η : ℝ) (hη : 0 < η) (hηhalf : η < 1/2)
       (m : ℕ) (hm : 0 < m) :
       ∃ C : ℝ, 0 < C ∧ ∀ (f : ArithmeticFunction ℂ), (∀ n, ‖f n‖ ≤ 1) →
         ∀ X H : ℝ, 0 < X → 1 ≤ H → H ≤ X → ∀ A B : ℝ, 0 ≤ A → 0 ≤ B →
         (∀ T : ℝ, 1 ≤ T →
           (∫ t in -T..T, ‖mellinPolynomial (Ioc ⌊X⌋₊ ⌊4 * X⌋₊) f t‖ ^ 2) ≤ A + B * T) →
         (1 / X) * (∫ x in X..2 * X, ‖complexShortAverage f H x‖ ^ 2) ≤
           C * (A + B * X / H) +
             2 * (3 / (m : ℝ) + 11 / H + H / X + 1 / X + 16 * η) ^ 2 := by
   …

   Mentions: OAI.JointDickman.mellinPolynomial