OAI/NumberTheory/TwoPoint/Halasz/HalaszNearActualScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Near-frequency energy with the single actual scale L=log N. The density and mean-value thresholds are taken independently before this diagonal specialization.

  1. theorem OAI.TwoPointCorrelations.halasz_band_near_actual_scale line 15
  2. lemma OAI.TwoPointCorrelations.halasz_center_window_room line 83
  3. theorem OAI.TwoPointCorrelations.halasz_near_restricted_actual_scale line 109