OAI/NumberTheory/TwoPoint/Bounds/QuantitativeCenteringAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The quantitative centering estimate for the same numerical bins used by the spectral and deletion bounds.

  1. def OAI.TwoPointCorrelations.progressionLiouvilleMean line 14
  2. def OAI.TwoPointCorrelations.canonicalRawBin line 18
  3. theorem OAI.TwoPointCorrelations.quantitative_centering_assembly line 23