Motivation

The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system

$$\dot x = P(x,y),\qquad \dot y = Q(x,y),$$

where $P,Q$ are real polynomials of degree at most $d$. Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for $d = 2$ it is not known whether the number of limit cycles is uniformly bounded.

J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.

Timeline (as reported in the survey):

• 1891–1897 — Poincaré introduces limit cycles and proves finiteness for systems without saddle connections.
• 1900 — Hilbert poses the 16th problem.
• 1923 — Dulac claims every polynomial system has finitely many limit cycles; in 1985 Ilyashenko finds a gap.
• 1957/1959 — Petrovskii and Landis claim $H(2)=3$ and later find an error; 1979 (Chen–Wang) and 1982 (Shi) give quadratic systems with 4 limit cycles.
• 1986 — Bamon proves finiteness for quadratic systems; 1991/1992 — Ilyashenko and Écalle independently prove finiteness for all polynomial systems.
• 2001 — Christopher realises any non-singular algebraic curve's bounded components as hyperbolic limit cycles of a system of the same degree (Christopher 2001).
• 2004 — Llibre and Rodríguez show every configuration of limit cycles is realisable by algebraic limit cycles (Llibre–Rodríguez 2004).
• 2007 — Llibre and Zhao give a cubic system with two algebraic limit cycles (Llibre–Zhao 2007).
• 2010 — Llibre, Ramírez and Sadovskaia bound the number of algebraic limit cycles when all invariant algebraic curves are generic, and state the conjecture.

Setting

A polynomial vector field is a pair $V = (P, Q)$ of real polynomials in $x,y$; its degree is $\max(\deg P, \deg Q)$. A solution is a differentiable curve $\gamma:\mathbb R\to\mathbb R^2$ with $\gamma'(t) = (P,Q)(\gamma(t))$ for all $t$. A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit $O$ that is isolated among periodic orbits: some open set $U \supseteq O$ contains no periodic orbit other than $O$.

A limit cycle is algebraic if it is contained in the zero set $\{f = 0\}$ of a non-zero real polynomial $f$. The algebraic Hilbert number $H_a(d)$ is the supremum, over all polynomial vector fields of degree at most $d$, of the number of algebraic limit cycles (a value in $\mathbb N \cup \{\infty\}$).

A curve $f = 0$ is invariant with cofactor $K$ if $P\,f_x + Q\,f_y = K f$. A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.

Formalization targets

Goal — Conjecture 1 (Llibre–Ramírez–Sadovskaia)

$$H_a(d) = 1 + \frac{(d-1)(d-2)}{2}\qquad (d \ge 2).$$

The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most $d$, and that the bound is attained.

Milestones (in the order of the survey)

1. §2, Problem 1 — every polynomial vector field has finitely many limit cycles (Écalle, Ilyashenko).
2. §3 — $H(1) = 0$: vector fields of degree at most $1$ have no limit cycles.
3. Theorem 1(a),(b) — every configuration of limit cycles is realised, and realised by algebraic limit cycles in degree $\le 2(n+r)-1$.
4. Theorem 2 (Christopher) — the bounded components of a non-singular curve $f = 0$ are exactly the limit cycles, all hyperbolic, of $\dot x = \alpha f - D f_y$, $\dot y = \beta f + D f_x$.
5. Proposition 3 — invariance of $f$ is equivalent to invariance of its irreducible factors, with $K_f = \sum n_i K_{f_i}$.
6. Theorem 4(a),(b) — for degree $d \ge 2$ and generic invariant curves, at most $1 + \frac{(d-1)(d-2)}{2}$ (even $d$) or $\frac{(d-1)(d-2)}{2}$ (odd $d$) algebraic limit cycles, and the bounds are attained.
7. §7 example — the cubic system $\dot x = 2y(10+xy)$, $\dot y = 20x + y - 20x^3 - 2x^2 y + 4y^3$ has two algebraic limit cycles in $2x^4 - 4x^2 + 4y^2 + 1 = 0$.
8. Conjecture 2 — $H_a(2) = 1$.
9. Theorem 5 (Giacomini–Llibre–Viano) — an inverse integrating factor vanishes on every limit cycle.

Significance

A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even $d$, and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 ($d = 2$) is its first open case.

On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.

Difficulty

The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree $d$ can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.

Formalization scope

• Polynomials are MvPolynomial (Fin 2) ℝ with variable 0 as $x$ and 1 as $y$; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of $P$ and $Q$, and $H_a(d)$ ranges over fields of degree at most $d$, matching equation (1) of the survey.
• Counts of limit cycles are Set.encard values in ℕ∞, so an infinite family is $\infty$, never silently $0$; $H_a(d)$ is an iSup in ℕ∞, so the goal also asserts finiteness.
• Solutions are global (HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.
• Genericity conditions (i), (iii), (iv) are imposed at complex points of $\mathbb C^2$; (ii), (v) use square-freeness and coprimality in $\mathbb R[x,y]$; "distinct curves" means non-associated polynomials.
• Hyperbolicity of a limit cycle is encoded by a non-zero divergence integral over one period.
• Theorem 1(b) is formalized without its final sentence (existence of a Darboux first integral).
• Trivializing encodings are ruled out: algebraic limit cycles require a non-zero polynomial, and the conjecture is an equality in ℕ∞, not an inequality over a possibly empty family.

Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.

Selected references

• J. Llibre, Sobre el problema 16 de Hilbert, La Gaceta de la RSME 18 (2015), no. 3, 543–554 (source of this mission).
• J. Llibre, R. Ramírez, N. Sadovskaia, On the 16th Hilbert problem for algebraic limit cycles, J. Differential Equations 248 (2010), 1401–1409. https://doi.org/10.1016/j.jde.2009.11.023
• J. Llibre, G. Rodríguez, Configurations of limit cycles and planar polynomial vector fields, J. Differential Equations 198 (2004), 374–380. https://doi.org/10.1016/j.jde.2003.10.008
• C. Christopher, Polynomial vector fields with prescribed algebraic limit cycles, Geom. Dedicata 88 (2001), 255–258. https://doi.org/10.1023/a:1013171019668
• H. Giacomini, J. Llibre, M. Viano, On the nonexistence, existence and uniqueness of limit cycles, Nonlinearity 9 (1996), 501–516. https://doi.org/10.1088/0951-7715/9/2/013
• J. Llibre, Y. Zhao, Algebraic limit cycles in polynomial systems of differential equations, J. Phys. A 40 (2007), 14207–14222. https://doi.org/10.1088/1751-8113/40/47/012
• Yu. Ilyashenko, Centennial history of Hilbert's 16th problem, Bull. Amer. Math. Soc. 39 (2002), 301–354. https://doi.org/10.1090/s0273-0979-02-00946-1
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998), no. 2, 7–15. https://doi.org/10.1007/bf03025291

