OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactIncomingTransform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Entire compact incoming corrections after the actual integral Mobius action. This permits residue observations at every positive height.

  1. lemma OAI.CubicFirstMoment.cubicThetaCompactIncomingTransform_differentiable line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedIncomingWindow_differentiable line 59