OAI/Combinatorics/RamseyFive/Geometry/Outside.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ScoreGeometry.outsideAt line 18
  2. def OAI.SharpRamseyFive.ScoreGeometry.radialWeight line 21
  3. def OAI.SharpRamseyFive.ScoreGeometry.pencilLines line 25
  4. lemma OAI.SharpRamseyFive.ScoreGeometry.mass_inFlat line 28
  5. lemma OAI.SharpRamseyFive.ScoreGeometry.mass_pencil line 36
  6. lemma OAI.SharpRamseyFive.ScoreGeometry.mass_overlap line 42
  7. lemma OAI.SharpRamseyFive.ScoreGeometry.weight_pos_lower line 53
  8. lemma OAI.SharpRamseyFive.ScoreGeometry.overlap_pos_lower line 63
  9. lemma OAI.SharpRamseyFive.ScoreGeometry.one_anchor_count line 78
  10. lemma OAI.SharpRamseyFive.ScoreGeometry.two_anchor_count line 94
  11. lemma OAI.SharpRamseyFive.ScoreGeometry.pencil_size line 111
  12. lemma OAI.SharpRamseyFive.ScoreGeometry.submodule_eq_ker_annihilator line 126
  13. lemma OAI.SharpRamseyFive.ScoreGeometry.kernel_injective line 138
  14. lemma OAI.SharpRamseyFive.ScoreGeometry.mass_pairPoints line 145
  15. lemma OAI.SharpRamseyFive.ScoreGeometry.distinctPairs_ext line 154
  16. lemma OAI.SharpRamseyFive.ScoreGeometry.pair_strength_count_le line 162
  17. theorem OAI.SharpRamseyFive.ScoreGeometry.score_pair_count_four line 194