QualitativeWindowScale.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed-length MRT error on the interval scales of the qualitative transfer. Its constants are uniform over the finite set of modified primes.

theorem OAI.TwoPointCorrelations.eventually_qualitative_window_error line 14

theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.qualitative_window_scale line 57

Source documentation

The actual progression-window sum, uniformly over every finite-prime modification, on the manuscript qualitative interval scales.

theorem MRTShortExponentialInput.qualitative_window_scale
    (hMRT : MRTShortExponentialInput) {f : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (hf : OneBounded f)
    (C₀ : ℝ) (hC₀ : 1 ≤ C₀) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℝ in atTop,
      ∀ (P : Finset ℕ) (D : ℕ), 10 ≤ D →
      (1 / 2 : ℝ) * Real.exp (B ^ (9999 / 10000 : ℝ)) ≤ D →
      (D : ℝ) ≤ Real.exp (C₀ * B) →
      ∀ᶠ 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,
…

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