Motivation

Large retailers hold point-of-sale and loyalty-card data that their suppliers cannot observe, and many of them sell access to it through data-sharing programs; others share the same data for free, or with only some suppliers (Shang, Ha & Tong 2016, §1). When two competing manufacturers sell through one common retailer, sharing a demand signal with a manufacturer changes how he sets his wholesale price, which in turn changes the retailer's margins and the rival's demand. Whether the retailer wants to share, with how many manufacturers, and at what price, is therefore a question about a multistage game with incomplete information.

Shang, Ha and Tong answer it for linear demand, a linear-expectation signal and quadratic production costs, under two contracting protocols. This mission covers the production economy case (marginal cost decreasing in volume, §6 of the paper), in which the retailer may have an incentive to share information even without payment. A companion mission covers production diseconomy (§5).

Setting

Two manufacturers $i \in \{0,1\}$ sell substitutable products through a common retailer. Demand for product $i$ is

$$q_i = a + \theta - (1+\phi)p_i + \phi p_j ,$$

where $p_i$ is the retail price, $\phi > 0$ measures competition intensity and $\theta$ is a demand shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ with $E[Y \mid \theta] = \theta$ and a linear-expectation structure $E[\theta \mid Y] = \beta Y$, where $\beta = \beta(t,\sigma)$ is the signal weight. Producing $q$ units costs $bq - c_e q^2$ with $c_e > 0$; the paper writes $c = -c_e$ and assumes $c_e < 2/(1+\phi)$ (the Assumption, p. 251). Retailing is costless.

The game has three stages.

1. Information contracting. Under concurrent contracting the retailer offers both manufacturers the same payment $T \ge 0$ for the signal; they decide simultaneously and play a Pareto-optimal pure equilibrium. Under sequential contracting she offers a payment $T_f$ to a first manufacturer $k$ and, after his decision, a payment $T_s$ to the other; the outcome is a subgame-perfect equilibrium (SPE). The retailer commits not to share for free after a rejection (§6.2).
2. Pricing. Given the information statuses $X_i \in \{I, U\}$, each manufacturer sets a wholesale price $w_i$ (a function of $Y$ if informed, a constant otherwise), then the retailer sets retail prices; the solution concept is Bayesian Nash equilibrium.
3. Demand realizes and profits are collected.

The ex ante profits of the pricing equilibrium are denoted $\pi_M(0)$, $\pi_M^U(1)$, $\pi_M^I(1)$, $\pi_M(2)$ for a manufacturer and $\pi_R(n)$ for the retailer, $n$ the number of informed manufacturers. $n_e^N$, $n_e^C$, $n_e^S$ denote the equilibrium number of informed manufacturers without contracting, under concurrent and under sequential contracting.

Formalization targets

Goal: Proposition 8(d)

For every $\phi > 0$ and $0 < c_e < 2/(1+\phi)$, pricing equilibria exist, concurrent outcomes and sequential SPEs exist, and for every concurrent outcome and every SPE (either first mover)

$$\Pi_R^C \le \Pi_R^S, \qquad \Pi_M^S \le \Pi_M^C ,$$

where $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The second inequality is asserted for all $c_e$ except at most two values depending only on $\phi$. The comparisons about every pricing equilibrium family exclude the single value $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$ (see Formalization scope). The paper says "higher"; the inequalities are weak because both sides coincide on intervals of positive length.

Milestones

1. Lemma 1: the pricing equilibrium exists and, for $c_e \ne c_e^*$, is unique and linear in $Y$ with explicit coefficients.
2. §4.2: the ex ante profits $\pi_M(\cdot)$ and $\pi_R(\cdot)$ in closed form.
3. Lemma 5(a)–(c) and Lemma 5(d): sign comparisons of these profits in $c_e$, with thresholds $1/(1+\phi)$, $(4+5\phi)/[(2+3\phi)(1+\phi)]$, $c_e^a$ and $c_e^N$.
4. Proposition 7: thresholds $c_e^C$, $c_e^S$ such that

$$n_e^Z = 0 \text{ for } c_e < \tfrac{1}{1+\phi}, \quad n_e^Z = 2 \text{ for } \tfrac{1}{1+\phi} \le c_e < c_e^Z, \quad n_e^Z = 1 \text{ for } c_e^Z \le c_e < \tfrac{2}{1+\phi}.$$

5. Proposition 6(b): the same structure for $n_e^N$ with a threshold $c_e^N$.
6. Proposition 8(a): $c_e^N < c_e^S \le c_e^C$.

Significance

Proposition 8(d) says that a common retailer who sells information prefers to sell it sequentially, and that the manufacturers bear the cost: sequential offers let her extract a larger payment from the first manufacturer, because his outside option depends on what she will do with the second. Together with Propositions 6 and 7 it explains why retailers under production economy share with only a subset of suppliers once economies of scale or competition are strong, and why a retailer may share data for free, a practice the diseconomy model cannot produce.

The results are proved in the paper, partly by "it is straightforward" arguments (the proofs of Lemmas 2–5 are omitted). No part of the paper is formalized. A formalization adds a machine-checked account of the equilibrium selection at the boundary payments, where the paper's case analysis is informal, and of the points at which the retailer is indifferent between outcomes.

Difficulty

