OAI/Combinatorics/MatchingCount/Probability/Tv.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Variation.tv line 13
  2. lemma OAI.MatchingFPRAS.Variation.tv_nonneg line 15
  3. lemma OAI.MatchingFPRAS.Variation.tv_symm line 18
  4. lemma OAI.MatchingFPRAS.Variation.tv_triangle line 22
  5. def OAI.MatchingFPRAS.Variation.event line 27
  6. lemma OAI.MatchingFPRAS.Variation.event_nonneg line 29
  7. theorem OAI.MatchingFPRAS.Variation.event_sub_le line 34
  8. def OAI.MatchingFPRAS.Variation.bind line 55
  9. lemma OAI.MatchingFPRAS.Variation.bind_nonneg line 58
  10. lemma OAI.MatchingFPRAS.Variation.bind_sum line 62
  11. lemma OAI.MatchingFPRAS.Variation.bind_contraction line 69
  12. lemma OAI.MatchingFPRAS.Variation.bind_perturbation line 81
  13. def OAI.MatchingFPRAS.Variation.push line 101
  14. lemma OAI.MatchingFPRAS.Variation.push_nonneg line 105
  15. lemma OAI.MatchingFPRAS.Variation.push_sum line 111
  16. lemma OAI.MatchingFPRAS.Variation.push_contraction line 114
  17. def OAI.MatchingFPRAS.Variation.tensor line 123
  18. lemma OAI.MatchingFPRAS.Variation.tensor_tv line 125
  19. lemma OAI.MatchingFPRAS.Variation.tv_equiv line 140
  20. def OAI.MatchingFPRAS.Variation.iid line 145
  21. lemma OAI.MatchingFPRAS.Variation.iid_nonneg line 148
  22. lemma OAI.MatchingFPRAS.Variation.iid_sum line 151
  23. theorem OAI.MatchingFPRAS.Variation.iid_tv line 156
  24. def OAI.MatchingFPRAS.Variation.product line 178
  25. lemma OAI.MatchingFPRAS.Variation.product_marginal line 180
  26. def OAI.MatchingFPRAS.Variation.sigmaLift line 212
  27. lemma OAI.MatchingFPRAS.Variation.sigmaLift_nonneg line 216
  28. lemma OAI.MatchingFPRAS.Variation.sigmaLift_sum line 220
  29. lemma OAI.MatchingFPRAS.Variation.sigmaLift_tv line 224
  30. def OAI.MatchingFPRAS.Transport.tierBound line 234
  31. lemma OAI.MatchingFPRAS.Transport.base_block line 236
  32. lemma OAI.MatchingFPRAS.Transport.tierBound_reaches line 247
  33. def OAI.MatchingFPRAS.Transport.ladderTier line 267
  34. lemma OAI.MatchingFPRAS.Transport.ladderTier_spec line 271
  35. lemma OAI.MatchingFPRAS.Transport.ladderTier_le line 276
  36. lemma OAI.MatchingFPRAS.Transport.ladderTier_min line 279
  37. lemma OAI.MatchingFPRAS.Transport.topClamp_eq line 282
  38. lemma OAI.MatchingFPRAS.FiniteChain.walk_nonneg line 300
  39. lemma OAI.MatchingFPRAS.FiniteChain.walk_sum line 306
  40. def OAI.MatchingFPRAS.Transport.topSlot line 330
  41. lemma OAI.MatchingFPRAS.Transport.topSlot_tier line 332
  42. lemma OAI.MatchingFPRAS.Transport.ladder_top_marginal line 335
  43. lemma OAI.MatchingFPRAS.Transport.slotWeight_top line 341
  44. def OAI.MatchingFPRAS.Enlargement.revealLaw line 368
  45. lemma OAI.MatchingFPRAS.Enlargement.sourceBagWeight_pos line 371
  46. lemma OAI.MatchingFPRAS.Enlargement.revealLaw_ideal line 376
  47. lemma OAI.MatchingFPRAS.Enlargement.revealLaw_tv line 398
  48. theorem OAI.MatchingFPRAS.Enlargement.source_marked_sampling line 415