OAI/Combinatorics/PerfectMatching/Contraction.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Contraction of tight odd cuts and gluing of perfect matchings and their laws.

  1. def OAI.MatchingEntropy.LooplessGraph.onSide line 23

    Source documentation

    Contraction of the complement of S to a new vertex. Edges retain identities; only edges with both endpoints outside S are discarded.

    def onSide (G : LooplessGraph V E) (S : Finset V) :
    LooplessGraph (Option {v // v ∈ S}) {e // G.left e ∈ S ∨ G.right e ∈ S} where
…
  2. theorem OAI.MatchingEntropy.LooplessGraph.onSide_incident_some line 40
  3. theorem OAI.MatchingEntropy.LooplessGraph.onSide_incident_none line 61
  4. def OAI.MatchingEntropy.LooplessGraph.boundaryEdge line 69
  5. theorem OAI.MatchingEntropy.LooplessGraph.boundaryEdge_mem line 73
  6. theorem OAI.MatchingEntropy.LooplessGraph.boundaryEdge_crosses line 78
  7. theorem OAI.MatchingEntropy.LooplessGraph.eq_boundaryEdge line 83
  8. def OAI.MatchingEntropy.LooplessGraph.liftedEdges line 88
  9. theorem OAI.MatchingEntropy.LooplessGraph.mem_liftedEdges line 92
  10. theorem OAI.MatchingEntropy.LooplessGraph.liftedEdges_keep line 104
  11. theorem OAI.MatchingEntropy.LooplessGraph.lifted_cross_eq_boundary line 111
  12. theorem OAI.MatchingEntropy.LooplessGraph.boundary_mem_lifted line 118
  13. theorem OAI.MatchingEntropy.LooplessGraph.crosses_of_kept_both line 123
  14. theorem OAI.MatchingEntropy.LooplessGraph.lifted_other_subset line 132

    Source documentation

    A compatible pair only duplicates its common boundary edge.

    theorem lifted_other_subset (G : LooplessGraph V E) (S : Finset V)
    (M₁ : (G.onSide S).Matching) (M₂ : (G.onSide Sᶜ).Matching)
    (heq : (G.boundaryEdge S M₁).val = (G.boundaryEdge Sᶜ M₂).val)
    {e : E} (he : e ∈ G.liftedEdges Sᶜ M₂)
    (hkeep : G.left e ∈ S ∨ G.right e ∈ S) : e ∈ G.liftedEdges S M₁ := by
…

    Mentions: OAI.MatchingEntropy.LooplessGraph.Matching

  15. theorem OAI.MatchingEntropy.LooplessGraph.mem_glued_left line 144

    Source documentation

    Gluing compatible perfect matchings preserves each retained edge choice.

    theorem mem_glued_left (G : LooplessGraph V E) (S : Finset V)
    (M₁ : (G.onSide S).Matching) (M₂ : (G.onSide Sᶜ).Matching)
    (heq : (G.boundaryEdge S M₁).val = (G.boundaryEdge Sᶜ M₂).val)
    (e : {e // G.left e ∈ S ∨ G.right e ∈ S}) :
    e.val ∈ G.liftedEdges S M₁ ∪ G.liftedEdges Sᶜ M₂ ↔ e ∈ M₁.val := by
…

    Mentions: OAI.MatchingEntropy.LooplessGraph.Matching

  16. theorem OAI.MatchingEntropy.LooplessGraph.mem_glued_right line 158
  17. theorem OAI.MatchingEntropy.LooplessGraph.glued_perfect line 176
  18. def OAI.MatchingEntropy.LooplessGraph.glueMatching line 206
  19. theorem OAI.MatchingEntropy.LooplessGraph.indicator_glue_left line 213
  20. theorem OAI.MatchingEntropy.LooplessGraph.indicator_glue_right line 221
  21. theorem OAI.MatchingEntropy.LooplessGraph.boundary_eq_iff_mem line 229
  22. theorem OAI.MatchingEntropy.LooplessGraph.boundary_fiber line 240
  23. theorem OAI.MatchingEntropy.LooplessGraph.boundary_fiber_zero line 251
  24. theorem OAI.MatchingEntropy.LooplessGraph.couple_laws line 262

    Source documentation

    Exact coupling across a cut, for multigraphs with distinct edge identities.

    theorem couple_laws (G : LooplessGraph V E) (S : Finset V) (x : E → ℝ)
    {p : (G.onSide S).Matching → ℝ} {q : (G.onSide Sᶜ).Matching → ℝ}
    (hp : p ∈ probabilitySimplex (G.onSide S).Matching)
    (hq : q ∈ probabilitySimplex (G.onSide Sᶜ).Matching)
    (hpx : ∀ e, (G.onSide S).mean p e = x e.val)
    (hqx : ∀ e, (G.onSide Sᶜ).mean q e = x e.val) :
    ∃ r, r ∈ G.feasibleLaws x := by
…

    Mentions: OAI.MatchingEntropy.LooplessGraph.Matching, OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.LooplessGraph.mean

  25. def OAI.MatchingEntropy.LooplessGraph.sideMap line 301
  26. def OAI.MatchingEntropy.LooplessGraph.liftVertices line 304
  27. theorem OAI.MatchingEntropy.LooplessGraph.mem_liftVertices line 307
  28. theorem OAI.MatchingEntropy.LooplessGraph.sideMap_some line 312
  29. theorem OAI.MatchingEntropy.LooplessGraph.liftVertices_card line 316
  30. theorem OAI.MatchingEntropy.LooplessGraph.onSide_cut_crosses line 340
  31. theorem OAI.MatchingEntropy.LooplessGraph.crosses_lift_kept line 347
  32. theorem OAI.MatchingEntropy.LooplessGraph.onSide_cutMass line 356
  33. theorem OAI.MatchingEntropy.LooplessGraph.onSide_degree_some line 366
  34. theorem OAI.MatchingEntropy.LooplessGraph.onSide_degree_none line 380
  35. theorem OAI.MatchingEntropy.LooplessGraph.odd_compl_of_even line 392
  36. theorem OAI.MatchingEntropy.LooplessGraph.restriction_mem_constraints line 403

    Source documentation

    Exact inheritance of the odd-cut system under contraction of a tight odd cut.

    theorem restriction_mem_constraints (G : LooplessGraph V E) {x : E → ℝ}
    (hx : x ∈ G.constraintPolytope) (S : Finset V) (hS : Odd S.card)
    (htight : G.cutMass x S = 1) :
    (fun e : {e // G.left e ∈ S ∨ G.right e ∈ S} => x e.val) ∈
      (G.onSide S).constraintPolytope := by
…

    Mentions: OAI.MatchingEntropy.LooplessGraph.constraintPolytope