OAI/Combinatorics/MatchingCount/Sampling/ChosenChord.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.IndexedCycle.chosenChord line 17
  2. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.chosenChord_eq line 23
  3. def OAI.MatchingFPRAS.Transport.IndexedCycle.diagramGain line 29
  4. def OAI.MatchingFPRAS.Transport.IndexedCycle.diagramTerm line 32
  5. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.diagramGain_short line 40
  6. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.diagramGain_root line 51
  7. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.diagram_cell_recurrence line 67
  8. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.sum_cells_identity line 89
  9. structure OAI.MatchingFPRAS.Cells.CycleData.CellIndex line 104
  10. def OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cellList line 115
  11. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.mem_cellList line 120
  12. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cellList_length line 135
  13. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cellList_separated line 141
  14. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cellList_nodup line 153
  15. def OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cellSet line 182
  16. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cellSet_card line 184
  17. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.sumCells_eq_sum line 187
  18. def OAI.MatchingFPRAS.Transport.IndexedCycle.diagramEnergy line 213
  19. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.diagramEnergy_nonneg line 223
  20. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.diagramTerm_sq_le line 230
  21. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.cycle_cell_square_bound line 246
  22. def OAI.MatchingFPRAS.Transport.IndexedCycle.subdivision line 291
  23. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.exchange_cell_square_bound line 296
  24. abbrev OAI.MatchingFPRAS.Transport.LongComponent line 342
  25. instance OAI.MatchingFPRAS.Transport.LongComponent.(instance at line 349) line 349
  26. def OAI.MatchingFPRAS.Transport.LongComponent.cycle line 351
  27. lemma OAI.MatchingFPRAS.Transport.LongComponent.cycle_set line 354
  28. lemma OAI.MatchingFPRAS.Transport.LongComponent.cycle_union line 357
  29. lemma OAI.MatchingFPRAS.Transport.LongComponent.mem_components line 360
  30. lemma OAI.MatchingFPRAS.Transport.LongComponent.anchor_recovers line 364
  31. abbrev OAI.MatchingFPRAS.Transport.CellDemands.Demand line 387