OAI/NumberTheory/CubicMoment/Estimates/PrimeMomentCoefficient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the structured moment with the original squarefree ordered-prime coefficient, including numerator and exclusion.

  1. lemma OAI.CubicFirstMoment.mellinPhase_norm_prod line 14
  2. lemma OAI.CubicFirstMoment.orderedConvolution_norm_twist line 27
  3. lemma OAI.CubicFirstMoment.squarefreeConvolution_norm_twist line 39
  4. def OAI.CubicFirstMoment.primeMomentCoefficient line 47
  5. def OAI.CubicFirstMoment.structuredPrimeMoment line 50
  6. lemma OAI.CubicFirstMoment.mixedCubic_numerator line 57
  7. lemma OAI.CubicFirstMoment.principal_residue_value line 63
  8. lemma OAI.CubicFirstMoment.squarefreePrimeTuple_principal_base line 71
  9. lemma OAI.CubicFirstMoment.structuredPrimeMoment_eq_tuple line 91

    Source documentation

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

    lemma structuredPrimeMoment_eq_tuple (hpub : CubicSupplementaryPeriodicity)
    (a b v e : Eisenstein) (ha : primary a) (hb : primary b) (hv : v ≠ 0)
    (u : ℝ) (W : ι → ℝ → ℂ) (X : ι → ℝ) (V : ℝ → ℂ) (Y : ℝ) :
    structuredPrimeMoment a b v e u W X V Y =
      primarySquarefreePrimeTuple 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.structuredPrimeMoment, OAI.CubicFirstMoment.primarySquarefreePrimeTuple, OAI.CubicFirstMoment.productResidueChar, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.cubicNumeratorChar