LowRankColumnEncoding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Low-rank lit departures give a full code for the actual short-block column.

def OAI.TwoPointCorrelations.imperfectColumnCount line 16
theorem OAI.TwoPointCorrelations.imperfectColumnCount_le line 19
def OAI.TwoPointCorrelations.ShortColumnGeometry line 24
Source documentation
The geometric conclusions required on every actual short perfect block.
```
def ShortColumnGeometry (label : Fin n → α) (hn : 0 < n)
    (coefficient : ℕ → ℝ) (perfect : Finset (Fin n)) (s : ℕ) : Prop :=
…
```

theorem OAI.TwoPointCorrelations.low_rank_short_column_code line 40

Source documentation

Only actual lit departures enter the low-rank premise. The short blocks and their complete decoder are constructed, not supplied as data.

theorem low_rank_short_column_code (label : Fin n → α) (hn : 0 < n)
    (coefficient : ℕ → ℝ) (perfect : Finset (Fin n)) (s r : ℕ) (hs : 0 < s)
    (hno : ∀ S : Finset (EqualLabelPairs (fun i : perfect => label i.val)), S.card = r →
      ¬LinearIndependent ℝ (pairFamily (labelPairVectors (fun i : perfect => label i.val)
        (fun i => formalDeparture (columnNatLabel label hn) coefficient i.val.val)) S))
    (hgeometry : ShortColumnGeometry label hn coefficient perfect s) :
    ∃ omittedLabels blocks segments omittedRuns : ℕ,
      omittedLabels < 2 * r ∧
      blocks ≤ n / s + imperfectColumnCount perfect + 1 ∧
      segments ≤ (omittedLabels + 1) * blocks ∧
      omittedRuns ≤ omittedLabels * blocks ∧
      segments ≤ n ∧ omittedRuns ≤ n ∧
…

Mentions: OAI.TwoPointCorrelations.EqualLabelPairs, OAI.TwoPointCorrelations.pairFamily, OAI.TwoPointCorrelations.labelPairVectors, OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.columnNatLabel, OAI.TwoPointCorrelations.ShortColumnGeometry, OAI.TwoPointCorrelations.imperfectColumnCount