OAI/NumberTheory/JointDickman/Analysis/MellinShortLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.exists_mellin_smoothing_parameters line 11
2. theorem OAI.JointDickman.shortAverage_tendsto_zero_of_mellin_bound line 31

   Source documentation

   This purely analytic implication applies also to the iterated scale filter. Its premise is the literal finite Dirichlet-polynomial estimate.

   theorem shortAverage_tendsto_zero_of_mellin_bound {ι : Type*} (l : Filter ι)
       (f : ι → ArithmeticFunction ℂ) (hf : ∀ i n, ‖f i n‖ ≤ 1)
       (H X A B : ι → ℝ) (hH : Tendsto H l atTop) (hX : Tendsto X l atTop)
       (hHX : Tendsto (fun i => H i / X i) l (𝓝 0))
       (hA : ∀ i, 0 ≤ A i) (hB : ∀ i, 0 ≤ B i)
       (hbudget : Tendsto (fun i => A i + B i * X i / H i) l (𝓝 0))
       (hspectral : ∀ᶠ i in l, ∀ T : ℝ, 1 ≤ T →
         (∫ t in -T..T, ‖mellinPolynomial (Ioc ⌊X i⌋₊ ⌊4 * X i⌋₊) (f i) t‖ ^ 2) ≤
           A i + B i * T) :
       Tendsto (fun i => (1 / X i) * (∫ x in X i..2 * X i,
         ‖complexShortAverage (f i) (H i) x‖ ^ 2)) l (𝓝 0) := by
   …

   Mentions: OAI.JointDickman.mellinPolynomial