OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeLowerValue.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The lower-chart value is a genuine function modulo p^3. Its scaled versions descend to the smaller residue rings used in the valuation split.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrincipalLower_add line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrincipalLower_zero line 21
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerValue line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerValue_congr line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerValue_scaled_congr line 46
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerValue_canonical line 55
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerValue_zero line 63