OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonLogSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The three proved common-factor costs give every logarithmic saving for polynomial coefficient length and the actual logarithmic roughness cutoff.

  1. theorem OAI.CubicFirstMoment.bounded_rough_divisor_common_log_saving line 14