OAI/NumberTheory/CubicMoment/Theta/CubicThetaHilbertCompact.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactness of a diagonal cusp operator whose compact radial blocks tend to zero in operator norm.

  1. theorem OAI.CubicFirstMoment.cubicThetaHilbertDiagonal_compact line 13