OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticGlobalWeak.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite arithmetic chart reconstruction and continuity extend the literal remainder's weak equation to every global energy test.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticWeakDefect_compact line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticWeakDefect_energy line 64
  3. theorem OAI.CubicFirstMoment.cubicThetaArithmetic_global_weak line 78