OAI/NumberTheory/TwoPoint/Bounds/ObservedReciprocalBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extra-reciprocal estimates require the lower prime bound only on used tuple coordinates.

  1. lemma OAI.TwoPointCorrelations.designation_sdiff_decidable line 12
  2. theorem OAI.TwoPointCorrelations.full_word_designated_reciprocal_bound_on_support line 19