OAI/NumberTheory/TwoPoint/ShortIntervals/MRTDyadicPrefix.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite halving of a prefix. The at most one omitted integer at each halving step is absorbed in the dyadic allowance, without counting the number of steps.

  1. theorem OAI.TwoPointCorrelations.mrt_dyadic_prefix_bound line 13