OAI/NumberTheory/TwoPoint/Bounds/NearbyCutoffs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded positive-prefix mean changes little when the real cutoff is moved within one logarithmic bin.

  1. lemma OAI.TwoPointCorrelations.positivePrefix_sub_norm_le line 13
  2. lemma OAI.TwoPointCorrelations.real_prefix_nearby line 26
  3. lemma OAI.TwoPointCorrelations.real_prefix_log_bin line 62