OAI/NumberTheory/CubicMoment/Estimates/OuterDualBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summation of every dual frequency in the common-factor Gram kernel, with the unit zero mode explicitly subtracted.

  1. theorem OAI.CubicFirstMoment.coprimeGramForm_outer_dual_bound line 13