OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateEnergyClosure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact C1 coordinate function supported in one injective chart belongs to the actual closed global energy graph, by explicit smoothing.

  1. theorem OAI.CubicFirstMoment.cubicThetaCoordinateData_mem_energy line 13