OAI/NumberTheory/TwoPoint/Halasz/HalaszBandDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Literal natural-indexed MRT bands in the dyadic density and pairwise-disjointness interfaces used by the energy estimates.

  1. lemma OAI.TwoPointCorrelations.halasz_actual_bands_disjoint line 14
  2. theorem OAI.TwoPointCorrelations.halasz_actual_band_density line 23