OAI/NumberTheory/TwoPoint/Bounds/WeightedRetainedBins.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Real bin endpoints introduce factors floor(T)/T of norm at most one. The per-bin spectral bounds remain valid with these factors.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_weighted_bin_sum_uniform line 13