MRTWeightedPrefix.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite partial summation from ordinary prefix cancellation to a normalized Dirichlet polynomial on a bounded-ratio interval.

lemma OAI.TwoPointCorrelations.mrt_range_zero_extension line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTWeightedPrefix.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_reciprocal_summation_by_parts line 25
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTWeightedPrefix.lean:25 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_reciprocal_gap line 44
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTWeightedPrefix.lean:44 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_weighted_prefix_bound line 57
Source documentation
A prefix bound on the same scale controls the normalized polynomial on every interval of ratio at most three.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTWeightedPrefix.lean:57 (same declaration text).
```
theorem mrt_weighted_prefix_bound (F : ℕ → ℂ) {m n : ℕ}
    (hm : 0 < m) (hmn : m ≤ n) (hn3 : n ≤ 3 * m)
    {A : ℝ} (hA : 0 ≤ A)
    (hF : ∀ k ∈ Icc m n, ‖∑ i ∈ Icc 1 k, F i‖ ≤ A * k) :
    ‖∑ i ∈ Ioc m n, F i / (i : ℂ)‖ ≤ 5 * A := by
…
```