MRTNearBandSum.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual MRT band count absorbs the finite near-mask sum into a uniform logarithmic error while retaining the centered typical amplitude.

theorem OAI.TwoPointCorrelations.mrt_band_near_renormalization line 15

Source documentation

Near-center renormalization for the literal family of original bands. The -3/50 exponent leaves room for the finite inclusion-exclusion cost.

theorem mrt_band_near_renormalization :
    ∀ᶠ N : ℕ in atTop, ∀ P Q : ℝ, ∀ J : ℕ,
      1≤Real.log Q → 1≤J →
      (∀ j∈Icc 1 J, mrtBandUpper Q j ≤ Real.exp (Real.sqrt (Real.log N))) →
      ∀ F : ℕ → ℂ, F 1=1 → Multiplicative F → OneBounded F →
      ∀ τ : ℝ, squaredDistance F (mrtArchimedeanTwist τ) (2*N) ≤
        Real.log (Real.log (2*N:ℕ))/10 →
      ∀ u : ℝ, |u|≤(Real.log N)^(1/16:ℝ) → ∀ k∈Icc N (2*N),
      ‖halaszPhaseMean (halaszTwistedFunction (mrtTypicalCoefficient (Icc 1 J)
        (fun j => mrtPrimeBand (mrtBandLower P Q j) (mrtBandUpper Q j)) F) τ) u k -
        (halaszPowerPhase u k/(1+(-u:ℂ)*Complex.I))*
          halaszPhaseMean (halaszTwistedFunction (mrtTypicalCoefficient (Icc 1 J)
…

Mentions: OAI.TwoPointCorrelations.mrtBandUpper, OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.mrtPrimeBand, OAI.TwoPointCorrelations.mrtBandLower, OAI.TwoPointCorrelations.halaszPowerPhase