MRTCorrectionQuotient.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The small-divisor terms in the general-multiplicative correction use literal divided origin ranges, divided window lengths, and dilated additive frequencies. The rounding cost is one term per original origin.

theorem OAI.TwoPointCorrelations.mrt_dilation_integral_quotient line 14
theorem OAI.TwoPointCorrelations.mrt_correction_quotient_tail line 34
theorem OAI.TwoPointCorrelations.mrt_correction_typical_quotient_tail line 51
lemma OAI.TwoPointCorrelations.mrt_quotient_length_le_two line 71
lemma OAI.TwoPointCorrelations.mrt_small_correction_quotient_bound line 80

theorem OAI.TwoPointCorrelations.mrt_correction_typical_quotient_mean line 137

Source documentation

A uniform divided-window estimate transfers to the original typical coefficient with an absolute correction constant and explicit rounding loss.

theorem mrt_correction_typical_quotient_mean {ι : Type*} (J : Finset ι)
    (P : ι → Finset ℕ) (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
    (F : ℕ → ℂ) (hF : Multiplicative F) (hFb : OneBounded F) (hF1 : F 1 = 1)
    (X H W : ℕ) (hW : 0 < W) (hWH : W ≤ H) (hHX : H ≤ X)
    (hlarge : ∀ j ∈ J, ∀ p ∈ P j, W < p) (α ε : ℝ) (hε : 0 ≤ ε)
    (hmean : ∀ d ∈ (Icc 1 (X + H)).filter (fun d => d ≤ W),
      shortExponentialIntegral (mrtTypicalCoefficient J P (mrtCompletePart F))
        (X / d + 1) (H / d + 1) (d * α) ≤ ε * (X / d + 1 : ℕ) * (H / d + 1 : ℕ)) :
    shortExponentialIntegral (mrtTypicalCoefficient J P F) X H α ≤
      mrtCorrectionBound * X * H *
        (4 * ε + (W : ℝ) / H + 2 * (W : ℝ) ^ (-(1 / 4 : ℝ))) := by
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.mrtCompletePart, OAI.TwoPointCorrelations.mrtCorrectionBound