SieveResidue.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The residue sum after squarefree majorization

The actual collected coefficients agree with Möbius below the truncation. Their uniformly convergent norm series therefore differs from the true Möbius residue by O(D⁻¹ᐟ²).

def OAI.CubicFirstMoment.squarefreeSieveResidueTerm line 19
def OAI.CubicFirstMoment.moebiusResidueTerm line 24
lemma OAI.CubicFirstMoment.squarefreeTruncation_spec line 27
lemma OAI.CubicFirstMoment.squarefreeSieveCoefficient_zero line 32
lemma OAI.CubicFirstMoment.sieveResidueTerm_eq_of_norm_le line 41
theorem OAI.CubicFirstMoment.sieveResidue_difference_bound line 54
Source documentation
Uniform pointwise majorant with the entire discrepancy beyond D.
```
theorem sieveResidue_difference_bound :
    ∃ K : ℝ, 0 < K ∧ ∀ D : ℝ, ∀ e : Eisenstein,
      |squarefreeSieveResidueTerm D e - moebiusResidueTerm e| ≤
        if D < norm e then K*norm e^(-(7/4:ℝ)) else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.squarefreeSieveResidueTerm, OAI.CubicFirstMoment.moebiusResidueTerm, OAI.CubicFirstMoment.norm
lemma OAI.CubicFirstMoment.moebiusResidueTerm_abs_le line 89
lemma OAI.CubicFirstMoment.summable_moebiusResidueTerm line 101
lemma OAI.CubicFirstMoment.summable_sieveResidue_difference line 106
lemma OAI.CubicFirstMoment.summable_squarefreeSieveResidueTerm line 117
theorem OAI.CubicFirstMoment.sieveResidue_difference_le line 123
Source documentation
The sieve residue has a uniform square-root truncation error.
```
theorem sieveResidue_difference_le :
    ∃ C : ℝ, 0 < C ∧ ∀ D : ℝ, 0 < D →
      |(∑' e : Eisenstein, squarefreeSieveResidueTerm D e) -
        (∑' e : Eisenstein, moebiusResidueTerm e)| ≤ C*D^(-(1/2:ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.squarefreeSieveResidueTerm, OAI.CubicFirstMoment.moebiusResidueTerm
theorem OAI.CubicFirstMoment.sieveResidue_difference_isBigO line 155
Source documentation
In particular, the precise series replacing the sieve coefficients has an error of order D⁻¹ᐟ²; it is not an assumed residue identity.
```
theorem sieveResidue_difference_isBigO :
    (fun D : ℝ => (∑' e : Eisenstein, squarefreeSieveResidueTerm D e) -
      (∑' e : Eisenstein, moebiusResidueTerm e)) =O[Filter.atTop]
      (fun D : ℝ => D^(-(1/2:ℝ))) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.squarefreeSieveResidueTerm, OAI.CubicFirstMoment.moebiusResidueTerm