OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedFullObservation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The full translated-cusp observation, including the entire incoming correction at low height. Its residue is unchanged.

  1. lemma OAI.CubicFirstMoment.cubicThetaCompactShiftedFamily_remainder line 12
  2. def OAI.CubicFirstMoment.cubicThetaShiftedIncomingWindow line 30
  3. def OAI.CubicFirstMoment.cubicThetaShiftedFullObservation line 36
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedFullObservation_meromorphic line 41
  5. lemma OAI.CubicFirstMoment.cubicThetaShiftedIncomingWindow_integrable line 48
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedFullObservation_right line 59
  7. lemma OAI.CubicFirstMoment.cubicThetaShiftedFullObservation_residue line 85