OAI/NumberTheory/TwoPoint/Bounds/QualitativeCanonicalCentering.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual canonical nonraw complex bins: the cost of every padding dilation is summed against its exact reciprocal law.

  1. lemma OAI.TwoPointCorrelations.nonrawComplexBin_real_denominator line 16
  2. theorem OAI.TwoPointCorrelations.qualitative_canonical_nonraw_bin line 36