OAI/NumberTheory/CubicMoment/Theta/CubicThetaEnergyRegularizer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

At every real spectral parameter below two the energy pencil admits an explicit compact correction which is invertible. This is the local Fredholm reduction used for continuation across the real axis.

  1. def OAI.CubicFirstMoment.cubicThetaEnergyRegularizer line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaEnergy_real_smul_inner line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaEnergyRegularizer_inner line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaEnergyRegularizer_unit line 41
  5. theorem OAI.CubicFirstMoment.cubicThetaEnergyPencil_compact_regularizer line 70