Functional Analysis

Motivation

Many problems in convex optimization, variational inequalities, game theory and signal processing are systems of monotone inclusions coupled by linear operators: several unknowns $x_i$ in different Hilbert spaces, each subject to its own maximally monotone, cocoercive and Lipschitzian operators, and tied together through linear maps $L_{ki}$ and composite terms. Bùi and Combettes (arXiv:2002.06135, Mathematics of Operations Research, 2022) introduce a single model, Problem 1.1, that contains a large part of these formulations and design algorithms for it that are fully split (each operator is used separately, set-valued operators through their resolvents and single-valued ones through forward evaluations), block-iterative (only some blocks are updated at each iteration) and asynchronous (updates may use information computed up to $T$ iterations earlier).

The paper places itself after a line of primal-dual splitting methods: Briceño-Arias and Combettes (SIAM J. Optim. 2011, doi:10.1137/10081602x) for a two-operator monotone+skew model, Alotaibi, Combettes and Shahzad (SIAM J. Optim. 2014) for Fejér approximation of a Kuhn–Tucker set, Combettes and Eckstein (Math. Program. B168, 2018) for asynchronous block-iterative primal-dual decomposition, and the projective splitting methods of Johnstone and Eckstein (2020–2021). These earlier methods work in the primal-dual space $\mathcal H\oplus\mathcal G$. The new idea is to reformulate the problem as finding a zero of a saddle operator on a larger space and to approximate that zero set from outside by half-spaces.

Setting

Let $I$ and $K$ be finite index sets and let $(\mathcal H_i)_{i\in I}$, $(\mathcal G_k)_{k\in K}$ be real Hilbert spaces, with Hilbert direct sums $\mathcal H=\bigoplus_i\mathcal H_i$ and $\mathcal G=\bigoplus_k\mathcal G_k$. For every $i$ and $k$ the data are:

• $A_i:\mathcal H_i\to2^{\mathcal H_i}$ maximally monotone, $C_i$ cocoercive with constant $\alpha^c_i>0$, $Q_i$ monotone and $\alpha^\ell_i$-Lipschitzian, and $R_i:\mathcal H\to\mathcal H_i$ such that $R=(R_i)_i$ is monotone and $\chi$-Lipschitzian on $\mathcal H$;
• $B^m_k$, $D^m_k$ maximally monotone on $\mathcal G_k$, $B^c_k$, $D^c_k$ cocoercive with constants $\beta^c_k,\delta^c_k>0$, and $B^\ell_k$, $D^\ell_k$ monotone and Lipschitzian with constants $\beta^\ell_k,\delta^\ell_k$;
• bounded linear $L_{ki}:\mathcal H_i\to\mathcal G_k$, and vectors $s^*_i\in\mathcal H_i$, $r_k\in\mathcal G_k$.

The parallel sum of $B,D:\mathcal G_k\to2^{\mathcal G_k}$ is $B\,\square\,D=(B^{-1}+D^{-1})^{-1}$. Write $\mathsf B_k=B^m_k+B^c_k+B^\ell_k$ and $\mathsf D_k=D^m_k+D^c_k+D^\ell_k$. The primal problem (1.1) asks for $\overline x\in\mathcal H$ with

$$s^*_i\in A_i\overline x_i+C_i\overline x_i+Q_i\overline x_i+R_i\overline x+\sum_{k\in K}L^*_{ki}\Big((\mathsf B_k\,\square\,\mathsf D_k)\Big(\sum_{j\in I}L_{kj}\overline x_j-r_k\Big)\Big)\quad(\forall i\in I).$$

Its set of solutions is $\mathscr P$. The dual problem (1.2) asks for $\overline v^*\in\mathcal G$ such that some $x\in\mathcal H$ satisfies $s^*_i-\sum_jL^*_{ji}\overline v^*_j\in A_ix_i+C_ix_i+Q_ix_i+R_ix$ and $\overline v^*_k\in(\mathsf B_k\,\square\,\mathsf D_k)(\sum_jL_{kj}x_j-r_k)$; its set of solutions is $\mathscr D$. The Kuhn–Tucker set $\mathsf Z\subset\mathcal H\oplus\mathcal G$ (2.13) collects the pairs $(\overline x,\overline v^*)$ satisfying the first condition at $\overline x$ and $\sum_jL_{kj}\overline x_j-r_k\in\mathsf B_k^{-1}\overline v^*_k+\mathsf D_k^{-1}\overline v^*_k$.

On $\mathbf X=\mathcal H\oplus\mathcal G\oplus\mathcal G\oplus\mathcal G$ the saddle operator $\boldsymbol{\mathcal S}$ (2.11) maps $(x,y,z,v^*)$ to the product of the sets $-s^*_i+A_ix_i+C_ix_i+Q_ix_i+R_ix+\sum_kL^*_{ki}v^*_k$, $\ B^m_ky_k+B^c_ky_k+B^\ell_ky_k-v^*_k$, $\ D^m_kz_k+D^c_kz_k+D^\ell_kz_k-v^*_k$ and $\{r_k+y_k+z_k-\sum_iL_{ki}x_i\}$. It splits as $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$ (Definition 2.4), where $\mathbf C$ collects the cocoercive operators.

Algorithm 3.4 runs, at iteration $n$, over activated blocks $I_n\subset I$, $K_n\subset K$. For $i\in I_n$ it computes a resolvent step $a_{i,n}=J_{\gamma A_i}(\cdot)$ from the delayed iterate $x_{\pi_i(n)}$; for $k\in K_n$ it computes $b_{k,n}$, $d_{k,n}$ from resolvents of $B^m_k$, $D^m_k$ at the delayed iterate $\omega_k(n)$. Blocks that are not activated keep their previous values. From these quantities it forms a half-space containing $\operatorname{zer}\boldsymbol{\mathcal S}$, measured by a number $\Delta_n$ that involves $\alpha=\min\{\alpha^c_i,\beta^c_k,\delta^c_k\}$. If $\Delta_n>0$, it moves $(x_n,y_n,z_n,v^*_n)$ toward that half-space with relaxation $\lambda_n\in[\varepsilon,2-\varepsilon]$; otherwise the iterate stays put.

Formalization targets

Goal: Theorem 3.5

Under Assumptions 3.1–3.3 (step-size ranges tied to $\alpha$, $\sigma>1/(4\alpha)$ and $\varepsilon$ by (3.1); every block activated at least once in every $P+1$ consecutive iterations; delays at most $T$), if the dual problem has a solution, then every run of Algorithm 3.4 satisfies

