OAI/NumberTheory/JointDickman/Amplification/HalaszMeanLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ordinary mean decay from the proved Halász estimate

  1. lemma OAI.JointDickman.primeDistanceSquared_nonneg line 13
  2. lemma OAI.JointDickman.minimumDistance_le_primeDistance line 24
  3. theorem OAI.JointDickman.halasz_mean_tendsto_zero line 36

    Source documentation

    This allows the coefficients and integer cutoff to vary together. The uniform distance hypothesis is proved for the actual nonprincipal bin data.

    theorem halasz_mean_tendsto_zero {ι : Type*} (l : Filter ι)
    (N : ι → ℕ) (hN : Tendsto N l atTop)
    (f : ι → ArithmeticFunction ℂ) (hf : ∀ i, (f i).IsMultiplicative)
    (hnorm : ∀ i n, ‖f i n‖ ≤ 1)
    (hd : ∀ R : ℝ, ∀ᶠ i in l, ∀ t : ℝ, |t| ≤ (N i : ℝ) →
      R ≤ primeDistanceSquared (f i) (N i) t) :
    Tendsto (fun i => (∑ n ∈ Icc 1 (N i), f i n) / (N i : ℂ)) l (𝓝 0) := by
…