The pricing stage is a Bayesian game with a continuum of strategies: an informed manufacturer's strategy is an arbitrary square-integrable function of the signal. Lemma 1's uniqueness needs the Assumption (without it the manufacturer's problem is not concave) and a conditional-expectation argument, not a finite-dimensional computation. The comparisons of Lemma 5 are sign conditions on rational functions of $(c_e, \phi)$ whose thresholds $c_e^a$, $c_e^N$ are implicit roots. The contracting stage is where the naive argument fails: at the boundary payments several equilibria give the retailer the same payoff but the manufacturers different payoffs, so "the" outcome is not well defined there, and a direct comparison of closed-form profits at the paper's selected equilibria does not cover every equilibrium.

Formalization scope

Lean represents manufacturers by Fin 2, statuses by an inductive type with informed and uninformed, and a pricing strategy by a function of the signal value. The committed conventions are these.

1. Admissible strategies are measurable with square-integrable $w_i(Y)$, and constant for an uninformed manufacturer; ex ante optimality over them is the Bayesian equilibrium condition.
2. The retailer's rule is a best response for every wholesale price pair and signal value, off path included.
3. The production cost is the uncapped quadratic $bq - c_e q^2$. The paper caps the quantity at $\bar q = b/(2c_e)$ but assumes the cap is reached with negligible probability (footnote 11, p. 251) and computes every result of §4.2 and §6 without it. The condition $b < a$ of that footnote is not imposed.
4. Contracting uses pure strategies, nonnegative payments, and no free-sharing move after a rejection.
5. A concurrent outcome is a payment and a pure equilibrium whose retailer payoff equals the supremum of her payoffs over Pareto-optimal equilibria. The supremum is not always attained: for large $c_e$ the paper's optimal payment $\pi_M^I(1) - \pi_M(0)$ makes $(U,U)$ an equilibrium that Pareto-dominates the one-informed outcome it selects.
6. Threshold statements take the two-clause form: the stated value of $n$ is attained on each region with its printed endpoints, and is the only value on the region's interior. Thresholds depend only on $\phi$ and are quantified before all other parameters.
7. The manufacturers' comparison in the goal excludes at most two values of $c_e$. At the thresholds $c_e^C$, $c_e^S$ outcomes with different manufacturer totals coexist, and the universal comparison fails.
8. A correction of the paper. At $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$, which lies in $(1/(1+\phi), 2/(1+\phi))$, the slope of the best-response wholesale price (2) is exactly $-1$. The equations $w_i = \hat w_i(w_j)$ are then singular, and every status profile has a continuum of pricing equilibria (for $n = 0$, $w_{1,2} = \bar w \pm t$ for every $t$) whose ex ante profits differ. Lemma 1's uniqueness claim fails there, so do the §4.2 identities for every equilibrium family, and so does every statement built on them. Each statement that quantifies over all pricing equilibria therefore assumes $c_e \ne c_e^*$; existence is still asserted at $c_e^*$.

The ex ante profits in every statement are those of an equilibrium of the pricing game on the signal model, not the §4.2 closed forms; a formalization that defined them by the closed forms would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out. The model layer (signal model, pricing equilibrium, payoff table, both contracting games) is shared, name for name, with the production diseconomy mission. Contributions are welcome on each milestone, and on reusable pieces: linear-expectation signals, and pointwise optimization under conditional expectation.

Selected references

• Shang W., Ha A. Y., Tong S., Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• Ericson W. A., A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969 (cited for the formula of $\beta(t,\sigma)$, which this mission does not use).
• Vives X., Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999, §2.7.2.
• Li L., Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177

Motivation

Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each $0$–$1$ matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.

Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without $Q_6$ or $b(Q_6)$ minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.

Setting

All sets are finite. A clutter $\mathbf L$ is a finite collection of finite sets, no member of which is contained in another; $\emptyset$ and $\{\emptyset\}$ are the two trivial clutters. Its ground set is $E(\mathbf L)=\bigcup_{A\in\mathbf L}A$. The blocker $b(\mathbf L)$ is the collection of minimal subsets of $E(\mathbf L)$ that meet every member of $\mathbf L$, and $\tau(\mathbf L)$ is the minimum cardinality of a member of $b(\mathbf L)$.

$\mathbf L$ is Mengerian if $\mathbf L=\{\emptyset\}$, or if for every weight map $w:E(\mathbf L)\to\mathbb Z^+$ there is an integral packing $q:\mathbf L\to\mathbb Z^+$ with $\sum_{A\ni x}q(A)\le w(x)$ for each $x\in E(\mathbf L)$ and

$$\sum_{A\in\mathbf L}q(A)=\min_{B\in b(\mathbf L)}\sum_{x\in B}w(x).$$

For a set $Z$, the deletion is $\mathbf L\setminus Z=\{A\in\mathbf L:A\cap Z=\emptyset\}$ and the contraction $\mathbf L/Z$ is the collection of minimal members of $\{A-Z:A\in\mathbf L\}$ (minimal, not minimal nonempty). A minor of $\mathbf L$ is any clutter obtained by a finite sequence of deletions and contractions.

A clutter is binary if $|A\cap B|$ is odd for all $A\in\mathbf L$ and $B\in b(\mathbf L)$; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally

$$Q_6=\{\{1,3,5\},\{1,4,6\},\{2,3,6\},\{2,4,5\}\},$$

the triangles of $K_4$ with its edges labelled $1,\dots,6$.

For the structure theory, a circuit of a binary clutter is a minimal nonempty $C\subseteq E(\mathbf L)$ with $|C\cap B|$ even for every $B\in b(\mathbf L)$; $x$ and $y$ are parallel when $\{x,y\}$ is a circuit, and the point $\langle x\rangle$ is the parallel class of $x$. With $mb(\mathbf L)=\{B\in b(\mathbf L):|B|=\tau(\mathbf L)\}$, $\mathbf L$ is critical if $E(mb(\mathbf L))=E(\mathbf L)$. In a critical binary clutter, $x\to y$ means that every member of $mb(\mathbf L)$ containing $x$ contains $y$ while $y\notin\langle x\rangle$, and $y$ is initial if no $x$ has $x\to y$. MBC abbreviates "Mengerian binary clutter".

Formalization targets

Goal: Seymour's theorem (p. 209)

For every binary clutter $\mathbf L$,

$$\mathbf L\ \text{is Mengerian}\iff \mathbf L\ \text{has no minor isomorphic to } Q_6 .$$

Milestones

In the order the proof uses them:

• (2.3) Every minor of a Mengerian clutter is Mengerian.
• Section 1, p. 193. $Q_6$ is not Mengerian. With (2.3) this is the "only if" direction.
• (3.6)(i) Circuits of a binary clutter have at least two elements.
• (3.6)(iii) If $Z\subseteq E(\mathbf L)$ meets every member of $b(\mathbf L)$ evenly, then $Z$ is a disjoint union of circuits. If it meets every member oddly, then $Z$ is a disjoint union of circuits and one member of $\mathbf L$.
• (4.3) In a critical MBC, $x\to y$ implies $y\not\to x$.
• (4.4) In a critical MBC, $x\to y$ gives a circuit $C\ni x,y$ with $|C|\ge3$, $z\to y$ for $z\in C-\{y\}$, and $|B-(C-\{y\})|\ge\tau(\mathbf L)-1$ for $B\in b(\mathbf L)$.
• (4.5) In a critical MBC, a non-initial $x$ lies on a circuit $C$ with $|C|\ge3$ whose other elements are initial and point to $x$, and $|B\cap(C-\{x\})|\le1$ for $B\in mb(\mathbf L)$.
• (4.6) A nontrivial critical MBC has a member consisting of initial elements.
• (5.1) A binary clutter with six elements $x_1,y_1,x_2,y_2,x_3,y_3$ whose only circuits are the three sets $\{x_i,y_i,x_j,y_j\}$, together with a member $A$ that meets each pair $\{x_i,y_i\}$ once and satisfies a minimality condition, has a $Q_6$ minor.

Significance

The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system $Mx\ge1$, $x\ge0$ has integral optimal primal and dual solutions for every integral cost vector, and it identifies $Q_6$ as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid $M$ the port $\Omega(M)$ is Mengerian for every element $\Omega$ if and only if $M$ is binary and has no $F_7^*$ minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining $s$ to $s'$ or $t$ to $t'$ is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).

