SquarefreeJoin.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Collecting the squarefree majorant by least common multiples

The join is the product of the union of the primary prime factors. Its square divides an element exactly when both input squares divide it.

def OAI.CubicFirstMoment.primarySquarefreeJoin line 17
lemma OAI.CubicFirstMoment.join_factor_primaryPrime line 20
lemma OAI.CubicFirstMoment.primarySquarefreeJoin_primary line 26
lemma OAI.CubicFirstMoment.primarySquarefreeJoin_squarefree line 30
lemma OAI.CubicFirstMoment.dvd_primarySquarefreeJoin_left line 40
lemma OAI.CubicFirstMoment.dvd_primarySquarefreeJoin_right line 45
theorem OAI.CubicFirstMoment.primarySquarefreeJoin_sq_dvd_iff line 51
Source documentation
This is the divisor condition used in the collected sieve square.
```
theorem primarySquarefreeJoin_sq_dvd_iff {a b : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (n : Eisenstein) :
    (primarySquarefreeJoin a b)^2 ∣ n ↔ a^2 ∣ n ∧ b^2 ∣ n := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primarySquarefreeJoin
lemma OAI.CubicFirstMoment.primarySquarefreeJoin_dvd_mul line 71
lemma OAI.CubicFirstMoment.norm_le_of_dvd_nonzero line 82
lemma OAI.CubicFirstMoment.primarySquarefreeJoin_norm_le line 88
def OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient line 94
lemma OAI.CubicFirstMoment.weighted_image_sum line 98
theorem OAI.CubicFirstMoment.truncatedSquareDivisorSum_collected line 114
Source documentation
The square of the truncated Möbius sum is exactly a finite divisor sum with the collected coefficients.
```
theorem truncatedSquareDivisorSum_collected (C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c ∧ Squarefree c) (n : Eisenstein) :
    (truncatedSquareDivisorSum C n)^2 =
      ∑ e ∈ (C.product C).image (fun t => primarySquarefreeJoin t.1 t.2),
        collectedSquarefreeSieveCoefficient C e * (if e^2 ∣ n then (1 : ℝ) else 0) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.truncatedSquareDivisorSum, OAI.CubicFirstMoment.primarySquarefreeJoin, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient