HalaszNearRenormalization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform renormalization on the small neighborhood of the minimizing twist. This is the near-twist ingredient needed for the MRT Fourier energy estimate.

theorem OAI.TwoPointCorrelations.halasz_near_renormalization line 15
Source documentation
The elementary unit-correction argument loses only log(N)^(-1/16) on the whole near-center frequency interval.
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearRenormalization.lean:15 (same declaration text).
```
theorem halasz_near_renormalization :
    ∀ᶠ N : ℕ in atTop, ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
      ∀ (Q : Finset ℕ), (∀ p ∈ Q, p.Prime) →
      (∀ p ∈ Q, (p : ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
      ∀ t : ℝ, squaredDistance F (mrtArchimedeanTwist t) N ≤
        Real.log (Real.log N) / 8 →
      ∀ u : ℝ, |u| ≤ (Real.log N) ^ (1 / (16 : ℝ)) →
      let G := halaszTwistedFunction (mrtMissingCoefficient F Q) t
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtMissingCoefficient