OAI/Combinatorics/MatchingCount/Graphs/Marked.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.Marking.Marked line 16
  2. def OAI.MatchingFPRAS.Marking.mass line 18
  3. def OAI.MatchingFPRAS.Marking.collapse line 21
  4. lemma OAI.MatchingFPRAS.Marking.sum_marks line 24
  5. theorem OAI.MatchingFPRAS.Marking.total_mass line 31
  6. lemma OAI.MatchingFPRAS.Marking.mass_nonneg line 37
  7. def OAI.MatchingFPRAS.Marking.law line 40
  8. lemma OAI.MatchingFPRAS.Marking.law_nonneg line 44
  9. lemma OAI.MatchingFPRAS.Marking.law_sum line 51
  10. lemma OAI.MatchingFPRAS.Marking.law_marginal line 56
  11. lemma OAI.MatchingFPRAS.Marking.pattern_sum line 62
  12. lemma OAI.MatchingFPRAS.Marking.allReal_mean line 74
  13. def OAI.MatchingFPRAS.Marking.completionEquiv line 97
  14. lemma OAI.MatchingFPRAS.Marking.completion_sum line 111
  15. def OAI.MatchingFPRAS.Marking.conditional line 116
  16. lemma OAI.MatchingFPRAS.Marking.conditional_sum line 120
  17. lemma OAI.MatchingFPRAS.Marking.law_from_reveal line 130
  18. lemma OAI.MatchingFPRAS.Marking.fixed_pattern_mass line 141
  19. lemma OAI.MatchingFPRAS.Marking.sum_if_subtype line 157
  20. lemma OAI.MatchingFPRAS.Marking.fixed_pattern_sum line 165
  21. theorem OAI.MatchingFPRAS.Marking.fixed_probe_mean line 186
  22. def OAI.MatchingFPRAS.Enlargement.frozenActivity line 225
  23. def OAI.MatchingFPRAS.Enlargement.frozenPortion line 231
  24. def OAI.MatchingFPRAS.Enlargement.sourceC line 234
  25. lemma OAI.MatchingFPRAS.Enlargement.sourceC_pos line 238
  26. lemma OAI.MatchingFPRAS.Enlargement.frozenPortion_partition line 242
  27. lemma OAI.MatchingFPRAS.Enlargement.frozenPortion_full line 254
  28. lemma OAI.MatchingFPRAS.Enlargement.frozenPortion_probe line 259
  29. lemma OAI.MatchingFPRAS.Enlargement.profile_reweight line 272
  30. def OAI.MatchingFPRAS.Enlargement.rawReweight line 281
  31. def OAI.MatchingFPRAS.Enlargement.bagReweight line 284
  32. lemma OAI.MatchingFPRAS.Enlargement.bagReweight_on line 288
  33. lemma OAI.MatchingFPRAS.Enlargement.bagReweight_identity line 296
  34. lemma OAI.MatchingFPRAS.Enlargement.bagReweight_range line 310
  35. def OAI.MatchingFPRAS.Enlargement.centralEdge line 328
  36. lemma OAI.MatchingFPRAS.Enlargement.centralEdge_injective line 331
  37. def OAI.MatchingFPRAS.Enlargement.probePortion line 335
  38. lemma OAI.MatchingFPRAS.Enlargement.probePortion_on line 339
  39. def OAI.MatchingFPRAS.Enlargement.sourcePortions line 344
  40. lemma OAI.MatchingFPRAS.Enlargement.sourcePortions_collapse line 348
  41. lemma OAI.MatchingFPRAS.Enlargement.sourcePortions_nonneg line 353
  42. lemma OAI.MatchingFPRAS.Enlargement.centralEdge_ends line 368
  43. lemma OAI.MatchingFPRAS.Enlargement.probe_support line 378
  44. lemma OAI.MatchingFPRAS.Enlargement.probe_survivors line 394
  45. def OAI.MatchingFPRAS.Enlargement.probePartial line 403
  46. abbrev OAI.MatchingFPRAS.Enlargement.SourceMarked line 417
  47. def OAI.MatchingFPRAS.Enlargement.sourceLaw line 420
  48. def OAI.MatchingFPRAS.Enlargement.observableA line 423
  49. def OAI.MatchingFPRAS.Enlargement.observableD line 426
  50. def OAI.MatchingFPRAS.Enlargement.observableProbe line 429
  51. def OAI.MatchingFPRAS.Enlargement.sourceBagZ line 435
  52. lemma OAI.MatchingFPRAS.Enlargement.sourceLaw_sum line 438
  53. lemma OAI.MatchingFPRAS.Enlargement.sourceLaw_nonneg line 443
  54. theorem OAI.MatchingFPRAS.Enlargement.observableA_mean line 449
  55. theorem OAI.MatchingFPRAS.Enlargement.observableD_mean line 457
  56. theorem OAI.MatchingFPRAS.Enlargement.observableProbe_mean line 467
  57. lemma OAI.MatchingFPRAS.Enlargement.observableA_range line 482
  58. lemma OAI.MatchingFPRAS.Enlargement.observableD_range line 488
  59. lemma OAI.MatchingFPRAS.Enlargement.observableProbe_range line 500