OAI/NumberTheory/CubicMoment/Angular/AngularComplexWeightedConvolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubicFirstMoment.angularTwistedProductPolynomial_eq_unsplit line 15

   Source documentation

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

   theorem angularTwistedProductPolynomial_eq_unsplit (A : ι → EisensteinArithmeticFunction)
       {a b : Eisenstein} (ha : primary a) (hb : primary b)
       (q : ι → Eisenstein) (η : (i : ι) → MulChar (Residues (q i)) ℂ)
       (hη : ∀ i, AngularUnitCompatible (q i) (η i) ℓ)
       (t : ι → ℝ) (V : ℝ → ℂ) {Y : ℝ} (hY : 0 < Y)
       (hV : ∀ x, 2 < x → V x = 0) :
       primaryComplexProductPolynomial (fun i => angularTwistArithmetic ℓ (q i) (η i) (t i) (A i))
         (mixedCubic a b) V Y = primaryAngularUnsplitTuple ℓ A a b q η t V Y := by
   …

   Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.AngularUnitCompatible, OAI.CubicFirstMoment.primaryComplexProductPolynomial, OAI.CubicFirstMoment.angularTwistArithmetic, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.primaryAngularUnsplitTuple