OAI/NumberTheory/CubicMoment/Theta/CubicThetaContinuedWeakEquation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At every regular parameter the continued inverse solves the actual global variational equation. The equation uses the completed gradient graph and is not an abstract substitute for the geometric Laplacian.

  1. def OAI.CubicFirstMoment.cubicThetaContinuedEnergyLift line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaContinuedEnergyLift_value line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaContinuedEnergyLift_equation line 23
  4. theorem OAI.CubicFirstMoment.cubicThetaContinuedEnergyLift_weak line 34