The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.

Difficulty

The "only if" direction is short: minors of Mengerian clutters are Mengerian, and $Q_6$ fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a $Q_6$-free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and $Q_6$ itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the $Q_6$ minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.

Formalization scope

Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, $E(\mathbf L)$ is the union of members, and deletion and contraction take an arbitrary finite set $Z$. Weights $w$ and packings $q$ are $\mathbb N$-valued. The minimum in the Mengerian condition is expressed as "some $B\in b(\mathbf L)$ of least weight has weight equal to the packing value", never as an infimum. $\{\emptyset\}$ is Mengerian by the paper's convention, and $\tau(\{\emptyset\})$, which the paper leaves undefined, has the junk value $0$ in Lean; every item reading $\tau$ excludes $\{\emptyset\}$ or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a $Q_6$ minor" means that some minor equals the image of $Q_6$ (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.

Four readings would change the theorem and are ruled out: real-valued packings $q$ (the weak max-flow min-cut property, which $Q_6$ has, so the goal would be false), a non-minimal blocker or one not restricted to $E(\mathbf L)$, dropping the $\{\emptyset\}$ exception, and reading "$Q_6$ minor" as literal equality instead of isomorphism.

A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation $\mathbf L_w$. The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts $b(b(\mathbf L))=\mathbf L$, (2.1) and (2.2), and of the equivalences in (3.2) are welcome.

Selected references

• P. D. Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977) 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• J. Edmonds and D. R. Fulkerson, Bottleneck extrema, J. Combin. Theory 8 (1970) 299–306. https://doi.org/10.1016/S0021-9800(70)80083-7
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956) 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conf. Ser. in Appl. Math. 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105

Motivation

In quantum mechanics the spectrum of a Hamiltonian splits into two parts that behave very differently under perturbation. Isolated eigenvalues of finite multiplicity (bound states) move, split or disappear when the operator is changed even slightly; the rest of the spectrum, which carries scattering states and accumulation points of eigenvalues, is far more rigid. Weyl's theorem makes this rigidity precise: if two self-adjoint operators have resolvents that differ by a compact operator, their essential spectra coincide. It is the standard first step in locating the spectrum of a Schrödinger operator $-\Delta + V$: one shows that $V$ is a relatively compact perturbation of $-\Delta$, concludes $\sigma_{ess}(-\Delta + V) = \sigma_{ess}(-\Delta) = [0,\infty)$, and is left with the discrete eigenvalues below zero.

The result goes back to H. Weyl's 1909 work on compact perturbations of bounded self-adjoint operators; the resolvent formulation for unbounded operators is the one used in modern texts such as Reed–Simon (Vol. IV, Sec. XIII.4) and Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Section 6.4, which this mission follows.

Setting

Let $\mathfrak H$ be a complex Hilbert space and $A$ a linear operator with domain $\mathfrak D(A) \subseteq \mathfrak H$. For $z \in \mathbb C$, the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $\mathfrak H$ with a bounded inverse. The resolvent set $\rho(A)$ is the set of such $z$, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$.

The discrete spectrum $\sigma_d(A)$ is the set of eigenvalues $z$ of $A$ that are isolated points of $\sigma(A)$ and whose eigenspace $\operatorname{Ker}(A - z)$ is finite dimensional. The essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$.

A sequence $\psi_n \in \mathfrak D(A)$ with $\|\psi_n\| = 1$, $\langle \varphi, \psi_n \rangle \to 0$ for every $\varphi$ (weak convergence to zero) and $\|(A - z)\psi_n\| \to 0$ is a singular Weyl sequence for $A$ at $z$.

An operator is compact if it maps bounded sets to relatively compact sets; $\mathfrak C(\mathfrak H)$ denotes the compact operators. An operator $K$ is relatively compact with respect to $A$ if $\mathfrak D(A) \subseteq \mathfrak D(K)$ and $K R_A(z) \in \mathfrak C(\mathfrak H)$ for one $z \in \rho(A)$. $B$ is $A$ bounded if $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\|B\psi\| \le a\|A\psi\| + b\|\psi\|$ on $\mathfrak D(A)$; the infimum of admissible $a$ is the $A$-bound. A symmetric operator $A$ has defect indices $d_\pm(A) = \dim \operatorname{Ran}(A \pm i)^\perp$.

Formalization targets

Goal: Weyl's theorem (Theorem 6.19)

For self-adjoint $A$ and $B$,

$$\exists\, z \in \rho(A) \cap \rho(B):\ R_A(z) - R_B(z) \in \mathfrak C(\mathfrak H) \quad\Longrightarrow\quad \sigma_{ess}(A) = \sigma_{ess}(B).$$

Milestones

• Weyl criterion (Lemma 6.17). For self-adjoint $A$: $z \in \sigma_{ess}(A)$ if and only if a singular Weyl sequence at $z$ exists; if so, it can be chosen orthonormal.
• Compact perturbations (Lemma 6.18). For self-adjoint $A$ and compact self-adjoint $K$, $\sigma_{ess}(A + K) = \sigma_{ess}(A)$, and

$$\sigma_{ess}(A) = \bigcap_{K \in \mathfrak C(\mathfrak H),\, K^* = K} \sigma(A + K).$$

• Independence of $z$ (Lemma 6.21, first part). If $R_A(z) - R_B(z)$ is compact for one $z \in \rho(A) \cap \rho(B)$, it is compact for all such $z$.
• Self-adjoint extensions (Theorem 6.20). If $A$ is symmetric with $d_+(A) = d_-(A) < \infty$, all self-adjoint extensions of $A$ have the same essential spectrum.
• Relative compactness is infinitesimal (Lemma 6.22). For self-adjoint $A$, a relatively compact $K$ has $A$-bound $0$.
• Stability of relative compactness (Lemma 6.23). If $A$ is self-adjoint, $B$ symmetric with $A$-bound less than one, and $K$ relatively compact with respect to $A$, then $K$ is relatively compact with respect to $A + B$.

