OAI/NumberTheory/CubicMoment/Estimates/CoprimeUnitFrequency.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The sole zero-frequency contribution of coprime squarefree rows comes from the literal unit row.

  1. lemma OAI.CubicFirstMoment.gramDualTerm_unit_zero line 12
  2. lemma OAI.CubicFirstMoment.coprimePoissonDyad_unit_frequency line 16