OAI/NumberTheory/CubicMoment/Theta/CubicThetaKernelEquation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The hyperbolic eigenvalue equation for the actual height-power kernel, in Cartesian coordinates on the upper half-space.

  1. def OAI.CubicFirstMoment.cubicThetaCartesianKernel line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaCartesian_horizontal_second line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaCartesian_y_second line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaCartesian_vertical line 38
  5. lemma OAI.CubicFirstMoment.cubicThetaKernel_jet_equation line 45
  6. theorem OAI.CubicFirstMoment.cubicThetaCartesian_eigenvalue line 81