OAI/NumberTheory/TwoPoint/Bounds/QuantitativeFinalWindows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The final logarithmic bins meet both the analytic and spectral long-window hypotheses, uniformly in the absolute exponent A.

  1. lemma OAI.TwoPointCorrelations.exp_neg_nat_lt_log_two line 12
  2. lemma OAI.TwoPointCorrelations.floor_exp_half_bound line 30
  3. lemma OAI.TwoPointCorrelations.final_bin_windows line 49
  4. theorem OAI.TwoPointCorrelations.eventually_quantitative_final_windows line 65
  5. lemma OAI.TwoPointCorrelations.final_log_scale_exact line 87
  6. lemma OAI.TwoPointCorrelations.final_log_scale_tendsto line 93