OAI/NumberTheory/CubicMoment/Theta/CubicThetaAnnularSeries.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The fixed open-annulus transport of a continuous radial profile. At most one actual primitive row contributes at any point.

  1. instance OAI.CubicFirstMoment.cubicThetaBottomRow_countable line 14
  2. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.pointHeight_continuous line 19
  3. def OAI.CubicFirstMoment.cubicThetaAnnularTerm line 25
  4. def OAI.CubicFirstMoment.cubicThetaAnnularSeries line 30
  5. lemma OAI.CubicFirstMoment.cubicThetaAnnularTerm_high line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaAnnularTerm_support line 39
  7. lemma OAI.CubicFirstMoment.cubicThetaAnnularTerm_measurable line 45
  8. lemma OAI.CubicFirstMoment.cubicThetaAnnularSeries_measurable line 53
  9. lemma OAI.CubicFirstMoment.cubicThetaAnnularTerm_norm line 57
  10. lemma OAI.CubicFirstMoment.cubicThetaAnnularSeries_norm line 66
  11. lemma OAI.CubicFirstMoment.cubicThetaAnnularSeries_add line 82
  12. lemma OAI.CubicFirstMoment.cubicThetaAnnularSeries_smul line 92
  13. lemma OAI.CubicFirstMoment.cubicThetaAnnularSeries_forcing line 104