OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateSectionNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The norm of a periodized C1 coordinate function is exactly its local hyperbolic energy integral when its support lies in one chart.

  1. lemma OAI.CubicFirstMoment.cubicThetaCoordinateSection_norm_sq line 15