HalaszMeanValue.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An ordinary Halász mean estimate, with an absolute constant and the logarithmic-height range needed in the MRT argument.

theorem OAI.TwoPointCorrelations.halasz_mean_value line 17

Source documentation

Uniform ordinary mean estimate for completely multiplicative functions. The distance lower bound is required only for |t| ≤ (log N)^8.

Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszMeanValue.lean:17 (same declaration text).

theorem halasz_mean_value : ∃ C X₀ : ℝ, 0 < C ∧
    ∀ (N : ℕ), X₀ ≤ N →
    ∀ (f : ℕ → ℂ), f 1 = 1 →
      (∀ a b, 0 < a → 0 < b → f (a * b) = f a * f b) → OneBounded f →
    ∀ (M : ℝ), 0 ≤ M →
      (∀ t ∈ Set.Icc (-(Real.log (N : ℝ) ^ 8)) (Real.log (N : ℝ) ^ 8),
        M ≤ squaredDistance f (mrtArchimedeanTwist t) N) →
      ‖∑ n ∈ Icc 1 N, f n‖ ≤ C * N *
        ((M + 1) * Real.exp (-M) + Real.log (Real.log N) / Real.log N) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist