OAI/NumberTheory/TwoPoint/Walks/TupleColumnWords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Each actual tuple word has the one-column resampling form used by the forest proof.

  1. def OAI.TwoPointCorrelations.cyclicIndex line 13
  2. lemma OAI.TwoPointCorrelations.cyclicIndex_val line 16
  3. def OAI.TwoPointCorrelations.columnTuple line 21
  4. def OAI.TwoPointCorrelations.columnTupleWord line 24
  5. def OAI.TwoPointCorrelations.tupleColumnPattern line 28
  6. lemma OAI.TwoPointCorrelations.tupleColumnPattern_label line 37
  7. lemma OAI.TwoPointCorrelations.columnTuple_split line 43
  8. lemma OAI.TwoPointCorrelations.tupleColumnPattern_step line 48
  9. lemma OAI.TwoPointCorrelations.tupleColumnPattern_word line 55
  10. lemma OAI.TwoPointCorrelations.tupleColumnPattern_not_dvd_other line 67

    Source documentation

    Disjoint column pools ensure the resampled prime cannot divide any of the fixed other-column coefficients.

    lemma tupleColumnPattern_not_dvd_other {J R : ℕ} {P : Fin J → Finset ℕ}
    (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
    (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J)
    (hprime : ∀ l, ∀ p ∈ P l, p.Prime) (hdisjoint : ∀ l, l ≠ j → Disjoint (P j) (P l)) :
    ∀ p : P j, ∀ t < R,
      ¬p.val ∣ (tupleColumnPattern w hR forward padding j).otherColumns t := by
…

    Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.tupleColumnPattern