OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreArguments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The supported core indices and free primary factors give exactly the nonzero domain of the full dual sum, with all zero extensions retained.

  1. def OAI.CubicFirstMoment.cubicThetaCoreArgument line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaCoreArgument_injective line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaCoreArgument_range line 22
  4. def OAI.CubicFirstMoment.cubicThetaCoreFreeArgument line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaCoreFreeArgument_injective line 36
  6. theorem OAI.CubicFirstMoment.cubicTheta_core_free_tsum line 42