OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveContraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The slit resolvent of a positive Hilbert-space contraction. This common argument is used for the constant block and the full cusp operator; it does not require compactness of the constant block.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveContraction_unit line 13