OAI/NumberTheory/CubicMoment/Theta/CubicThetaDerivativeRemainder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic derivative remainder is dominated by the three summable coordinate families.

  1. def OAI.CubicFirstMoment.cubicThetaDerivativeRemainder line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaRemainderWeight_components line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaDerivativeRemainder_bound line 34
  4. lemma OAI.CubicFirstMoment.cubicThetaDerivativeRemainder_mass line 82