HalaszExceptionalMean.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The ordinary mean estimate retaining the location of one exceptional unit interval in the logarithmic-height Perron window.

theorem OAI.TwoPointCorrelations.halasz_exceptional_mean_value line 17

Source documentation

Completely multiplicative means with one unit interval excluded from the distance hypothesis. Its location supplies an additional decay term.

theorem halasz_exceptional_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.Ioc (-(Real.log (N : ℝ) ^ 8)) (Real.log (N : ℝ) ^ 8),
        t ∉ Set.Ioc (τ-1/2) (τ+1/2) → M ≤ squaredDistance f (mrtArchimedeanTwist t) N) →
      ‖∑ n ∈ Icc 1 N, f n‖ ≤ C * N *
        ((min M (Real.log (1+|τ|)) + 1) * Real.exp (-min M (Real.log (1+|τ|))) +
          Real.log (Real.log N) / Real.log N) := by
…

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