OAI/NumberTheory/CubicMoment/Theta/CubicThetaAxisDerivativeBalance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Inversion fixes the axis derivative at height one. A negative real arithmetic derivative determines the remaining sign of the base scalar.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticAxisDerivative line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticAxis_hasDerivAt line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticAxisDerivative_balance line 27
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticBaseScalar_eq_one_of_axisDerivative_neg line 55