OAI/NumberTheory/CubicMoment/Theta/CubicThetaHyperbolicChain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The hyperbolic chain rule, keeping the two coefficients explicit. They will be identified for the actual arithmetic row height using its already proved first and second power equations.

  1. def OAI.CubicFirstMoment.cubicThetaHeightChainQuadratic line 12
  2. def OAI.CubicFirstMoment.cubicThetaHeightChainLinear line 17
  3. theorem OAI.CubicFirstMoment.cubicThetaHyperbolic_chain line 23