DistinguishedProductPairs.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of the distinguished subset expansion by its primary product. The original finite support remains inside each row.

def OAI.CubicFirstMoment.distinguishedSubsetWeight line 12
theorem OAI.CubicFirstMoment.roughProduct_distinguished_primary_pairs line 15
theorem OAI.CubicFirstMoment.roughProduct_distinguished_finite_pairs line 32
theorem OAI.CubicFirstMoment.roughProduct_distinguished_slices line 57
Source documentation
The exact original rough weight is a sum of its distinguished rows, with the sharp product support retained in each row.
```
theorem roughProduct_distinguished_slices (S : Finset Eisenstein) (X : ℝ)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    (ψ : ℝ → ℝ) (w z : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ S, (roughProduct ψ z n:ℂ)*K n) =
      ∑ r ∈ primaryElementBall X, distinguishedSubsetWeight ψ w z r*
        ∑ u ∈ primaryProductSlice S X r, (roughProduct ψ w u:ℂ)*K (r*u) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.distinguishedSubsetWeight, OAI.CubicFirstMoment.primaryProductSlice