OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveStripRepresentative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative_coordinates line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative_measurable line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative_integrable line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative_sq_integrable line 40
  6. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative_pair_integrable line 54
  7. theorem OAI.CubicFirstMoment.cubicThetaPositiveStripRepresentative_pairing line 67