OAI/Combinatorics/SharpRamsey/Bounds/SumFiberCenter.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The off-diagonal Ramsey upper bound.

  1. theorem OAI.SharpLogRamsey.TriangleFree.sum_fiber_center line 17
  2. theorem OAI.SharpLogRamsey.TriangleFree.twice_sum_fiber_neighbors line 28
  3. def OAI.SharpLogRamsey.TriangleFree.Z line 43
  4. theorem OAI.SharpLogRamsey.TriangleFree.fiber_empty_of_not_admissible line 46
  5. theorem OAI.SharpLogRamsey.TriangleFree.sum_fiber_Z line 53
  6. theorem OAI.SharpLogRamsey.TriangleFree.exp_neg_log_two_mul line 62
  7. theorem OAI.SharpLogRamsey.TriangleFree.half_sum_exp_le_center line 67
  8. theorem OAI.SharpLogRamsey.TriangleFree.sum_Z_le_four_neighbors line 88
  9. theorem OAI.SharpLogRamsey.TriangleFree.sum_center line 108
  10. theorem OAI.SharpLogRamsey.TriangleFree.sum_neighbors line 112
  11. theorem OAI.SharpLogRamsey.TriangleFree.exp_mean_le line 134
  12. theorem OAI.SharpLogRamsey.TriangleFree.occupation_lower_bound line 144
  13. theorem OAI.SharpLogRamsey.TriangleFree.exists_occupation line 172
  14. theorem OAI.SharpLogRamsey.TriangleFree.indepNum_lower_bound line 252
  15. def OAI.SharpLogRamsey.Sampling.internalDegree line 271
  16. def OAI.SharpLogRamsey.Sampling.degreeMass line 274
  17. theorem OAI.SharpLogRamsey.Sampling.degreeMass_pair_sum line 276
  18. theorem OAI.SharpLogRamsey.Sampling.degreeMass_moment line 297
  19. theorem OAI.SharpLogRamsey.Sampling.exists_avoid_family line 325
  20. theorem OAI.SharpLogRamsey.Sampling.prune line 350
  21. theorem OAI.SharpLogRamsey.Sampling.induced_degree line 392
  22. theorem OAI.SharpLogRamsey.Sampling.sample_prune line 403
  23. theorem OAI.SharpLogRamsey.Sampling.triangle_count_le line 426