OAI/NumberTheory/CubicMoment/Theta/CubicThetaExceptionalProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite exceptional eigenspace has an actual orthogonal projection. Adding it to the self-adjoint real pencil removes its kernel.

  1. instance OAI.CubicFirstMoment.cubicThetaEnergyPencil_ker_complete line 11
  2. def OAI.CubicFirstMoment.cubicThetaExceptionalProjection line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaEnergyPencil_selfAdjoint line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaExceptionalProjection_compact line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaProjectedPencil_injective line 39
  6. theorem OAI.CubicFirstMoment.cubicThetaProjectedPencil_unit line 64