OAI/NumberTheory/CubicMoment/Theta/CubicThetaKernelFirstBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform first-coordinate derivative bounds for the kernel.

  1. lemma OAI.CubicFirstMoment.cubicThetaCartesian_x_deriv line 9
  2. theorem OAI.CubicFirstMoment.cubicThetaCartesian_x_deriv_bound line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaCartesian_v_deriv line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaCartesian_v_deriv_bound line 50
  5. lemma OAI.CubicFirstMoment.cubicThetaCartesian_swap line 66
  6. theorem OAI.CubicFirstMoment.cubicThetaCartesian_y_deriv_bound line 71