OAI/NumberTheory/CubicMoment/Decomposition/StoppedCubeScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary scales for the cube error of a bounded stopped row.

  1. lemma OAI.CubicFirstMoment.stopped_half_inverse_third line 9
  2. lemma OAI.CubicFirstMoment.stopped_log_ratio line 16
  3. lemma OAI.CubicFirstMoment.stopped_cube_error_scale line 22