OAI/NumberTheory/CubicMoment/Theta/CubicThetaEllipticTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed points give a trace bound by transporting to the base point. These are explicit matrix calculations for the actual hyperbolic action.

  1. lemma OAI.CubicFirstMoment.cubicThetaBaseFixed_row_norms line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaBaseFixed_trace_norm line 29
  3. lemma OAI.CubicFirstMoment.cubicThetaBaseFixed_trace_two line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaMatrixTrace_conjugate line 70
  5. lemma OAI.CubicFirstMoment.cubicThetaFixed_trace_norm line 79
  6. lemma OAI.CubicFirstMoment.cubicThetaFixed_trace_two line 84