OAI/NumberTheory/TwoPoint/Bounds/ActualPrimeSlots.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual prime factors give a complete bounded-slot code for a numerical word.

  1. abbrev OAI.TwoPointCorrelations.ActualPrimeSlot line 15
  2. def OAI.TwoPointCorrelations.actualSlotPrime line 18
  3. def OAI.TwoPointCorrelations.actualSlotKind line 23
  4. lemma OAI.TwoPointCorrelations.actualSlotPrime_prime line 28
  5. lemma OAI.TwoPointCorrelations.actualPrimeSlot_card_ge line 34
  6. theorem OAI.TwoPointCorrelations.actualPrimeSlot_card_le line 41
  7. def OAI.TwoPointCorrelations.actualPrimeSlotEquiv line 52
  8. def OAI.TwoPointCorrelations.actualPrimeSlotData line 56
  9. lemma OAI.TwoPointCorrelations.actualSlot_factor line 63
  10. lemma OAI.TwoPointCorrelations.actualPrimeSlotData_factor line 82
  11. theorem OAI.TwoPointCorrelations.actualPrimeSlotData_word line 100
  12. theorem OAI.TwoPointCorrelations.actual_word_code line 113

    Source documentation

    The explicit crude code and one number per observed prime class recover both factors of every step in the original word.

    theorem actual_word_code (w : Fin R → SignedStep)
    (ht : ∀ i, Squarefree (w i).tuple) (hq : ∀ i, Squarefree (w i).padding) :
    ∃ c : CrudeWordCode R (Fintype.card (ActualPrimeSlot w)) R,
      ∃ value : c.usedClasses → ℕ, c.numericalWord value = List.ofFn w := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.CrudeWordCode, OAI.TwoPointCorrelations.ActualPrimeSlot