$$\sum_n\|x_{i,n+1}-x_{i,n}\|^2<\infty,\qquad x_{i,n}-a_{i,n}\to0,\qquad v^*_{k,n}-e^*_{k,n}\to0,$$

together with the analogous statements for $y,z,v^*$ and $b,d$. There exist $\overline x\in\mathscr P$ and $\overline v^*\in\mathscr D$ with $(\overline x,\overline v^*)\in\mathsf Z$ such that

$$x_{i,n}\rightharpoonup\overline x_i,\qquad a_{i,n}\rightharpoonup\overline x_i,\qquad v^*_{k,n}\rightharpoonup\overline v^*_k.$$

Milestones

In attack order:

1. Proposition 2.2(i)–(ii): $\boldsymbol{\mathcal S}$ is maximally monotone and $\operatorname{zer}\boldsymbol{\mathcal S}$ is closed and convex.
2. Proposition 2.2(iii)–(iv): zeros of $\boldsymbol{\mathcal S}$ project into $\mathsf Z\subset\mathscr P\times\mathscr D$, and $\mathscr D\neq\varnothing\Leftrightarrow\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing\Leftrightarrow\mathsf Z\neq\varnothing\Rightarrow\mathscr P\neq\varnothing$.
3. Proposition 2.5: $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$, $\mathbf M$ maximally monotone, $\mathbf C$ $\alpha$-cocoercive, and the half-spaces containing $\operatorname{zer}\boldsymbol{\mathcal S}$.
4. Lemma A.4: the relaxed half-space outer-approximation iteration (A.3) is Fejér monotone and converges weakly when every weak sequential cluster point lies in $Z$.
5. Proposition 2.6: the iteration (2.32) on $\mathbf X$ converges weakly to a zero of $\boldsymbol{\mathcal S}$ when its three stated residual conditions hold.
6. Lemmas A.1, A.2 and A.3: boundedness of resolvent sequences, strong monotonicity of $\gamma^{-1}\mathrm{Id}-A$, and the vanishing of the delayed differences $x_{\vartheta_i(n)}-x_n$.

Significance

Theorem 3.5 gives weak convergence of a method that uses each operator of Problem 1.1 separately, needs no inversion of linear operators and no knowledge of $\|L\|$, and updates nonempty subsets of blocks subject to the coverage windows and bounded delays of Assumptions 3.2–3.3. It produces primal and dual solutions together. Section 4 of the paper derives from it algorithms for variational inequalities over sums of sets and for multivariate convex minimization with infimal convolutions. The hypothesis is dual solvability. Remark 2.3 shows that primal solvability alone is not enough: there are instances with $\mathscr P\neq\varnothing$ and $\mathsf Z=\varnothing$.

The theorem is proved in the paper. A formalization adds machine-checked foundations that later work in splitting methods can reuse: the saddle operator and its maximal monotonicity; the Fejér outer-approximation principle in Hilbert space (Lemma A.4, cited by the paper from an encyclopedia entry); and the asynchrony lemma (Lemma A.3). To our knowledge none of these results has been formalized before.

Difficulty

The obvious approach would be to show that Algorithm 3.4 is a Fejér-monotone iteration toward $\mathsf Z$ in $\mathcal H\oplus\mathcal G$. That approach fails: for the general Problem 1.1, no half-space separating the current point from $\mathsf Z$ can be computed from separate operator evaluations (Remark 2.3(iii)). The algorithm instead targets $\operatorname{zer}\boldsymbol{\mathcal S}$ in the larger space $\mathbf X$. The link back to $\mathscr P$, $\mathscr D$ and $\mathsf Z$ is Proposition 2.2.

The second difficulty is asynchrony. The half-space at iteration $n$ is built from points computed at earlier iterations, with stale step sizes. To show that the weak cluster points are zeros of $\boldsymbol{\mathcal S}$, one has to control these delays (Lemma A.3) and use the cocoercive and Lipschitzian terms uniformly over the step-size ranges (Lemmas A.1–A.2).

Formalization scope

• Spaces. Every space is a complete real inner product space. $\mathcal H$ and $\mathcal G$ are PiLp 2 over finite index types, and $\mathbf X$ is a nested WithLp 2 product, so all norms and inner products are the Hilbert ones (not sup norms).
• Operators. Set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity, zer, cocoercivity, resolvents and weak convergence are the published ThreeOpSplitting.Convergence definitions; inverses and sums of set-valued maps are the published DouglasRachfordPPA.GenDR ones.
• Runs. A run of Algorithm 3.4 is a predicate on given sequences that pins every assignment of (3.3). This includes the delayed indices inside the step sizes, the carry-over of inactive blocks (stated at $n+1$), the recomputation of $e_{k,n}$ for every $k$, and $\Delta_n$ with the factor $(4\alpha)^{-1}$ at the current iterates. The resolvents are given maps constrained by the resolvent identity at every positive step.
• Constants and assumptions. $\alpha$ is pinned as the least cocoercivity constant. The delay bound $n-T\le\pi_i(n)\le n$ is written without natural-number subtraction. "$\varlimsup\Delta_n\le0$" in Proposition 2.6 is stated as "eventually $\Delta_n\le\delta$ for every $\delta>0$".
• Ruling out trivial readings. The run predicate determines every assignment of (3.3), so no free choice of outputs makes the theorem trivial. The hypothesis is dual solvability $\mathscr D\neq\varnothing$ exactly as in (1.2), not the stronger-looking $\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing$ (equivalent only by Proposition 2.2). The conclusion is weak convergence to a pair that is simultaneously primal, dual and Kuhn–Tucker. A sorry-free check shows that the goal's hypotheses are jointly satisfiable.
• Not included. Theorem 3.7 (strong convergence of a Haugazeau-type variant) with Proposition 2.7 and Lemma A.5, Proposition 2.2(v), and the applications of Section 4.
• Reusable parts. The saddle operator and its splitting, Lemma A.4, Lemma A.3, and Lemmas A.1–A.2 are stated in general form and can serve other splitting missions. Contributions of auxiliary results are welcome, for example demiclosedness of maximally monotone operators, Minty's theorem in the published encoding, and Fejér-monotone weak convergence (Opial).

Selected references

