OAI/NumberTheory/JointDickman/Analysis/MellinPrefixBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.angularMellinPolynomial_cpow line 11
2. theorem OAI.JointDickman.angularMellinPolynomial_le_of_prefix line 28

   Source documentation

   A uniform prefix error D on [X,4X] yields the explicit bounded-frequency cost (5+3*T)*D/X.

   theorem angularMellinPolynomial_le_of_prefix (a : ℕ → ℂ) {X T D t : ℝ}
       (hX : 0 < X) (hT : 0 ≤ T) (hD : 0 ≤ D) (ht : |t| ≤ T)
       (hprefix : ∀ u ∈ Set.Icc X (4 * X), ‖∑ n ∈ Icc 0 ⌊u⌋₊, a n‖ ≤ D) :
       ‖angularMellinPolynomial (Ioc ⌊X⌋₊ ⌊4 * X⌋₊) a t‖ ≤
         (5 + 3 * T) * D / X := by
   …

   Mentions: OAI.JointDickman.angularMellinPolynomial