OAI/NumberTheory/CubicMoment/Theta/CubicThetaExteriorEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The sharp exterior estimate extends by density to the actual closed automorphic energy space. Its remainders are compact operators already constructed from local Rellich compactness.

  1. theorem OAI.CubicFirstMoment.cubicThetaExterior_energy line 14