OAI/NumberTheory/CubicMoment/Theta/CubicThetaC1Pairing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The sesquilinear differential pairing descends to the arithmetic quotient; its value is independent of the measurable frame choice.

  1. lemma OAI.CubicFirstMoment.cubicThetaC1Gradient_norm_invariant line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaC1Gradient_inner_invariant line 20
  3. def OAI.CubicFirstMoment.cubicThetaC1Pairing line 44
  4. lemma OAI.CubicFirstMoment.cubicThetaC1Pairing_apply line 48
  5. lemma OAI.CubicFirstMoment.cubicThetaC1Pairing_continuous line 59
  6. lemma OAI.CubicFirstMoment.cubicThetaC1Pairing_representative line 70
  7. lemma OAI.CubicFirstMoment.cubicThetaChart_complex_integral line 79