SieveMobius.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The Möbius coefficient below the sieve truncation

The union convolution of the squarefree Möbius weights is the same Möbius weight. This proves the exact low-divisor coefficient identity, which is stronger than a divisor bound and is needed in the residue.

lemma OAI.CubicFirstMoment.insert_union_eq_iff line 18
lemma OAI.CubicFirstMoment.union_step line 28

theorem OAI.CubicFirstMoment.squarefree_mobius_union line 50

Source documentation

The exact union convolution of the signed subset weights.

theorem squarefree_mobius_union {ι : Type*} [DecidableEq ι] (U : Finset ι) :
    (∑ s ∈ U.powerset, ∑ t ∈ U.powerset,
      if s ∪ t = U then (-1:ℝ)^s.card*(-1)^t.card else 0) = (-1)^U.card := by
…

lemma OAI.CubicFirstMoment.primaryPrimeFactors_finset_prod line 77
lemma OAI.CubicFirstMoment.primaryPrimeFactors_prod_injective line 92
lemma OAI.CubicFirstMoment.primaryPrime_product_squarefree line 102
lemma OAI.CubicFirstMoment.collectedSieveCoefficient_restrict_divisors line 110
lemma OAI.CubicFirstMoment.primary_divisors_eq_subset_products line 129
theorem OAI.CubicFirstMoment.collectedSieveCoefficient_eq_moebius line 151
Source documentation
If the truncation contains every divisor of e, the collected coefficient is exactly the ideal Möbius function.
```
theorem collectedSieveCoefficient_eq_moebius (C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c ∧ Squarefree c) {e : Eisenstein}
    (he : primary e) (hse : Squarefree e)
    (hcomplete : ∀ c, primary c → Squarefree c → c ∣ e → c ∈ C) :
    collectedSquarefreeSieveCoefficient C e = (idealMoebius e : ℝ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient, OAI.CubicFirstMoment.idealMoebius
def OAI.CubicFirstMoment.squarefreeDivisorTruncation line 206
Source documentation
Terms at nonsquarefree divisors have zero Möbius weight, so this finite truncation gives exactly the original truncated divisor sum.
```
def squarefreeDivisorTruncation (D : ℝ) : Finset Eisenstein :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.mem_squarefreeDivisorTruncation line 209
lemma OAI.CubicFirstMoment.truncatedSquareDivisorSum_squarefree line 219
theorem OAI.CubicFirstMoment.squarefreeSieveCoefficient_small line 233
Source documentation
The exact low-divisor identity for the concrete norm truncation.
```
theorem squarefreeSieveCoefficient_small {D : ℝ} {e : Eisenstein}
    (he : primary e) (hse : Squarefree e) (hD : norm e ≤ D) :
    collectedSquarefreeSieveCoefficient (squarefreeDivisorTruncation D) e =
      (idealMoebius e : ℝ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient, OAI.CubicFirstMoment.squarefreeDivisorTruncation, OAI.CubicFirstMoment.idealMoebius