OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactShiftedFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded observations of the actual translated-cusp Eisenstein family. Their residues are the already constructed arithmetic theta model, sampled at the same Mobius transform.

  1. lemma OAI.CubicFirstMoment.cubicThetaIncoming_shifted_zero line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaRemainder_shifted line 27
  3. def OAI.CubicFirstMoment.cubicThetaCompactShiftedFamily line 36
  4. lemma OAI.CubicFirstMoment.cubicThetaCompactShiftedFamily_meromorphic line 41
  5. lemma OAI.CubicFirstMoment.cubicThetaCompactShiftedFamily_right line 47
  6. lemma OAI.CubicFirstMoment.cubicThetaCompactShiftedFamily_residue line 67
  7. lemma OAI.CubicFirstMoment.cubicThetaCompactShiftedResidue_model line 88