OAI/Combinatorics/MatchingCount/Sampling/Sewn.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.embeddedPair_outside line 15
  2. lemma OAI.MatchingFPRAS.Transport.CellPaths.through_subset_contextOne line 40
  3. lemma OAI.MatchingFPRAS.Transport.CellPaths.contextOne_self line 50
  4. lemma OAI.MatchingFPRAS.Transport.CellPaths.contextError_short_left line 55
  5. lemma OAI.MatchingFPRAS.Transport.CellPaths.contextError_short_right line 64
  6. lemma OAI.MatchingFPRAS.Transport.CellPaths.contextError_derivative line 71
  7. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_injective_range line 103
  8. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_eq_iff line 125
  9. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.intervalPattern_disjoint line 140
  10. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.parity_sdiff_interval line 150
  11. def OAI.MatchingFPRAS.Transport.IndexedCycle.sewn line 164
  12. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.forward_conversion line 167
  13. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.complementary_conversion line 179
  14. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_mem_parity line 199
  15. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.short_through line 205
  16. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.short_closed line 212
  17. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.sewn_short line 217
  18. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.sewn_root line 228
  19. def OAI.MatchingFPRAS.Transport.IndexedCycle.signedGain line 254
  20. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.signedGain_short line 258
  21. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.signedGain_root line 267
  22. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.cornerSewn line 276
  23. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.context_eq_sewn line 282
  24. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.signedLocalTerm line 303
  25. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.signed_cell_recurrence line 312
  26. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.signed_cancellation_bounded line 361