OAI/Probability/SignedSweeps/WeightedNoIsolates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.finite_sum_le_of_injective line 12
  2. def OAI.SignedSweeps.NoIsolatedVertex line 33
  3. def OAI.SignedSweeps.noIsolatesWeight line 36
  4. lemma OAI.SignedSweeps.matching_univ line 39
  5. lemma OAI.SignedSweeps.noIsolatesWeight_le_matching_sum line 43
  6. lemma OAI.SignedSweeps.product_one_add_le_exp_sum line 93
  7. lemma OAI.SignedSweeps.noIsolatesWeight_bound line 100
  8. def OAI.SignedSweeps.fixedNoIsolatesWeight line 163
  9. lemma OAI.SignedSweeps.fixedNoIsolatesWeight_le line 167
  10. lemma OAI.SignedSweeps.fixedNoIsolatesWeight_smul line 178
  11. lemma OAI.SignedSweeps.weighted_noIsolates_fixed_card line 189
  12. theorem OAI.SignedSweeps.noIsolates_probability_bound line 221