OAI/NumberTheory/TwoPoint/Bounds/AmbientTupleLabels.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual tuple slots have the same equality pattern in the ambient prime pool and column coordinates.

  1. lemma OAI.TwoPointCorrelations.columnPrimeValue_injective line 14
  2. lemma OAI.TwoPointCorrelations.tuple_label_eq_iff line 25
  3. lemma OAI.TwoPointCorrelations.tuple_label_singletonSlots line 36
  4. lemma OAI.TwoPointCorrelations.tuple_label_singleton_count line 50
  5. lemma OAI.TwoPointCorrelations.tuple_label_perfectRows line 62
  6. lemma OAI.TwoPointCorrelations.tuple_label_reciprocal line 70
  7. theorem OAI.TwoPointCorrelations.designatedReciprocal_le_tuple line 88