OAI/NumberTheory/TwoPoint/Halasz/HalaszTypicalCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact dyadic atypical count in terms of the translated probability used by the proved MRT density theorem.

  1. lemma OAI.TwoPointCorrelations.halasz_typical_dyadic_count line 14
  2. lemma OAI.TwoPointCorrelations.halasz_typical_dyadic_density_bound line 48