Functional Analysis

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

Motivation

Optimal control of partial differential equations under uncertainty asks for a single deterministic control $u$ that performs well when the data of the PDE are random. When a constraint on the state must hold, the modeller has to decide how strictly: with high probability (a probabilistic constraint), for almost every realization (an almost-sure constraint), or for every realization in a support set (a robust constraint). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for all three forms on a common model problem. This mission covers §3.1 of that paper, the almost-sure case.

Almost-sure state constraints are the natural model when a bound (a temperature, a stress, a concentration) must never be violated, and they appear throughout risk-averse PDE-constrained optimization (Geiersbach and Wollner, SIAM J. Optim. 2021; Geiersbach and Hintermüller, ESAIM:COCV 2022). Their difficulty is functional-analytic: the constraint lives in $L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D))$, a space whose dual is not a function space, so Lagrange multipliers are a priori only finitely additive objects.

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$ with $\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$. For $F\in L^2(D)$ the Dirichlet problem $-\Delta y=F$ in $D$, $y=0$ on $\partial D$ has a unique weak solution $y\in H^1_0(D)\cap\mathcal C(\bar D)$; the solution map is a continuous linear operator $A^{-1}:L^2(D)\to\mathcal C(\bar D)$.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $\tilde f\in L^\infty_{\mathbb P}(\Omega,L^2(D))$ a random source. For a control $u\in L^2(D)$ the random state $y(\cdot,\omega)$ solves $-\Delta y(\cdot,\omega)=u+\tilde f(\cdot,\omega)$, $y(\cdot,\omega)=0$ on $\partial D$. With $\mathcal B$ the embedding of $L^2(D)$ into constant elements of $L^\infty_{\mathbb P}(\Omega,L^2(D))$ and $[\mathcal A^{-1}y](\omega)=A^{-1}y(\cdot,\omega)$, the control-to-state operator is $\mathcal S(u)=\mathcal A^{-1}(\mathcal Bu+\tilde f)$ and the constraint map is $\mathcal G(u)=\mathcal S(u)-\boldsymbol\alpha$, where $\boldsymbol\alpha$ is the constant function $\alpha\in\mathbb R$. The problem is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad\mathcal G(u)\in\mathcal K,\qquad(51)$$

