OAI/NumberTheory/TwoPoint/Bounds/ComplexBinWindows.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Enlarging a closed-low logarithmic bin by one bin on its left gives the strict-low convention in the rough-shift theorem.

  1. def OAI.TwoPointCorrelations.enlargedBinStart line 10
  2. lemma OAI.TwoPointCorrelations.enlargedBinStart_pos line 13
  3. lemma OAI.TwoPointCorrelations.enlarged_partial_bin_window line 17
  4. lemma OAI.TwoPointCorrelations.enlargedBinStart_upper line 36
  5. lemma OAI.TwoPointCorrelations.rough_bin_forces_start_lower line 45