OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreDenominator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite sum of squared genuine core bumps is smooth upstairs and bounded below by one on the arithmetic compact core.

  1. def OAI.CubicFirstMoment.cubicThetaCoreDenominator line 13
  2. def OAI.CubicFirstMoment.cubicThetaCoreDenominatorFunction line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaCoreDenominator_continuous line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaCoreDenominator_nonneg line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaCoreDenominatorFunction_contDiff line 29
  6. lemma OAI.CubicFirstMoment.cubicThetaCoreDenominatorFunction_apply line 37
  7. lemma OAI.CubicFirstMoment.cubicThetaCoreDenominator_covers line 49