OAI/NumberTheory/TwoPoint/Bounds/ExtractedWindowScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An absolute long-interval scale survives extraction of every bounded padding divisor and every partial tuple product, including both floor operations.

  1. lemma OAI.TwoPointCorrelations.extracted_window_lower line 11