HalaszCenteredPrefix.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Centered prefix cancellation from the proved general Halasz theorem. The lower bound on distance stays at the original large cutoff.

lemma OAI.TwoPointCorrelations.halasz_distance_monotone line 14
lemma OAI.TwoPointCorrelations.halasz_decay_half line 25

theorem OAI.TwoPointCorrelations.halasz_centered_prefix line 39

Source documentation

Uniform centered prefixes on a dyadic interval. The pretentious lower bound is imposed only at the original cutoff X, not at smaller scales or on a modified multiplicative function.

theorem halasz_centered_prefix : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ N : ℕ in atTop, ∀ X : ℕ, N ≤ 2 * X → X ≤ N ^ 3 →
      ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
      ∀ (t T M : ℝ), 0 ≤ M → |t| + Real.log (2 * N : ℕ) ^ 8 ≤ T →
      (∀ v : ℝ, |v| ≤ T → M ≤ squaredDistance F (mrtArchimedeanTwist v) X) →
      ∀ k ∈ Icc N (2 * N),
        ‖halaszPhaseMean (halaszTwistedFunction F t) 0 k‖ ≤
          C * (Real.exp (-M / 2) + Real.log (Real.log N) / Real.log N) * k := by
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszTwistedFunction