QualitativeRoughBins.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual real divisor bins in the analytic centering argument are contained in the natural windows used by the finite Fourier proof.

lemma OAI.TwoPointCorrelations.rough_bin_ceil_window line 13
lemma OAI.TwoPointCorrelations.ceil_exp_scale_bound line 23

theorem OAI.TwoPointCorrelations.qualitative_rough_shifts_real_bins line 37

Source documentation

The rough estimate for the real bins (M,τM] that arise after writing an expanded divisor as u*w.

theorem qualitative_rough_shifts_real_bins (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 ℕ) (M τ : ℝ), 1 < τ → τ < 2 →
      Real.exp (B ^ (9999 / 10000 : ℝ)) / τ ≤ M →
      M ≤ Real.exp (C₀ * B) →
      ∀ᶠ Y : ℕ in atTop, ∀ b g : ℕ → ℂ,
      Multiplicative b → OneBounded b → OneBounded g →
      (∀ p, Nat.Prime p → p ∉ P → b 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