OAI/NumberTheory/CubicMoment/Theta/CubicThetaMetricDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact hyperbolic metric scaling of the derivative follows from the proved two-point identity, by taking real directional secants.

  1. lemma OAI.CubicFirstMoment.cubicThetaMobius_derivative_scale line 14