OAI/Combinatorics/MatchingCount/Graphs/PushedFlow.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Replica.pushedFlow line 14
  2. lemma OAI.MatchingFPRAS.Replica.pushedFlow_nonneg line 18
  3. lemma OAI.MatchingFPRAS.Replica.pushedFlow_test line 24
  4. lemma OAI.MatchingFPRAS.Replica.pushedFlow_row_test line 46
  5. lemma OAI.MatchingFPRAS.Replica.pushedFlow_col_test line 55
  6. lemma OAI.MatchingFPRAS.Replica.pushedFlow_energy line 65
  7. def OAI.MatchingFPRAS.Replica.pairFlow line 82
  8. lemma OAI.MatchingFPRAS.Replica.slice_mean line 86
  9. lemma OAI.MatchingFPRAS.Replica.pairFlow_row line 98
  10. lemma OAI.MatchingFPRAS.Replica.pairFlow_col line 107
  11. lemma OAI.MatchingFPRAS.Replica.pairFlow_nonneg line 116
  12. lemma OAI.MatchingFPRAS.Replica.pairFlow_energy line 119
  13. def OAI.MatchingFPRAS.Replica.baseFlow line 123
  14. lemma OAI.MatchingFPRAS.Replica.baseFlow_nonneg line 126
  15. lemma OAI.MatchingFPRAS.Replica.baseFlow_row line 130
  16. lemma OAI.MatchingFPRAS.Replica.baseFlow_col line 140
  17. lemma OAI.MatchingFPRAS.Replica.baseFlow_energy line 150
  18. def OAI.MatchingFPRAS.Replica.updateCount line 168
  19. def OAI.MatchingFPRAS.Replica.scanFlow line 171
  20. lemma OAI.MatchingFPRAS.Replica.localEnergy_add line 185
  21. lemma OAI.MatchingFPRAS.Replica.localEnergy_div line 189
  22. lemma OAI.MatchingFPRAS.Replica.localEnergy_sum line 194
  23. lemma OAI.MatchingFPRAS.Replica.localEnergy_diag line 203
  24. lemma OAI.MatchingFPRAS.Replica.updateCount_pos line 219
  25. lemma OAI.MatchingFPRAS.Replica.scanFlow_nonneg line 222
  26. lemma OAI.MatchingFPRAS.Replica.scanFlow_lazy line 233
  27. lemma OAI.MatchingFPRAS.Replica.scanFlow_row line 242
  28. lemma OAI.MatchingFPRAS.Replica.scanFlow_col line 261
  29. lemma OAI.MatchingFPRAS.Replica.scanFlow_energy line 280
  30. def OAI.MatchingFPRAS.FiniteChain.sqNorm line 297
  31. def OAI.MatchingFPRAS.FiniteChain.massMean line 299
  32. def OAI.MatchingFPRAS.FiniteChain.stepDensity line 301
  33. lemma OAI.MatchingFPRAS.FiniteChain.stepDensity_mean line 305
  34. lemma OAI.MatchingFPRAS.FiniteChain.stepDensity_one line 314
  35. lemma OAI.MatchingFPRAS.FiniteChain.stepDensity_linear line 319
  36. lemma OAI.MatchingFPRAS.FiniteChain.stepDensity_jensen line 329
  37. lemma OAI.MatchingFPRAS.FiniteChain.energy_norm_cross line 348
  38. def OAI.MatchingFPRAS.FiniteChain.unlazyFlow line 361
  39. lemma OAI.MatchingFPRAS.FiniteChain.unlazyFlow_nonneg line 365
  40. lemma OAI.MatchingFPRAS.FiniteChain.unlazyFlow_row line 373
  41. lemma OAI.MatchingFPRAS.FiniteChain.unlazyFlow_col line 379
  42. lemma OAI.MatchingFPRAS.FiniteChain.unlazyFlow_step line 385
  43. lemma OAI.MatchingFPRAS.FiniteChain.lazy_l2 line 394