Polytope.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Tutte's criterion and Edmonds' perfect matching polytope theorem for multigraphs.

def OAI.MatchingEntropy.LooplessGraph.supportSimple line 22
Source documentation
The simple support graph forgets only parallel-edge identities.
```
def supportSimple (G : LooplessGraph V E) (x : E → ℝ) : SimpleGraph V where
…
```
theorem OAI.MatchingEntropy.LooplessGraph.supportSimple_edge line 30
theorem OAI.MatchingEntropy.LooplessGraph.sum_pred_le_one line 33

theorem OAI.MatchingEntropy.LooplessGraph.odd_family_bound line 49

Source documentation

The weighted cut-counting argument in Tutte's criterion.

theorem odd_family_bound (G : LooplessGraph V E) {x : E → ℝ}
    (hx : x ∈ G.constraintPolytope) {C : Type*} [Fintype C] [DecidableEq C]
    (U : Finset V) (T : C → Finset V)
    (hodd : ∀ c, Odd (T c).card)
    (hdisj : ∀ c v, v ∈ T c → v ∉ U)
    (huniq : ∀ a b v, v ∈ T a → v ∈ T b → a=b)
    (hclosed : ∀ e, 0 < x e → G.left e ∉ U → G.right e ∉ U →
      ∀ c, G.left e ∈ T c ↔ G.right e ∈ T c) :
    Fintype.card C ≤ U.card := by
…

theorem OAI.MatchingEntropy.LooplessGraph.supportSimple_has_perfectMatching line 138
theorem OAI.MatchingEntropy.LooplessGraph.exists_supported_matching line 194
theorem OAI.MatchingEntropy.LooplessGraph.crosses_singleton line 240
theorem OAI.MatchingEntropy.LooplessGraph.cutMass_singleton line 248

theorem OAI.MatchingEntropy.LooplessGraph.constraint_eventually_line line 254

Source documentation

Local two-sided perturbations for the degree and odd-cut constraint system.

theorem constraint_eventually_line (G : LooplessGraph V E) {x : E → ℝ}
    (hx : x ∈ G.constraintPolytope) (u : E → ℝ)
    (hzero : ∀ e, x e=0 → u e=0) (hdeg : ∀ v, G.degree u v=0)
    (hcut : ∀ S, Odd S.card → G.cutMass x S=1 → G.cutMass u S=0) :
    ∀ᶠ t : ℝ in 𝓝 0, x+t • u ∈ G.constraintPolytope := by
…

theorem OAI.MatchingEntropy.LooplessGraph.degree_sub line 293
theorem OAI.MatchingEntropy.LooplessGraph.cutMass_sub line 299

theorem OAI.MatchingEntropy.LooplessGraph.trivial_tight_cut_preserved line 306

Source documentation

Without a nontrivial tight odd cut, only degrees constrain a supported direction.

theorem trivial_tight_cut_preserved (G : LooplessGraph V E) {x : E → ℝ}
    (heven : Even (Fintype.card V))
    (hnt : ¬∃ S : Finset V, Odd S.card ∧ 3≤S.card ∧ 3≤Sᶜ.card ∧ G.cutMass x S=1)
    (u : E → ℝ) (hdeg : ∀ v, G.degree u v=0) :
    ∀ S, Odd S.card → G.cutMass x S=1 → G.cutMass u S=0 := by
…

theorem OAI.MatchingEntropy.LooplessGraph.extreme_no_tight_integral line 325

theorem OAI.MatchingEntropy.LooplessGraph.constraint_subset_polytope_aux line 345

Source documentation

Induction over even orders, using only proved cut coupling and Mathlib Tutte.

theorem constraint_subset_polytope_aux (n : ℕ) :
    ∀ {W F : Type*} [Fintype W] [Fintype F] [DecidableEq W] [DecidableEq F]
      (G : LooplessGraph W F), Fintype.card W=n → Even n →
      G.constraintPolytope ⊆ G.polytope := by
…

theorem OAI.MatchingEntropy.LooplessGraph.polytope_eq_constraints line 384
Source documentation
Edmonds' perfect matching polytope equality, with parallel edges retained.
```
theorem polytope_eq_constraints (G : LooplessGraph V E) (heven : Even (Fintype.card V)) :
    G.polytope = G.constraintPolytope := by
…
```