OAI/NumberTheory/CubicMoment/Theta/CubicThetaC1Energy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The value and differential of compact C1 sections define genuine L2 data. Smooth approximation will place these data in the energy graph.

  1. lemma OAI.CubicFirstMoment.cubicThetaC1Differential_automorphy line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaC1Energy_invariant line 39
  3. lemma OAI.CubicFirstMoment.cubicThetaC1Energy_continuous line 56