OAI/NumberTheory/TwoPoint/Halasz/HalaszLogWeights.lean
2 declarations, 0 contain sorry, 0 declared as axioms
The three competing degree weights for the logarithmic phase.
- lemma
OAI.TwoPointCorrelations.halasz_log_weight_identityline 11 - lemma
OAI.TwoPointCorrelations.halasz_normalized_weight_productline 28