OAI/Combinatorics/SharpRamsey/Bounds/SamplingParameter.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The off-diagonal Ramsey upper bound.

  1. theorem OAI.SharpLogRamsey.Upper.sampling_parameter line 17
  2. theorem OAI.SharpLogRamsey.Upper.alteration_bound line 66
  3. theorem OAI.SharpLogRamsey.Upper.graph_recurrence line 131
  4. theorem OAI.SharpLogRamsey.Upper.ramsey_recurrence line 187
  5. theorem OAI.SharpLogRamsey.Upper.ramsey_three line 200
  6. theorem OAI.SharpLogRamsey.Upper.eventually_log_pow_le_sqrt line 233
  7. theorem OAI.SharpLogRamsey.Upper.ramsey_upper_scaled line 245
  8. theorem OAI.SharpLogRamsey.Upper.ramsey_upper line 295