OAI/NumberTheory/CubicMoment/Theta/CubicThetaSmoothGlobalWeak.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite compact chart reconstruction and energy completion turn the actual smooth pointwise equation into the global weak equation.

  1. lemma OAI.CubicFirstMoment.cubicThetaSmoothWeakDefect_compact line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSmoothWeakDefect_energy line 67
  3. theorem OAI.CubicFirstMoment.cubicThetaSmooth_global_weak line 85