• M. N. Bùi and P. L. Combettes, Multivariate monotone inclusions in saddle form, Mathematics of Operations Research, 2022; preprint arXiv:2002.06135v3, 2021. https://arxiv.org/abs/2002.06135
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• L. M. Briceño-Arias and P. L. Combettes, A monotone+skew splitting model for composite monotone inclusions in duality, SIAM Journal on Optimization 21, 2011. https://doi.org/10.1137/10081602x
• P. L. Combettes and J. Eckstein, Asynchronous block-iterative primal-dual decomposition methods for monotone inclusions, Mathematical Programming B168, pp. 645–672, 2018 (reference [25] of arXiv:2002.06135).
• P. L. Combettes, Fejér-monotonicity in convex optimization, in: Encyclopedia of Optimization, vol. 2, pp. 106–114, Springer, 2001 (reference [22] of arXiv:2002.06135; source of Lemma A.4).

Motivation

Firms carry risks they cannot insure directly. A farmer's revenue depends on local yield and on local price; an airline's cost depends on jet fuel at a specific airport; an energy retailer's margin depends on load and on weather. Exchange-traded derivatives are written on standardized indices, so the exposure that matters is only partly claimable. Guiotto and Roncoroni (Operations Research 2022) study the design of a combined custom hedge: one over-the-counter claim written on the claimable part $X$ of the firm's risk, plus a second claim written on a side index $I$ that is correlated with the unclaimable part. The question is when such a pair is well defined, that is, when the firm's mean–variance hedging problem has one and only one optimal pair of claims.

Single-claim custom hedging goes back to Chowdhry and Howe (1999) and Caldentey and Haugh (2006; 2009, Operations Research 57(1)), whose framework prices claims through a pricing kernel $dQ/dP$ known to the firm; that framework is adopted here. With two claims on two different random elements the optimal pair is coupled, and existence and uniqueness are no longer automatic.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying three random elements, valued in arbitrary measurable spaces: the claimable term $X$, the nonclaimable term $Y$ and the side index $I$. Write $\mathcal F_X=\sigma(X)$ and $\mathcal F_I=\sigma(I)$. The firm's business position is $\pi=\pi(X,Y)$ for a Borel revenue function $\pi$, assumed square-integrable.

A claim on $X$ is a random variable $H$ that is $\mathcal F_X$-measurable and has finite variance; the set of such claims is $\mathcal H_X$, and $\mathcal H_I$ is defined likewise. The centered subspace $\mathbb H_X\subseteq\mathcal H_X$ consists of claims with $\mathbb E[H]=0$.

Claims are priced by a pricing kernel $dQ/dP$, the density of an equivalent martingale measure $Q$: it is positive almost surely, has mean one and is square-integrable, and $\mathbb E_Q[Z]=\mathbb E[Z\,dQ/dP]$. The firm ranks positions by the mean–variance criterion

$$\mathcal U(Z)=\varrho\,\mathbb E[Z]-\tfrac a2\operatorname{Var}[Z],\qquad \varrho\ge 0,\ a>0 .$$

The value-centered design problem is

$$\max\Big\{\mathcal U\big(\pi+[H+G]\big)\ :\ H\in\mathcal H_X,\ G\in\mathcal H_I,\ \mathbb E_Q[H]=\mathbb E_Q[G]=0\Big\}.\qquad(4)$$

A maximizer $(H^*,G^*)$ is an optimal combined claim pair. The dependence between $X$ and $I$ is measured by the maximal correlation

$$r_{XI}=\sup\big\{\rho(\phi,\psi)\ :\ \phi\in\mathbb H_X,\ \psi\in\mathbb H_I\big\}\in[0,1],\qquad(6)$$

with $\rho$ the Pearson correlation. Finally $\mathcal K=\pi+(\varrho/a)\,dQ/dP$ is the optimal hedging kernel, $\Pi^X_0=-\mathbb E\big[\mathcal K-\mathbb E[\mathcal K\mid\mathcal F_I]\mid\mathcal F_X\big]$, and $T[Z]=\mathbb E\big[\mathbb E[Z\mid\mathcal F_I]\mid\mathcal F_X\big]$.

Formalization targets

Goal: Theorem 1 (p. 11)

If $r_{XI}<1$, then

1. an optimal combined claim pair $(H^*,G^*)$ of (4) exists;
2. it is unique up to $P$-null sets, and so is the hedge $H^*+G^*$;
3. the value-centered optimal claim $H^*_0=H^*-\mathbb E[H^*]$ solves

$$H^*_0=\Pi^X_0+\mathbb E\big[\mathbb E[H^*_0\mid\mathcal F_I]\mid\mathcal F_X\big].\qquad(7)$$

Milestones

• Proposition 1 (p. 9): every optimal pair is $H^*=H^*_0-\mathbb E_Q[H^*_0]$, $G^*=G^*_0-\mathbb E_Q[G^*_0]$ with $P$-centered $(H^*_0,G^*_0)$ solving the first-order system (5).
• (EC.25)–(EC.26) (p. ec24): a centered solution of (5) satisfies $H_0=\Pi_0+T[H_0]$.
• $T$ on $\mathbb H_X$ (p. ec24): $\mathbb E[T[Z]]=\mathbb E[Z]$, $T(\mathbb H_X)\subseteq\mathbb H_X$, and $\Pi_0\in\mathbb H_X$.
• Inner-product bound (p. ec25): $\langle\mathbb E[\phi\mid\mathcal F_I],\psi\rangle\le r_{XI}\|\phi\|_2\|\psi\|_2$ for $\phi\in\mathbb H_X$, $\psi\in\mathbb H_I$.
• (EC.28) (p. ec25): $\|\mathbb E[\phi\mid\mathcal F_I]\|_2\le r_{XI}\|\phi\|_2$.
• $\|T\|\le r_{XI}$ (p. ec25) on $\mathbb H_X$.
• (EC.27) (p. ec25): if $r_{XI}<1$, $H_0=\Pi_0+T[H_0]$ has a unique solution in $\mathbb H_X$.

Significance

The result. Theorem 1 makes the combined hedge an object: without it the optimal pair may fail to exist or may be non-unique (the paper points to Appendix EC.1(F) for non-uniqueness), and the paper's later results, the design integral equation (Theorem 2) and the value of combining claims (Theorem 3 and Definitions 1–3), are stated for the optimal pair whose existence and uniqueness Theorem 1 provides. Equation (7) separates the optimal claim into a part determined by the kernel $\mathcal K$ alone and a cross-claim feedback through $I$. The condition $r_{XI}<1$ is checkable: for jointly lognormal $(X,I)$ it reduces to $|\rho_{Z,W}|<1$ for the underlying normals (Example 4).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof needs a Hilbert-space treatment of conditional expectations onto two σ-algebras, a formal maximal-correlation index, and an existence argument for the maximization problem itself, which the paper's proof leaves implicit (see below). The intermediate statements are general facts about pairs of σ-algebras with maximal correlation below one and are reusable outside hedging.

