OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactC1Energy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every compact C1 automorphic section belongs to the actual closed energy graph, by finite reconstruction from smoothed coordinate pieces.

  1. theorem OAI.CubicFirstMoment.cubicThetaCompactC1_mem_energy line 14