OAI/Combinatorics/TriangleRemoval/Probability/TrueProbabilityMap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpTerminalLeave.trueProbability_map line 16
  2. theorem OAI.SharpTerminalLeave.boolean_coupling_bound line 21
  3. theorem OAI.SharpTerminalLeave.ExposureTree.independent_exposure_error line 43
  4. theorem OAI.SharpTerminalLeave.pmf_map_congr_support line 62
  5. theorem OAI.SharpTerminalLeave.productPMF_coord line 69
  6. theorem OAI.SharpTerminalLeave.productPMF_pair line 83
  7. theorem OAI.SharpTerminalLeave.boolean_union_bound line 102
  8. theorem OAI.SharpTerminalLeave.grid_table_pair_tie line 127
  9. theorem OAI.SharpTerminalLeave.grid_table_ties_bound line 145