OAI/NumberTheory/TwoPoint/Bounds/SingletonCenteredCatalog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete singleton word contribution is bounded by the numerical witness catalog.

  1. theorem OAI.TwoPointCorrelations.singleton_centered_words_le_catalog line 13