OAI/Combinatorics/IndependentSets/Reduction/SwapOccurrence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.swapOccurrence line 10
  2. lemma OAI.LargeIndependentSets.swapOccurrence_involutive line 14
  3. lemma OAI.LargeIndependentSets.expect_update line 22
  4. lemma OAI.LargeIndependentSets.expect_indicator line 29
  5. theorem OAI.LargeIndependentSets.separated_lists_probability line 34
  6. def OAI.LargeIndependentSets.ListsSeparated line 53
  7. lemma OAI.LargeIndependentSets.all_separated_probability line 56
  8. lemma OAI.LargeIndependentSets.LayerLaw.badMass_le_one line 93
  9. lemma OAI.LargeIndependentSets.good_pair_probability line 101
  10. lemma OAI.LargeIndependentSets.separated_cut line 123
  11. theorem OAI.LargeIndependentSets.source_lists_probability line 135