OAI/NumberTheory/CubicMoment/Estimates/DivisorRowEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The total energy of all rows in the genuine coprimality expansion. Every coefficient occurs once per squarefree primary divisor, so the loss is bounded by an arbitrarily small norm power.

  1. lemma OAI.CubicFirstMoment.prime_subset_divisor_count line 14
  2. theorem OAI.CubicFirstMoment.divisor_row_energy_small_power line 28