Significance

The result. Weyl's theorem reduces the determination of the essential spectrum of a perturbed operator to that of a simpler reference operator. Combined with Lemma 6.22 and the Kato–Rellich theorem, it yields $\sigma_{ess}(A + K) = \sigma_{ess}(A)$ for every relatively compact symmetric $K$; Lemma 6.23 extends this to perturbations of the form $B + K$. These are the inputs to the HVZ theorem for $N$-body systems, to the spectral analysis of one-particle Schrödinger operators with decaying potentials, and, via Theorem 6.20, to the observation that boundary conditions at a limit-circle endpoint do not affect the essential spectrum of a Sturm–Liouville operator. The Weyl criterion is independently useful: it is how points are shown to lie in $\sigma_{ess}$ in concrete examples.

Formalizing it. The results are classical and proved in every text on the subject. None of them is formalized: Mathlib has compact operators and the adjoint of a densely defined LinearPMap, but no resolvent set or spectrum for unbounded operators, no discrete or essential spectrum and no relative compactness. This mission asks for formal proofs of Teschl's statements and, with them, a reusable layer of definitions (resolvent of a LinearPMap, $\sigma_d$, $\sigma_{ess}$, singular Weyl sequences, relative compactness) on which later chapters (free Schrödinger operator, HVZ theorem) can build.

Difficulty

The obvious route to all of these statements goes through the spectral theorem: Teschl's proof of the Weyl criterion uses spectral projections $P_A((\lambda - \varepsilon, \lambda + \varepsilon))$ and spectral measures $\mu_{\psi_n}$, and his characterization (6.27)–(6.28) of $\sigma_{ess}$ by ranks of spectral projections presupposes the functional calculus. Mathlib has no spectral theorem for unbounded self-adjoint operators, so this route requires either building it or finding arguments that avoid it. The definition of $\sigma_{ess}$ used here is deliberately the PVM-free one of p. 145, which makes the statements expressible now but moves the difficulty into the proofs: showing that a point of $\sigma(A) \setminus \sigma_d(A)$ carries a singular Weyl sequence requires controlling approximate eigenvectors near a non-isolated spectral point or an eigenvalue of infinite multiplicity without projections.

A second difficulty is domain bookkeeping. $A + K$, $A + B$, $K R_A(z)$ and $R_{A+B}(z)$ all involve unbounded operators with different domains, and identities such as the second resolvent formula $K R_{A+B}(z) = K R_A(z)(\mathbb I - B R_{A+B}(z))$ must be established on the correct domains. Theorem 6.20 requires relating the resolvents of two self-adjoint extensions through the finite-dimensional defect spaces.

Formalization scope

The Hilbert space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since no statement of the section needs it. Unbounded operators are Mathlib LinearPMaps H →ₗ.[ℂ] H, self-adjointness is Mathlib's IsSelfAdjoint (which implies a dense domain), and symmetric operators are densely defined by definition, as in the book. The resolvent is the bounded two-sided inverse of $A - z$ of p. 73 (IsResolventAt), and $\rho(A)$, $\sigma(A)$ are defined from it; Mathlib's Banach-algebra spectrum is not used. "For one $z \in \rho(A) \cap \rho(B)$" is an existential over $z$ and the two resolvents. Compactness is Mathlib's IsCompactOperator, which on a Hilbert space agrees with the book's norm closure of finite rank operators. $A + K$ for bounded $K$ is K +ᵥ A (domain $\mathfrak D(A)$); $A + B$ for unbounded $B$ is the LinearPMap sum with domain $\mathfrak D(A) \cap \mathfrak D(B)$. The $A$-bound is valued in $[0,\infty]$ and is $\infty$ for an operator that is not $A$ bounded. The defect indices are "equal and finite" when both defect spaces are finite dimensional with equal finrank.

No projection-valued measure or functional calculus is taken as data, and none is needed: every statement is phrased without $f(A)$. For this reason the second half of Lemma 6.21, $f(A) - f(B) \in \mathfrak C(\mathfrak H)$ for $f \in C_\infty(\mathbb R)$, and the form-compactness results Lemma 6.26 and Corollary 6.27 of Section 6.5 are not part of the mission.

A trivializing formalization is ruled out: the discrete spectrum requires all three of "eigenvalue", "isolated in $\sigma(A)$" and "finite-dimensional eigenspace", so $\sigma_{ess}$ is neither empty nor all of $\sigma(A)$ by definition, and the resolvent hypothesis of Weyl's theorem is an existential over genuine resolvents, never a junk value outside $\rho(A)$.

A complete development needs the resolvent identities for LinearPMaps, the relation between self-adjointness and real spectrum, weak convergence of bounded sequences, and the fact that compact operators map weakly null sequences to norm-null ones. The definitions of resolvent, $\sigma_{ess}$, relative compactness and $A$-bound are shared with other chapters of this series and are intended for reuse. Contributions of general lemmas on LinearPMap resolvents are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Section 6.4. https://doi.org/10.1090/gsm/099
• H. Weyl, Über beschränkte quadratische Formen, deren Differenz vollstetig ist, Rendiconti del Circolo Matematico di Palermo 27 (1909), 373–392. https://doi.org/10.1007/BF03019655
• M. Reed and B. Simon, Methods of Modern Mathematical Physics IV: Analysis of Operators, Academic Press, 1978, Section XIII.4.
• T. Kato, Perturbation Theory for Linear Operators, 2nd ed., Springer, 1980, Section IV.5. https://doi.org/10.1007/978-3-642-66282-9

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716

Why holomorphic functions of several variables

Several complex variables studies functions of $z = (z_1, \dots, z_n) \in \mathbb{C}^n$ that are holomorphic in every coordinate. It underlies complex geometry, the theory of analytic spaces, and parts of mathematical physics and harmonic analysis. Every later topic of the subject (domains of holomorphy, pseudoconvexity, the $\bar\partial$-problem, the Bergman kernel, analytic varieties) starts from the same foundation: a function that is holomorphic in each variable separately and locally bounded is jointly smooth and is locally the sum of a convergent power series. This mission formalizes that foundation as it appears in the first chapter of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv).

Historically, the step from separate to joint regularity is due to Osgood (1899), who showed that a continuous (later: locally bounded) function that is holomorphic in each variable separately is holomorphic; Hartogs (1906) later removed the boundedness assumption altogether, a much harder theorem not covered here.

Setting

Points of $\mathbb{C}^n$ are $z = (z_1, \dots, z_n)$. For a center $a \in \mathbb{C}^n$ and a polyradius $\rho = (\rho_1, \dots, \rho_n)$ with every $\rho_k > 0$, the polydisc is

