All missions

Motivation

The logarithm of a share price is commonly modelled as a Brownian motion with drift, $X_t=\sigma B_t+ct$. The Black–Scholes option pricing formula needs the volatility $\sigma$ but not the drift $c$, so a practitioner must estimate $\sigma^2$ from data. Observing the whole path would give $\sigma^2$ exactly through its quadratic variation, but a real observer sees far less. The most readily available daily information is the opening and closing prices together with the day's high and low.

Parkinson (1980) proposed an estimator from the high–low range, and Garman and Klass (1980) found the minimum-variance estimator among a class of quadratic functions of high, low and close. Both were derived assuming zero drift, $c=0$, and the Garman–Klass estimator is biased when $c\neq0$. Rogers and Satchell (Ann. Appl. Probab. 1 (1991) 504–512) proposed the estimator

$$\hat\sigma^2\equiv S_1(S_1-X_1)+I_1(I_1-X_1),$$

which is unbiased for every drift. Their estimator is now a standard tool in empirical finance for range-based volatility measurement.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying a standard Brownian motion $B=(B_t)_{t\ge0}$: $B_0=0$, its increments over disjoint intervals are independent and Gaussian with variance equal to the length of the interval, and every sample path $t\mapsto B_t(\omega)$ is continuous. Fix a drift $c\in\mathbb R$ and a volatility $\sigma\ge0$. The log-price is

$$X_t=\sigma B_t+ct,\qquad t\ge0,$$

and, for a trading period $[0,t]$, the running maximum and running minimum are

$$S_t=\sup_{0\le u\le t}X_u,\qquad I_t=\inf_{0\le u\le t}X_u.$$

Thus $S_t$, $I_t$ and $X_t$ are the high, the low and the close of the log-price (with the open normalized to $X_0=0$). In Lean these are logPrice σ c B t ω, runMax σ c B t ω and runMin σ c B t ω in the namespace RogersSatchell.Unbiased.

The proof in the paper passes through an exponential time: a random variable $T$ with $P(T>x)=e^{-\lambda x}$ (rate $\lambda>0$, mean $\lambda^{-1}$), independent of the whole path $B$. For $\sigma>0$ the rates

$$\alpha=\frac{\sqrt{c^2+2\lambda\sigma^2}-c}{\sigma^2},\qquad \beta=\frac{\sqrt{c^2+2\lambda\sigma^2}+c}{\sigma^2}$$

appear, in Lean alpha σ c lam and beta σ c lam.

Formalization targets

Goal: display (3)

For every $c\in\mathbb R$, every $\sigma\ge0$ and every $t\ge0$, $S_t(S_t-X_t)+I_t(I_t-X_t)$ is integrable and

$$E\big[S_t(S_t-X_t)+I_t(I_t-X_t)\big]=\sigma^2t.$$

At $t=1$ this is the unbiasedness of $\hat\sigma^2$ of display (2). The statement quantifies over all drifts; the absence of $c$ on the right-hand side is the content.

Milestones (Section 2, pp. 505–506)

