OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateAxis.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate lines used for the spatial derivatives of the series.

  1. inductive OAI.CubicFirstMoment.CubicThetaAxis line 9
  2. def OAI.CubicFirstMoment.cubicThetaCoordinateLine line 12
  3. def OAI.CubicFirstMoment.cubicThetaCoordinateCenter line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaCoordinateLine_center line 24
  5. lemma OAI.CubicFirstMoment.cubicThetaCoordinateLine_continuous line 29
  6. lemma OAI.CubicFirstMoment.cubicThetaCoordinateLine_analytic line 33