OAI/NumberTheory/CubicMoment/Theta/CubicThetaC1ChartNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full energy norm of a compact C1 section supported in an injective chart equals its literal integral over that covering sheet.

  1. lemma OAI.CubicFirstMoment.cubicThetaC1EnergyData_chart_norm line 12