OAI/Combinatorics/SharpRamsey/Bounds/Lower.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transfer of finite prime-field graph constructions to all sufficiently large orders.

  1. def OAI.SharpLogRamsey.LowerTransfer.PrimeConstruction line 14
  2. theorem OAI.SharpLogRamsey.LowerTransfer.prime_interval line 19
  3. theorem OAI.SharpLogRamsey.LowerTransfer.witness_bound line 34
  4. theorem OAI.SharpLogRamsey.LowerTransfer.eventual_scale line 53
  5. theorem OAI.SharpLogRamsey.LowerTransfer.interval_bounds line 70
  6. theorem OAI.SharpLogRamsey.LowerTransfer.scalar_lower line 97
  7. theorem OAI.SharpLogRamsey.LowerTransfer.lower_from_prime_construction line 133
  8. theorem OAI.SharpLogRamsey.LowerTransfer.all_epsilon_lower line 166