ColumnPatternRecovery.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Pass from recovery of canonical names to the universal equality-pattern count.

def OAI.TwoPointCorrelations.decodeColumnPrefixPattern line 9
theorem OAI.TwoPointCorrelations.column_prefix_pattern_recovers line 13
theorem OAI.TwoPointCorrelations.card_column_prefix_patterns line 31
Source documentation
Restricting to the original column positions does not enlarge the coefficient-independent universe of patterns.
```
theorem card_column_prefix_patterns {n N S O I : ℕ} (hn : n ≤ N) :
    Nat.card (Set.range (@decodeColumnPrefixPattern n N S O I hn)) ≤
      2 ^ (6 * N + 1) * N ^ (2 * S + O + I) := by
…
```
Mentions: OAI.TwoPointCorrelations.decodeColumnPrefixPattern