OAI/NumberTheory/JointDickman/Analysis/MellinApplicationLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.eventually_short_scales line 12
2. lemma OAI.JointDickman.eventually_short_energy_nonneg line 20
3. theorem OAI.JointDickman.centeredShortAverage_tendsto_zero_of_mellin_bound line 31

   Source documentation

   The same spectral limit gives centered short means, including a scale-dependent dyadic long mean of norm at most two.

   theorem centeredShortAverage_tendsto_zero_of_mellin_bound {ι : Type*} (l : Filter ι)
       (f : ι → ArithmeticFunction ℂ) (hf : ∀ i n, ‖f i n‖ ≤ 1)
       (c : ι → ℂ) (hc : ∀ i, ‖c i‖ ≤ 2)
       (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⌋₊)
           (centeredShortCoefficients (f i) (c 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 - c i‖ ^ 2)) l (𝓝 0) := by
   …

   Mentions: OAI.JointDickman.mellinPolynomial, OAI.JointDickman.centeredShortCoefficients

4. theorem OAI.JointDickman.shortAverage_tendsto_zero_of_typical_mellin_bound line 60

   Source documentation

   The typical-set sieve error is paid in ordinary counting density.

   theorem shortAverage_tendsto_zero_of_typical_mellin_bound {ι : Type*} (l : Filter ι)
       (S : ι → ℕ → Prop) [∀ i, DecidablePred (S i)]
       (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⌋₊)
           (restrictArithmetic (S i) (f i)) t‖ ^ 2) ≤ A i + B i * T)
       (hmissing : Tendsto (fun i =>
         (((range (⌊3 * X i⌋₊ + 1)).filter fun n => ¬S i n).card : ℝ) / X i) l (𝓝 0)) :
   …

   Mentions: OAI.JointDickman.mellinPolynomial, OAI.JointDickman.restrictArithmetic