OAI/Combinatorics/SharpRamsey/Bounds/FromConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two-sided Ramsey bounds and the logarithmic limit from a prime-field construction.

  1. theorem OAI.SharpLogRamsey.mainLimit_of_mainBounds line 11
  2. theorem OAI.SharpLogRamsey.main_of_primeConstruction line 62