OAI/NumberTheory/CubicMoment/Angular/AngularPrimeMomentCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.structuredAngularPrimeMoment line 13
2. lemma OAI.CubicFirstMoment.structuredAngularPrimeMoment_eq_tuple line 22

   Source documentation

   The literal numerator and excluded-prime factors are assembled into one explicitly constructed finite character of modulus 9ve.

   lemma structuredAngularPrimeMoment_eq_tuple (hpub : CubicSupplementaryPeriodicity)
       (a b v e : Eisenstein) (ha : primary a) (hb : primary b) (hv : v ≠ 0)
       (u : ℝ) (W : ι → ℝ → ℂ) (X : ι → ℝ) (V : ℝ → ℂ) (Y : ℝ) :
       structuredAngularPrimeMoment ℓ a b v e u W X V Y =
         primaryAngularSquarefreePrimeTuple ℓ a b (fun _ : ι => 1*((9*v)*e))
           (fun _ => productResidueChar (1 : MulChar (Residues (1:Eisenstein)) ℂ)
             (productResidueChar (cubicNumeratorChar hpub v hv) (1 : MulChar (Residues e) ℂ)))
           (fun _ => u) W X V Y := by
   …

   Mentions: OAI.CubicFirstMoment.CubicSupplementaryPeriodicity, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.structuredAngularPrimeMoment, OAI.CubicFirstMoment.primaryAngularSquarefreePrimeTuple, OAI.CubicFirstMoment.productResidueChar, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.cubicNumeratorChar

3. lemma OAI.CubicFirstMoment.structuredAngularPrimeMoment_eq_lifted_tuple line 51