OAI/NumberTheory/TwoPoint/Bounds/QualitativeStrongRight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.qualitative_strong_rough_shifts_right line 13

   Source documentation

   The second-factor counterpart of qualitative_rough_shifts, with the same exponent and uniformity in finite prime changes.

   theorem qualitative_strong_rough_shifts_right (hM : PrimeReciprocalInput)
       (hMRT : MRTShortExponentialInput) {f : ℕ → ℂ}
       (hfnp : UniformlyNonpretentious f) (hf : OneBounded f)
       (h : ℕ) (hh : 0 < h) (C₀ : ℝ) (hC₀ : 1 ≤ C₀) :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℝ in atTop,
         ∀ (P : Finset ℕ) (D : ℕ),
         (1 / 2 : ℝ) * Real.exp (B ^ (9999 / 10000 : ℝ)) ≤ D →
         (D : ℝ) ≤ Real.exp (C₀ * B ^ (2 : ℕ)) →
         ∀ᶠ Y : ℕ in atTop, ∀ b g : ℕ → ℂ,
         OneBounded b → Multiplicative g → OneBounded g →
         (∀ p, Nat.Prime p → p ∉ P → g p = f p) →
         ∀ (l : ℕ) [NeZero l] (a : ZMod l) (Z : Finset ℕ) (c : ℕ → ℂ),
   …

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