- definitions
- theorems and lemmas
- in Mathlib
- statement formalized
- statement ready to formalize
- statement not ready
- proof complete, including dependencies
- proof formalized
- proof ready to formalize
In the setting of Theorem 21, define \(\eta ^*(e) := \sigma (e) \rho ^*(e) / \operatorname {Mod}_{2,\sigma }(\Gamma )\) for \(e \in E\). Then \(\eta ^* \in \operatorname {Adm}(\widehat\Gamma )\) and \(\eta ^*\) is extremal for \(\operatorname {Mod}_{2,\sigma ^{-1}}(\widehat\Gamma )\), with
This recovers the \(p = q = 2\) case of Theorem 14 without the general machinery.
Let \(\Gamma \) be a finite family of objects on \(G\) with Fulkerson dual \(\widehat\Gamma \). For any \(\rho \in \operatorname {Adm}(\Gamma )\) and \(\eta \in \operatorname {Adm}(\widehat\Gamma )\),
with equality if and only if \(\rho \) and \(\eta \) are optimal for \(\operatorname {Mod}_2(\Gamma )\) and \(\operatorname {Mod}_2(\widehat\Gamma )\) respectively.
For any \(\rho \in \operatorname {Adm}(\Gamma )\) and any \(\lambda \in \mathbb R_{\ge 0}^\Gamma \),
with equality if and only if \(\rho \) and \(\lambda \) satisfy the stationarity and complementary slackness conditions of Theorem 21.
A density \(\rho \in \mathbb R_{\ge 0}^E\) is admissible for a family \(\Gamma \) if \(\ell _\rho (\gamma ) \ge 1\) for every \(\gamma \in \Gamma \). The admissible set of \(\Gamma \) is defined as
For \(\mu \in P(\Gamma _G)\) and \(e \in E\), the edge usage probability of \(e\) under \(\mu \) is
Let \(1 \le p \le \infty \) and let \(G = (V, E, \sigma )\) be a multigraph. The energy of a density \(\rho \) is
A density \(\rho ^* \in \operatorname {Adm}(\Gamma )\) is extremal (or optimal) for \(\operatorname {Mod}_{p,\sigma }(\Gamma )\) if
A spanning tree \(\gamma \in \Gamma _G\) is a fair tree if \(\mu ^*(\gamma ) {\gt} 0\) for some law \(\mu ^*\) optimal for \(\operatorname {FEU}(\Gamma _G)\). The set of fair trees is denoted \(\Gamma _G^f\). A tree \(\gamma \in \Gamma _G \setminus \Gamma _G^f\) (if any exist) is a forbidden tree.
A family of objects \(\Gamma \) has no zero object if every \(\gamma \in \Gamma \) has \(\gamma (e) {\gt} 0\) for some edge \(e \in E\), i.e. \(\gamma \ne 0\). This rules out the trivial all-zero object, for which no density could ever be admissible.
Let \(G = (V, E)\) be a multigraph. A family of objects on \(G\) is a nonempty countable set \(\Gamma \subseteq \mathbb R_{\ge 0}^E\) (\(\eta \)-space). In practice, each each \(\gamma \in \Gamma \) is associated with graph-theoretic object (a spanning tree, path, cut, etc.) identified with its usage vector: \(\gamma (e)\) is the usage of edge \(e\) by \(\gamma \).
A feasible partition of \(G = (V, E)\) is a partition \(P = \{ V_1, \dots , V_{k_P}\} \) of \(V\) into \(k_P \ge 2\) parts such that each induced subgraph \(G(V_i)\) is connected. Its edge set \(E_P \subseteq E\) consists of the edges joining vertices belonging to different parts.
The fairest edge usage (FEU) problem asks for the edge usage probability function \(\eta \colon E \to [0,1]\) of minimal variance over \(\mu \in P(\Gamma _G)\):
We write \(\operatorname {FEU}(\Gamma _G)\) for this problem.
Let \(\Gamma \) be a finite family of objects on \(G = (V, E)\). The Fulkerson dual family of \(\Gamma \) is \(\widehat\Gamma := \operatorname {ext}(\operatorname {Adm}(\Gamma )) \subset \mathbb R_{\ge 0}^E\), the set of extreme points of \(\operatorname {Adm}(\Gamma )\).
Let \(\rho \) be a density on \(G\). The length of an object \(\gamma \in \Gamma \) with respect to \(\rho \) is
Implementation note: the sum is implemented with finsum rather than Finset.sum over Finset.univ, so that it only requires Finite E, not a Fintype instance. See docs/common.md for details.
For \(\mu \in P(\Gamma _G)\), let \(\underline\gamma , \underline\gamma ' \sim \mu \) be independent. The expected overlap of \(\mu \) is
The minimum expected overlap (MEO) problem is
A law achieving this minimum is optimal for \(\operatorname {MEO}(\Gamma _G)\).
Let \(G = (V, E, \sigma )\) be a multigraph. Fix \(1 \le p \le \infty \). The \(p\)-modulus of a family of objects \(\Gamma \) on \(G\) is
A density achieving this infimum is called extremal (or optimal).
Following the paragraph preceding Section 1.1 of Albin, Clemens, Hoare, Poggi-Corradini, Sit, and Tymochko (2021): throughout, \(G = (V, E)\) denotes a finite, connected multigraph with vertex set \(V\) and edge set \(E\). Parallel edges are allowed; self-loops are not.
To formalize this, a multigraph on vertex type \(V\) and edge type \(E\) consists of a map \(\mathrm{endpoints} \colon E \to \operatorname {Sym}^2(V)\) assigning to each edge its (unordered) pair of endpoints. By making the edges a separate type (rather than a relation on \(V\) or a subset of unordered pairs of vertices), we implicilty allow parallel edges. They are simply distinct elements of \(E\) with the same image under \(\mathrm{endpoints}\). Finiteness, connectedness, and the absence of self-loops are not built into the type itself. Instead, they are added explicitly wherever a paper’s results need them, matching the “throughout this paper” statement.
Throughout, we write \(G = (V, E, \sigma )\) for a multigraph \(G = (V, E)\) together with an edge-weight function \(\sigma \in \mathbb R_{{\gt}0}^E\). However, \(\sigma \) is not part of the multigraph structure itself. We use the triple notation for modulus results, which is where the edge weights are relevant. . For the weight-agnostic combinatorial defintions and theorems (families of objects, densities, admissibility, the Fulkerson dual) we write the plain pair \(G = (V, E)\) instead, since none of those notions depend on \(\sigma \).
A set of edges \(T \subseteq E\) is a spanning tree of \(G\) if it touches every vertex of \(V\) and contains no cycle. In particular, this immediately rules out parallel edges, which would form a 2-cycle.
This is formalized in Multigraph.IsSpanningTree: \(T\) is acyclic (no loops, no parallel edges within \(T\), and the simple graph obtained by forgetting edge identities is acyclic) and that same simple graph is connected, i.e. touches and joins every vertex of \(V\).
Let \(G = (V, E)\) be a finite, connected multigraph and let \(\Gamma _G\) be its (finite) set of spanning trees. A law on \(\Gamma _G\) is a probability mass function \(\mu \colon \Gamma _G \to [0,1]\) with \(\sum _{\gamma \in \Gamma _G} \mu (\gamma ) = 1\); we write \(\mu \in P(\Gamma _G)\). A random spanning tree \(\underline\gamma \) has law \(\mu \) (written \(\underline\gamma \sim \mu \)) if \(\mathbb P_\mu (\underline\gamma = \gamma ) = \mu (\gamma )\) for every \(\gamma \in \Gamma _G\).
Let \(\Gamma \) be a finite family of objects on \(G = (V, E, \sigma )\) with \(\operatorname {Adm}(\Gamma ) \ne \emptyset \). There is a unique density \(\rho ^* \in \operatorname {Adm}(\Gamma )\) achieving \(\operatorname {Mod}_{2,\sigma }(\Gamma )\).
For any finite family of objects \(\Gamma \), \(\widehat{\widehat\Gamma } \subseteq \Gamma \).
Let \(\Gamma \) be a finite family of objects on \(G = (V, E, \sigma )\) with \(\operatorname {Adm}(\Gamma ) \ne \emptyset \), and fix \(1 {\lt} p {\lt} \infty \). Then there is a unique density \(\rho ^* \in \operatorname {Adm}(\Gamma )\) achieving \(\operatorname {Mod}_{p,\sigma }(\Gamma )\).
Let \(G = (V, E, \sigma )\) be a multigraph. Let \(\Gamma \) be a finite family of objects on \(G\). Let \(1 {\lt} p {\lt} \infty \) and let \(q\) satisfy \(pq = p + q\). Then
and the extremal density \(\eta ^*\) for \(\operatorname {Mod}_{q,\sigma ^{1-q}}(\widehat\Gamma )\) is related to the extremal density \(\rho ^*\) for \(\operatorname {Mod}_{p,\sigma }(\Gamma )\) by
In particular, when \(p = q = 2\),
Let \(\Gamma = \Gamma _G\) be the (finite) family of spanning trees of \(G = (V, E)\) and let \(\widehat\Gamma \) be its Fulkerson dual. Densities \(\rho , \eta \in \mathbb R_{\ge 0}^E\) and a law \(\mu \in P(\Gamma )\) are simultaneously optimal for \(\operatorname {Mod}_2(\Gamma )\), \(\operatorname {Mod}_2(\widehat\Gamma )\), and \(\operatorname {MEO}(\Gamma )\) respectively if and only if
In particular,
Let \(\Gamma _G\) be the (finite) family of spanning trees of \(G = (V, E)\), with usage given by the indicator vectors \(\mathbf1_{\{ e \in \gamma \} }\). The Fulkerson dual family \(\widehat{\Gamma _G}\) is the set of vectors \(\frac{1}{k_P - 1} \mathbf1_{E_P}\), ranging over all feasible partitions \(P\) of \(G\).
Let \(\Gamma \) be a finite family of objects on \(G = (V, E, \sigma )\) with \(\operatorname {Adm}(\Gamma ) \ne \emptyset \), and let \(\rho ^*\) be the extremal density for \(\operatorname {Mod}_{2,\sigma }(\Gamma )\). There exists \(\lambda ^* \in \mathbb R_{\ge 0}^\Gamma \) such that
and