OAI/NumberTheory/TwoPoint/Halasz/HalaszLargePrimeEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The large-extra-prime branch of the actual cofactor product. The only analytic premise here is the explicitly cited prime sparse input; the large-value sample count and set-integral transfer are proved.

  1. theorem OAI.TwoPointCorrelations.HalaszPrimeSparseInput.large_prime_product_energy line 16