OAI/NumberTheory/CubicMoment/Theta/CubicThetaSmoothWeakDefect.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A continuous weak defect for an actual smooth section and its compact forcing. This will pass the coordinate equation to the energy closure.

  1. def OAI.CubicFirstMoment.cubicThetaSmoothWeakDefect line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSmoothWeakDefect_continuous line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaSmoothWeakDefect_C1 line 35
  4. lemma OAI.CubicFirstMoment.cubicThetaSmoothWeakDefect_coordinate line 53