OAI/Combinatorics/RamseyFive/Geometry/RadialAlternatives.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.GlobalRadial.localLines_mass line 14
  2. lemma OAI.SharpRamseyFive.GlobalRadial.no_radial_exception_of_mass line 41
  3. lemma OAI.SharpRamseyFive.GlobalRadial.radial_exception_scale line 52
  4. lemma OAI.SharpRamseyFive.GlobalRadial.radial_exception_uniform line 69
  5. lemma OAI.SharpRamseyFive.ScoreGeometry.biUnion_card_real_le line 104
  6. def OAI.SharpRamseyFive.ScoreGeometry.strengthDyads line 112
  7. lemma OAI.SharpRamseyFive.ScoreGeometry.strengthDyads_card line 115
  8. lemma OAI.SharpRamseyFive.ScoreGeometry.boundedOverlapDyads_subset line 123
  9. def OAI.SharpRamseyFive.ScoreGeometry.radialExceptions line 132
  10. lemma OAI.SharpRamseyFive.ScoreGeometry.off_radialExceptions line 137
  11. theorem OAI.SharpRamseyFive.ScoreGeometry.radialExceptions_card line 146
  12. lemma OAI.SharpRamseyFive.ScoreScalars.radial_mass_of_scalar line 180
  13. lemma OAI.SharpRamseyFive.ScoreScalars.radial_small_strength line 192
  14. lemma OAI.SharpRamseyFive.ScoreScalars.radial_low_density line 211
  15. theorem OAI.SharpRamseyFive.ScoreGeometry.captured_radial_exception_bound line 228
  16. theorem OAI.SharpRamseyFive.ScoreGeometry.residual_radial_exception_bound line 287