OAI/NumberTheory/CubicMoment/Theta/CubicThetaMassFactorization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence and factorization of the literal coefficient mass. The unramified factors retain the primary and squarefree restrictions.

  1. abbrev OAI.CubicFirstMoment.CubicThetaSquarefreePrimary line 13
  2. def OAI.CubicFirstMoment.cubicThetaPrimaryMass line 15
  3. def OAI.CubicFirstMoment.cubicThetaSquarefreeMass line 18
  4. def OAI.CubicFirstMoment.cubicThetaMassPairEquiv line 21
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimaryMass_summable line 28
  6. lemma OAI.CubicFirstMoment.cubicThetaSquarefreeMass_summable line 32
  7. def OAI.CubicFirstMoment.cubicThetaPairMassTerm line 36
  8. lemma OAI.CubicFirstMoment.cubicThetaPairMassTerm_nonneg line 39
  9. lemma OAI.CubicFirstMoment.cubicThetaPairMassTerm_summable line 44
  10. lemma OAI.CubicFirstMoment.cubicThetaPairMassTerm_sum line 52
  11. lemma OAI.CubicFirstMoment.cubicThetaRamifiedMass_summable line 62
  12. lemma OAI.CubicFirstMoment.cubicThetaRamifiedMass_total line 70
  13. lemma OAI.CubicFirstMoment.cubicThetaCoefficientMassTerm_common line 82
  14. lemma OAI.CubicFirstMoment.cubicThetaCoefficientMass_common_summable line 89
  15. lemma OAI.CubicFirstMoment.cubicThetaCoefficientMassTerm_summable line 99
  16. theorem OAI.CubicFirstMoment.cubicThetaCoefficientMass_factorization line 109