OAI/NumberTheory/TwoPointCorrelations/DivisibilityPrefix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact change of variables x=u*z for a divisibility indicator, including the floor endpoint floor(X/u).

  1. lemma OAI.TwoPointCorrelations.positivePrefix_eq_Icc line 15

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/DivisibilityPrefix.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.divisibility_positivePrefix line 19

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/DivisibilityPrefix.lean:19 (same declaration text).