DilationMRT.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

MRT at the exact quotient-window lengths needed by a fixed dilation. The published input is unchanged; only finite reindexing is performed.

lemma OAI.TwoPointCorrelations.zero_origin_sum_le line 15
lemma OAI.TwoPointCorrelations.shortWindowSum_norm_bound line 21
theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.modified_zero_windows line 28

theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.modified_quotient_windows line 68

Source documentation

Each quotient length is fixed before taking the long average. Thus all shorter MRT estimates hold on a common tail, uniformly in the modified function and in frequency.

theorem MRTShortExponentialInput.modified_quotient_windows
    (hMRT : MRTShortExponentialInput) {f : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (hf : OneBounded f) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ) (q D K : ℕ), 0 < q →
      (∀ a ∈ Icc 1 K, 10 ≤ D / a + 1) →
      ∀ ε : ℝ, 0 < ε → ∀ᶠ Y : ℕ in atTop,
        ∀ b : ℕ → ℂ, Multiplicative b → OneBounded b →
        (∀ p, Nat.Prime p → p ∉ P → b p = f p) →
        ∀ a ∈ Icc 1 K, ∀ α : ℝ,
        (∑ m ∈ range (Y / a + 1),
          ‖shortWindowSum (coprimeRestriction q b) (D / a + 1) α m‖) ≤
          C * (D / a + 1 : ℕ) * (Y / a + 1 : ℕ) *
…

Mentions: OAI.TwoPointCorrelations.MRTShortExponentialInput, OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.shortWindowSum, OAI.TwoPointCorrelations.coprimeRestriction