OAI/NumberTheory/CubicMoment/Theta/CubicThetaPointC1TraceIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The gradient trace adjoint on the actual finite cover, obtained from the pointwise isometry identity and justified finite integration.

  1. theorem OAI.CubicFirstMoment.cubicThetaPointC1Trace_gradient_integral line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPointC1Pair_flip line 31
  3. theorem OAI.CubicFirstMoment.cubicThetaPointC1Trace_gradient_integral_left line 44