OAI/Probability/FirstPassage/WitnessDecomposition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.total line 12
  2. theorem OAI.PlanarFPP.total_nil line 13
  3. theorem OAI.PlanarFPP.total_cons line 14
  4. theorem OAI.PlanarFPP.total_append line 16
  5. theorem OAI.PlanarFPP.first_drop line 19
  6. theorem OAI.PlanarFPP.witness_decomposition line 37
  7. theorem OAI.PlanarFPP.decomposition_lower_bound line 66
  8. theorem OAI.PlanarFPP.disjoint_witness_decomposition line 82
  9. theorem OAI.PlanarFPP.defect_bound_from_witness_capacity line 97
  10. theorem OAI.PlanarFPP.edge_disjoint_witness_decomposition line 116
  11. theorem OAI.PlanarFPP.full_chunk_lower_bound line 136