PerfectRows.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The imperfect-row budget comes from actual singleton and unlit slots.

lemma OAI.TwoPointCorrelations.singleton_slot_count line 14
lemma OAI.TwoPointCorrelations.unlit_slot_count line 29
def OAI.TwoPointCorrelations.PerfectRow line 48
Source documentation
Every slot in a perfect row is lit and belongs to a nonsingleton label.
```
def PerfectRow (label : Fin n × Fin J → ι) (lit : Fin n × Fin J → Bool)
    (r : Fin n) : Prop :=
…
```
theorem OAI.TwoPointCorrelations.imperfect_rows_le_singletons_add_unlit line 54
Source documentation
Charge a bad row to one singleton slot or one unlit nonsingleton slot. The image under the row projection can only decrease cardinality.
```
theorem imperfect_rows_le_singletons_add_unlit (label : Fin n × Fin J → ι)
    (lit : Fin n × Fin J → Bool) :
    (univ.filter (fun r : Fin n => ¬PerfectRow label lit r)).card ≤
      (singletonLabels label).card +
        ∑ i : nonsingletonLabels label, (unlitOccurrences label lit i.val).card := by
…
```
Mentions: OAI.TwoPointCorrelations.PerfectRow, OAI.TwoPointCorrelations.singletonLabels, OAI.TwoPointCorrelations.nonsingletonLabels, OAI.TwoPointCorrelations.unlitOccurrences