OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootFourierL2Bounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Each completed root Fourier projection is a contraction in the actual Hilbert norm.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootFourierL2_norm_le line 11