OAI/NumberTheory/TwoPoint/Halasz/HalaszHyperbolaRows.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Row decomposition of the finite positive hyperbola.

  1. theorem OAI.TwoPointCorrelations.halasz_hyperbola_rows line 12

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszHyperbolaRows.lean:12 (same declaration text).