OAI/NumberTheory/CubicMoment/Estimates/LowCommonSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the literal common-factor blocks costs a convergent arithmetic series, without a power of the short-variable length.

  1. theorem OAI.CubicFirstMoment.ProfileControl.low_common_sum_height_log_saving line 13