MRTCorrectionSummability.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Absolute summability of the prime-power correction in MRT's reduction from multiplicative to completely multiplicative functions.

def OAI.TwoPointCorrelations.mrtCorrectionWeight line 13
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:13 (same declaration text).
def OAI.TwoPointCorrelations.mrtCorrectionEulerConstant line 16
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:16 (same declaration text).
def OAI.TwoPointCorrelations.mrtCorrectionBound line 19
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionWeight_nonneg line 22
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:22 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionWeight_zero line 26
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:26 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionWeight_one line 29
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:29 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionWeight_mul line 32
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:32 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionWeight_prime_pow line 41
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:41 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionEulerConstant_nonneg line 48
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:48 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_correction_local_summable line 53
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:53 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_correction_local_sum_bound line 69
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:69 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_correction_summable line 123
Source documentation
Uniform absolute convergence at exponent 3/4, exactly as required by the general-multiplicative reduction in corrected MRT.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:123 (same declaration text).
```
theorem mrt_correction_summable (f : ℕ → ℂ) (hf : OneBounded f) (h1 : f 1 = 1) :
    Summable (mrtCorrectionWeight f) ∧
      (∑' n : ℕ, mrtCorrectionWeight f n) ≤ mrtCorrectionBound := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtCorrectionWeight, OAI.TwoPointCorrelations.mrtCorrectionBound
theorem OAI.TwoPointCorrelations.mrt_correction_tail_bound line 134
Source documentation
The large-divisor correction costs O(W^(-1/4)), with an absolute constant independent of the multiplicative function and of the finite sum.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionSummability.lean:134 (same declaration text).
```
theorem mrt_correction_tail_bound (f : ℕ → ℂ) (hf : OneBounded f) (h1 : f 1 = 1)
    {W : ℕ} (hW : 0 < W) (S : Finset ℕ) (hS : ∀ n ∈ S, W ≤ n) :
    (∑ n ∈ S, ‖mrtCorrection f n‖ / (n : ℝ)) ≤
      mrtCorrectionBound * (W : ℝ) ^ (-(1 / 4 : ℝ)) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtCorrection, OAI.TwoPointCorrelations.mrtCorrectionBound