OAI/NumberTheory/TwoPoint/Bounds/ActualSlotClasses.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual squarefree prime occurrences satisfy the code's class conditions.

  1. lemma OAI.TwoPointCorrelations.PrimeSlotData.code_value_injective line 17
  2. lemma OAI.TwoPointCorrelations.PrimeSlotData.code_value_image line 30
  3. lemma OAI.TwoPointCorrelations.PrimeSlotData.code_kindConsistent line 41
  4. lemma OAI.TwoPointCorrelations.PrimeSlotData.code_rowInjective line 47
  5. lemma OAI.TwoPointCorrelations.actualSlot_eq_of_data line 60
  6. lemma OAI.TwoPointCorrelations.actualSlot_kind_of_prime line 71
  7. theorem OAI.TwoPointCorrelations.actualPrimeSlotData_code_kindConsistent line 85
  8. theorem OAI.TwoPointCorrelations.actualPrimeSlotData_code_rowInjective line 92