TupleColumnCover.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Apply the numerical forest cover simultaneously to all actual tuple columns.

def OAI.TwoPointCorrelations.ColumnLowRank line 12

theorem OAI.TwoPointCorrelations.tuple_column_array_cover line 24

Source documentation

A surviving lit numerical word supplies one member of the fixed joint code universe. Its assumptions are the actual low-rank and arithmetic conditions; no combinatorial covering assumption is made.

theorem tuple_column_array_cover {J R : ℕ} (P : Fin J → Finset ℕ)
    (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
    (forward : Fin R → Bool) (padding : Fin R → ℕ)
    (hprime : ∀ j, ∀ p ∈ P j, p.Prime)
    (hdisjoint : ∀ j l, l ≠ j → Disjoint (P j) (P l))
    {h s r : ℕ} {supply : ℕ → ℕ → Prop} {x : ℤ} (hh : 0 < h) (hs : 0 < s)
    (perfect : Finset (Fin R)) (cut : Fin R)
    (hlit : ∀ i ∈ perfect, ((padding i : ℤ) * columnTuple w i) ∣
      x + wordDisplacement h ((columnTupleWord w forward padding).take i.val))
    (heligible : ∀ a ∈ columnTupleWord w forward padding, supply a.tuple a.padding)
    (hq : ∀ a ∈ columnTupleWord w forward padding, 0 < a.padding)
    (hsq : ∀ a ∈ columnTupleWord w forward padding, Squarefree a.tuple)
…

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