OAI/NumberTheory/CubicMoment/Theta/CubicThetaMetricScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The two-point metric identity gives exact scaling of Euclidean squared lengths under the actual hyperbolic action.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadius_smul line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRadius_continuous line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaMobius_secant_scale line 21