PrimaryWeightedConvolution.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Collecting the actual weighted element tuples gives exactly the primary polynomial of the product of their ideal arithmetic functions.

def OAI.CubicFirstMoment.primaryConvolutionPolynomial line 14
lemma OAI.CubicFirstMoment.coeff_product_eq_convolution line 19
theorem OAI.CubicFirstMoment.primaryConvolutionPolynomial_eq_tuple line 32
Source documentation
The global smooth cutoff permits collection on one finite primary ball, although the unrestricted product support is much larger.
```
theorem primaryConvolutionPolynomial_eq_tuple (A : ι → EisensteinArithmeticFunction)
    (χ : Eisenstein → ℂ) (V : ℝ → ℂ) {Y : ℝ} (hY : 0 < Y)
    (hV : ∀ x, 2 < x → V x = 0) :
    primaryConvolutionPolynomial A χ V Y =
      ∑ n ∈ Fintype.piFinset (fun _ : ι => primaryElementBall (2*Y)),
        (∏ i, ((MvPowerSeries.coeff (idealExponentOf (n i)) (A i):ℝ):ℂ))*
          χ (∏ i, n i)*V ((∏ i, norm (n i))/Y) := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryConvolutionPolynomial, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.norm