OAI/Combinatorics/RamseyFive/Probability/OwnFraction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.ScoreRegularity.cellMass_nonneg line 15
  2. lemma OAI.SharpRamseyFive.ScoreRegularity.cellMass_mono line 19
  3. lemma OAI.SharpRamseyFive.ScoreRegularity.cellMass_union line 24
  4. lemma OAI.SharpRamseyFive.ScoreRegularity.filter_sdiff_eq line 36
  5. lemma OAI.SharpRamseyFive.ScoreRegularity.cellMass_sdiff line 42
  6. lemma OAI.SharpRamseyFive.ScoreRegularity.cellMass_erase line 52
  7. lemma OAI.SharpRamseyFive.ScoreRegularity.typical_deviation line 76
  8. def OAI.SharpRamseyFive.ScoreRegularity.ownFraction line 82
  9. def OAI.SharpRamseyFive.ScoreRegularity.outsideMass line 85
  10. def OAI.SharpRamseyFive.ScoreRegularity.queryLoss line 88
  11. lemma OAI.SharpRamseyFive.ScoreRegularity.queryLoss_bounds line 92
  12. lemma OAI.SharpRamseyFive.ScoreRegularity.outsideMass_deviation line 102
  13. theorem OAI.SharpRamseyFive.ScoreRegularity.typical_mass_bounds line 122
  14. lemma OAI.SharpRamseyFive.ScoreRegularity.typical_variance_component line 157
  15. lemma OAI.SharpRamseyFive.ScoreRegularity.Q_le_two_pow line 185
  16. lemma OAI.SharpRamseyFive.ScoreRegularity.typical_pencil_card line 198
  17. lemma OAI.SharpRamseyFive.ScoreRegularity.queryLoss_square_sum line 214
  18. lemma OAI.SharpRamseyFive.ScoreRegularity.four_sq line 241
  19. theorem OAI.SharpRamseyFive.ScoreRegularity.typical_mass_variance line 244