OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticWeakDefect.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A continuous additive defect for the literal arithmetic weak PDE. Its vanishing can be glued and passed to the energy completion.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticWeakDefect line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticWeakDefect_continuous line 29
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticWeakDefect_C1 line 40
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticWeakDefect_coordinate line 60