Difficulty

The optimal pair is coupled: the claim on $X$ depends on the conditional expectation of the claim on $I$ given $X$ and conversely, so neither can be computed first. When $X$ and $I$ share information, the two claim spaces overlap and the sum $\mathcal H_X+\mathcal H_I$ need not be closed in $L^2$; a maximizing sequence can then escape, and two different pairs can produce the same hedge. The condition $r_{XI}<1$ excludes this, and the work lies in turning it into a quantitative bound on the alternating conditional-expectation operator.

A second difficulty is a gap in the printed argument. The paper derives the first-order system (5) as a necessary condition and then proves that the resulting fixed-point equation has a unique solution. It does not show that the pair built from that solution is optimal for (4), so existence of a maximizer needs a separate argument that the first-order condition is also sufficient or that the maximum is attained. The goal is stated for maximizers of (4), so this step cannot be skipped.

Formalization scope

Everything lives in the namespace CustomHedge.Exist. A Market bundles $P$, $X$, $Y$, $I$, the revenue function, the kernel D $=dQ/dP$, rho $=\varrho$ and a; Standing collects the assumptions above. Conventions:

• Claims are random variables $\Omega\to\mathbb R$, strongly measurable for $\sigma(X)$ (resp. $\sigma(I)$) and in $L^2(P)$, not payoff functions $x\mapsto H(x)$.
• Optimality is maximization of U over all feasible pairs; uniqueness and the equations (5), (7), (EC.25), (EC.27) hold $P$-almost surely.
• $\mathbb E_Q$ centers the budget constraint; $\mathbb E=\mathbb E_P$ centers $H^*_0$, $\mathbb H_X$ and the maximal correlation.
• The paper allows $a\ge0$; the formalization requires $a>0$, because $\mathcal K$ divides by $a$ and with $a=0$ problem (4) generally has no maximizer. $\varrho=0$ is allowed.
• The maximal correlation is a real supremum over pairs with positive variances (where $\rho$ is defined), with $\sup\emptyset=0$; the set is bounded by one.
• $\|Z\|_2=(\mathbb E[Z^2])^{1/2}$; conditional expectation is Mathlib's condExp.

A trivializing formalization is ruled out: the goal quantifies over maximizers of (4), not over solutions of the first-order system or of (EC.27), which are separate milestones. A sorry-free check confirms the standing assumptions and $r_{XI}<1$ hold together with a non-trivial $\sigma(X)$.

Needed infrastructure: $L^2$ conditional expectation as an orthogonal projection, the identity $\mathbb E[\mathbb E[\phi\mid\mathcal G]\psi]=\mathbb E[\phi\psi]$ for $\mathcal G$-measurable $\psi$, Banach's fixed-point theorem on a closed subspace of $L^2$, and concave maximization over a closed affine subspace. The maximal-correlation file is reusable beyond this mission. Proofs of individual milestones, and a proof of the goal by any route, are welcome.

Selected references

• P. Guiotto and A. Roncoroni, Combined custom hedging: optimal design, noninsurable exposure, and operational risk management, Operations Research 70(3), 2022. https://doi.org/10.1287/opre.2021.2133 (cited from manuscript OPRE-2019-01-058.R3)
• R. Caldentey and M. Haugh, Optimal control and hedging of operations in the presence of financial markets, Mathematics of Operations Research 31(2), 2006. https://doi.org/10.1287/moor.1060.0193
• B. Chowdhry and J. T. B. Howe, Corporate risk management for multinational corporations: financial and operational hedging policies, European Finance Review 2, 229–246, 1999 (as cited in the paper; no link verified).
• A. Rényi, On measures of dependence, Acta Mathematica Academiae Scientiarum Hungarica 10, 1959. https://doi.org/10.1007/BF02024507
• B. Schweizer and E. F. Wolff, On nonparametric measures of dependence for random variables, Annals of Statistics 9(4), 1981. https://doi.org/10.1214/aos/1176345528

Why continuum Fisher markets matter

A Fisher market divides a supply of goods among buyers with fixed budgets. In a finite market, each good is a separate coordinate. Fair division can instead involve a continuum of items, such as locations along an interval or points in a region, where a buyer's valuation varies measurably from point to point. Finite dimensional existence and duality arguments do not automatically apply: the allocation is now a function, and the feasible set need not be compact in its natural function space. Gao and Kroer formulate a market and two Eisenberg–Gale programs for this setting, then prove that their optima exist and characterize equilibrium Gao and Kroer, §3.

The result also connects market equilibrium to fair division. A pure allocation assigns measurable regions of the item space to buyers, allowing overlap only on null sets. Existence of a pure optimizer means that a market outcome can be represented by such a division, rather than by fractional shares at each item. The same paper derives Pareto optimality, budget weighted envy freeness, and proportionality for equilibrium allocations Gao and Kroer, Theorems 1 and 3.

Market, allocations, and programs

The item space $\Theta$ is a compact subset of $\mathbb R^d$ with restricted Lebesgue measure $\mu$. There are $n$ buyers. Buyer $i$ has a budget $B_i>0$ and a nonnegative integrable valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$. The utility of a bounded nonnegative bundle $x_i$ is $\langle v_i,x_i\rangle=\int_\Theta v_i x_i\,d\mu$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. It is pure when each $x_i$ equals the indicator of a measurable set $\Theta_i\subseteq\Theta$, up to almost everywhere equality, and these sets are pairwise disjoint up to null sets. Leftover items are allowed.

A nonnegative integrable price density $p$ defines a buyer's affordable bundles by $\langle p,x_i\rangle\le B_i$. A market equilibrium $(x,p)$ is a feasible allocation and price at which every buyer maximizes utility among affordable bundles and $\langle p,1-\sum_i x_i\rangle=0$. Thus unallocated supply may remain only where it has zero price. The paper's primal Eisenberg–Gale program, $\mathcal P_{EG}$, maximizes weighted log utility over feasible allocations. Its dual program, $\mathcal D_{EG}$, minimizes total price minus weighted log multipliers subject to $p\ge\beta_i v_i$ almost everywhere Gao and Kroer, pp. 6–8.

Formalization targets

The goal is the three part Theorem 1. In the notation above, it asserts attainment of the primal objective at a pure allocation, attainment of the dual objective with a unique multiplier vector $\beta^*$ and price $p^*=\max_i\beta_i^*v_i$ almost everywhere, and the equivalence

