QualitativeDivisorTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite assembly of the actual u*w expansion at Y = floor(X/u). The reciprocal weight of each retained divisor is preserved exactly, and the long-average threshold is uniform over all admissible Fourier twists.

structure OAI.TwoPointCorrelations.RoughBinData line 15
def OAI.TwoPointCorrelations.RoughBinData.Admissible line 21

theorem OAI.TwoPointCorrelations.qualitative_divisor_transfer line 31

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 (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).Admissible f (P u) (H / (u : ℝ)) τ
…

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