1. At an independent exponential time $T$ of rate $\lambda$: $S_T\sim\operatorname{Exp}(\alpha)$ and $-I_T\sim\operatorname{Exp}(\beta)$.
2. The Wiener–Hopf splitting: $S_T$ and $S_T-X_T$ are independent, and $S_T-X_T$ has the law of $-I_T$.
3. $E[S_T(S_T-X_T)]=1/(\alpha\beta)=\sigma^2/2\lambda$.
4. $E[S_T(S_T-X_T)]=\int_0^\infty\lambda e^{-\lambda t}\,E[S_t(S_t-X_t)]\,dt$.
5. $E[S_t(S_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
6. $E[I_t(I_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
7. (off the goal's path) With $Y_1=S_1(S_1-X_1)$, $Y_2=I_1(I_1-X_1)$: $E Y_1^2=EY_2^2=\sigma^4/2$, $E(Y_1+Y_2)^2\le2\sigma^4$ and $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, for every drift $c$.

Significance

The goal certifies a drift-free unbiased volatility estimator built from four numbers per trading day. Because only $\sigma^2$ enters the Black–Scholes formula, an estimator whose mean does not depend on the nuisance parameter $c$ is exactly what is needed. Milestone 7 complements this with a drift-uniform bound on its variance, $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, while the exact value $0.331\sigma^4$ quoted in the paper is only available at $c=0$.

On the formalization side, the results are classical and proved; none is machine-checked as far as the platform's catalog shows. A complete development would give the first formal treatment of the joint law of the running maximum of drifted Brownian motion at an exponential time, of the Wiener–Hopf splitting at the maximum, and of a Laplace-inversion argument for a moment function of the time horizon. All three are reusable well beyond volatility estimation: in ruin theory, queueing (reflected Brownian motion), and the pricing of lookback and barrier options.

Difficulty

The obvious approach, computing $E[S_t(S_t-X_t)]$ directly from the joint density of $(S_t,X_t)$ for drifted Brownian motion, requires the reflection principle combined with a Girsanov change of measure, followed by a double integral involving Gaussian tails, done separately for each sign of $c$. The cancellation that makes the drift disappear is not visible in that computation, and a statement specialized to $c=0$ (where the reflection principle alone suffices) does not carry over. Every step of the milestone list rests on path properties of Brownian motion (the strong Markov property, the law of the running maximum, splitting at the maximum) that Mathlib does not yet provide for IsBrownianReal, and the passage from milestone 4 to milestone 5 needs uniqueness of the Laplace transform.

Formalization scope

• Brownian motion is Mathlib's ProbabilityTheory.IsBrownianReal B P with B : ℝ≥0 → Ω → ℝ, plus the hypothesis that every sample path is continuous (the standard choice of a continuous version). Time is ℝ≥0.
• $S_t$ and $I_t$ are the real sSup/sInf of the path over the interval $[0,t]$; with continuous paths they are attained. The supremum is never taken over all times or in extended reals.
• "$E$" is the Bochner integral, and every expectation identity also asserts integrability, so no identity can hold through Lean's convention that a non-integrable function integrates to $0$.
• "$T$ exponential with mean $\lambda^{-1}$" is HasLaw T (expMeasure λ) P; "parameter $\alpha$" is read as rate $\alpha$. "Independent of $B$" is independence from the path-valued random variable with the product σ-algebra. $S_T$ is evaluated at $T$ truncated to $[0,\infty)$.
• "Has the same law as" is equality of image measures, together with the almost-everywhere measurability of both maps.
• "Inversion of the Laplace transform gives" becomes the fixed-time identity for every $t\ge0$ (milestones 5 and 6), separate from the Laplace identity (milestone 4).
• Milestones 1 and 3 assume $\sigma>0$ because $\alpha,\beta$ divide by $\sigma^2$; the Wiener–Hopf splitting, the goal, and milestones 4–7 allow $\sigma\ge0$.

A formalization that specializes to $c=0$, takes the supremum over all of $[0,\infty)$, or omits the integrability conjuncts is not the statement of this mission.

Infrastructure that a complete development needs: the reflection principle or the strong Markov property for Brownian motion, the exponential-time law of the running maximum of a Lévy process, and uniqueness of Laplace transforms for continuous functions. All of these are reusable; contributions of any of them are welcome. Related platform items cover other objects and are credited here: running maxima and exit problems for spectrally negative Lévy processes (Avram2004.Exit.reflected), a drifted Brownian motion in characteristic-function form in a queueing-network setting (Reiman84.QueueLength.Paths), and a GI/G/1 Wiener–Hopf transform identity (QueueingFundamentals.GG1.wiener_hopf_transform).

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4), 1991, 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1), 1980, 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1), 1980, 61–65. https://doi.org/10.1086/296071
• P. Greenwood and J. Pitman, Fluctuation identities for Lévy processes and splitting at the maximum, Advances in Applied Probability 12(4), 1980, 893–902. https://doi.org/10.2307/1426747

Why a grid has a tangle

Robertson and Seymour introduced tangles as a way to describe a region of a graph that cannot be isolated by a separation of low order. A separation divides the edges into two sides, and its order counts the vertices shared by those sides. A tangle makes a consistent choice of the side regarded as small at every order below a threshold. This turns an informal idea of a highly connected region into an object with explicit axioms. In Graph Minors. X, the authors connect tangles with branch-width, tree-width and grid minors; the grid construction is the direct example behind that connection. The paper states the existence of a tangle of order $\theta$ in every $\theta$-grid as (7.3) on p. 173. Robertson and Seymour, 1991.

The result is already proved in the paper. The present target is its Lean statement and proof, together with the two numbered results from §7 on which the construction rests. This mission concerns the grid itself. The paper's further assertion that a grid minor induces a tangle in a larger graph uses the separate minor-transfer result (6.1), whose edge identities require additional definitions. Robertson and Seymour, 1991, pp. 170–173.

The grid, its edge boundary and its small sets

Fix an integer $\theta\ge2$. The $\theta$-grid $G$ has vertices $(i,j)$ for $1\le i,j\le\theta$. Two vertices are adjacent exactly when their coordinate differences have absolute values summing to one. For each $i$, $P_i$ is the horizontal row with vertices $(i,1),\ldots,(i,\theta)$; for each $j$, $Q_j$ is the vertical column. Write $E(P_i)$ and $E(Q_j)$ for their edge sets. The Lean development uses the already published definition of this same simple graph, with coordinates shifted to start at zero. The shift changes no adjacency or row and column relation. Robertson and Seymour, 1991, p. 171.

For an edge set $X\subseteq E(G)$, the edge boundary $\partial(X)$ consists of vertices incident both with an edge in $X$ and with an edge outside $X$. The source prints “vertices $v\in X$” when introducing this set. Since $X$ is a set of edges, this is a type slip; the two incidence conditions give the intended reading. An edge set is small if $|\partial(X)|<\theta$ and it contains no complete row edge set $E(P_i)$. These are two separate requirements. An edge set can have a small boundary while still containing a whole row. Robertson and Seymour, 1991, pp. 171–172.

A subhypergraph $A$ specifies subsets $V(A)$ and $E(A)$ of the grid's vertices and edges, retaining the incidences of the ambient grid. A separation $(A,B)$ satisfies $A\cup B=G$ and $E(A\cap B)=\varnothing$; its order is $|V(A\cap B)|$. Although the grid is a simple graph, these are the paper's hypergraph definitions. A tangle $\mathcal T$ of order $\theta$ contains only separations of order below $\theta$ and satisfies three axioms: it chooses an orientation of every such separation; the union of the first sides of any three chosen separations is not $G$; and no chosen first side contains every vertex of $G$. The chosen three may coincide. Robertson and Seymour, 1991, pp. 153–154.

Formalization targets

The first milestone, (7.1), identifies a symmetry between rows and columns under a low boundary:

$$|\partial(X)|<\theta\quad\Longrightarrow\quad \bigl(\exists i,\ E(P_i)\subseteq X\bigr) \Longleftrightarrow \bigl(\exists j,\ E(Q_j)\subseteq X\bigr).$$

The second milestone, (7.2), says that three small edge sets cannot cover all the grid's edges:

$$X_1\cup X_2\cup X_3=E(G) \quad\Longrightarrow\quad \neg\bigl(X_1,X_2,X_3\text{ are all small}\bigr).$$

The goal, (7.3), defines $\mathcal T_\theta$ rather than taking it as an arbitrary set. It selects precisely the separations $(A,B)$ of order less than $\theta$ for which $E(A)$ is small, and asserts

$$\mathcal T_\theta\text{ is a tangle in }G\text{ of order }\theta.$$

These are the numbered §7 results on pp. 171–173, in the order used by the paper. Robertson and Seymour, 1991, pp. 171–173.

What the result supplies

The theorem gives an explicit tangle in a familiar graph for every order $\theta\ge2$. A tangle is more than a numerical connectivity bound: it records coherent choices across all separations below its order. In the paper, the grid tangle feeds the link between large grids and tangles of high order. The extension from a grid minor in another graph to a tangle of that graph invokes (6.1), beyond this mission's goal. The converse direction, that large tree-width forces a large grid minor, is (7.4), proved in Graph Minors V (Robertson and Seymour, 1986); the published definitions and statements of that paper on this platform are about grid minors and tree-width, not tangles. Robertson and Seymour, 1991, pp. 170, 173.

Formalizing (7.3) will make the grid tangle available as a checked object alongside the already published grid graph. It will also produce reusable definitions for an edge boundary, small edge sets and the paper's hypergraph separations. The Lean files here are draft statements with open proofs; the published 1986 grid definition is the existing checked ingredient. No machine-checked proof of (7.1), (7.2) or (7.3) is claimed by this proposal.

Where the difficulty lies

The obvious attempt at (7.2) counts boundary vertices column by column. If every column $Q_j$ has all its edges in $X_1\cup X_2$ and meets both sets, each column contributes at least two vertices to $|\partial(X_1)|+|\partial(X_2)|$, so the two boundaries together have at least $2\theta$ vertices. This only works when the third set misses the first and last rows; in general the third set can absorb edges of every column, and no single count over the whole grid bounds all three boundaries at once. The statement is a covering property of three sets, not a bound on any one of them, and the paper's argument for it is credited to D. Kleitman and M. Saks. The goal must then meet all three tangle axioms. The page's proof of (7.3) argues the first axiom and says only that the rest follows from (7.2); the third axiom, $V(A)\ne V(G)$, is part of the definition and must be established, not dropped. Robertson and Seymour, 1991, pp. 172–173.

Formalization scope

The source assumes finite hypergraphs throughout, and §7 fixes $\theta\ge2$. Lean uses a finite simple graph on Fin θ × Fin θ, reusing RobertsonSeymour1986.GM5.grid, and views its edge set as the edge type of a local hypergraph. Subhypergraphs hold vertex and edge subsets with inherited incidence. Set.ncard counts boundary vertices and separation order. Rows and columns use all grid edges whose two endpoints have the specified coordinate. This representation keeps every grid edge's identity, even though it is written as a SimpleGraph edge subtype.

IsSmall retains both $|\partial(X)|<\theta$ and the exclusion of full row edge sets. boundary requires an incident edge on each side of $X$. Both details are necessary for the claimed tangle: an IsSmall without the row clause would call every set with a small boundary small, including sets that contain whole rows, and the resulting set of separations is not a tangle; a boundary defined with "every edge outside $X$" instead of "some edge outside $X$" would be empty and make the size condition vacuous. The formalization keeps the third tangle axiom and does not replace it with an easier condition. The definitions of hypergraph, separation and tangle duplicate the shared encoding used by the other missions for this paper and can later be consolidated. The definitions also include the paper's tangle number and maximum edge size for that shared layer, though the grid goal does not invoke them; on finite inputs their maxima are bounded, and their empty-set value is zero.

The companion missions are Graph Minors. X. Obstructions to Tree-Decomposition I: Tangle Number Equals max(Branch-Width, Largest Edge Size), max(β(G), γ(G)) = θ(G); Graph Minors. X. Obstructions to Tree-Decomposition II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1); Graph Minors. X. Obstructions to Tree-Decomposition IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions; and Graph Minors. X. Obstructions to Tree-Decomposition V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}. Those missions address the paper's other main results; this one isolates the grid construction.

