CutoffDivisorTransfer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite retained-divisor assembly for the actual two-cutoff averages. The original nonpretentious factor may be either member of the pair.

theorem OAI.TwoPointCorrelations.qualitative_cutoff_rough_shifts_either line 13
structure OAI.TwoPointCorrelations.RoughCoefficients line 47
def OAI.TwoPointCorrelations.RoughCoefficients.InBin line 51
def OAI.TwoPointCorrelations.cutoffRoughProfile line 55

theorem OAI.TwoPointCorrelations.qualitative_cutoff_divisor_transfer line 64

Source documentation

The actual cutoff terms at scales floor(X/u) retain exactly the reciprocal divisor mass. The finite coefficient family remains uniform.

theorem qualitative_cutoff_divisor_transfer (hM : PrimeReciprocalInput)
    (hMRT : MRTShortExponentialInput) {f g : ℕ → ℂ}
    (hf : OneBounded f) (hg : OneBounded g)
    (hfm : Multiplicative f) (hgm : Multiplicative g)
    (hnp : UniformlyNonpretentious f ∨ UniformlyNonpretentious g)
    (h : ℕ) (hh : 0 < h) (C₀ : ℝ) (hC₀ : 1 ≤ C₀) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℝ in atTop,
      ∀ (U : Finset ℕ) (a : ℕ → ℂ) (H τ : ℝ) (P Q : ℕ → Finset ℕ),
      (∀ u ∈ U, ∀ p ∈ P u, Nat.Prime p) →
      (∀ u ∈ U, ∀ p ∈ Q u, Nat.Prime p) →
      1 < τ → τ < 2 → (∀ u ∈ U, 0 < u) →
      (∀ u ∈ U, Real.exp (B ^ (9999 / 10000 : ℝ)) / τ ≤ H / (u : ℝ)) →
…

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