OAI/NumberTheory/TwoPoint/Bounds/ActualColumnCatalog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Structural properties of the column fiber of actual closed matrix paths.

  1. lemma OAI.TwoPointCorrelations.singletonLabels_card_le_slots line 12
  2. lemma OAI.TwoPointCorrelations.actualColumnCatalog_pairs line 22
  3. lemma OAI.TwoPointCorrelations.actualColumnCatalog_chains line 36
  4. lemma OAI.TwoPointCorrelations.actualColumnCatalog_crude_cost line 55