with the cone $\mathcal K=\{y\in L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)):y(x,\omega)\le0\text{ on }\bar D,\ \mathbb P\text{-a.s.}\}$ and its polar $\mathcal K^-\subseteq(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$. The cost $F$ is convex and continuously Fréchet differentiable.

For a separable Banach space $X$, a functional $v\in(L^\infty_{\mathbb P}(\Omega,X))^*$ is absolutely continuous if $\langle v,x\rangle=\int_\Omega\langle x^*(\omega),x(\omega)\rangle\,d\mathbb P$ for a weakly measurable $x^*:\Omega\to X^*$ with $\int\|x^*\|\,d\mathbb P<\infty$ (the set $\Lambda_1(X^*)$ of such $x^*$), and singular if it vanishes on every $x$ that vanishes on some $F_n$, for a decreasing sequence of events with $\mathbb P(F_n)\to0$ (the set $\Lambda_\circ(X^*)$).

Formalization targets

Goal: Theorem 3.10

Under the constraint qualification $0\in\operatorname{int}\{\mathcal G(L^2(D))-\mathcal K\}$, $u^*$ solves (51) if and only if there are $\lambda\in\Lambda_1(\mathcal C(\bar D)^*)$, $\lambda^\circ\in\Lambda_\circ(\mathcal C(\bar D)^*)$ and a state $y^*$ with

$$DF(u^*)+\mathbb E[A^{-*}\lambda]+\mathcal B^*\mathcal A^{-*}\lambda^\circ=0,\qquad Ay^*(\cdot,\omega)=u^*+\tilde f(\cdot,\omega),$$ $$y^*(\cdot,\omega)\le\alpha,\quad\lambda(\cdot,\omega)\ge0,\quad\langle\lambda(\cdot,\omega),y^*(\cdot,\omega)-\boldsymbol\alpha\rangle=0\ \ \mathbb P\text{-a.s.},\qquad\lambda^\circ\in\mathcal K^-,\quad\langle\lambda^\circ,y^*-\boldsymbol\alpha\rangle=0.$$

Milestones

1. Lemma 3.6: the random state exists, is a.s. unique, lies in $L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D))$, and obeys the bound (52).
2. Lemma 3.7: the abstract KKT system (53) with a multiplier $\lambda^*\in(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$.
3. Theorem 3.9 (Ioffe–Levin): every $v^*\in(L^\infty_{\mathbb P}(\Omega,X))^*$ splits uniquely as $v^a+v^\circ$ with $\|v^*\|=\|v^a\|+\|v^\circ\|$.
4. The splitting $\langle\lambda^*,\mathcal A^{-1}\mathcal Bh\rangle=\mathbb E[\langle\lambda,A^{-1}h\rangle]+\langle\lambda^\circ,\mathcal A^{-1}\mathcal Bh\rangle$.
5. (57): $\lambda^*\in\mathcal K^-$ passes to both parts.
6. (59) and pointwise complementarity: $\lambda(\omega)\ge0$ and $\langle\lambda(\omega),y^*(\omega)-\boldsymbol\alpha\rangle=0$ almost surely.

Significance

The result. Lemma 3.7 gives a multiplier in the dual of $L^\infty$, which cannot be evaluated scenario by scenario. Theorem 3.10 shows that, for this problem, the multiplier consists of an honest random variable $\lambda(\omega)\in\mathcal C(\bar D)^*$ (a random signed measure on $\bar D$) satisfying sign and complementarity conditions for almost every realization, plus a singular remainder. This is the form needed to write adjoint equations and to design discretizations and algorithms (Proposition 3.12 of the paper). As Remark 3.11 notes, the derivation does not require reflexivity of the state space, unlike earlier work on $L^\infty_{\mathbb P}(\Omega,X)$-constraints.

Formalizing it. The paper's argument is complete, but it rests on two cited results: the regularity theory behind Lemma 1.2/3.6 (Stampacchia-type continuity of weak solutions on class-S domains, Kinderlehrer–Stampacchia) and the Ioffe–Levin decomposition of $(L^\infty_{\mathbb P}(\Omega,X))^*$ (Ioffe–Levin, Appendix 1, Theorem 3, and Levin 1974). Neither is in Mathlib. A formal development produces machine-checked versions of both, of a Robinson-type KKT theorem in Banach spaces, and of the multiplier refinement itself. None of these results has a machine-checked proof as far as the platform's catalog shows.

Difficulty

The obvious route is to apply the Riesz representation pointwise in $\omega$. It fails: $(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$ contains purely finitely additive functionals that are not given by any integrand, so $\lambda^*$ has no density in general. The decomposition theorem isolates them, and the proof of Theorem 3.10 must then show that the sign condition $\lambda^*\in\mathcal K^-$ and the complementarity condition pass to each part separately. The step from $\mathbb E[\langle\lambda,y\rangle]\le0$ for all $y\in\mathcal K$ to "$\lambda(\omega)\ge0$ for almost every $\omega$, simultaneously for all nonnegative test functions" requires the separability of $\mathcal C(\bar D)$; a version with a null set depending on the test function is weaker and is not the statement. Lemma 3.6 needs $\mathcal C(\bar D)$-regularity of weak solutions, which is where class S and $d\le3$ enter.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $L^2(D)$ is Lp ℝ 2 (volume.restrict D) and $L^\infty_{\mathbb P}(\Omega,X)$ is Lp X ⊤ P; their elements are a.e. classes, so every pointwise statement in $\omega$ is stated $\mathbb P$-a.s. $\mathcal C(\bar D)$ is C(closure D, ℝ) with [CompactSpace (closure D)] as an instance argument (implied by boundedness). Weak derivatives use the published HunterPDE.Shared.HasWeakDeriv; a weak solution in $H^1_0(D)\cap\mathcal C(\bar D)$ is encoded as continuity on $\bar D$, zero boundary values, $L^2$ weak gradient and the weak form. $A^{-1}$ is a hypothesis: a continuous linear map $L^2(D)\to\mathcal C(\bar D)$ whose values are weak solutions. "$\le0$ a.e. in $D$" for a function continuous on $\bar D$ is read as "$\le0$ on $\bar D$"; "$\lambda(\cdot,\omega)\ge0$" as positivity of the functional. "Solution of (51)" is a global minimizer. (56a) is stated applied to every direction $h$.

Trivializing formalizations are ruled out: the state operator is tied to the PDE, not an arbitrary bounded operator; the multipliers carry their sign and complementarity conditions; absolutely continuous functionals require a weakly measurable, integrable density; singular functionals are concentrated on a decreasing sequence of events of vanishing probability, not merely "not absolutely continuous"; optimality is global.

Needed infrastructure: Lax–Milgram on $H^1_0(D)$ and continuity of weak solutions (Lemma 3.6); a KKT theorem under Robinson's constraint qualification (Lemma 3.7); the Yosida–Hewitt decomposition for finitely additive measures and a weak*-measurable representation of $L^1(\Omega,X)^*$ (Theorem 3.9). The decomposition theorem is reusable far beyond this mission; contributions toward any of these 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
• A. D. Ioffe, V. L. Levin, Subdifferentials of convex functions, Trudy Moskov. Mat. Obshch. 26, 3–73, 1972 (Appendix 1, Theorem 3).
• V. L. Levin, The Lebesgue decomposition for functionals on the vector-function space $L^\infty_X$, Funct. Anal. Appl. 8(4), 314–317, 1974. https://doi.org/10.1007/bf01075488
• K. Yosida, E. Hewitt, Finitely additive measures, Trans. Amer. Math. Soc. 72, 1952. https://doi.org/10.1090/S0002-9947-1952-0045194-X
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• C. Geiersbach, W. Wollner, Optimality conditions for convex stochastic optimization problems in Banach spaces with almost sure state constraints, SIAM J. Optim. 31(4), 2455–2480, 2021.
• C. Geiersbach, M. Hintermüller, Optimality conditions and Moreau–Yosida regularization for almost sure state constraints, ESAIM: COCV 28, Paper No. 80, 2022. https://doi.org/10.1051/cocv/2022070
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (Chapter II, Appendices B and C). https://doi.org/10.1137/1.9780898719451

Motivation

Hemivariational inequalities were introduced by Panagiotopoulos in the 1980s to model mechanical problems whose energy functional is neither convex nor smooth: nonmonotone friction, adhesion, delamination and unilateral contact with nonmonotone multivalued laws. Where a variational inequality expresses the optimality condition of a convex energy, a hemivariational inequality expresses a stationarity condition of a locally Lipschitz energy through Clarke's generalized directional derivative. When in addition the admissible set depends on the unknown state, as in contact problems with a solution-dependent gap or in Nash-type equilibrium problems with coupled constraints, the problem becomes a quasi-hemivariational inequality.

Zeng, Migórski and Khan (SIAM J. Control Optim. 59 (2021)) treat a general form of this problem that contains a multivalued operator $T$, a bifunction $\varphi$ and a constraint map $K$ at once. Their existence theorem for it, Theorem 3.8, is the base of an optimal control result (Section 4) and of an application to a frictional contact problem in elasticity (Section 5). This mission formalizes the existence part, Sections 2 and 3 of the paper.

Setting

Let $V$ be a real reflexive Banach space with dual $V^*$ and pairing $\langle\cdot,\cdot\rangle$, and let $X$, $Y$ be real Banach spaces. The data are: a nonempty closed convex set $C\subseteq V$; a multivalued constraint map $K:C\to2^C$; a multivalued operator $T:C\to2^{V^*}$; a function $\varphi:V\times V\to\mathbb R$; a locally Lipschitz functional $J:X\to\mathbb R$; bounded linear operators $\gamma:V\to X$ and $\pi:V\to Y$; a functional $f\in Y^*$; and an auxiliary function $h:V\to\mathbb R$.

For a locally Lipschitz $J$, the Clarke generalized directional derivative and the generalized gradient are

$$J^0(u;v)=\limsup_{\lambda\to0^+,\ w\to u}\frac{J(w+\lambda v)-J(w)}{\lambda},\qquad \partial J(u)=\{\xi\in X^*:\ J^0(u;v)\ge\langle\xi,v\rangle\ \forall v\in X\}.$$

Problem 1.1 asks for $u\in C$ and $u^*\in T(u)$ such that $u\in K(u)$ and

$$\langle u^*,v-u\rangle+\varphi(v,u)+J^0(\gamma u;\gamma(v-u))\ge\langle f,\pi(v-u)\rangle_{Y^*\times Y}\quad\text{for all }v\in K(u).$$

Its solution set is $\Gamma(f)$. Fixing the constraint set gives Problem 3.3: find $u\in C$ and $u^*\in T(u)$ with the same inequality for all $v\in C$; its solution set is $\mathrm{SOL}(C;T,J,\varphi,f)$. The variational selection $S:C\to2^C$ maps $w\in C$ to the solution set of Problem 3.3 with $C$ replaced by $K(w)$; its fixed points are exactly the solutions of Problem 1.1.

The hypotheses of the paper (p. 1250) are: $T$ has nonempty, compact, convex values and is upper semicontinuous; $T(\cdot)+\gamma^*\partial J(\gamma\,\cdot)$ is $(\varphi,h)$-stably pseudomonotone with respect to $\pi^*f$, where $\limsup_{t\to0^+}h(tu)/t\ge0$ and $h$ is weakly sequentially upper semicontinuous in the limsup sense (3.1); $\varphi$ is convex and l.s.c. in its first argument, concave and u.s.c. in its second, and vanishes on the diagonal; $K$ has nonempty closed convex values and satisfies two Mosco-type conditions (HK); a bounded set $C_0$ meets every $K(u)$ and, if $C$ is unbounded, a coercivity condition (3.2) holds at each point of $C_0$. Theorem 3.8 adds that $\gamma$ is compact, $h$ is convex, and $\limsup_n\varphi(v_n,u_n)\le\varphi(v,u)$ whenever $v_n\to v$ strongly and $u_n\rightharpoonup u$ weakly (3.19).

Formalization targets

Goal: Theorem 3.8 (ii)

Under all hypotheses of Theorem 3.8,

$$\Gamma(f)\neq\emptyset,\qquad \Gamma(f)\ \text{is bounded},\qquad \Gamma(f)\ \text{is weakly closed in }V.$$

Milestones

1. Proposition 2.5 (i)–(iii): $J^0(x;\cdot)$ is sublinear, $J^0(x;v)=\max\{\langle\xi,v\rangle:\xi\in\partial J(x)\}$, and $(u,v)\mapsto J^0(u;v)$ is upper semicontinuous.
2. Theorem 2.7 (Kluge): a multivalued self-map of a nonempty closed convex subset of a reflexive Banach space, with nonempty closed convex values and a sequentially weakly closed graph, has a fixed point if its domain or its range is bounded.
3. Theorem 3.4 (i)–(iii): for Problem 3.3, the Minty-type characterization

$$\langle v^*,v-u\rangle+\varphi(v,u)+\langle\eta_v,\gamma(v-u)\rangle\ge\langle f,\pi(v-u)\rangle+h(v-u)\quad\forall v\in C,\ v^*\in T(v),\ \eta_v\in\partial J(\gamma v);$$

nonemptiness, boundedness and weak closedness of $\mathrm{SOL}(C;T,J,\varphi,f)$; and its convexity when $h$ is convex. 4. Theorem 3.8 (i): the same characterization for Problem 1.1, with $C$ replaced by $K(u)$. 5. Two claims from the proof of Theorem 3.8 (ii): the graph of $S$ is sequentially weakly closed, and $S(C)=\bigcup_{w\in C}S(w)$ is bounded.

Significance

Theorem 3.8 is the existence result on which the rest of the paper rests: the optimal control problem of Section 4 minimizes $F(f)=\inf_{u\in\Gamma(f)}g(u,f)$ over $f\in Y^*$, and Section 5 casts an approximate static elastic contact model, with a multivalued normal compliance condition and a frictional law with slip-dependent friction coefficient, in the form of Problem 1.1 on a space of displacements. The theorem unifies several existence results for variational, hemivariational and quasi-variational inequalities: for single-valued $T$, $J=0$, $\pi=\mathrm{id}$, $h=0$ and $\varphi(v,u)=\phi(v)-\phi(u)$, its Corollary 3.9 reduces to an earlier existence result for quasi-variational inequalities (Remark 3.10), and Theorem 3.4 removes the compactness of $\gamma$ required in earlier work (Remark 3.6).

The results are proved in the paper. None of them, nor Clarke's calculus on a Banach space, nor Kluge's fixed point theorem, has a machine-checked proof to our knowledge. A formalization adds a checked version of a proof that combines a KKM-type fixed point theorem, Minty's trick for pseudomonotone multivalued operators, and a fixed point argument for the variational selection.

Difficulty

The obvious route to Problem 1.1 is to fix $w$, solve the inequality on $K(w)$, and take a fixed point of the solution map. Two steps resist. First, the solution map is multivalued and its values are only weakly closed, so a Schauder- or Kakutani-type theorem in the norm topology does not apply; the fixed point theorem must work with sequentially weakly closed graphs, and the graph closedness of $S$ has to be proved by passing to the limit in inequalities in which $u_n$ converges only weakly while the test points $v_n\in K(w_n)$ must converge strongly. That passage uses the compactness of $\gamma$, the upper semicontinuity of $J^0$, condition (3.19) and the Mosco-type conditions together. Second, in the "there exists $u^*\in T(u)$" form of the problem the inequality is not stable under weak limits in $u$, which is why the Minty reformulation and the stable pseudomonotonicity with the auxiliary function $h$ are needed.

Formalization scope

All spaces are real normed spaces with CompleteSpace; $V^*$ is V →L[ℝ] ℝ with the operator-norm topology; reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ V. No inner product and no finite dimension is assumed. Multivalued maps are total functions V → Set _, constrained on $C$ only. Weak convergence $x_n\rightharpoonup x$ means $\ell(x_n)\to\ell(x)$ for every $\ell\in V^*$; "weakly closed" is sequential weak closedness, which for the bounded sets $\Gamma(f)$ and $\mathrm{SOL}$ in a reflexive space agrees with weak closedness. Adjoints are composition: $\langle\gamma^*\eta,w\rangle=\eta(\gamma w)$, $\langle\pi^*f,w\rangle=f(\pi w)$. $J^0$ is a real Filter.limsup and is used only under LocallyLipschitz J. Every $\limsup$, infimum and limit in the hypotheses ($\limsup_{t\to0^+}h(tu)/t\ge0$, (3.1), (3.2), (3.19)) is written with explicit $\varepsilon$–$N$ quantifiers, so no default value of a real $\limsup$ or $\inf$ can make a hypothesis vacuous.

Four corrections to the printed hypotheses are built in and stated in each item's note: the pairing in (3.2) is $\langle\eta_u,\gamma(u-v_0)\rangle$ (the page's $\langle\eta_u,u-v_0\rangle$ does not typecheck); $T(u)$ is nonempty for $u\in C$; the condition (3.2) assumed in Theorem 3.4 refers to a bounded set $C_0$ that meets $C$; and for Theorem 3.8 (ii) and the boundedness of $S(C)$, (3.2) in (HC0) holds uniformly in $v_0\in C_0$ (one $R$ for each $M$), which is what the proof on pp. 1260–1261 uses. With (3.2) only at each fixed $v_0\in C_0$, as printed, $\Gamma(f)$ can be unbounded; the counterexample is in the note of Theorem 3.8 (ii). Theorem 3.8 (i) and the graph-closedness of $S$ keep (HC0) as printed. A formalization in which $T$ may have empty values, $C_0$ may be empty or disjoint from $C$, $V$ is a Hilbert or finite-dimensional space, a real $\limsup$ default value makes the conditions on $h$ or (3.19) vacuous, or "bounded" or "weakly closed" is dropped from the conclusion, would be a different and weaker theorem.

The development needs Clarke's calculus on a Banach space (Proposition 2.5, which relies on the Hahn–Banach theorem), Eberlein–Šmulian or Kakutani's theorem on weak compactness of bounded closed convex sets in reflexive spaces, Mazur's lemma, a KKM-type fixed point theorem in Hausdorff topological vector spaces, and Kluge's fixed point theorem. These pieces are reusable beyond this mission: Clarke's calculus for every nonsmooth optimization statement on Banach spaces, and the fixed point theorems for variational and quasi-variational inequalities in general. Contributions of any of them, of alternative proofs, and of proofs of the milestones in any order are welcome.

Selected references

• S. Zeng, S. Migórski, A. A. Khan, Nonlinear quasi-hemivariational inequalities: existence and optimal control, SIAM J. Control Optim. 59(2) (2021) 1246–1274. https://doi.org/10.1137/19M1282210
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; reprinted SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309
• R. Kluge, Nichtlineare Variationsungleichungen und Extremalaufgaben, VEB Deutscher Verlag der Wissenschaften, Berlin, 1979.
• S. Migórski, A. Ochal, M. Sofonea, Nonlinear Inclusions and Hemivariational Inequalities, Springer, 2013. https://doi.org/10.1007/978-1-4614-4232-5
• P. D. Panagiotopoulos, Hemivariational Inequalities: Applications in Mechanics and Engineering, Springer, 1993. https://doi.org/10.1007/978-3-642-51677-1