OAI/NumberTheory/CubicMoment/Theta/CubicThetaTorusCellTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact measurable transport between the arithmetic period cell and the torus. This also applies to measurable L2 representatives.

  1. def OAI.CubicFirstMoment.cubicThetaTorusCellPoint line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaTorusCellPoint_embedding line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaTorusCellPoint_map line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaTorusCellPoint_character line 50
  5. lemma OAI.CubicFirstMoment.cubicThetaTorusCellPoint_memLp line 60
  6. lemma OAI.CubicFirstMoment.cubicThetaTorusCellPoint_integral line 67