Selected references

• N. Robertson and P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, Journal of Combinatorial Theory, Series B 52 (1991), 153–190. DOI: 10.1016/0095-8956(91)90061-n.
• N. Robertson and P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, Journal of Combinatorial Theory, Series B 41 (1986), 92–114. DOI: 10.1016/0095-8956(86)90030-4.

Motivation

Tangles were introduced by Robertson and Seymour in Graph Minors. X (JCTB 1991) to make precise the idea of a "highly connected region" of a graph. A tangle orients every low-order separation of the graph towards one side, consistently. They are the organising notion of the later papers of the Graph Minors series, which culminate in the graph structure theorem and the proof of Wagner's conjecture.

Section 11 of Graph Minors X, Structure relative to a tangle, asks how local and global structure are related. In the paper's words: suppose that $G$ has large tangle number, but relative to each high-order tangle the graph has a structure of a certain kind $X$. What can be inferred about the global structure of $G$? One might guess that $G$ has a tree-decomposition into pieces each with structure $X$, but that is false. The theorem of §11 shows that $G$ does have a tree-decomposition into pieces which almost have structure $X$. The authors state that they need this for an application in a later paper of the series, cited as [6], Graph minors. XVII. Excluding a non-planar graph (submitted); it appeared as Graph Minors XVI (2003), where the local structure relative to a tangle is a near-embedding in a surface.

Setting

