OAI/Combinatorics/RamseyFive/Geometry/GeometricRestriction.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ProjectiveRestriction.Domain line 14
  2. def OAI.SharpRamseyFive.ProjectiveRestriction.image line 16
  3. lemma OAI.SharpRamseyFive.ProjectiveRestriction.image_eq_iff line 19
  4. def OAI.SharpRamseyFive.ProjectiveRestriction.normalized line 24
  5. lemma OAI.SharpRamseyFive.ProjectiveRestriction.normalized_nonzero line 30
  6. lemma OAI.SharpRamseyFive.ProjectiveRestriction.mk_normalized line 37
  7. lemma OAI.SharpRamseyFive.ProjectiveRestriction.normalized_injective line 43
  8. lemma OAI.SharpRamseyFive.ProjectiveRestriction.affine_fiber_card_le line 52
  9. theorem OAI.SharpRamseyFive.ProjectiveRestriction.fiber_card_le line 71
  10. theorem OAI.SharpRamseyFive.ProjectiveRestriction.dual_restriction_fiber_card_le line 81
  11. lemma OAI.SharpRamseyFive.ProjectiveRestriction.incident_restriction line 98
  12. lemma OAI.SharpRamseyFive.ProjectiveRestriction.incident_of_zero_restriction line 114
  13. lemma OAI.SharpRamseyFive.ProjectiveRestriction.restriction_nonzero_of_degree_lt line 123
  14. def OAI.SharpRamseyFive.DyadicLifts.multiplicity line 141
  15. def OAI.SharpRamseyFive.DyadicLifts.bin line 144
  16. def OAI.SharpRamseyFive.DyadicLifts.restrictions line 147
  17. def OAI.SharpRamseyFive.DyadicLifts.enclosure line 150
  18. lemma OAI.SharpRamseyFive.DyadicLifts.multiplicity_pos line 153
  19. lemma OAI.SharpRamseyFive.DyadicLifts.multiplicity_mono line 157
  20. lemma OAI.SharpRamseyFive.DyadicLifts.bin_fiber line 161
  21. lemma OAI.SharpRamseyFive.DyadicLifts.bin_multiplicity_bounds line 174
  22. lemma OAI.SharpRamseyFive.DyadicLifts.bin_mass_bounds line 186
  23. lemma OAI.SharpRamseyFive.DyadicLifts.restrictions_subset_enclosure line 205
  24. lemma OAI.SharpRamseyFive.DyadicLifts.enclosure_mass line 213
  25. theorem OAI.SharpRamseyFive.DyadicLifts.exists_massive_bin line 224
  26. lemma OAI.SharpRamseyFive.ProjectiveRestriction.finite_lift_bound line 253
  27. theorem OAI.SharpRamseyFive.ProjectiveRestriction.exists_restriction_dyad line 271
  28. theorem OAI.SharpRamseyFive.FiniteRemoval.retain_card line 302
  29. theorem OAI.SharpRamseyFive.FiniteRemoval.large_cell_retains_half line 324
  30. def OAI.SharpRamseyFive.ProjectiveRestriction.flatDegree line 358
  31. def OAI.SharpRamseyFive.ProjectiveRestriction.goodLifts line 362
  32. def OAI.SharpRamseyFive.ProjectiveRestriction.nonzeroLifts line 366
  33. lemma OAI.SharpRamseyFive.ProjectiveRestriction.goodLifts_nonzero line 369
  34. lemma OAI.SharpRamseyFive.ProjectiveRestriction.card_nonzeroLifts line 378
  35. lemma OAI.SharpRamseyFive.ProjectiveRestriction.nonzeroLifts_mono line 383
  36. lemma OAI.SharpRamseyFive.ProjectiveRestriction.card_nonzeroLifts_le line 386
  37. lemma OAI.SharpRamseyFive.ProjectiveRestriction.restricted_flatDegree line 392
  38. lemma OAI.SharpRamseyFive.ProjectiveRestriction.restricted_degree_bound line 400
  39. lemma OAI.SharpRamseyFive.ProjectiveRestriction.reduced_incidence_bound line 411
  40. theorem OAI.SharpRamseyFive.ProjectiveRestriction.large_cell_restriction line 435
  41. lemma OAI.SharpRamseyFive.ProjectiveRestriction.logarithmic_gap_of_cross line 509
  42. lemma OAI.SharpRamseyFive.ProjectiveRestriction.restriction_product_loss line 522
  43. theorem OAI.SharpRamseyFive.ProjectiveRestriction.large_cell_pair_with_losses line 540