OAI/NumberTheory/TwoPoint/Bounds/ComplexBinSummation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum arbitrary complex directed bins against their actual reciprocal divisor mass.

  1. def OAI.TwoPointCorrelations.canonicalComplexPrefix line 14
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_complex_bin_sum line 27