SieveCoefficients.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Support and divisor bounds for the dispersion sieve coefficients

The coefficients are the actual finite least-common-multiple collection of the truncated Möbius square, not an abstract majorant hypothesis.

lemma OAI.CubicFirstMoment.collectedSieveCoefficient_nonzero line 18
theorem OAI.CubicFirstMoment.collectedSieveCoefficient_support line 34
Source documentation
A pair of divisors of length at most D contributes only at a primary squarefree modulus of norm at most D².
```
theorem collectedSieveCoefficient_support (C : Finset Eisenstein) {D : ℝ} (hD : 0 ≤ D)
    (hC : ∀ c ∈ C, primary c ∧ Squarefree c ∧ norm c ≤ D) (e : Eisenstein)
    (he : collectedSquarefreeSieveCoefficient C e ≠ 0) :
    primary e ∧ Squarefree e ∧ norm e ≤ D^2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient
lemma OAI.CubicFirstMoment.abs_idealMoebius_real_le_one line 45
theorem OAI.CubicFirstMoment.collectedSieveCoefficient_abs_le line 50
Source documentation
The number of possible ordered divisor pairs controls the collected coefficient. This is the square-divisor bound required for the sieve.
```
theorem collectedSieveCoefficient_abs_le (C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c ∧ Squarefree c) (e : Eisenstein) :
    |collectedSquarefreeSieveCoefficient C e| ≤
      ((2 : ℝ)^(primaryPrimeFactors e).card)^2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient, OAI.CubicFirstMoment.primaryPrimeFactors
theorem OAI.CubicFirstMoment.collectedSieveCoefficient_small_power line 95
Source documentation
The divisor loss is an arbitrarily small fixed power, uniformly in all choices of the truncation set.
```
theorem collectedSieveCoefficient_small_power {ε : ℝ} (hε : 0 < ε) :
    ∃ K : ℝ, 0 < K ∧ ∀ (C : Finset Eisenstein),
      (∀ c ∈ C, primary c ∧ Squarefree c) → ∀ e : Eisenstein,
      |collectedSquarefreeSieveCoefficient C e| ≤ K*norm e^ε := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient, OAI.CubicFirstMoment.norm