OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinatePairing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic tangent inner product is the literal three-coordinate sesquilinear sum. This fixes the local normalization of the weak form.

  1. lemma OAI.CubicFirstMoment.cubicThetaLinear_inner_of_norm_eq line 13
  2. def OAI.CubicFirstMoment.cubicThetaTangentValues line 23
  3. def OAI.CubicFirstMoment.cubicThetaCoordinateValues line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaTangentValues_norm line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaTangentValues_inner line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaSectionGradient_pair_coordinates line 49