A hypergraph $G$ has a finite vertex set $V(G)$, a finite edge set $E(G)$ and an incidence relation. A subhypergraph $G' \subseteq G$ has $V(G') \subseteq V(G)$ and $E(G') \subseteq E(G)$, with every end of an edge of $G'$ in $V(G')$. A separation of $G$ is a pair $(A, B)$ of subhypergraphs with $A \cup B = G$ and $E(A \cap B) = \emptyset$, and its order is $|V(A \cap B)|$.

For $\theta \ge 1$, a tangle of order $\theta$ in $G$ is a set $\mathcal T$ of separations of order $< \theta$ such that (i) for each separation $(A, B)$ of order $< \theta$ one of $(A,B)$, $(B,A)$ is in $\mathcal T$; (ii) no three members $(A_i, B_i)$ of $\mathcal T$ have $A_1 \cup A_2 \cup A_3 = G$; (iii) $V(A) \ne V(G)$ for $(A, B) \in \mathcal T$.

A tree-decomposition $(T, \tau)$ of $G$ is a tree $T$ and subhypergraphs $\tau(t)$, $t \in V(T)$, whose union is $G$, which are pairwise edge-disjoint, and with $\tau(t) \cap \tau(t'') \subseteq \tau(t')$ whenever $t'$ lies on the path of $T$ between $t$ and $t''$.

A design is a pair $(H, M)$ of a hypergraph $H$ and a set $M$ of subsets of $V(H)$.

• The design of a node $t_0$ of $(T, \tau)$ with neighbours $t_1, \dots, t_k$ is $(\tau(t_0), \{V(\tau(t_0) \cap \tau(t_i))\})$. A tree-decomposition is over a class $\mathcal S$ of designs if the design of every node belongs to $\mathcal S$.
• $(H', M')$ is an $n$-enlargement of $(H, M)$ if, for some $Z \subseteq V(H')$ with $|Z| \le n$, $H \subseteq H'$, $V(H') - V(H) \subseteq Z$, $E(H') \subseteq E(H)$, and $X \cap V(H) \in M$ for every $X \in M'$ other than $Z$. $\mathcal S^n$ is the class of $n$-enlargements of members of $\mathcal S$, and $\mathcal R_n$ is the class of designs with at most $n$ vertices.
• A location in $G'$ is a set of separations $(A_i, B_i)$ of $G'$ with $A_i \subseteq B_j$ for $i \ne j$. Its design is $(G' \cap B_1 \cap \dots \cap B_k, \{V(A_i \cap B_i)\})$.
• A class $\mathcal S$ is $\theta$-pervasive in $G$ if for every subhypergraph $G' \subseteq G$ and every tangle $\mathcal T$ in $G'$ of order $\ge \theta$, some location $\mathcal L \subseteq \mathcal T$ in $G'$ has its design in $\mathcal S$.
• The $Z$-extension of $(H, M)$ is $(H, M \cup \{Z\})$.

Formalization targets

Goal: (11.1), p. 185

For $\theta \ge 1$ and a class $\mathcal S$ that is $\theta$-pervasive in $G$,

$$G \text{ has a tree-decomposition over } \mathcal S^{3\theta-2} \cup \mathcal R_{4\theta-3}.$$

Milestone: (11.2), pp. 185–186

If $\mathcal S$ is $\theta$-pervasive in $G$ and $|Z| = 3\theta - 2$, then either some separation $(A, B)$ of order $< \theta$ has

$$|(Z \cup V(A)) \cap V(B)|,\ |(Z \cup V(B)) \cap V(A)| \le 3\theta - 3,$$

or some location $\{(A_i, B_i)\}$ in $G$ with design in $\mathcal S$ has $|Z \cap V(A_i)| \le |V(A_i \cap B_i)| < \theta$ for all $i$.

Milestone: (11.3), p. 186

If $|Z| \le 3\theta - 2$, there is a tree-decomposition of $G$ over $\mathcal S' = \mathcal S^{3\theta-2} \cup \mathcal R_{4\theta-3}$ with a node $t_0$ such that $Z \subseteq V(\tau(t_0))$ and the $Z$-extension of the design of $t_0$ is in $\mathcal S'$. The goal is the case $Z = \emptyset$.

Companion: the remark on p. 188

For every $\theta \ge 1$, if $G$ has no tangle of order $\theta$, then

$$\omega(G) \le 4\theta - 4.$$

Consequently $\omega(G) \le 4\theta(G)$, where $\theta(G)$ is the tangle number. This is the p. 188 remark following (11.3).

Significance

(11.1) converts local information, stated tangle by tangle, into a global decomposition. Every piece of the decomposition is either small (at most $4\theta - 3$ vertices) or differs from a structure in $\mathcal S$ by at most $3\theta - 2$ added vertices. This is the kind of local-to-global step the later Graph Minors papers need: there the local structure near each high-order tangle is a near-embedding in a surface, and a result of this shape glues such local structures along a tree. With $\mathcal S = \emptyset$ it gives a tree-width bound $\omega(G) \le 4\theta(G)$, a weaker form of the tangle/tree-width duality.

The result has been proved since 1991. To our knowledge no proof assistant formalizes it, and none formalizes the hypergraph tangles or tree-decompositions of this paper. This mission produces machine-checked statements of the paper's notions of design, enlargement, location and pervasiveness, the structure theorem, and its inductive strengthening.

Difficulty

The first idea is to take the pieces in $\mathcal S$ themselves as the pieces of the tree-decomposition. That fails, and the paper says so: the pieces can only almost have the structure. Locations for different tangles interact, and the decomposition must absorb up to $3\theta - 2$ extra vertices into each piece. The induction also has to control a set $Z$ of attachment vertices of bounded size: a piece built at one node must still accept the vertices through which it is glued to the rest of the tree. Keeping $|Z| \le 3\theta - 2$ throughout the recursion is the delicate point, and it is why the strengthened statement (11.3), not (11.1), is the one that admits induction.

Formalization scope

• Hypergraphs. A hypergraph is a structure Hypergraph V E with an incidence relation. Finiteness is [Finite V] [Finite E] on every theorem. Subhypergraphs, separations, tangles and tree-decompositions are the series' shared encodings (namespace RobertsonSeymour1991.GM10.Structure). The tree of a tree-decomposition is a SimpleGraph on Fin n satisfying IsTree.
• Designs. Every design the statements involve has as hypergraph a subhypergraph of the fixed $G$. So a design is a $G$-design G.Sub × Set (Set V), and a class of designs is a set of $G$-designs. Classes need not be closed under isomorphism; the paper never uses that.
• Relative tangles. Separations, tangles and locations in a subhypergraph $G'$ are pairs of subhypergraphs of $G$ whose union is $G'$. For $G' = G$ they agree definitionally with the absolute notions.
• Pervasiveness. It quantifies over every subhypergraph $G'$ and every order $\theta' \ge \theta$. Restricting to $G' = G$ would be a different, stronger theorem. The paper's opening remark in the proof of (11.3), that pervasiveness passes to subhypergraphs, is immediate in this encoding and is not a separate item.
• Edge cases. The empty set is a location; its design is $(G', \emptyset)$.
• Integer arithmetic. Since $\theta \ge 1$, the bounds $3\theta-2$, $3\theta-3$ and $4\theta-3$ are exact natural numbers. Tree-width is an integer, and it is $-1$ for an empty vertex set.
• No trivial instances. IsPervasive is satisfiable: the class of all designs is $\theta$-pervasive, through the empty location. The conclusion is satisfiable too: the one-node decomposition lies over $\mathcal R_{|V(G)|}$. So neither the hypothesis nor the conclusion of (11.1) is vacuous.

The other main results of the paper are separate missions of this series:

• Graph Minors. X. Obstructions to Tree-Decomposition I (tangle number versus branch-width);
• II (branch-width versus tree-width);
• III (the grid tangle);
• IV (the tree-decomposition separating mutually distinguishable tangles).

Contributions are welcome on any item: proofs of (11.2) and (11.3), and of the p. 188 companion. The companion needs two auxiliary facts: a tangle of order $\ge \theta$ in a subhypergraph yields one of order $\theta$ in $G$, and tree-width is bounded by bag size.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-n
• N. Robertson, P. D. Seymour, Graph Minors. XVI. Excluding a non-planar graph, J. Combin. Theory Ser. B 89 (2003) 43–76. https://doi.org/10.1016/S0095-8956(03)00042-X
• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a planar graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4

Motivation

Tree-width measures how closely a graph resembles a tree. It is the central width parameter of the Graph Minors series of N. Robertson and P. D. Seymour, which proves that finite graphs are well-quasi-ordered by the minor relation, and it governs the complexity of many algorithms: problems that are NP-hard in general become solvable in linear time on graphs of bounded tree-width (Courcelle's theorem). Branch-width, introduced in Graph Minors X (Robertson, Seymour 1991), is a second width parameter, defined from ternary trees whose leaves carry the edges of the graph. It is the natural parameter for the paper's main minimax theorem, which equates branch-width with the maximum order of a tangle, the obstruction to small decompositions.

Section 5 of Graph Minors X shows that the two parameters are equivalent, within a factor 3/2. This is what transfers the tangle duality from branch-width to tree-width, and it is why later work (for instance on matroid branch-width and on rank-width) treats branch-width as an interchangeable substitute for tree-width.

Setting

All objects are finite. A hypergraph $G$ has a vertex set $V(G)$, an edge set $E(G)$, and an incidence relation; the ends of an edge are the vertices incident with it, and an edge may have any number of ends. $\gamma(G)$ is the maximum number of ends of an edge, or $0$ if $E(G)=\emptyset$. A subhypergraph consists of subsets of $V(G)$ and $E(G)$ such that every end of a chosen edge is a chosen vertex; unions, intersections and inclusion of subhypergraphs are taken setwise.

A tree is a connected non-null graph without circuits; its leaves are its vertices of valency at most $1$, and it is ternary if every valency is $1$ or $3$.

A branch-decomposition of $G$ is a pair $(T,\tau)$ with $T$ a ternary tree and $\tau$ a bijection from the leaves of $T$ onto $E(G)$. The order of an edge $f$ of $T$ is the number of vertices $v$ of $G$ such that $v$ is an end both of an edge labelling a leaf in one component of $T\setminus f$ and of an edge labelling a leaf in the other. The width of $(T,\tau)$ is the maximum order of an edge of $T$, and the branch-width $\beta(G)$ is the minimum width, or $0$ if $|E(G)|\le 1$.

A tree-decomposition of $G$ is a pair $(T,\tau)$ with $T$ a tree and $\tau(t)$ a subhypergraph of $G$ for every $t\in V(T)$, such that

1. the union of all $\tau(t)$ is $G$;
2. for distinct $t,t'$, the parts $\tau(t)$ and $\tau(t')$ share no edge;
3. if $t'$ lies on the path of $T$ between $t$ and $t''$, then $\tau(t)\cap\tau(t'')\subseteq\tau(t')$.

Its width is $\max_t\,(|V(\tau(t))|-1)$, and the tree-width $\omega(G)$ is the minimum width; $\omega(G)=-1$ exactly when $V(G)=\emptyset$. Each part is a subhypergraph and each edge lies in exactly one part, which differs from the familiar vertex-bag tree-decompositions of graphs, but gives the same tree-width on graphs.

The tangle number $\theta(G)$ is the maximum order of a tangle in $G$ (p. 154), or $0$ if there are none.

Formalization targets

Goal: (5.1)

$$\max\bigl(\beta(G),\gamma(G)\bigr)\;\le\;\omega(G)+1\;\le\;\max\bigl(\lfloor\tfrac32\beta(G)\rfloor,\ \gamma(G),\ 1\bigr)\qquad\text{for every finite hypergraph } G.$$

Milestones

• Second inequality of (5.1): $\omega(G)+1\le\max(\lfloor\tfrac32\beta(G)\rfloor,\gamma(G),1)$.
• Claims (1), (2), (3) of the proof of (5.1), under the proof's standing assumptions $\gamma(G)>0$, $|E(G)|\ge 2$ and no isolated vertices: there is a tree-decomposition of width $\omega(G)$ in which (1) every edge $e$ is the only edge of a leaf part whose vertices are exactly the ends of $e$, and parts at vertices of valency $\ge2$ have no edges; (2) moreover every leaf part has exactly one edge; (3) moreover every vertex of $T$ has valency at most $3$. The claims are cumulative.
• First inequality of (5.1): $\max(\beta(G),\gamma(G))\le\omega(G)+1$.

Companion: (5.2)

$$\theta(G)\;\le\;\omega(G)+1\;\le\;\tfrac32\,\theta(G).$$

Significance

The result. (5.1) shows that branch-width and tree-width bound each other up to the factor $3/2$ and the edge-size correction, and the page records that both bounds are attained ($K_n$ with $3\mid n$ for the right-hand side, $K_{n,n}$ minus a perfect matching for the left-hand side). Together with the minimax theorem (4.3) of the same paper, $\max(\beta(G),\gamma(G))=\theta(G)$ unless $\gamma(G)=0$ and $V(G)\ne\emptyset$, it yields (5.2): tangles are, up to the factor $3/2$, the exact obstruction to tree-decompositions of small width. That duality is the form in which tree-width enters the later papers of the Graph Minors series.

Formalizing it. The result is proved (1991); no machine-checked proof of it is known to exist. The platform holds tree-width statements for simple graphs with vertex bags (Graph Minors V, RobertsonSeymour1986.GM5.treewidth_le_theta9 and excluding_planar_graph), which are a different theorem about a different object. This mission formalizes the hypergraph tree-decomposition and branch-decomposition of Graph Minors X and the comparison between them. The companion missions of this series are Graph Minors. X. Obstructions to Tree-Decomposition I (the minimax theorem (4.3)), III (the grid tangle (7.3)), IV (the tree-decomposition separating distinguishable tangles (10.3)) and V (the structure theorem (11.1)).

Difficulty

The second inequality converts a branch-decomposition into a tree-decomposition; the difficulty is to obtain the bound with the floor $\lfloor\tfrac32\beta\rfloor$ and the separate $\gamma(G)$ term exactly, not up to an additive error.

The first inequality is where the obvious approach stalls: a tree-decomposition of minimum width is not a branch-decomposition. Its tree may have vertices of any valency, its leaves may carry no edge or several, and an edge may sit at an internal vertex. The three claims of the proof normalize an optimal tree-decomposition step by step without increasing its width. Each step modifies a tree on a finite vertex type while preserving three structural conditions (covering, edge-disjointness, the path condition), and the final step, suppressing vertices of valency $2$, must be shown to produce a ternary tree with the edge orders bounded by part sizes. Most of the formal work is this tree surgery.

Formalization scope

• Every theorem quantifies over types V, E with [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154) and a hypergraph G : Hypergraph V E given by its incidence relation.
• Trees are SimpleGraph (Fin n) with IsTree (connected, hence non-null, and acyclic). A leaf is a vertex of valency at most $1$; valency is (T.neighborSet t).ncard.
• A branch-decomposition stores $\tau$ as its inverse, an injective map from edges onto the leaves. $\beta(G)$ is set to $0$ when $|E(G)|\le1$ and is otherwise the sInf of the widths, which is a genuine minimum because a branch-decomposition exists when $|E(G)|\ge2$.
• Widths of tree-decompositions are integers, so that $\omega(G)=-1$ when $V(G)=\emptyset$. $\omega(G)$ is the sInf in $\mathbb Z$ of all $w$ bounding every $|V(\tau(t))|-1$; the set is nonempty (one-vertex tree with $\tau=G$) and bounded below by $-1$, so the sInf is the minimum width and not a junk value.
• $\lfloor\tfrac32\beta(G)\rfloor$ is the natural-number division 3 * β / 2; the ceiling would be a weaker statement. In (5.2), $\omega(G)+1\le\tfrac32\theta(G)$ is stated as $2(\omega(G)+1)\le3\theta(G)$, which is equivalent.
• The claims read "we may assume X" as "some tree-decomposition of width $\omega(G)$ satisfies X", under the proof's standing assumptions $\gamma(G)>0$, $|E(G)|\ge2$ and no isolated vertices (p. 168).
• Condition (ii) of a tree-decomposition, edge-disjointness of the parts, is kept as on the page. Replacing it by "every edge lies in some part", or allowing an empty tree, would change the tree-width and trivialize the comparison; both are ruled out.

Infrastructure needed and reusable beyond this mission: tree surgery on SimpleGraph (Fin n) (attaching a leaf, deleting a leaf, splitting a vertex, suppressing valency-2 vertices), the existence of branch-decompositions for $|E|\ge2$, and the computation of sInf-defined widths. Contributions of such lemmas, of proofs of the individual claims, and of small examples ($K_n$, grids) are welcome.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-n
• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• B. Courcelle, The monadic second-order logic of graphs. I. Recognizable sets of finite graphs, Information and Computation 85 (1990) 12–75. https://doi.org/10.1016/0890-5401(90)90043-H

Motivation

Many approximation results in probability and operations research take the form of a sequence of discrete or jump-driven systems converging to a diffusion or another limit process. When the approximating systems are written as stochastic integral equations, $X_n(t) = X_n(0) + \int_0^t \sigma(X_n(s-))\,dY_n(s)$, the key step is to show that the stochastic integrals converge whenever the integrands and the integrators converge. That this is not automatic was known from the work of Wong and Zakai (1965): smooth approximations of Brownian motion produce a Stratonovich, not an Itô, limit. Kurtz and Protter (1991) give a condition on the integrators under which convergence in distribution of the pair (integrand, integrator) in the Skorohod topology implies convergence in distribution of the triple (integrand, integrator, integral). The result is essentially the theorem of Jakubowski, Mémin and Pagès (1989), with a formulation and proof that avoid the general theory of semimartingale characteristics. It underlies diffusion approximations for queueing and storage networks, approximation schemes for stochastic differential equations, and limit theorems for statistics and filters that are written as stochastic integrals.

Setting

Time is $[0,\infty)$. A path $x:[0,\infty)\to E$ in a metric space $E$ is cadlag if it is right-continuous and has a left limit $x(t-)$ at every $t>0$; $D_E[0,\infty)$ is the set of cadlag paths, and $x(0-)=x(0)$. Let $\Lambda$ be the set of continuous, strictly increasing maps of $[0,\infty)$ onto itself. Cadlag paths $x_n$ converge to $x$ in the Skorohod (J1) topology if there are $\lambda_n\in\Lambda$ with $x_n\circ\lambda_n(t)\to x(t)$ and $\lambda_n(t)\to t$ uniformly on bounded intervals. For a product space $E_1\times E_2$ the pair $(x_n,y_n)$ converges if one sequence $\lambda_n$ serves both components; this is strictly stronger than convergence of each component.

Let $\mathbb M^{km}$ be the real $k\times m$ matrices. For a $\mathbb M^{km}$-valued process $X$ and an $\mathbb R^m$-valued process $Y$, the stochastic integral (1.7) is

$$\int_0^t X(s-)\,dY(s)=\lim\sum_i X(t_i)\big(Y(t_{i+1})-Y(t_i)\big),$$

the limit in probability along partitions $\{t_i\}$ of $[0,t]$ whose mesh tends to zero. Throughout, $\int X\,dY$ means $\int X(s-)\,dY(s)$. An $\{\mathcal F_t\}$-adapted cadlag process $Y$ is a semimartingale if $Y=M+A$ with $M$ an $\{\mathcal F_t\}$-local martingale and $A$ of finite variation on bounded intervals, with total variation $T_t(A)$ on $[0,t]$. $[M]$ denotes the quadratic variation.

For $\delta\in(0,\infty]$ let $h_\delta(r)=(1-\delta/r)^+$ and

$$J_\delta(x)(t)=\sum_{s\le t}h_\delta\big(|x(s)-x(s-)|\big)\big(x(s)-x(s-)\big),$$

which collects the part of the jumps larger than $\delta$; $Y^\delta=Y-J_\delta(Y)$ then has jumps of size at most $\delta$. Condition C2.2(i) on a sequence $Y_n$ asks for decompositions $Y_n^\delta=M_n^\delta+A_n^\delta$ such that for each $\alpha>0$ there are stopping times $\tau_n^\alpha$ with $P\{\tau_n^\alpha\le\alpha\}\le1/\alpha$ and $\sup_nE\big[[M_n^\delta]_{t\wedge\tau_n^\alpha}+T_{t\wedge\tau_n^\alpha}(A_n^\delta)\big]<\infty$. $\Rightarrow$ denotes convergence in distribution.

Formalization targets

Goal: Theorem 2.2 (distributional part)

For each $n$, let $(X_n,Y_n)$ be $\{\mathcal F^n_t\}$-adapted with paths in $D_{\mathbb M^{km}\times\mathbb R^m}[0,\infty)$, $Y_n$ an $\{\mathcal F^n_t\}$-semimartingale satisfying C2.2(i) for some $\delta\in(0,\infty]$. If $(X_n,Y_n)\Rightarrow(X,Y)$ in the Skorohod topology on $D_{\mathbb M^{km}\times\mathbb R^m}[0,\infty)$, then $Y$ is a semimartingale with respect to a filtration to which $X$ and $Y$ are adapted, and

$$\Big(X_n,\,Y_n,\,\int X_n\,dY_n\Big)\Rightarrow\Big(X,\,Y,\,\int X\,dY\Big)\quad\text{in }D_{\mathbb M^{km}\times\mathbb R^m\times\mathbb R^k}[0,\infty).$$

Milestones, in the order the proof uses them

• Lemma 2.1: time-change-equivariant maps that are continuous for local uniform convergence are Skorohod-continuous, jointly with their argument.
• Continuity of $J_\delta$ (after (2.1)): $(x_n,J_\delta(x_n))\to(x,J_\delta(x))$ and $(x_n,x_n-J_\delta(x_n))\to(x,x-J_\delta(x))$.
• Lemma 6.2: a sequential characterization of Skorohod convergence.
• The step approximation $I_\varepsilon$ of §6, with $r(z(t),I_\varepsilon(z)(t))\le\varepsilon$.
• Lemma 6.1: $z_n\to z$ implies $(z_n,I_\varepsilon(z_n))\to(z,I_\varepsilon(z))$ almost surely in the random thresholds.
• (1.12)–(1.13): integrals against step functions with uniformly bounded jump counts converge, jointly with integrand and integrator.
• (2.2): $\int x_n(s-)\,dJ_\delta(y_n)(s)\to\int x(s-)\,dJ_\delta(y)(s)$.
• (2.7): $E\big[\sup_{s\le t\wedge\tau}|R(s)|\big]\le\varepsilon\big(2E[[M]_{t\wedge\tau}]^{1/2}+E[T_{t\wedge\tau}(A)]\big)$ for $R=\int H\,d(M+A)$ with $|H|\le\varepsilon$.
• Remark 2.4: the limit $Y$ is a semimartingale.

Significance

The result. Theorem 2.2 reduces convergence of stochastic integrals to two checks: joint convergence of integrand and integrator, and the uniform control C2.2(i) on the integrators. Remarks 2.3 and 2.5 give simple sufficient conditions (stochastic boundedness of $T_t(A_n^\delta)$ plus a second-moment bound; relative compactness for a fixed integrator), and Section 5 of the paper derives from it weak limit theorems for stochastic differential equations driven by semimartingales, including Wong–Zakai-type corrections. Without the theorem, each diffusion approximation that passes through an integral equation needs its own ad hoc argument.

Formalizing it. The theorem is proved and classical; nothing here is open. Lean's Mathlib has no Skorohod space, no stochastic integral against a semimartingale and no semimartingale, so the mission produces the first machine-checked definitions of J1 convergence on $D_E[0,\infty)$, of the left-point stochastic integral (1.7), and of convergence in distribution of cadlag processes, together with the deterministic facts about them that a proof of Theorem 2.2 needs. The definitions are meant to be reused by later missions on weak convergence of processes and on stochastic differential equations (the paper's Theorem 5.4 is planned as a follow-up that references them).

Difficulty

The obvious argument — the integral is a continuous function of the pair (integrand, integrator), so the continuous mapping theorem applies — fails in two ways. First, the map $(x,y)\mapsto\int x(s-)\,dy(s)$ is not continuous in the Skorohod topology, and for a general semimartingale integrator it is not even defined path by path. Example 1.1 makes the failure concrete: with $X=Y=X_n=\chi_{[1,\infty)}$ and $Y_n=\chi_{[1+1/n,\infty)}$, each component converges, yet $\int_0^tX_n\,dY_n=1$ for $t>1+1/n$ while $\int_0^tX\,dY=0$, because the jumps of integrand and integrator coalesce in the wrong order; joint convergence of the pair excludes this. Second, Example 1.2 shows that joint convergence is still not enough: integrators whose variation grows without bound (piecewise linear interpolations of Brownian motion) produce an extra drift $\tfrac12t$ in the limit. C2.2(i) is the condition that excludes this, and the identification of the limit integral also requires knowing that the limit $Y$ is a semimartingale, which is not given.

Formalization scope

Time is ℝ≥0; a process is a map ℝ≥0 → Ω → E. $\mathbb R^m$ is Fin m → ℝ and $\mathbb M^{km}$ is Fin k → Fin m → ℝ, with the sup metric; products carry the max metric (J1 convergence does not depend on the product metric). The conventions the formal statements commit to:

• "$x_n\to x$ in the Skorohod topology" is the sequential definition of pp. 1037–1038 with one time change sequence; "uniformly for $t$ in bounded intervals" is uniformly on $[0,T]$ for every $T$. For a pair or a triple the time change is shared by all components.
• "$\Rightarrow$" is convergence in distribution in coupling form: a probability space carrying copies of the processes and of the limit, with almost sure Skorohod convergence. Laws are taken on the product σ-algebra of path space; for the finite-dimensional state spaces here this is equivalent to weak convergence of the laws on $D_E[0,\infty)$.
• The coupling relation is defined for Polish state spaces with their Borel σ-algebras. Every state space in the probabilistic milestones is a finite-dimensional real product and satisfies this requirement.
• $\int X\,dY$ is the in-probability limit of left-point Riemann sums (1.7) over all partition sequences with mesh tending to zero, with cadlag paths. The prelimit integrals are given processes with this property; the limit integral is produced in the conclusion.
• The semimartingale conclusion of Theorem 2.2 is stated for a copy of $(X,Y)$ on a space that may carry extra randomness, with a filtration making both adapted.
• In C2.2(i) the free $t$ is universally quantified ("for every $t\ge0$") and the stopping times are chosen before $t$; expectations of nonnegative quantities are taken in $[0,\infty]$; $t\wedge\tau=t$ when $\tau=\infty$.
• $[M]=\sum_j[M_j]$ with $[M](0)=0$; since C2.2(i) asks for some decomposition, this agrees with Protter's convention $[M](0)=M(0)^2$.
• In (2.1), $|x|=\sum_i|x_i|$ (the paper's convention for vectors, p. 1049); in (2.7), Euclidean norms for $R$ and $T(A)$ and the Frobenius norm for the integrand.
• "a.s." in Lemma 6.1 refers to the law of the thresholds $\theta_k$, i.i.d. uniform on $[\frac12,1]$, and the null set may depend on the convergent sequence.
• $\delta$ ranges over $(0,\infty]$, with $J_\infty=0$.

The theorem has trivializing formalizations, all excluded here: componentwise convergence of $(X_n,Y_n)$ in place of joint convergence; an integral not pinned to (1.7) (any process would do); and assuming the limit integral, or the semimartingale property of $Y$, as a hypothesis.

Local martingales and cross variations reuse the published Ethier–Kurtz definitions EthierKurtz_IsSourceLocalMartingale and EthierKurtz_HasCrossVariation. A complete development needs the Skorohod space and its tightness theory, the stochastic integral against semimartingales (existence and the Burkholder–Davis–Gundy/Doob estimates), and the quasimartingale criterion of Meyer and Zheng. Contributions to any of these layers are welcome; the deterministic milestones (Lemma 2.1, Lemma 6.2, the continuity of $J_\delta$, (1.12)–(1.13), Lemma 6.1) are independent of the probabilistic ones and reusable for any work on the J1 topology.

Selected references

• T. G. Kurtz and P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19 (1991), 1035–1070. https://doi.org/10.1214/aop/1176990334
• A. Jakubowski, J. Mémin and G. Pagès, Convergence en loi des suites d'intégrales stochastiques sur l'espace D¹ de Skorokhod, Probab. Theory Related Fields 81 (1989), 111–137. https://doi.org/10.1007/BF00343739
• S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. https://doi.org/10.1007/978-3-662-02619-9
• E. Wong and M. Zakai, On the convergence of ordinary integrals to stochastic integrals, Ann. Math. Statist. 36 (1965), 1560–1564. https://doi.org/10.1214/aoms/1177699916
• P. A. Meyer and W. A. Zheng, Tightness criteria for laws of semimartingales, Ann. Inst. H. Poincaré Probab. Statist. 20 (1984), 353–372. http://www.numdam.org/item/AIHPB_1984__20_4_353_0/

Motivation

An investor in a continuous-time market chooses, at every instant, how to split wealth between a bond and $d$ stocks and how fast to consume, so as to maximize expected utility of consumption and terminal wealth. Without constraints on the portfolio, this problem was solved by the martingale method: Pliska (1986), Karatzas, Lehoczky and Shreve (1987) and Cox and Huang (1989) showed that in a complete market the optimal terminal wealth and consumption are explicit functions of a single state-price density, and the portfolio that finances them comes from the martingale representation theorem.

Real investors face constraints: no short selling, no borrowing, a cap on the fraction of wealth in a sector, an incomplete market in which some stocks cannot be traded at all. Each makes the market effectively incomplete, and the single state-price density no longer exists. Karatzas, Lehoczky, Shreve and Xu (1991) treated incompleteness, Xu (1990, thesis) short-selling prohibition, and He and Pearson (1991) short-sale constraints in a general setting. Cvitanić and Karatzas (1992) unified these cases: the portfolio must take values in an arbitrary nonempty closed convex set $K\subset\mathbb R^d$, and the problem is embedded in a family of auxiliary unconstrained markets indexed by a dual process $\nu$. This mission formalizes the paper's central characterization, Theorem 10.1, and the results its proof rests on.

Setting

A standard Brownian motion $W$ in $\mathbb R^d$ lives on a complete probability space with its augmented filtration $\{\mathcal F_t\}$, on a finite horizon $[0,T]$. The market $\mathcal M$ has progressively measurable interest rate $r$, appreciation rates $b$ and volatility matrix $\sigma$, with $r\ge-\eta$, $\xi^*\sigma\sigma^*\xi\ge\varepsilon\|\xi\|^2$, $E\int_0^Tr\,dt<\infty$, and a relative risk $\theta=\sigma^{-1}(b-r\mathbf 1)$ with $E\int_0^T\|\theta\|^2dt<\infty$. The state-price density is $H_0=\gamma_0Z_0$, with $\gamma_0(t)=e^{-\int_0^tr}$ and $Z_0(t)=\exp(-\int_0^t\theta^*dW-\frac12\int_0^t\|\theta\|^2)$.

A portfolio $\pi$ gives the proportions of wealth in the stocks, a consumption rate is $c\ge0$, and the wealth solves

$$dX=(rX-c)\,dt+X\pi^*\sigma\,(dW+\theta\,dt),\qquad X(0)=x>0.$$

The pair is admissible, $(\pi,c)\in\mathcal A_0(x)$, if $X\ge0$. With utility functions $U_1(t,\cdot)$, $U_2$ (strictly increasing, strictly concave, $C^1$, $U'(0+)=\infty$, $U'(\infty)=0$), inverse marginals $I_1,I_2$ and conjugates $\tilde U_1,\tilde U_2$, the investor maximizes

$$J(x;\pi,c)=E\int_0^TU_1(t,c(t))\,dt+EU_2(X(T))$$

over $\mathcal A'(x)$, the admissible pairs with integrable utility losses and $\pi\in K$ almost everywhere. The value is $V(x)$.

The support function $\delta(\nu)=\sup_{\pi\in K}(-\pi^*\nu)\in\mathbb R\cup\{+\infty\}$ drives the duality. For $\nu$ in the class $\mathcal D$ of square-integrable processes with $E\int_0^T\delta(\nu)\,dt<\infty$, the auxiliary market $\mathcal M_\nu$ has interest rate $r+\delta(\nu)$ and appreciation rates $b+\nu+\delta(\nu)\mathbf 1$, state-price density $H_\nu$ and unconstrained value $V_\nu(x)$. For $\lambda$ in the subclass $\mathcal D'$ (where $\mathcal X_\lambda(y)=E[\int_0^TH_\lambda I_1(t,yH_\lambda)\,dt+H_\lambda(T)I_2(yH_\lambda(T))]$ is finite for all $y>0$), let $y=\mathcal Y_\lambda(x)$ solve $\mathcal X_\lambda(y)=x$. The $\mathcal M_\lambda$-optimal consumption, terminal wealth and wealth are $c_\lambda=I_1(t,yH_\lambda)$, $\xi_\lambda=I_2(yH_\lambda(T))$ and $X_\lambda$.

Formalization targets

Goal: Theorem 10.1

Five conditions are considered for a capital $x>0$: (A) optimality of a pair $(\hat\pi,\hat c)\in\mathcal A'(x)$, together with $E[\int_0^T\hat cU_1'(t,\hat c)\,dt+\hat X(T)U_2'(\hat X(T))]<\infty$; and, for $\lambda\in\mathcal D'$, (B) financibility: some $\hat\pi_\lambda\in K$ with $\delta(\lambda)+\hat\pi_\lambda^*\lambda=0$ finances $(c_\lambda,\xi_\lambda)$ in $\mathcal M$; (C) minimality: $V_\lambda(x)\le V_\nu(x)$ for all $\nu\in\mathcal D$, with $V_\lambda(x)$ attained by $(c_\lambda,\xi_\lambda)$; (D) dual optimality: $\lambda$ minimizes $\nu\mapsto E[\int_0^T\tilde U_1(t,yH_\nu)\,dt+\tilde U_2(yH_\nu(T))]$ over $\mathcal D$; (E) parsimony: $E[\int_0^TH_\nu c_\lambda\,dt+H_\nu(T)\xi_\lambda]\le x$ for all $\nu\in\mathcal D$. The theorem asserts

$$(\mathrm B)\iff(\mathrm C)\iff(\mathrm D)\iff(\mathrm E)\implies(\mathrm A)\text{ for }(\hat\pi_\lambda,c_\lambda),$$

and, under the conditions (5.8) ($c\mapsto cU'(c)$ nondecreasing), (8.25) (a uniform growth bound $\alpha U'(x)\ge U'(\gamma x)$) and (12.2) (finiteness of the dual functional for some $\nu$), that (A) implies (B)–(E) for some $\lambda\in\mathcal D'$ with $\hat\pi_\lambda=\hat\pi$.

Milestones

In proof order: the conjugate inequalities (5.5)–(5.6); the budget constraint (3.6); the unconstrained solution (Lemma 7.2, Proposition 7.3, Theorem 7.4); the embedding (8.14), $V(x)\le V_\nu(x)$; Proposition 8.3, (B) $\Rightarrow$ optimality; the constrained budget constraint (9.4) and the hedging Theorem 9.1, (E) $\Rightarrow$ (B); and Appendix A's Lemma A.1, Lemma A.2 and Proposition A.4, the steps of (A) $\Rightarrow$ (B).

Significance

Theorem 10.1 turns a constrained stochastic control problem into a family of unconstrained ones plus a minimization over the dual process $\lambda$. Condition (D) is a convex minimization over $\nu$ that does not involve portfolios. It leads to the dual problem of Section 12, whose solvability gives existence of optimal constrained policies (Theorem 13.1, the companion mission). Section 9's hedging theorem is the superreplication principle under convex constraints, the basis of later work on constrained hedging and pricing. With logarithmic utility the theorem gives explicit optimal policies, and for deterministic coefficients the dual problem reduces to a deterministic one.

These results are proved in the paper, which is the standard reference for the convex-duality approach. To our knowledge they have no machine-checked proof. The mission's statements also produce a reusable Lean model of a continuous-time Itô market with stochastic coefficients, admissible portfolios, consumption, utility functions and their conjugates.

Difficulty

The obvious argument, Lagrange duality for $\max J$ subject to $\pi\in K$, fails at the first step: the constraint is on the control process, not on terminal wealth, so there is no static budget constraint to dualize. The paper's dual variable is a process, and for each candidate it changes both the interest rate and the drift. The direction (B) $\Rightarrow$ (A) is relatively direct. The direction (E) $\Rightarrow$ (B) is a hedging theorem under convex constraints (Theorem 9.1), where financing a claim requires the portfolio to land in $K$ and to satisfy the complementary-slackness identity $\delta(\lambda)+\pi^*\lambda=0$, which no unconstrained construction delivers. The converse (A) $\Rightarrow$ (B) must produce the dual process $\lambda$ from an optimal pair that is only assumed to exist, and the paper needs the extra growth conditions (5.8), (8.25), (12.2) for it. In Lean, stochastic integrals for integrands that are square integrable only almost surely, the martingale representation theorem for the Brownian filtration, and the product rule for Itô processes are not available in Mathlib.

Formalization scope

Processes are functions $\mathbb R_{\ge0}\times\Omega\to E$ constrained on $[0,T]$; vectors are EuclideanSpace ℝ (Fin d), matrices Matrix (Fin d) (Fin d) ℝ. The Brownian motion is the published EthierKurtz.IsStandardBrownian. The stochastic integral is a binder I, constrained only by the standing hypothesis that it is an Itô integral for every locally square-integrable integrand. This almost-sure variant of EthierKurtz.HasBrownianItoIntegral uses the published dyadic step helpers itoStepValue and itoStepSum. The hypothesis is satisfiable, by the classical construction.

The following readings are explicit in the Lean.

• Triples. Classes are sets of triples $(\pi,c,X)$ with $X$ a wealth process: an adapted, a.s. continuous solution of the integral form of (3.1) or (8.10) whose integrals exist.
• Extended reals. Utility expectations are extended reals, computed as positive minus negative parts. A utility at $0$ is $U(0+)$. Suprema are taken in the extended reals.
• The support function. $\delta$ takes values in the extended reals. In drifts and discounts it enters as a real number, which is finite almost everywhere for $\nu\in\mathcal D$. The page's "$E\int\delta(\nu)\le\infty$" in (8.1) is read as "$<\infty$".
• Inverse marginals and conjugates. $I(y)=\inf\{x>0: U'(x)\le y\}$ and $\tilde U(y)=\sup_{x>0}(U(x)-xy)$.
• The inverse $\mathcal Y_\lambda$. $\mathcal Y_\lambda(x)$ and $\mathcal Y_0(x)$ are represented by a number $y>0$ with $\mathcal X(y)=x$.
• The wealth $X_\lambda$. It is a conditional expectation for each $t$. "$X=X_\lambda$" means $X(t)=X_\lambda(t)$ a.s. for every $t\le T$.
• Almost everywhere. "$\ell\otimes P$-a.e." is almost everywhere for the product of Lebesgue measure on $[0,T]$ and $P$. "a.s." is almost everywhere for $P$.
• Theorem 9.1. Its conclusion "$(\pi,c)\in\mathcal A'(x)$" is formalized as $\mathcal A_0(x)$ plus $\pi\in K$ a.e., since the theorem involves no utility.
• (4.4). By Remark 4.2 it is not used in Theorem 10.1. It is kept, because the paper assumes it throughout.

A formalization in which the stochastic integral is an unconstrained function, a wealth process need not solve its equation, or $\delta$ is real-valued (so that $\sup$ over an unbounded set returns $0$) would make the statements vacuous or false; each is ruled out above. The proof will need almost-surely-square-integrable Itô integrals, Itô's product rule, nonnegative local martingales as supermartingales, and martingale representation in the Brownian filtration. All of these are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Cvitanić and I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4) (1992) 767–818. https://doi.org/10.1214/aoap/1177005576
• I. Karatzas, J. P. Lehoczky and S. E. Shreve, Optimal portfolio and consumption decisions for a "small investor" on a finite horizon, SIAM J. Control Optim. 25 (1987) 1557–1586. https://doi.org/10.1137/0325086
• J. C. Cox and C. F. Huang, Optimal consumption and portfolio policies when asset prices follow a diffusion process, J. Econom. Theory 49 (1989) 33–83. https://doi.org/10.1016/0022-0531(89)90067-7
• S. R. Pliska, A stochastic calculus model of continuous trading: optimal portfolios, Math. Oper. Res. 11 (1986) 371–382. https://doi.org/10.1287/moor.11.2.371
• I. Karatzas, J. P. Lehoczky, S. E. Shreve and G. L. Xu, Martingale and duality methods for utility maximization in an incomplete market, SIAM J. Control Optim. 29 (1991) 702–730. https://doi.org/10.1137/0329039
• H. He and N. D. Pearson, Consumption and portfolio policies with incomplete markets and short-sale constraints: the infinite-dimensional case, J. Econom. Theory 54 (1991) 259–304. https://doi.org/10.1016/0022-0531(91)90123-L
• I. Karatzas and S. E. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1988. https://doi.org/10.1007/978-1-4684-0302-2