ConvolutionTail.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite truncation estimates for roughness removal

The large-divisor part of the convolution is bounded before invoking any Selberg–Delange input. The bound needs only the elementary |g_z| ≤ 1.

theorem OAI.JointDickman.squarefreeWeight_abs_le_one line 17
Distinct definitions of this name: OAI/NumberTheory/JointDickman/Analysis/SquarefreeDirichletSeries.lean:23 (same statement text; different proof or body). Qualify references as OAI.JointDickman.squarefreeWeight_abs_le_one@path.
theorem OAI.JointDickman.squarefreeWeight_sum_abs_le line 26
def OAI.JointDickman.roughConvolutionTail line 34
Source documentation
The part indexed by divisors greater than the chosen truncation.
```
noncomputable def roughConvolutionTail (E : Finset ℕ) (z : ℝ) (N V : ℕ) : ℝ :=
…
```
theorem OAI.JointDickman.roughConvolutionTail_abs_le line 38

theorem OAI.JointDickman.harmonic_tail_rankin line 64

Source documentation

The elementary Rankin inequality for the harmonic tail.

theorem harmonic_tail_rankin {ι : Type*} (s : Finset ι) (v a : ι → ℝ)
    {V ε : ℝ} (hV : 0 < V) (hε : 0 ≤ ε)
    (hv : ∀ i ∈ s, V ≤ v i) (ha : ∀ i ∈ s, 0 ≤ a i) :
    (∑ i ∈ s, a i / v i) ≤
      (∑ i ∈ s, a i / (v i) ^ (1 - ε)) / V ^ ε := by
…

theorem OAI.JointDickman.roughConvolutionTail_rankin line 85

Source documentation

Quantitative large-divisor truncation in terms of one weighted moment of the correction coefficients.

theorem roughConvolutionTail_rankin (E : Finset ℕ) {z ε : ℝ}
    (hz : 0 ≤ z) (hz1 : z ≤ 1) (hε : 0 ≤ ε) (N V : ℕ) (hV : 0 < V) :
    |roughConvolutionTail E z N V| ≤
      ((N : ℝ) / (V : ℝ) ^ ε) *
        ∑ v ∈ Ioc V N, |smoothCorrection E z v| / (v : ℝ) ^ (1 - ε) := by
…

Mentions: OAI.JointDickman.roughConvolutionTail, OAI.JointDickman.smoothCorrection