OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedMiddleSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exactly two unit classes can contribute to the middle ramified row above a frequency congruent to one modulo lambda.

  1. def OAI.CubicFirstMoment.cubicThetaOmegaUnit line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaLambda_dvd_omega_pow_sub_one line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaThree_dvd_lambda_mul line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaRamifiedMiddleFactor_eq line 30
  5. lemma OAI.CubicFirstMoment.cubicThetaRamifiedMiddleFactor_norm_le line 52
  6. theorem OAI.CubicFirstMoment.cubicThetaRamifiedMiddleFactor_support line 61