OAI/Combinatorics/KServer/MetricMatching.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

In a finite laminar tree, one matching simultaneously has the optimal crossing count at every cut. This is proved by the uncrossing minimizer, rather than assuming a transport/matching interface.

  1. def OAI.KServer.LaminarMatching.Laminar line 16
  2. def OAI.KServer.LaminarMatching.bit line 20
  3. def OAI.KServer.LaminarMatching.cross line 22
  4. def OAI.KServer.LaminarMatching.cost line 25
  5. lemma OAI.KServer.LaminarMatching.pair_inequality line 27
  6. lemma OAI.KServer.LaminarMatching.laminar_pair line 32
  7. lemma OAI.KServer.LaminarMatching.two_term_sum line 43
  8. lemma OAI.KServer.LaminarMatching.swapped_cuts line 59
  9. lemma OAI.KServer.LaminarMatching.swapped_strict line 74
  10. lemma OAI.KServer.LaminarMatching.bit_lt line 88
  11. lemma OAI.KServer.LaminarMatching.minimizing_oriented line 92

    Source documentation

    An optimal permutation has no opposite crossings at any cut.

    lemma minimizing_oriented {c:V→Z→Bool} (hc:Laminar c) (f g:I→Z) (π:Equiv.Perm I)
    (hm:∀ ρ,cost c f g π≤cost c f g ρ) (v:V):
    (∀ i,bit (c v (f i))≤bit (c v (g (π i)))) ∨
      (∀ i,bit (c v (g (π i)))≤bit (c v (f i))):=by
…

    Mentions: OAI.KServer.LaminarMatching.Laminar, OAI.KServer.LaminarMatching.cost, OAI.KServer.LaminarMatching.bit

  12. lemma OAI.KServer.LaminarMatching.oriented_cross line 108
  13. theorem OAI.KServer.LaminarMatching.exists_simultaneous line 123

    Source documentation

    One matching is optimal at every member of the laminar family.

    theorem exists_simultaneous {c:V→Z→Bool} (hc:Laminar c) (f g:I→Z):
    ∃ π:Equiv.Perm I,∀ v,(∑ i,cross c f g π v i)=
      |(∑ i,bit (c v (f i)))-(∑ i,bit (c v (g i)))|:=by
…

    Mentions: OAI.KServer.LaminarMatching.Laminar, OAI.KServer.LaminarMatching.cross, OAI.KServer.LaminarMatching.bit

  14. lemma OAI.KServer.Rounding.Tree.under_trans line 140
  15. lemma OAI.KServer.Rounding.Tree.ancestors_comparable line 159
  16. lemma OAI.KServer.Rounding.Tree.laminar line 180
  17. def OAI.KServer.Rounding.Tree.cutDistance line 205
  18. lemma OAI.KServer.Rounding.Tree.cutDistance_symm line 208
  19. lemma OAI.KServer.Rounding.Tree.cutDistance_self line 213
  20. lemma OAI.KServer.Rounding.Tree.cutDistance_peel line 216
  21. lemma OAI.KServer.Rounding.Tree.under_false_of_lt line 230
  22. theorem OAI.KServer.Rounding.Tree.metric_le_cutDistance line 236
  23. theorem OAI.KServer.Rounding.Tree.exists_metric_matching line 259

    Source documentation

    Actual permutation, not an assumed coupling cost bound.

    theorem Tree.exists_metric_matching {X I:Type*} [PseudoMetricSpace X] [Fintype I]
    (T:Tree n) (a:Fin n→X) (w:Fin n→ℝ)
    (he:∀ u,u≠0→dist (a u) (a (T.parent u))≤w u) (f g:I→Fin n):
    ∃ π:Equiv.Perm I,(∑ i,dist (a (f i)) (a (g (π i))))≤
      ∑ v,w v*|(∑ i,T.indicator v (f i))-(∑ i,T.indicator v (g i))|:=by
…

    Mentions: OAI.KServer.Rounding.Tree

  24. lemma OAI.KServer.Rounding.Tree.parent_under line 293
  25. lemma OAI.KServer.Rounding.Tree.path_child line 300
  26. lemma OAI.KServer.Rounding.Tree.common_cut line 317
  27. lemma OAI.KServer.Rounding.Tree.distinct_le_cut line 339
  28. lemma OAI.KServer.PrefixTree.hit_parent line 367
  29. lemma OAI.KServer.PrefixTree.under_depth line 378
  30. lemma OAI.KServer.PrefixTree.under_hit line 399
  31. def OAI.KServer.PrefixTree.nodeAnchor line 430
  32. def OAI.KServer.PrefixTree.nodeMotion line 435
  33. lemma OAI.KServer.PrefixTree.last_none line 440
  34. lemma OAI.KServer.PrefixTree.last_depth line 452
  35. lemma OAI.KServer.PrefixTree.weight_under line 460
  36. lemma OAI.KServer.PrefixTree.anchor_witness line 465
  37. lemma OAI.KServer.PrefixTree.witnessed_common_bound line 481
  38. def OAI.KServer.TreeRounding.Tree.toTravel line 546
  39. lemma OAI.KServer.TreeRounding.Tree.consistent_park line 551
  40. lemma OAI.KServer.TreeRounding.Tree.park_nats_sum line 558
  41. def OAI.KServer.TreeRounding.countEquiv line 576
  42. def OAI.KServer.TreeRounding.slots line 581
  43. lemma OAI.KServer.TreeRounding.slots_sum line 585
  44. lemma OAI.KServer.TreeRounding.slots_subtree line 597
  45. lemma OAI.KServer.TreeRounding.slots_positive line 604
  46. theorem OAI.KServer.Rounding.Tree.exists_cross_matching line 624
  47. def OAI.KServer.TreeRounding.Good line 666
  48. abbrev OAI.KServer.TreeRounding.Inventory line 668
  49. def OAI.KServer.TreeRounding.Inventory.slots line 670
  50. lemma OAI.KServer.TreeRounding.Inventory.slots_injective line 673
  51. instance OAI.KServer.TreeRounding.inventoryFintype line 696
  52. lemma OAI.KServer.TreeRounding.stock_good line 699
  53. instance OAI.KServer.TreeRounding.inventoryNonempty line 703
  54. def OAI.KServer.TreeRounding.pack line 705
  55. lemma OAI.KServer.TreeRounding.pack_val line 707
  56. lemma OAI.KServer.TreeRounding.good_of_valid line 710
  57. def OAI.KServer.PrefixTree.countConfig line 728
  58. lemma OAI.KServer.PrefixTree.count_matching line 731
  59. lemma OAI.KServer.TreeRounding.Inventory.slot_exists line 807
  60. lemma OAI.KServer.TreeRounding.Inventory.valid_slot_positive line 814
  61. lemma OAI.KServer.TreeRounding.balanced_one_le line 825
  62. lemma OAI.KServer.PrefixTree.count_witness line 835
  63. lemma OAI.KServer.PrefixTree.nodeMotion_sum line 856