QualitativeShortSums.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The published MRT theorem at fixed window length, uniformly over all finite-prime modifications of the original nonpretentious factor.

lemma OAI.TwoPointCorrelations.loglog_div_log_nonneg line 15

theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.modified_fixed_windows line 25

Source documentation

Fixed-length MRT, with an arbitrarily small residual error. The supremum over frequencies remains outside the sum over window origins.

theorem MRTShortExponentialInput.modified_fixed_windows
    (hMRT : MRTShortExponentialInput) {f : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (hf : OneBounded f) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ) (D : ℕ), 10 ≤ D → ∀ ε : ℝ, 0 < ε →
      ∀ᶠ Y : ℕ in atTop, ∀ b : ℕ → ℂ, Multiplicative b → OneBounded b →
        (∀ p, Nat.Prime p → p ∉ P → b p = f p) →
        ∀ (l : ℕ) [NeZero l] (a : ZMod l) (θ : AddCircle (1 : ℝ)),
        (∑ v ∈ range Y,
          ‖forwardWindowPolynomial (progressionSequence b l a) D (v + 1) θ‖) ≤
          C * D * Y * (Real.log (Real.log (D : ℝ)) / Real.log D + ε) := by
…

Mentions: OAI.TwoPointCorrelations.MRTShortExponentialInput, OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.progressionSequence