$$(x,p)\text{ is a market equilibrium} \quad\Longleftrightarrow\quad x\text{ optimizes }\mathcal P_{EG}\ \text{and}\ (p,\beta^*)\text{ optimizes }\mathcal D_{EG}.$$

The milestone list follows the results the paper uses to reach that goal. Lemma A.1 gives a convex, compact range for utility matrices and, under atomlessness, identifies mixed and partition based ranges. Lemma 1 specializes this to the market's feasible utility set $U$, proving that $U$ is compact and convex and equals the pure utility set $U'$. Lemma 2 establishes attainment and uniqueness in the finite dimensional reduction of the dual problem. Lemma 3 gives weak duality with the paper's constant $C=\sum_i B_i-\sum_i B_i\log B_i$ and its three optimality conditions. Theorem 2 expands the equivalence between optimality and equilibrium, including budget exhaustion and the utility formula $\langle v_i,x_i\rangle=B_i/\beta_i$. These are the paper's numbered results on pp. 8–10 and a1 Gao and Kroer, §3 and Appendix A.1.

The proposal also states Theorem 3, Lemma 4, and Corollaries 1–3 as companion results. They record the resulting fairness properties, normalized equilibrium bounds, winning sets, a construction of dual prices from a pure optimum, and a test for a pure equilibrium Gao and Kroer, pp. 10–11.

What the result provides

Theorem 1 shows that the two programs give actual allocations and prices in the continuum market, not merely limiting objective values. The pure optimizer provides measurable regions for buyers. The dual multipliers give a unique utility price for each buyer, while the price density is determined almost everywhere. Theorem 2 makes these program outputs economically interpretable: each buyer exhausts its budget at equilibrium. Theorem 3 then supplies efficiency and fairness guarantees for those allocations Gao and Kroer, Theorems 1–3.

These results are proved in the cited paper. This mission asks for machine checked Lean proofs of those mathematical statements. Its definitions of allocations, demand, equilibrium, the two programs, and feasible utilities could also support formalization of the paper's later geometric and quasilinear results. The draft declarations compile as open statements; compilation does not establish the theorems.

Why the proof is difficult

The feasible allocations are bounded in an infinite dimensional function space, but that does not make the set compact in the topology used for the optimization problem. The paper instead needs compactness of the finite dimensional set of achievable utility vectors. The range result in Lemma A.1 is therefore central, and its atomless conclusion must be strong enough to replace fractional allocations by measurable partitions Gao and Kroer, Lemma 1 and Appendix A.1.

Standard constraint qualification arguments also do not supply the required duality theorem here: the positive cone in $L^1(\Theta)$ has empty interior. The proposal consequently asks for the paper's specific weak duality inequality, attainment, and optimality characterization rather than assuming a general finite dimensional duality theorem applies Gao and Kroer, Remark 1.

Formalization scope

Lean uses real valued measurable functions on the ambient Euclidean space with measure $\mu=\mathrm{volume}|_\Theta$. It identifies prices and allocations up to $\mu$ almost everywhere equality, as the paper identifies $L^1$ and $L^\infty$ equivalence classes. Bundles must belong to $L^\infty(\mu)$ and prices and valuations must be integrable; these conditions prevent a nonintegrable product from receiving Lean's default integral value of zero. The number of buyers may be zero, consistent with the finite index formulation, while the standing positivity hypotheses apply to every buyer present.

The real logarithm in Lean returns zero at zero. The optimization predicates instead require positive utility or positive dual multipliers and compare only with other positive points, matching the paper's $\log 0=-\infty$ objective convention. The maximization over buyers is the finite supremum $\sup_i\beta_i v_i$. Price and allocation uniqueness is stated almost everywhere; multiplier uniqueness is exact. Lemma A.1 uses the paper's divisible measure condition for atomlessness and fixes its unnamed almost everywhere partition convention by requiring $\sum_jx_j=1$ everywhere. Corollary 3 explicitly requires each denominator $v_i(\Theta_i)$ to be positive. Lemma 4 alone assumes the normalizations $v_i(\Theta)=1$ and $\sum_iB_i=1$, which the paper recalls before its statement.

The goal remains the full three part theorem. It does not assume the range theorem, duality equality, or optimality conditions it is meant to establish. Contributions to the measure range theorem, utility set compactness, the dual reduction, and the equilibrium characterization are all within scope.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023; formalization follows arXiv:2010.03025v5, 2021, §§2–3 and Appendix A.1.

Motivation

Most online advertising is sold by auction, one impression at a time, to advertisers who manage a budget over many auctions rather than a value for a single one. Since 2019 the major ad exchanges have moved from second price to first price auctions, in which the winner pays its own bid. A budget-constrained advertiser in a first price auction must therefore shade its bids twice: once because of the budget, and once because of the payment rule. Whether these two effects admit a coherent equilibrium, and of what form, is the question behind Balseiro, Kroer and Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees (Management Science, 2023, doi:10.1287/mnsc.2023.4719).

