OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Common-factor geometry and energy for the literal stopped row. Zero coefficients are allowed on the ambient support: roughness is used only after finding an active coefficient.

  1. lemma OAI.CubicFirstMoment.rough_small_common_coefficient_zero line 17
  2. theorem OAI.CubicFirstMoment.bounded_common_energy_log line 34
  3. theorem OAI.CubicFirstMoment.stopped_common_energy_log line 63
  4. theorem OAI.CubicFirstMoment.stopped_early_common_block_zero line 89