Face.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Active face spaces, their codimension bounds, and local radial extension.

def OAI.MatchingEntropy.LooplessGraph.positiveExtension line 21
Source documentation
Restrict the ambient vector space to the genuinely positive edge coordinates.
```
def positiveExtension (x : E → ℝ) : ({e // 0<x e} → ℝ) →ₗ[ℝ] (E → ℝ) := by
…
```
theorem OAI.MatchingEntropy.LooplessGraph.positiveExtension_pos line 29
theorem OAI.MatchingEntropy.LooplessGraph.positiveExtension_zero line 34
def OAI.MatchingEntropy.LooplessGraph.degreeLinear line 38
def OAI.MatchingEntropy.LooplessGraph.cutLinear line 52
def OAI.MatchingEntropy.LooplessGraph.faceSpace line 58
Source documentation
The exact active degree and odd-cut kernel, on the positive edge support.
```
def faceSpace (G : LooplessGraph V E) (x : E → ℝ) : Submodule ℝ ({e // 0<x e} → ℝ) where
…
```
def OAI.MatchingEntropy.LooplessGraph.faceCodimension line 73
theorem OAI.MatchingEntropy.LooplessGraph.faceCodimension_no_tight line 77
theorem OAI.MatchingEntropy.LooplessGraph.faceSpace_eventually_line line 91
theorem OAI.MatchingEntropy.LooplessGraph.faceSpace_of_eventually_line line 98
abbrev OAI.MatchingEntropy.LooplessGraph.sideMarginal line 126
def OAI.MatchingEntropy.LooplessGraph.sideRestriction line 129
theorem OAI.MatchingEntropy.LooplessGraph.positiveExtension_side line 136
theorem OAI.MatchingEntropy.LooplessGraph.sideMarginal_line line 143

theorem OAI.MatchingEntropy.LooplessGraph.faceSpace_of_side_spaces line 151

Source documentation

Pullbacks of both contraction face spaces preserve every original active cut, including cuts crossing the chosen tight cut. This is the substantive coupling step.

theorem faceSpace_of_side_spaces (G : LooplessGraph V E) {x : E → ℝ}
    (heven : Even (Fintype.card V)) (hx : x ∈ G.constraintPolytope)
    (S : Finset V) (hS : Odd S.card) (ht : G.cutMass x S=1)
    {u : {e // 0<x e} → ℝ}
    (h1 : G.sideRestriction x S u ∈ (G.onSide S).faceSpace (G.sideMarginal x S))
    (h2 : G.sideRestriction x Sᶜ u ∈ (G.onSide Sᶜ).faceSpace (G.sideMarginal x Sᶜ)) :
    u ∈ G.faceSpace x := by
…

Mentions: OAI.MatchingEntropy.LooplessGraph.faceSpace

theorem OAI.MatchingEntropy.LooplessGraph.faceCodimension_le_sides line 180

theorem OAI.MatchingEntropy.LooplessGraph.faceCodimension_strong_aux line 192

Source documentation

Strong face-codimension induction for even orders at least four.

theorem faceCodimension_strong_aux (n : ℕ) :
    ∀ {W F : Type*} [Fintype W] [Fintype F] [DecidableEq W] [DecidableEq F]
      (G : LooplessGraph W F), Fintype.card W=n → Even n → 4≤n →
      ∀ x ∈ G.constraintPolytope, G.faceCodimension x ≤ 2*(n-2) := by
…

theorem OAI.MatchingEntropy.LooplessGraph.faceCodimension_bound line 237

Source documentation

The precise coarse face-codimension estimate used by the entropy argument.

theorem faceCodimension_bound (G : LooplessGraph V E) {x : E → ℝ}
    (heven : Even (Fintype.card V)) (hx : x ∈ G.polytope) :
    G.faceCodimension x ≤ 2*Fintype.card V := by
…

theorem OAI.MatchingEntropy.LooplessGraph.degree_add_smul line 253
theorem OAI.MatchingEntropy.LooplessGraph.cutMass_add_smul line 258
theorem OAI.MatchingEntropy.LooplessGraph.constraint_eventually_expand line 265
Source documentation
Radial extension for this actual matching polytope. This is needed to prove lower semicontinuity of the maximum entropy without assuming its regularity.
```
theorem constraint_eventually_expand (G : LooplessGraph V E) {x : E → ℝ}
    (hx : x ∈ G.constraintPolytope) {t : ℝ} (ht : 0<t) :
    ∀ᶠ y in 𝓝[G.constraintPolytope] x, x+t⁻¹ • (y-x) ∈ G.constraintPolytope := by
…
```
theorem OAI.MatchingEntropy.LooplessGraph.polytope_eventually_expand line 302