OAI/NumberTheory/CubicMoment/Theta/CubicThetaCircleInversion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Inversion takes every horizontal circle to a reversed horizontal circle. Its transformed height depends only on the radius.

  1. def OAI.CubicFirstMoment.cubicThetaCircleDualDirection line 15
  2. def OAI.CubicFirstMoment.cubicThetaCircleDualHeight line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaSignedCircle_radius line 21
  4. theorem OAI.CubicFirstMoment.cubicThetaInversion_circle line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaCircleDualDirection_limit line 46
  6. lemma OAI.CubicFirstMoment.cubicThetaCircleDualHeight_limit line 58