Earlier work on pacing equilibria treated second price auctions, where truthful bidding is dominant without budgets (Balseiro, Besbes and Weintraub 2015; Conitzer et al. 2022). In first price auctions with a single deterministic item, an equilibrium may fail to exist (the paper's Online Appendix A). The paper restores existence by letting items carry a random context and values depend on it linearly. This mission formalizes its first main result, Theorem 1: an equilibrium of a simple, interpretable form exists.

Setting

An item has a context $\alpha\in A\subset\mathbb R^d_{+}$, a feature vector drawn from a law $F$ with a density. There are $n$ buyers. Each buyer has a type $\theta=(w,B)$, a weight vector $w$ and a budget $B$, drawn independently from a law $G$ with a density on

$$\Theta=(0,U)^d\times(B_{\min},U).$$

Buyer $(w,B)$ values item $\alpha$ at $w^T\alpha$, and $\omega:=\sup_{(w,B)\in\Theta,\alpha\in A}w^T\alpha$. The seller reveals $\alpha$, then runs a first price auction with a public reserve price $r(\alpha)$: a bid $b(\alpha)$ wins if $b(\alpha)\ge\max(r(\alpha),\{\beta(\theta_i,\alpha)\}_i)$, where $\beta$ is the strategy of the $n-1$ competitors, and the winner pays its bid. A budget only needs to hold in expectation over $\alpha$ and the competitors' types.

A strategy $\beta^*:\Theta\times A\to\mathbb R_{\ge0}$ is a symmetric first price equilibrium (SFPE, Definition 1) if for $G$-almost every type $(w,B)$ the bid function $\beta^*(w,B,\cdot)$ solves

$$\max_{b:A\to\mathbb R_{\ge0}}\ \mathbb E\big[(w^T\alpha-b(\alpha))\mathbb 1\{b(\alpha)\ge\max(r(\alpha),\{\beta^*(\theta_i,\alpha)\}_i)\}\big]\ \ \text{s.t.}\ \ \mathbb E\big[b(\alpha)\mathbb 1\{\cdots\}\big]\le B .$$

A pacing function $\mu:\Theta\to\mathbb R_{\ge0}$ scales values down to paced values $w^T\alpha/(1+\mu(w,B))$. Let $H^\mu_\alpha$ be the distribution function of the highest of $n-1$ i.i.d. paced values, and for $x\ge r(\alpha)$ let

$$\sigma^\mu_\alpha(x)=x-\int_{r(\alpha)}^x\frac{H^\mu_\alpha(s)}{H^\mu_\alpha(x)}\,ds,$$

with $\sigma^\mu_\alpha(x)=0$ if $H^\mu_\alpha(x)=0$ and $\sigma^\mu_\alpha(x)=x$ if $x<r(\alpha)$. The value pacing–based strategy (Definition 2) is

$$\beta^\mu(w,B,\alpha)=\sigma^\mu_\alpha\Big(\frac{w^T\alpha}{1+\mu(w,B)}\Big).$$

For a buyer facing competitors who use $\beta^\mu$, the dual function is $q^\mu(w,B,t)=\sup_b\mathbb E[(w^T\alpha-(1+t)b(\alpha))\mathbb 1\{\cdots\}]+tB$ for $t\ge0$.

Formalization targets

Goal: Theorem 1 (p. 7)

$$\exists\,\mu:\Theta\to\mathbb R_{\ge0}\quad\text{such that}\quad \beta^\mu\ \text{is an SFPE}.$$

Milestones

• Lemma 1 (p. 8): for every type and every $t\ge0$, $\sigma^\mu_\alpha(w^T\alpha/(1+t))$ maximizes the Lagrangian $\mathbb E[(w^T\alpha/(1+t)-b(\alpha))\mathbb 1\{\cdots\}]$.
• Proposition 1 (p. 8): on a set $\Theta'$ of full $G$-measure, for every $\mu$, a minimizer $t^*$ of $q^\mu(w,B,\cdot)$ over $t\ge0$ makes $\sigma^\mu_\alpha(w^T\alpha/(1+t^*))$ optimal for the budget-constrained problem $Q^\mu(w,B)$.
• Lemma 2 (p. 10): the smallest minimizer $\ell^\mu(w,B)$ of $q^\mu(w,B,\cdot)$ over $[0,\omega/B_{\min}]$ is nondecreasing in each $w_i$ and nonincreasing in $B$.
• Lemma 3 (p. 10): $\ell^\mu\in L_1(\Theta)$ and its total variation is at most $V_0=(d+1)\max(U^d,U^{d+1})\,\omega/B_{\min}$. The paper prints $(d+1)U^{d+1}\omega/B_{\min}$, which agrees when $U\ge1$. For $U<1$ the printed bound fails by a rescaling argument, and the mission corrects the exponent to $d$ there.
• Lemma 4 (p. 10): $\mathcal X_0=\{\mu\in L_1(\Theta):0\le\mu\le\omega/B_{\min},\ V(\mu,\Theta)\le V_0\}$ is nonempty, compact and convex in $L_1(\Theta)$; $f(\mu,\hat\mu)=\mathbb E_G[q^\mu(w,B,\hat\mu(w,B))]$ is continuous; $C^*_0(\mu)=\arg\min_{\hat\mu\in\mathcal X_0}f(\mu,\hat\mu)$ is upper hemicontinuous with nonempty, convex, compact values.
• Lemma 5 (p. 10): a fixed point $\mu\in C^*_0(\mu)$ satisfies $\mu(w,B)\in\arg\min_{t\in[0,\omega/B_{\min}]}q^\mu(w,B,t)$ almost surely.
• Proposition 2 (p. 9): some $\mu$ satisfies $\mu(w,B)\in\arg\min_{t\ge0}q^\mu(w,B,t)$ almost surely.

The paper states that Proposition 2 combined with Proposition 1 implies Theorem 1.

Significance

Theorem 1 says that budget-constrained buyers in contextual first price auctions have an equilibrium that is described by one scalar per type: shade the value by the factor $1/(1+\mu(w,B))$, then bid as an unconstrained buyer would in an i.i.d. first price auction against paced competitors. This is the object on which the rest of the paper is built: revenue equivalence across standard auctions (Theorem 2) and a liquid-welfare price of anarchy of at least $1/2$ (Theorem 3) are both statements about pacing-based equilibria. Practically, it supports the use of pacing for budget management in first price auctions, with pacing multipliers computed as for second price auctions.

The result is proved in the paper; every proof is in its online appendix, which is not part of the source this mission cites. Nothing in the paper is formalized. A formalization would check a strong-duality argument for a non-convex problem and an infinite-dimensional fixed-point argument whose topology the authors chose with care, and it would produce reusable pieces: multivariate total variation, compactness of bounded-variation sets in $L_1$, and the first price equilibrium bid against an arbitrary (possibly atomic) value distribution with a reserve price.

Difficulty

The buyer's problem $Q^\mu(w,B)$ is not convex in the bid function, so standard convex duality does not give strong duality; Proposition 1 needs a direct argument combining Lagrangian optimality (Lemma 1), differentiability of $q^\mu$ in $t$, and complementary slackness. Lemma 1 itself cannot quote the textbook first price equilibrium, because the paced value distribution $\lambda^\mu_\alpha$ may have atoms and the reserve price creates discontinuities.

The fixed point lives in an infinite-dimensional space of pacing functions. The obvious topologies fail: the set $\mathcal X$ of bounded pacing functions is not compact in any $L_p$, and in the weak-* topology of $L_\infty$ upper hemicontinuity of the best-response correspondence is hard to obtain; restricting to Lipschitz functions loses the property that best responses stay in the set. The paper restricts to functions of bounded total variation, which requires the monotonicity of Lemma 2 and the variation bound of Lemma 3.

Formalization scope

Contexts are Fin d → ℝ, types are pairs (w, B) : (Fin d → ℝ) × ℝ, and $w^T\alpha$ is the explicit sum $\sum_i w_i\alpha_i$. A single Model structure holds $d,n,U,B_{\min},A,F,G,r$, and Model.Standing collects the assumptions of §2.2 together with four that the paper uses without stating them: $n\ge2$, $B_{\min}<U$, $A$ nonempty and bounded (so $\omega<\infty$), and measurability of $A$ and $r$. Pacing functions are measurable functions on $\mathbb R^d\times\mathbb R$ that are nonnegative on $\Theta$; values off $\Theta$ are irrelevant since $G(\Theta^c)=0$.

The conventions fixed in Lean:

• Ties win: the indicator is $b(\alpha)\ge\max(\cdots)$, as in the paper's tie-breaking rule.
• An admissible bid function is measurable, nonnegative on $A$, and has an integrable payment integrand. The problem of Definition 1, $Q^\mu$, $q^\mu$ and the Lagrangian of Lemma 1 all range over this class.
• An SFPE is jointly measurable in $(\theta,\alpha)$, so Theorem 1 must produce a measurable strategy.
• $q^\mu$ is the supremum over bids of p. 7, not the closed form of p. 8. $\sigma^\mu_\alpha$ has an explicit branch for $H^\mu_\alpha(x)=0$.
• Argmins are stated as membership plus IsMinOn, over $t\ge0$ in Propositions 1–2 and over $[0,\omega/B_{\min}]$ in Lemma 5 and $\ell^\mu$, as printed.
• $V(u,\Omega)$ takes values in EReal, with Euclidean $\|\phi(x)\|\le1$ and test fields supported in $\Omega$; $L_1(\Theta)$ is with respect to Lebesgue measure. Lemma 4 is stated on the image of $\mathcal X_0$ in Lp ℝ 1 (volume.restrict Θ), in its norm topology.

A formalization in which $q^\mu$ is defined by its closed form, in which non-integrable payments count as zero, or in which the strategy need not be measurable would make the milestones easier without proving the paper's theorem; these readings are excluded by the definitions above.

A complete development needs: first price equilibrium bids for general atomic distributions with reserves; measurability of parametric integrals; a duality argument for one-dimensional Lagrangian relaxations; multivariate bounded variation and its compact embedding in $L_1$ of a box; and the Kakutani–Fan–Glicksberg theorem in a locally convex space. The bounded-variation and fixed-point parts are reusable beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• S. R. Balseiro, C. Kroer, R. Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2023.4719
• S. R. Balseiro, O. Besbes, G. Y. Weintraub, Repeated Auctions with Budgets in Ad Exchanges: Approximations and Design, Management Science 61(4), 2015. https://doi.org/10.1287/mnsc.2014.2022
• V. Conitzer, C. Kroer, E. Sodomka, N. E. Stier-Moses, Multiplicative Pacing Equilibria in Auction Markets, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2167
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., CRC Press, 2015.

Motivation

Optimal control problems governed by partial differential equations (PDEs) often carry uncertainty in their data, for example a random source term. When the state must stay below a threshold, there are several ways to impose the constraint: with high probability (chance constraints), almost surely, or for every value in a fixed uncertainty set (robust constraints). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive first-order optimality conditions for all three models for the same elliptic model problem. This mission covers the robust model of §3.2 (pp. 23–25). Its Karush–Kuhn–Tucker (KKT) system has a Radon measure as multiplier, and it is related to the semi-infinite programming view of the same problem.

Robust state constraints are also the limiting case of the almost-sure model: by Lemma 3.4 of the paper (p. 19), an almost-sure constraint and the constraint for every parameter in the support of the distribution coincide when the constraint function is lower semicontinuous in the parameter. The robust multipliers live in $C(\bar D\times\Xi)^*$, which is a space of measures, whereas the almost-sure multipliers of §3.1 contain singular functionals with no such representation.

Setting

Let $D\subseteq\mathbb R^d$, $d\in\{1,2,3\}$, be open, bounded and of class S: there are $\gamma\in(0,1)$ and $r_0>0$ such that $\operatorname{meas}(B_r(x)\setminus D)\ge\gamma\operatorname{meas}(B_r(x))$ for all $x\in\partial D$ and $0<r<r_0$. Let $\Xi\subset\mathbb R^m$ be compact, let $f_0,\varphi_1,\dots,\varphi_m\in L^2(D)$, and set $f(x,z)=f_0(x)+\sum_{i=1}^m z_i\varphi_i(x)$ (Assumption 1.1, eq. (3)). The solution operator $A^{-1}:L^2(D)\to C(\bar D)$ maps $F$ to the unique weak solution $y\in H^1_0(D)\cap C(\bar D)$ of $-\Delta y=F$ in $D$, $y=0$ on $\partial D$.

For a control $u\in L^2(D)$, a cost $F:L^2(D)\to\mathbb R$ and a threshold $\alpha\in\mathbb R$, the robust problem (63) is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad -\Delta\hat y(\cdot,z)=u+f(\cdot,z)\ \text{in }D,\quad \hat y(\cdot,z)=0\ \text{on }\partial D,\quad \hat y(x,z)\le\alpha\ \ \forall (x,z)\in D\times\Xi.$$

The state is $\hat{\mathcal S}(u)\in C(\bar D\times\Xi)$, $[\hat{\mathcal S}(u)](x,z)=[A^{-1}(u+f(\cdot,z))](x)$, and $\hat{\mathcal G}(u)=\hat{\mathcal S}(u)-\alpha$. The cone is $\hat{\mathcal K}=\{y\in C(\bar D\times\Xi):y\le0\}$ and its polar cone is $\hat{\mathcal K}^-=\{y^*\in C(\bar D\times\Xi)^*:\langle y^*,y\rangle\le0\ \forall y\in\hat{\mathcal K}\}$. The linear part of the state is $[\hat{\mathcal A}^{-1}\hat{\mathcal B}h](x,z)=[A^{-1}h](x)$. The active set is $M(u)=\{(x,z)\in\bar D\times\Xi:[\hat{\mathcal S}(u)](x,z)=\max_{\bar D\times\Xi}\hat{\mathcal S}(u)\}$.

Formalization targets

Goal: Lemma 3.14 refined to (66), pp. 23–24

Let $F$ be convex and continuously Fréchet differentiable, and assume the constraint qualification $0\in\operatorname{int}\{\hat{\mathcal G}(L^2(D))-\hat{\mathcal K}\}$. Then $u^*$ is a solution of (63) if and only if there is a nonnegative finite Borel measure $\mu^*$ on $\bar D\times\Xi$ with, for $y^*=\hat{\mathcal S}(u^*)$,

$$\langle DF(u^*),h\rangle+\int_{\bar D\times\Xi}[A^{-1}h](x)\,d\mu^*(x,z)=0\quad\forall h\in L^2(D),$$ $$y^*\le\alpha\ \text{on }\bar D\times\Xi,\qquad\int_{\bar D\times\Xi}(y^*-\alpha)\,d\mu^*=0.$$

The page derives (66) from the abstract system (65) of Lemma 3.14 (necessity). Sufficiency is the converse direction of Lemma 3.14, since a nonnegative measure defines a multiplier in $\hat{\mathcal K}^-$ by integration. Both directions are part of the goal.

Milestones

1. Lemma 3.13: unique solvability of (63b)–(63c) in $C(\bar D\times\Xi)$ with the bound (64).
2. Lemma 3.14: the abstract KKT system (65) with $\lambda^*\in C(\bar D\times\Xi)^*$.
3. The identification $C(\bar D\times\Xi)^*\cong\mathcal M(\bar D\times\Xi)$ (p. 23): every $\lambda^*$ is integration against a signed measure.
4. Nonnegativity (p. 24): $\lambda^*\in\hat{\mathcal K}^-$ gives a nonnegative $\mu^*$.
5. Lemma 3.15: (66) is equivalent to the scalar-multiplier form (67): $\lambda^*\ge0$ and a probability measure $\tilde\mu$ on $M(u^*)$ with $\langle DF(u^*),h\rangle+\lambda^*\int[A^{-1}h](x)\,d\tilde\mu=0$, $\max y^*\le\alpha$, $\lambda^*(\max y^*-\alpha)=0$.
6. Lemma 3.16: the convex-hull condition (68) is equivalent to the existence of such a $\tilde\mu$.
7. Lemma 3.4: for lower semicontinuous $h$, $h(\xi)\le0$ almost surely if and only if $h\le0$ on the support of the law of $\xi$.

Significance

The goal gives the robust problem a KKT system whose multiplier is a nonnegative measure on $\bar D\times\Xi$ that is carried by the points where the constraint is active. Lemmas 3.15 and 3.16 turn this into a scalar multiplier times a probability measure on the active set, and into a convex-hull condition. These are the forms used by semi-infinite programming algorithms and by discretizations that approximate the measure by finitely many atoms. Together with Lemma 3.4, they say when the KKT system of the almost-sure model (§3.1, with its singular multipliers) can be replaced by the measure-valued system of the robust model.

All statements of the mission are proved in the paper, some by reference: Lemma 3.14's proof refers to the argument of Lemma 3.7, and Lemma 3.16 relies on Phelps's barycenter theorem. None of them is formalized. A formal development would also check two points that the page leaves implicit. Lemma 3.15's proof divides by the total mass of $\mu^*$ and does not treat $\mu^*=0$. Condition (68) is printed per direction $h$, while (67a) needs one measure for all $h$.

Difficulty

The necessity direction of the goal needs a Lagrange multiplier theorem in a Banach space whose constraint cone $\hat{\mathcal K}$ has nonempty interior. The multiplier is a priori only an element of $C(\bar D\times\Xi)^*$, and the Riesz–Markov–Kakutani theorem on the compact space $\bar D\times\Xi$ turns it into a measure. The state $\hat{\mathcal S}(u)$ must also be shown to lie in $C(\bar D\times\Xi)$. Continuity of each slice in $x$ is the regularity of Lemma 1.2 (continuity of $H^1_0$ solutions up to the boundary for class-S domains, from Kinderlehrer–Stampacchia), and joint continuity needs the bound (64), uniform in $z$. Working pointwise in $z$ does not give these: a family of continuous slices need not be jointly continuous without an estimate that is uniform in the parameter.

Formalization scope

$\bar D$ and $\Xi$ are subtypes of Euclidean spaces with CompactSpace instances, so $C(\bar D\times\Xi)$ carries its sup norm. Measures on $\bar D\times\Xi$ are Borel measures; on this compact metric space every finite Borel measure is regular, so "regular Borel (Radon) measure" is IsFiniteMeasure, and nonnegativity (66c) is built into Lean's Measure type. The solution operator is a hypothesis: a bounded linear map $L^2(D)\to C(\bar D)$ such that $A^{-1}F$ is, for every $F$, the weak solution in $H^1_0(D)\cap C(\bar D)$, encoded with the published weak-derivative definitions HunterPDE.Shared.WeakDeriv. The page's "$\le0$ in $D\times\Xi$" is encoded on $\bar D\times\Xi$, the same condition for continuous functions. "Solution" means global minimizer over the feasible set. $L^2(D)^*$ is identified with $L^2(D)$ through the Riesz map. In Lemma 3.16 the clco of (68) is the norm closure of the convex hull, which equals the weak closure.

Added hypotheses: $D$ and $\Xi$ nonempty in Lemmas 3.15 and 3.16 (no probability measure exists on an empty set). Pinned reading: (68) is posed as one inclusion $0\in DF(u^*)+\lambda^*\,\overline{\operatorname{co}}\{u_x:(x,z)\in M(u^*)\}$ in $L^2(D)$, where $u_x$ represents $h\mapsto[A^{-1}h](x)$. The page derives (68) from exactly this inclusion. The closed hull is kept because the page's remark that "co" suffices is not proved in infinite dimension.

Several trivializing formalizations are ruled out. The state operator is tied to the PDE and is never an arbitrary map into $C(\bar D\times\Xi)$. The multiplier carries its sign (a nonnegative measure, or $\lambda^*\in\hat{\mathcal K}^-$) together with complementarity. Optimality is global minimality, not a stationarity condition. All integrands are continuous functions on a compact space against finite measures, so no integral takes a junk value.

A complete development needs elliptic regularity in $C(\bar D)$ for class-S domains, a Banach-space Lagrange multiplier theorem under a Robinson-type constraint qualification, the Riesz–Markov–Kakutani theorem for $C(K)^*$ with signed measures (the platform's FamousTheorems.riesz_markov_kakutani covers positive functionals on $C_c$), and barycenters of probability measures on compact convex sets. The last three are reusable beyond this mission. Contributions of proofs for any of them are welcome.

Selected references

• C. Geiersbach, R. Henrion, Optimality conditions in control problems with random state constraints in probabilistic or almost-sure form, arXiv:2306.03965v2, 2024; Math. Oper. Res., 2025. https://arxiv.org/abs/2306.03965
• F. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719451
• R. R. Phelps, Lectures on Choquet's Theorem, 2nd ed., Lecture Notes in Mathematics 1757, Springer, 2001. https://doi.org/10.1007/b76887
• H. W. Alt, Lineare Funktionalanalysis, Springer, 2012. https://doi.org/10.1007/978-3-662-08386-4