$$\Delta_\rho(a) = \{ z \in \mathbb{C}^n : |z_k - a_k| < \rho_k,\ k = 1, \dots, n \},$$

a product of open discs $\Delta_1 \times \cdots \times \Delta_n$. Its distinguished boundary is the torus $\Gamma = \partial\Delta_1 \times \cdots \times \partial\Delta_n = \{ |\zeta_k - a_k| = \rho_k \text{ for all } k \}$, and $\overline{\Delta}$ denotes the closed polydisc.

A function $f$ on an open set $U \subset \mathbb{C}^n$ is holomorphic (the book's Definition 1.1.2) if it is locally bounded (every point of $U$ has a neighborhood on which $f$ is bounded) and complex-differentiable in each variable separately: for every $z \in U$ and every $k$, the one-variable limit

$$\lim_{\xi \to 0} \frac{f(z_1, \dots, z_k + \xi, \dots, z_n) - f(z)}{\xi}$$

exists. A map $f = (f_1, \dots, f_m) : U \to \mathbb{C}^m$ is holomorphic if every component is.

A multi-index is $\alpha = (\alpha_1, \dots, \alpha_n) \in \mathbb{N}_0^n$, with $\alpha! = \alpha_1! \cdots \alpha_n!$, $(z-a)^\alpha = \prod_k (z_k - a_k)^{\alpha_k}$ and $\rho^\alpha = \prod_k \rho_k^{\alpha_k}$. A power series $\sum_\alpha c_\alpha (z-a)^\alpha$ is summed over all multi-indices; since $\mathbb{N}_0^n$ has no natural order, convergence means absolute convergence, and the series converges uniformly absolutely on a set $X$ when $\sum_\alpha |c_\alpha (z-a)^\alpha|$ converges uniformly for $z \in X$. The Wirtinger derivative is $\partial/\partial z_k = \tfrac12(\partial/\partial x_k - i\,\partial/\partial y_k)$ for $z_k = x_k + i y_k$, and $\partial^{|\alpha|}/\partial z^\alpha$ applies $\partial/\partial z_k$ exactly $\alpha_k$ times for each $k$.

Formalization targets

Goal: Theorem 1.2.1 (power series on a polydisc)

Let $\Delta = \Delta_\rho(a)$ be a polydisc. If $f : \overline{\Delta} \to \mathbb{C}$ is continuous and holomorphic in $\Delta$, then there are coefficients $c_\alpha$ with

$$f(z) = \sum_\alpha c_\alpha (z-a)^\alpha \qquad (z \in \Delta),$$

the series converging uniformly absolutely on every compact subset of $\Delta$. Conversely, a function defined on $\Delta$ by such a series is holomorphic on $\Delta$. Both directions are part of the goal.

Milestones

In attack order:

1. Proposition 1.1.3. A holomorphic function on an open $U$ is $C^\infty$, and every $\partial f/\partial z_k$ is again holomorphic.
2. Theorem 1.1.4 (Cauchy integral formula). For $f$ continuous on $\overline{\Delta}$ and holomorphic in $\Delta$, and $z \in \Delta$,

$$f(z) = \frac{1}{(2\pi i)^n} \int_\Gamma \frac{f(\zeta)}{(\zeta_1 - z_1)\cdots(\zeta_n - z_n)}\, d\zeta_1 \wedge \cdots \wedge d\zeta_n.$$

3. Proposition 1.2.2. The derivative formula $\frac{\partial^{|\alpha|} f}{\partial z^\alpha}(z) = \frac{1}{(2\pi i)^n}\int_\Gamma \frac{\alpha!\, f(\zeta)}{(\zeta - z)^{\alpha+1}}\,d\zeta$, the coefficient formula $c_\alpha = \frac{1}{\alpha!}\frac{\partial^{|\alpha|} f}{\partial z^\alpha}(a)$, and the Cauchy estimates $|c_\alpha| \le \|f\|_\Gamma / \rho^\alpha$.
4. Proposition 1.2.3. A limit, uniform on compact subsets, of holomorphic functions is holomorphic, and all derivatives $\partial^{|\alpha|}/\partial z^\alpha$ converge uniformly on compact subsets.
5. Theorem 1.2.7 (identity theorem). On a domain, a holomorphic function vanishing on a nonempty open subset vanishes identically.
6. Theorem 1.2.8 (maximum principle). On a domain, if $|f|$ has a local maximum at $a$, then $f \equiv f(a)$.
7. Theorem 1.3.5. Compositions of holomorphic mappings are holomorphic.
8. Proposition 1.3.7. For holomorphic $f : U \to \mathbb{C}^n$, $|\det Df(p)|^2 = \det D_{\mathbb{R}} f(p)$.

Significance

Theorem 1.2.1 is the statement that makes the theory of several complex variables possible: it identifies the book's elementary, one-variable-at-a-time definition of holomorphy with local representability by power series. Uniqueness of the coefficients, the Cauchy estimates, the identity theorem, the maximum principle, and holomorphy of compositions and of implicit functions all follow from it, and every later chapter of the book (Hartogs figures, pseudoconvexity, the Bergman kernel, Weierstrass preparation) uses it without comment.

Mathlib already develops complex analysis in several variables for Fréchet-differentiable maps: analyticity of DifferentiableOn ℂ functions, torusIntegral, Cauchy integrals over circles, and Osgood-type regularity for maps on $\mathbb{C}^n$ are available or published on the platform. What this mission adds is the bridge from the weaker separate notion of holomorphy, with local boundedness, to these results, stated with multi-index power series and uniform absolute convergence on compact sets exactly as in the textbook. The results are classical and fully proved in the book; none has a machine-checked proof in this form.

Difficulty

The hypothesis controls $f$ only along complex lines parallel to the coordinate axes, plus a bound. Nothing in the definition says that $f$ is continuous, let alone jointly differentiable, so no joint limit, Fréchet derivative, or change of the order of integration is available at the start. Every tool that the one-variable theory and Mathlib's multivariable library supply presupposes joint regularity; the obstacle is to obtain it from separate information.

A second difficulty is bookkeeping: power series over $\mathbb{N}_0^n$ have no natural order, so convergence must be handled as unconditional summation with a uniformity statement over compact sets, and iterated Wirtinger derivatives must be related to derivatives of the series term by term.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ; multi-indices are Fin n → ℕ. A polyradius is ρ : Fin n → ℝ with the hypothesis ∀ k, 0 < ρ k; the polydisc is defined coordinatewise (not Metric.ball, which only gives equal radii).
• Holomorphy is the book's Definition 1.1.2, IsHolomorphicOn f U: local boundedness plus complex differentiability at $\xi = 0$ of $\xi \mapsto f(z_1, \dots, z_k + \xi, \dots, z_n)$ (via Function.update). Openness of $U$ is a hypothesis wherever the book says "open". Maps into $\mathbb{C}^m$ are holomorphic componentwise.
• Ruled out: defining holomorphy as Mathlib's DifferentiableOn ℂ. That makes Proposition 1.1.3 and the first half of the goal off-target (they would follow from existing library results) and is not the book's definition.
• The closed polydisc is closure (polydisc a ρ); "continuous on $\overline{\Delta}$, holomorphic in $\Delta$" keeps both hypotheses.
• Power series: HasSum (unconditional summation) of the terms $c_\alpha (z-a)^\alpha$ to $f(z)$, and uniform absolute convergence on a set $X$ means the finite partial sums of $|c_\alpha (z-a)^\alpha|$, directed by inclusion, converge uniformly on $X$. Mathlib's HasFPowerSeriesOnBall is not used: its balls for the sup norm are equiradial polydiscs only.
• The integral over $\Gamma$ is torusIntegral, whose parametrization $\zeta_k = a_k + \rho_k e^{i\theta_k}$ includes the Jacobian $\prod_k i\rho_k e^{i\theta_k}$ and orients each circle positively. The integrands are continuous on the compact torus, so no integrability hypothesis is needed.
• $\partial/\partial z_k$ is defined from real partial derivatives (deriv along $t \mapsto z_k + t$ and $t \mapsto z_k + it$); $\partial^{|\alpha|}/\partial z^\alpha$ iterates it. $\det D_{\mathbb{R}} f(p)$ is LinearMap.det of the real Fréchet derivative, which is basis independent.
• The Cauchy estimate is stated for every bound $M$ of $|f|$ on $\Gamma$, which is equivalent to the book's $\|f\|_\Gamma$ form.

A complete development needs the one-variable Cauchy integral formula (in Mathlib), iterated circle integrals and torusIntegral, and summation over Fin n → ℕ. The regularity bridge from separate to joint holomorphy and the multi-index power-series API are reusable across the whole series of missions on this book; contributions of either as standalone lemmas are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 1, §§1.1–1.3. https://www.jirka.org/scv/scv.pdf
• W. F. Osgood, "Note über analytische Functionen mehrerer Veränderlichen", Mathematische Annalen 52 (1899), 462–464.
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Chapter II.

Motivation

Chapter 8 is where discrete convex analysis explains why it needed two separate notions — M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly dual to each other, the discrete analogue of the fact that convex analysis's transform is self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a real-variable M-/L-convex-function layer the series had not yet built. That layer now exists, built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the Edmonds intersection theorem's own combinatorics is built from.

Setting

Fix a finite ground set $V$. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup_x [\langle p,x\rangle - f(x)]$. A polyhedral convex function $f$ is M-convex ($f \in M[\mathbb R \to \mathbb R]$) if it satisfies (M-EXC[R]); $g$ is L-convex ($g \in L[\mathbb R \to \mathbb R]$) if it satisfies (SBF[R]) and (TRF[R]). A concave function $h$ is always represented via $h_2 = -h$, an ordinary convex function, so every "$f \ge h$" hypothesis is restated as "$f + h_2 \ge 0$" — an equivalent formulation avoiding any need to represent $-\infty$ in the codomain. A polyhedral cone's polar is $C^\circ = \{y : \langle y,x\rangle \le 0\ \forall x \in C\}$. A function is M2-convex if it is the sum of two M-convex functions.

Formalization targets

Goal: the conjugacy theorem (Theorem 8.4)

The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one correspondence under the Legendre-Fenchel transform: $f \in M \Rightarrow f^\bullet \in L$, $g \in L \Rightarrow g^\bullet \in M$, and the transform is an involution ($f^{\bullet\bullet}=f$, $g^{\bullet\bullet}=g$) on each class, with the identical statement for the M$^\natural$/L$^\natural$ variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing infrastructure this series has since built.

Supporting structural targets

Twelve further results build the surrounding theory. Proposition 8.2 gives the easy two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31 (plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex, and their global optimality reduces to a finite local check.

Significance

The goal is the theorem that retroactively explains this entire series' two-track structure: missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are not two independent theories that happen to share techniques — they are conjugate images of each other, so every theorem proved on one side has a dual counterpart automatically available on the other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the diagram the book draws connecting $M_0[\mathbb R]$, $0L[\mathbb R\to\mathbb R]$, and submodular set functions $S[\mathbb R]$ (already correspondences this series proved independently, in missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of one single conjugacy fact rather than three separate coincidences. The separation and Fenchel duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex optimization course opens with, and the book is explicit that they are not corollaries of the classical versions plus convex extensibility — they carry genuinely combinatorial content, specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as examples the book itself gives.

None of these results are open — they are Murota's account of the duality at the heart of discrete convex analysis, the reason the theory needed two dual notions rather than one. What this mission contributes is a faithful, machine-checked formal statement of each, completing a theorem mission 10-conjugacy-i explicitly left for a future session once the necessary polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for $g^\bullet$ directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of $g$ itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about $g$'s own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result in this chunk requires — see HARD.md. Concave functions $h$ are always represented via $h_2 = -h$ and every inequality $f \ge h$ restated as $f + h_2 \ge 0$, avoiding WithTop ℝ negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate (printed = PDF $-$ 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every citation here uses the corrected offset. This mission's base vocabulary is redeclared from missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral M-/L-convex conjugacy theory this mission's real-variable results are drawn from).

Motivation

An investor with a fixed planning horizon, an initial fortune, and a personal attitude toward risk (a utility function) wants to allocate wealth between a riskless bond and several risky assets, rebalancing at each of $N$ periods, to maximize the expected utility of terminal wealth. This is the oldest and most basic problem of mathematical finance's dynamic-programming tradition, going back to Samuelson (1969) and Merton (1969, continuous time). Bäuerle and Rieder's Chapter 4 is where the abstract finite-horizon Markov Decision Process theory built up in Chapter 2 — the Bellman equation, existence of optimal policies under compactness and continuity, propagation of concavity through the value function — is first put to genuine financial work: the multiperiod terminal-wealth problem is shown to be exactly an instance of that general theory, and the reduction pays off immediately in six closed-form solutions for the standard families of utility functions used throughout the literature (power, HARA, logarithmic, exponential).

Setting

An investor with utility function $U : \mathrm{dom}\,U \to \mathbb{R}$ (Definition 3.4.1: strictly increasing, strictly concave, continuous) and wealth $x$ invests in a bond (interest rate $i_{n+1}$ on $[n,n+1)$) and $d$ risky assets with relative risk $R_{n+1}$ (Chapter 3). The one-period problem: admissible investments $D(x) := \{a \in \mathbb{R}^d : (1+i)(x+a\cdot R) \in \mathrm{dom}\,U \text{ a.s.}\}$, $u(x,a) := \mathbb{E}[U((1+i)(x+a\cdot R))]$, $v(x) := \sup_{a \in D(x)} u(x,a)$. The multiperiod problem is the $N$-stage Markov Decision Model with state space $E := \mathrm{dom}\,U$ (wealth), action space $\mathbb{R}^d$, transition $T_n(x,a,z) = (1+i_{n+1})(x+a\cdot z)$, zero one-stage reward, terminal reward $g_N := U$; its value functions are $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[U(X_N)]$ over Markov portfolio strategies $\pi$.

Formalization targets

Goal — Theorem 4.2.2

$$V_N = U, \qquad V_n(x) = \sup_{a \in D_n(x)} \mathbb{E}\bigl[V_{n+1}\bigl((1+i_{n+1})(x+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave and continuous, and an optimal portfolio strategy $(f_0^*,\dots,f_{N-1}^*)$ realized by maximizers of the recursion. This is the structural result every closed-form solution below specializes.

Eight milestones: the one-period existence/regularity theorem the induction step reduces to (Theorem 4.1.1); the upper bounding function that makes Chapter 2's existence machinery apply (Proposition 4.2.1); the zero-mean special case (Theorem 4.2.4); and four utility-specific closed forms plus the binomial-model comparative-statics lemma (Theorems 4.2.6, 4.2.11, 4.2.13, 4.2.15; Lemma 4.2.9).

Significance

Theorem 4.2.2 is the template for every dynamic portfolio problem in the rest of this book (consumption-investment in Chapter 4 §4.3-4.4, mean-variance and index tracking later in Chapter 4, and the partially-observed and jump-market analogues in Chapters 6 and 9): check a handful of structural conditions on the market data, and the existence, regularity, and recursive computability of the optimal policy follow automatically from Chapter 2's general theory rather than needing a bespoke argument each time. The six closed-form corollaries are the results practitioners actually use: the power/HARA/log/exponential-utility feedback rules are the standard textbook portfolio formulas (the logarithmic case is Kelly betting; the exponential case's wealth-independent optimal amount is the CARA-utility hallmark used throughout insurance and reinsurance mathematics), and Lemma 4.2.9's monotonicity result is the discrete-time analogue of the Merton ratio's dependence on the market's risk premium.

No result of this chunk was found on the platform (searched "terminal wealth", "portfolio optimization", "power utility", "HARA utility"). The proofs are complete in the book and mostly short (each utility-specific theorem reduces to checking the Structure Assumption via a transformation to a fraction-of-wealth variable); this mission's contribution is the precise formal statement of each closed form, with its own explicit recursion for $d_n$, since the six theorems share a structure but genuinely differ in which one-period sub-problem and which scaling variable ($x$, $x+bS^0_n/S^0_N$, or a wealth-independent constant) each uses.

Difficulty

The obvious shortcut for the goal is to prove existence of an optimal policy and its concavity/monotonicity properties by separate, ad hoc arguments at each stage; the actual content of Theorem 4.2.2 is that both reduce, via Theorem 4.1.1, to a single one-period fact applied identically at every stage — the induction step is exactly "if $v \in \mathrm{I\!M}_{n+1}$ [strictly increasing/concave/continuous with linear growth], then $v$ is a utility function on $E$ up to the growth bound, so Theorem 4.1.1 applies directly to $T_n v$." Missing this reduction leads to reproving compactness/upper-semicontinuity arguments from Chapter 2 by hand at every stage instead of invoking Theorem 4.1.1 once per stage. For the six closed-form theorems, the shared trap is conflating the different one-period sub-problems: the power- and HARA-utility theorems solve the same sub-problem (4.7) after a wealth-shift transformation, while the exponential-utility theorem's sub-problem (4.13) has a fundamentally different scaling (the optimal amount, not fraction, is wealth-independent) — collapsing these into one "utility-agnostic" statement would hide exactly the distinction the book is making.

Formalization scope

The multiperiod value function V is defined as an explicit supremum over admissible Markov portfolio strategies (not the Bellman recursion itself, and not full history-dependent strategies), following the book's own citation of Theorem 2.2.3 to justify restricting to Markov strategies for this model; this keeps the goal's parts (b)/(c) genuine content rather than restatements of the value function's own definition. The one-period vocabulary (OnePeriodD/OnePeriodU/OnePeriodV, NoArbitrageOnePeriod) is a self-contained restatement matching §4.1's own notation (a single $i$, $R$, no time index), independent of chunk 03's full market/portfolio apparatus, since Theorem 4.1.1's own content is exactly this one-period reduction. Proposition 4.2.1's proof cites two facts as already established elsewhere in the book (a concave function is dominated by an affine function; no-arbitrage bounds admissible actions linearly in wealth) — both are taken as explicit hypotheses of the Lean statement rather than re-derived, since re-deriving them is not this proposition's own content. HARA and power utility share one sub-problem definition (Afrac/vPower, Eq. (4.7)); logarithmic and exponential utility each need their own (AfracLog/vLog, vExp, Eqs. (4.11), (4.13)) since their admissibility sets and objective functions genuinely differ (a strict vs. non-strict inequality; a fraction vs. an absolute amount).

No trivializing formalization: each of the six closed-form theorems states its own explicit recursion for $d_n$ (a finite product or sum over $k=n,\dots,N-1$ of genuinely different per-stage terms) rather than a shared abstract "some sequence $d_n$ exists with $V_n = d_n \cdot (\text{shape})$" — the latter would hide exactly which recursion each utility function produces, the actual content the brief for this chunk flags as the point of having six near-identical theorems rather than one parametrized statement. Optimal strategies are stated in their exact feedback form ($f_n^*(x) = \alpha_n^* x$, or the HARA-specific affine shift, or the wealth-independent exponential-utility amount), not merely asserted to exist.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• R. C. Merton, "Lifetime portfolio selection under uncertainty: the continuous-time case", Review of Economics and Statistics, 1969 (the continuous-time analogue this discrete-time theory approximates, per Chapter 3's binomial-to-Black-Scholes convergence result).