ComplexWeightedConvolution.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Complex coefficient collection retains the distinct norm and residue twists of each original prime factor during short inversion.

def OAI.CubicFirstMoment.primaryComplexProductPolynomial line 16
lemma OAI.CubicFirstMoment.complex_coeff_product_eq_convolution line 21
theorem OAI.CubicFirstMoment.primaryComplexProductPolynomial_eq_tuple line 31
Source documentation
The global smooth cutoff permits collection on one finite primary ball, although the unrestricted product support is much larger.
```
theorem primaryComplexProductPolynomial_eq_tuple (A : ι → MvPowerSeries EisensteinIdealPrime ℂ)
    (χ : Eisenstein → ℂ) (V : ℝ → ℂ) {Y : ℝ} (hY : 0 < Y)
    (hV : ∀ x, 2 < x → V x = 0) :
    primaryComplexProductPolynomial 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.EisensteinIdealPrime, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryComplexProductPolynomial, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.twistedProductPolynomial_eq_unsplit line 88

Source documentation

Independent residue characters and Mellin heights remain attached to individual factors after exact collection.

theorem twistedProductPolynomial_eq_unsplit (A : ι → EisensteinArithmeticFunction)
    {a b : Eisenstein} (ha : primary a) (hb : primary b)
    (q : ι → Eisenstein) (η : (i : ι) → MulChar (Residues (q i)) ℂ)
    (hη : ∀ i, ∀ e : Eisensteinˣ, η i (Ideal.Quotient.mk (modulus (q i)) e) = 1)
    (t : ι → ℝ) (V : ℝ → ℂ) {Y : ℝ} (hY : 0 < Y)
    (hV : ∀ x, 2 < x → V x = 0) :
    primaryComplexProductPolynomial (fun i => twistArithmetic (q i) (η i) (t i) (A i))
      (mixedCubic a b) V Y = primaryUnsplitTuple A a b q η t V Y := by
…

Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.primaryComplexProductPolynomial, OAI.CubicFirstMoment.twistArithmetic, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.primaryUnsplitTuple