OAI/NumberTheory/CubicMoment/Theta/CubicThetaLogHeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic height conjugation of the radial hyperbolic operator. The conjugated radial operator is d^2/dt^2 - 1.

  1. def OAI.CubicFirstMoment.cubicThetaLogLift line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaLogLift_hasDerivAt line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaLogLift_second_deriv line 27
  4. theorem OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_logLift line 43