OAI/NumberTheory/TwoPoint/Halasz/HalaszOffCenterCofactor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual-band cofactor estimate on the entire off-center region, conditional only on the precisely cited high-frequency prime estimate.

  1. theorem OAI.TwoPointCorrelations.HalaszHighPrimeInput.actual_cofactor line 12