HalaszNearScales.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The near-center comparison is uniform on every prefix of the actual dyadic interval, with the pretentious condition at the original cutoff.

lemma OAI.TwoPointCorrelations.halasz_loglog_power_cutoff line 13

theorem OAI.TwoPointCorrelations.halasz_near_prefix_uniform line 27

Source documentation

Small distance at X suffices for every prefix in [N,2N], without redefining the minimizing twist at each prefix.

theorem halasz_near_prefix_uniform :
    ∀ᶠ N : ℕ in atTop, ∀ X : ℕ, N ≤ 2 * X → X ≤ N ^ 3 →
      ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
      ∀ t : ℝ, squaredDistance F (mrtArchimedeanTwist t) X ≤
        Real.log (Real.log X) / 10 →
      ∀ u : ℝ, |u| ≤ (Real.log N) ^ (1 / (16 : ℝ)) →
      ∀ k ∈ Icc N (2 * N),
      ‖halaszPhaseMean (halaszTwistedFunction F t) u k -
        (halaszPowerPhase u k / (1 + (-u : ℂ) * Complex.I)) *
          halaszPhaseMean (halaszTwistedFunction F t) 0 k‖ ≤
        (36 * (halaszPrimePowerLogConstant + 1) * Real.exp 8) *
          (Real.log N) ^ (-1 / (16 : ℝ)) * k := by
…

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