OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreBumps.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite family of genuine compactly supported smooth chart cutoffs controls the actual arithmetic core.

  1. def OAI.CubicFirstMoment.cubicThetaCoreBump line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaCoreBump_finite_cover line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaCoreBump_sum_sq line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaCoreBump_compact line 37