OAI/NumberTheory/CubicMoment/Theta/CubicThetaC1PairingIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quotient integration of the actual differential pairing agrees with the Hilbert L2 inner product. Compact tests give compact support.

  1. lemma OAI.CubicFirstMoment.cubicThetaC1Pairing_compact line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaC1Pairing_integrable line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaC1Pairing_L2 line 33