OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveGramDiagonal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The diagonal part of the literal finite-row Gram expansion.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveSeed_mul_strip line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPositiveProfileGram_zeroRow line 30