OAI/NumberTheory/TwoPoint/Walks/TupleWordPrimeSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Match the tuple/padding reciprocal factors to the full numerical word support.

  1. def OAI.TwoPointCorrelations.tuplePrimeSupport line 14
  2. lemma OAI.TwoPointCorrelations.mem_tuplePrimeSupport line 18
  3. lemma OAI.TwoPointCorrelations.tuplePrimeSupport_reciprocal line 28
  4. lemma OAI.TwoPointCorrelations.tupleWord_primeSupport line 45
  5. lemma OAI.TwoPointCorrelations.tupleWord_reciprocal line 74
  6. theorem OAI.TwoPointCorrelations.columnTupleWord_injective line 87

    Source documentation

    Fixed signs and the numerical step list recover every tuple column and every padding. Thus the full-word counting bound applies injectively to the actual matrix-word catalog.

    theorem columnTupleWord_injective {J R : ℕ} {P : Fin J → Finset ℕ}
    (forward : Fin R → Bool) (hprime : ∀ j, ∀ p ∈ P j, p.Prime)
    (hdisjoint : ∀ j l, l ≠ j → Disjoint (P j) (P l)) :
    Function.Injective (fun a : ColumnPrimeAssignment J R P × (Fin R → ℕ) =>
      columnTupleWord a.1 forward a.2) := by
…

    Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.columnTupleWord