OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateJets.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Common relative bounds for the first and second coordinate jets. They are preserved by scalar multiplication and horizontal translation.

  1. def OAI.CubicFirstMoment.cubicThetaAxisFunction line 13
  2. def OAI.CubicFirstMoment.cubicThetaFirstJetConstant line 20
  3. def OAI.CubicFirstMoment.cubicThetaSecondJetConstant line 22
  4. def OAI.CubicFirstMoment.CubicThetaCoordinateJetBound line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaJetConstants_nonneg line 32
  6. lemma OAI.CubicFirstMoment.cubicThetaCartesian_jetBound line 37
  7. lemma OAI.CubicFirstMoment.cubicThetaCoordinateJetBound_congr line 66
  8. lemma OAI.CubicFirstMoment.cubicThetaCoordinateJetBound_translate line 81