OAI/NumberTheory/TwoPoint/Bounds/QualitativeDivisorTransferRight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.RoughBinData.AdmissibleRight line 14
2. theorem OAI.TwoPointCorrelations.qualitative_divisor_transfer_right line 24

   Source documentation

   Uniform rough-shift cancellation summed over the finite retained- divisor family, with total weight sum |a_u|/u. Functions and coefficients may be chosen after the common long-average threshold.

   theorem qualitative_divisor_transfer_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,
         ∀ (U : Finset ℕ) (a : ℕ → ℂ) (H τ : ℝ) (P : ℕ → Finset ℕ)
           (l : ℕ) [NeZero l] (residue : ℕ → ZMod l),
         1 < τ → τ < 2 → (∀ u ∈ U, 0 < u) →
         (∀ u ∈ U, Real.exp (B ^ (9999 / 10000 : ℝ)) / τ ≤ H / (u : ℝ)) →
         (∀ u ∈ U, H / (u : ℝ) ≤ Real.exp (C₀ * B)) →
         ∀ᶠ X : ℕ in atTop, ∀ d : ℕ → RoughBinData,
         (∀ u ∈ U, (d u).AdmissibleRight f (P u) (H / (u : ℝ)) τ
   …

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