RoughProductPairs.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of the original rough-product divisor expansion as independent primary factors, with the original product support.

theorem OAI.CubicFirstMoment.roughProduct_primary_factor_pair line 13
theorem OAI.CubicFirstMoment.roughProduct_finite_factor_pairs line 34
Source documentation
The original finite support is kept as an exact product predicate. There is no coprimality assumption or replacement of its sharp cutoff.
```
theorem roughProduct_finite_factor_pairs (S : Finset Eisenstein) (X : ℝ)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ S, (roughProduct ψ w n:ℂ)*K n) =
      ∑ d ∈ primaryElementBall X, ∑ e ∈ primaryElementBall X,
        if d*e ∈ S then cutoffMoebius ψ w d*K (d*e) else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.cutoffMoebius