OAI/NumberTheory/CubicMoment/Theta/CubicThetaSectionPairing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The scalar Hermitian pairing of two actual automorphic sections descends to the quotient and agrees with the L2 inner product.

  1. def OAI.CubicFirstMoment.cubicThetaSectionPairing line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaSectionPairing_invariant line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaSectionPairing_apply line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaSectionPairing_continuous line 30
  5. lemma OAI.CubicFirstMoment.cubicThetaSectionPairing_support line 38
  6. lemma OAI.CubicFirstMoment.cubicThetaSectionPairing_L2 line 47