OAI/NumberTheory/CubicMoment/Theta/CubicThetaTwiceDifferentiation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local twice differentiation for the complex coordinate series used below. Both summable derivative bounds are supplied by actual grid estimates.

  1. lemma OAI.CubicFirstMoment.cubicTheta_twice_hasDerivAt_tsum line 14
  2. lemma OAI.CubicFirstMoment.cubicTheta_twice_deriv_tsum line 42