OAI/Probability/MatroidProphet/GroupConditioning.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.MainAlgorithm.trueGroup line 12
  2. lemma OAI.MatroidProphet.MainAlgorithm.mem_trueGroup line 16
  3. lemma OAI.MatroidProphet.MainAlgorithm.trueGroup_disjoint line 21
  4. lemma OAI.MatroidProphet.MainAlgorithm.trueGroup_disjoint_H line 29
  5. lemma OAI.MatroidProphet.MainAlgorithm.mem_listed_iff line 35
  6. def OAI.MatroidProphet.MainAlgorithm.withMasks line 48
  7. lemma OAI.MatroidProphet.MainAlgorithm.candidate_withMasks line 51
  8. lemma OAI.MatroidProphet.MainAlgorithm.trueGroup_withMasks line 55
  9. lemma OAI.MatroidProphet.MainAlgorithm.groups_withMasks_guards line 59
  10. def OAI.MatroidProphet.MainAlgorithm.focalMasks line 63
  11. lemma OAI.MatroidProphet.MainAlgorithm.candidate_focalMasks line 66
  12. lemma OAI.MatroidProphet.MainAlgorithm.trueGroup_focalMasks line 70
  13. lemma OAI.MatroidProphet.MainAlgorithm.listed_focalMasks line 74
  14. def OAI.MatroidProphet.MainAlgorithm.focalReference line 115
  15. lemma OAI.MatroidProphet.MainAlgorithm.groups_focalMasks line 119
  16. lemma OAI.MatroidProphet.MainAlgorithm.focal_mem_reference_groups line 129
  17. lemma OAI.MatroidProphet.MainAlgorithm.groupMask_at_key line 137
  18. lemma OAI.MatroidProphet.MainAlgorithm.replaceMask_inter_self line 144
  19. lemma OAI.MatroidProphet.MainAlgorithm.replaceMask_inter_other line 155
  20. def OAI.MatroidProphet.MainAlgorithm.focalIndex line 167
  21. lemma OAI.MatroidProphet.MainAlgorithm.focal_group_key line 171
  22. lemma OAI.MatroidProphet.MainAlgorithm.focal_group_mask line 178
  23. lemma OAI.MatroidProphet.MainAlgorithm.lower_group_mask line 187
  24. lemma OAI.MatroidProphet.guardedPath_congr_prefix line 213
  25. lemma OAI.MatroidProphet.nominalPath_congr_prefix line 223
  26. lemma OAI.MatroidProphet.lowerCompetition_congr_prefix line 230
  27. lemma OAI.MatroidProphet.MainAlgorithm.focal_prefix_masks line 251
  28. lemma OAI.MatroidProphet.MainAlgorithm.focal_incoming_path line 265
  29. lemma OAI.MatroidProphet.MainAlgorithm.focal_lowerCompetition line 277
  30. lemma OAI.MatroidProphet.MainAlgorithm.focal_nominal_path line 292
  31. lemma OAI.MatroidProphet.MainAlgorithm.focal_observed_inter line 306
  32. lemma OAI.MatroidProphet.MainAlgorithm.focal_listed_iff_nonempty line 316
  33. def OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic line 323
  34. def OAI.MatroidProphet.MainAlgorithm.listedRankStatistic line 332
  35. lemma OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic_focal_empty line 340
  36. lemma OAI.MatroidProphet.MainAlgorithm.listedRankStatistic_focal_empty line 348
  37. lemma OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic_focal_nonempty line 356
  38. lemma OAI.MatroidProphet.MainAlgorithm.listedRankStatistic_focal_nonempty line 370
  39. lemma OAI.MatroidProphet.MainAlgorithm.focal_density_inter line 384