OAI/Probability/SignedSweeps/IndependentNetworks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.subsetFiber line 14
  2. lemma OAI.SignedSweeps.mem_subsetFiber line 19
  3. def OAI.SignedSweeps.subsetFiberEquiv line 22
  4. lemma OAI.SignedSweeps.subset_iff_fibers line 29
  5. lemma OAI.SignedSweeps.card_subset_fibers line 37
  6. def OAI.SignedSweeps.independentSubsetLaw line 43
  7. lemma OAI.SignedSweeps.independentSubsetLaw_nonneg line 46
  8. lemma OAI.SignedSweeps.independentSubsetLaw_mass line 50
  9. lemma OAI.SignedSweeps.independentSubsetLaw_card_support line 55
  10. lemma OAI.SignedSweeps.independentSubsetLaw_upper_inclusion line 65
  11. lemma OAI.SignedSweeps.network_weight_product line 76
  12. lemma OAI.SignedSweeps.independentSubsetLaw_inclusion_bound line 87
  13. def OAI.SignedSweeps.independentSweptLaw line 110
  14. lemma OAI.SignedSweeps.independentSweptLaw_nonneg line 113
  15. lemma OAI.SignedSweeps.independentSweptLaw_mass line 117
  16. lemma OAI.SignedSweeps.independentSweptLaw_card_support line 123
  17. lemma OAI.SignedSweeps.independentSweptLaw_upper_inclusion line 129
  18. theorem OAI.SignedSweeps.swept_network_noIsolates_bound line 136