OAI/NumberTheory/CubicMoment/Theta/CubicThetaStripRepresentative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A measurable coordinate representative of every actual cusp L2 vector, with its first and second moment densities on the literal cell.

  1. def OAI.CubicFirstMoment.cubicThetaStripRepresentative line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaStripRepresentative_coordinates line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaStripRepresentative_measurable line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaStripRepresentative_integrable line 24
  5. lemma OAI.CubicFirstMoment.cubicThetaStripRepresentative_sq_integrable line 37
  6. lemma OAI.CubicFirstMoment.cubicThetaStripRepresentative_pair_integrable line 51
  7. theorem OAI.CubicFirstMoment.cubicThetaStripRepresentative_pairing line 64