Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

9 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record≤ 70Open frontier

3 provers on it7 of 8 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

9 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record≤ 70Open frontier

3 provers on it7 of 8 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Machine Learning Probability Statistics·Captain: mikedeng1

Distribution-Free, Risk-Controlling Prediction Sets I: Upper Confidence Bound Calibration Selects a λ̂ Whose Risk Is at Most α with Probability at Least 1 − δ (Theorem 1)Research Paper

Motivation

A trained classifier or regressor returns a point prediction, but many uses of machine learning need a prediction set: a set of plausible labels together with a guarantee about how often, or how badly, it misses the truth. Medical imaging, protein structure prediction and multi-label classification are examples where a user wants a set whose expected loss is bounded, not just a best guess. Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 68(6), 2021) give a procedure that wraps any black-box predictor and returns sets whose risk is controlled, with no assumption on the data distribution beyond i.i.d. calibration data.

The procedure generalizes split conformal prediction (Vovk, Gammerman and Shafer, 2005) and the tolerance regions of Wilks (1941), which control only the probability of missing the label, to an arbitrary monotone loss on sets (false-negative rate, coverage of a segmentation mask, a hierarchical loss). This mission formalizes its central guarantee, Theorem 1 (p. 5), together with the abstract form Theorem A.1 (p. 26) from which the paper derives it.

Setting

Let $(X, Y)$ be a random pair in $\mathcal X \times \mathcal Y$ with law $P$ , and let $\mathcal Z$ be a set of labels. A set-valued predictor is a map $\mathcal T : \mathcal X \to 2^{\mathcal Z}$ . The paper considers a family $\{\mathcal T_\lambda\}_{\lambda \in \Lambda}$ indexed by a closed set $\Lambda \subseteq \mathbb R \cup \{\pm\infty\}$ that is nested:

\lambda_1 < \lambda_2 \implies \mathcal T_{\lambda_1}(x) \subseteq \mathcal T_{\lambda_2}(x). \tag{1}

A loss on sets $L(y, S) \ge 0$ is required to decrease as the set grows:

S \subseteq S' \implies L(y, S) \ge L(y, S'). \tag{2}

The risk of $\mathcal T_\lambda$ is $R(\lambda) = \mathbb E[L(Y, \mathcal T_\lambda(X))]$ , and the section assumes some $\lambda_{\max} \in \Lambda$ with $R(\lambda_{\max}) = 0$ .

A risk-controlling prediction set at levels $(\alpha, \delta)$ (Definition 1, p. 2) is a data-dependent predictor $\mathcal T$ with $R(\mathcal T) \le \alpha$ with probability at least $1 - \delta$ .

Given an i.i.d. calibration sample $D = ((X_1, Y_1), \dots, (X_n, Y_n))$ , a pointwise upper confidence bound is a function $\widehat R^+(\lambda) = \widehat R^+(D, \lambda)$ with

P\big(R(\lambda) \le \widehat R^+(\lambda)\big) \ge 1 - \delta \quad \text{for each fixed } \lambda. \tag{3}

UCB calibration selects

\hat\lambda = \inf\big\{\lambda \in \Lambda : \widehat R^+(\lambda') < \alpha \ \ \forall \lambda' \in \Lambda,\ \lambda' \ge \lambda\big\}. \tag{4}

In Lean, the risk is RiskControl.UCB.risk P L T lam, the calibration set of (4) for one realization r of $\widehat R^+$ is calSet Λ r α, and $\hat\lambda$ is lambdaHat Λ r α.

Formalization targets

Goal: Theorem 1 (p. 5)

In the setting above, if (3) holds for every $\lambda \in \Lambda$ and $R$ is continuous on $\Lambda$ , then

P^n\big(R(\mathcal T_{\hat\lambda}) \le \alpha\big) \ge 1 - \delta .

Nothing is assumed of $\widehat R^+$ beyond (3); $\alpha$ and $\delta$ are arbitrary reals.

Milestones

Monotone risk (§2.1, pp. 4–5): (1) and (2) make $R$ nonincreasing on $\Lambda$ .
The failure point (proof of Theorem A.1, p. 26, corrected): $\lambda^\dagger = \sup\{\lambda \in \Lambda : R(\lambda) > \alpha\}$ lies in $\Lambda$ and $R(\lambda^\dagger) \ge \alpha$ .
Failure implies a low bound at $\lambda^\dagger$ (p. 26, corrected): deterministically, $R(\hat\lambda) > \alpha$ implies $\widehat R^+(\lambda^\dagger) < \alpha$ .
Theorem A.1 (p. 26): for any continuous nonincreasing $R : \Lambda \to \mathbb R$ and any $\widehat R^+$ satisfying (3) on an abstract probability space, $P(R(\hat\lambda) \le \alpha) \ge 1 - \delta$ .

Significance

Theorem 1 turns a confidence bound for one fixed parameter into a guarantee for a parameter chosen from the data. No uniform convergence over $\Lambda$ is needed, so any concentration inequality for a mean (Hoeffding, Bentkus, the betting bound of Waudby-Smith and Ramdas) yields a calibration procedure immediately; the paper's Theorems 2–5 and 9–10 are of exactly this form, and the later Learn-then-Test and conformal risk control frameworks build on the same template.

The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked version of an argument whose printed form has a gap. The printed proof of Theorem A.1 introduces $\lambda^* = \inf\{\lambda \in \Lambda : R(\lambda) \le \alpha\}$ and asserts $R(\lambda^*) = \alpha$ "by continuity", which is false when $\Lambda$ is not an interval. Finite grids, the usual choice of $\Lambda$ in practice, are not intervals. The theorem remains true, and milestones 2 and 3 state the corrected steps. No formalization of risk-controlling prediction sets or of conformal prediction is known to exist in Lean or on this platform.

Difficulty

The obvious argument applies the confidence bound at $\hat\lambda$ ; that fails because $\hat\lambda$ depends on the data, so (3) says nothing at $\lambda = \hat\lambda$ . The proof must find one deterministic point at which a failure of calibration forces a failure of (3). The paper's choice $\lambda^*$ works only when $R$ attains the value $\alpha$ on $\Lambda$ ; on $\Lambda = \{0, 1\}$ with $R(0) = 1$ , $R(1) = 0$ , $\alpha = 1/2$ and the exact bound $\widehat R^+ = R$ , the event $\{\widehat R^+(\lambda^*) < \alpha\}$ has probability one, so the printed last step does not bound anything. The second difficulty is boundary behaviour: $\Lambda$ may contain $\pm\infty$ , the infimum in (4) may be over an empty set, and the calibration set need not contain its own infimum.

Formalization scope

$\Lambda$ is a closed subset of EReal (the extended reals with the order topology); $\lambda$ is only compared, never added. Continuity of $R$ is in the subspace topology of $\Lambda$ .
Set-valued predictions are Set 𝒵, i.e. $\mathcal Y' = 2^{\mathcal Z}$ (the paper uses $2^{\mathcal Y}$ for most of its examples).
The risk is the published definition WassersteinDRO.Duality.nominalRisk, a Bochner integral. Because a non-integrable integrand integrates to $0$ in Lean, Theorem 1 assumes $(x, y) \mapsto L(y, \mathcal T_\lambda(x))$ is $P$ -integrable for every $\lambda \in \Lambda$ .
The standing assumptions of §2.1 are hypotheses of Theorem 1: $\Lambda$ closed, (1) on $\Lambda$ , (2), $L \ge 0$ , and $R(\lambda_{\max}) = 0$ for some $\lambda_{\max} \in \Lambda$ . The monotonicity of $R$ is not assumed in Theorem 1; it is milestone 1. Theorem A.1 assumes it, as printed.
The i.i.d. sample is Fin n → 𝒳 × 𝒴 under the product measure $P^n$ . $\widehat R^+$ is an arbitrary real function of the sample and of $\lambda$ ; an infinite bound is represented by any value $\ge \alpha$ .
"With probability at least $1 - \delta$ " is written as a failure probability at most $\delta$ , measured as an outer measure; no measurability of $\widehat R^+$ or $\hat\lambda$ is assumed. For a measurable event this is the page's statement.
$\hat\lambda$ is an infimum in EReal, so $\inf \emptyset = +\infty$ as on the page. Since $+\infty$ need not belong to $\Lambda$ , the failure event is "the set in (4) is nonempty and $R(\hat\lambda) > \alpha$ "; when the set is nonempty, $\hat\lambda \in \Lambda$ . When it is empty the procedure certifies nothing, and the natural output is $\mathcal T_{\lambda_{\max}}$ , of risk $0$ .
Corrections of the print: Theorem A.1's conclusion reads $P(R(\lambda) \le \alpha)$ , stated here with $\hat\lambda$ ; the proof's point $\lambda^*$ and the claim $R(\lambda^*) = \alpha$ are replaced by $\lambda^\dagger = \sup\{\lambda \in \Lambda : R(\lambda) > \alpha\}$ and $R(\lambda^\dagger) \ge \alpha$ , which coincide with the page for an interval $\Lambda$ .
A formalization that assumes $R$ monotone in Theorem 1, quantifies over $\widehat R^+$ inside the event, takes a real-valued infimum (which is $0$ on unbounded sets) or drops the integrability guard would state a different theorem; the statement here does none of these.

Needed infrastructure is small: closed subsets of EReal and their infima and suprema (IsClosed.sInf_mem, IsClosed.sSup_mem), continuity within a set, monotonicity of the Bochner integral, and monotonicity of outer measure. Proofs of the milestones are welcome individually; the deterministic milestones 2 and 3 are reusable for every UCB-calibration theorem of the paper.

Selected references

S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, J. ACM 68(6), 2021; arXiv:2101.02703v3. https://arxiv.org/abs/2101.02703
V. Vovk, A. Gammerman, G. Shafer, Algorithmic Learning in a Random World, Springer, 2005. https://doi.org/10.1007/b106715
S. S. Wilks, Determination of sample sizes for setting tolerance limits, Ann. Math. Statist. 12(1), 1941. https://doi.org/10.1214/aoms/1177731788
I. Waudby-Smith, A. Ramdas, Estimating means of bounded random variables by betting, arXiv:2010.09686, 2020. https://arxiv.org/abs/2010.09686

7 thms1 active userReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Turán Graphs with Bounded Matching Number 2: For Color-Critical H of Chromatic Number k+1 > 2, Large s and n ≫ s, H-Free Graphs with Matching Number at Most s Have at Most g(n,k,s) EdgesResearch Paper

Motivation

Two classical extremal results bound the number of edges of an $n$ -vertex graph under a single restriction. Turán's theorem (1941) says that a graph with no clique on $k+1$ vertices has at most $t(n,k)$ edges, the edge count of the balanced complete $k$ -partite graph. The Erdős–Gallai theorem (1959) gives the maximum number of edges of an $n$ -vertex graph whose largest matching has at most $s$ edges. N. Alon and P. Frankl, Turán graphs with bounded matching number (arXiv:2210.15076v1; J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002), combine the two restrictions. Their Theorem 1.1 determines the maximum for the clique constraint and every $n\ge 2s+1$ (mission 1 of this series). Their Proposition 3.1, the goal here, treats a whole class of forbidden graphs, the color-critical ones, when $s$ is large in terms of the forbidden graph and $n$ is large in terms of $s$ .

Color-critical graphs are the natural class for exact Turán results: by a theorem of M. Simonovits (1968), for a color-critical $H$ of chromatic number $k+1$ the Turán graph $T(N,k)$ is extremal for $H$ -freeness once $N$ is large. Proposition 3.1 is the analogue of Simonovits' theorem under a matching constraint.

Setting

All graphs are finite and simple. For a graph $G$ , a matching is a set of pairwise disjoint edges, and the matching number $\nu(G)$ is the largest size of a matching. For a graph $H$ , $G$ is $H$ -free if it contains no subgraph (not necessarily induced) isomorphic to $H$ . The chromatic number $\chi(H)$ is the least number of colors in a proper vertex coloring. $H$ is color-critical if it has an edge $e$ with $\chi(H-e)<\chi(H)$ ; examples are complete graphs and odd cycles.

The Turán graph $T(n,k)$ is the complete $k$ -partite graph on $n$ vertices with classes of sizes as equal as possible; $t(n,k)$ is its number of edges. For $k\ge 2$ and $2s\le n$ , the graph $G(n,k,s)$ is the complete $k$ -partite graph on $n$ vertices consisting of $k-1$ classes of sizes as equal as possible whose total size is $s$ , and one further class of size $n-s$ . Its number of edges is $g(n,k,s)$ .

In the Lean development, vertices of $G$ are Fin n; the shared objects of this series live in TuranMatching.Clique.Setting: $\nu$ is matchingNumber, $t(n,k)$ is turanNum n k (Mathlib's turanGraph), $G(n,k,s)$ is bigGraph n k s, $g(n,k,s)$ is gNum n k s, color-criticality is IsColorCritical, and the set $X$ of vertices of degree exceeding $2s$ is highDeg G s.

Formalization targets

Goal: Proposition 3.1 (p. 5)

There is $n_0:\mathbb N\to\mathbb N$ such that for every color-critical $H$ with $\chi(H)=k+1>2$ there is $s_0(H)$ with: for all $s>s_0(H)$ and $n>n_0(s)$ ,

\max\{|E(G)| : |V(G)|=n,\ G\ H\text{-free},\ \nu(G)\le s\}=g(n,k,s).

The maximum is stated as an upper bound for every admissible $G$ together with an admissible graph attaining $g(n,k,s)$ . The thresholds $s_0$ and $n_0$ are left existential, as on the page.

Milestones (pp. 5–6)

$G(n,k,s)$ is $k$ -colorable, $H$ -free for every $H$ with $\chi(H)=k+1$ , and $\nu(G(n,k,s))=s$ (for $2s\le n$ ).
If $\nu(G)\le s$ then at most $s$ vertices have degree exceeding $2s$ : $|X|\le s$ .
If every degree is at most $2s$ and $\nu(G)\le s$ , then $|E(G)|\le(2s+1)s$ .
If $\nu(G)\le s$ and $|X|<s$ , then $|E(G)|<(s-1)n+2(s+1)s$ .
$(s-1)n+2(s+1)s<g(n,k,s)$ for $n>3s^2+2s$ .
If $\nu(G)\le s$ and $|X|=s$ , then $V-X$ is independent.
Simonovits' theorem: an $H$ -free graph on $N\ge N_0(H)$ vertices has at most $t(N,k)$ edges.
If $|X|=s$ , $V-X$ is independent, $Z$ is disjoint from $X$ with $|Z|=\lfloor s/(k-1)\rfloor$ and $G[X\cup Z]$ has at most $t(s+\lfloor s/(k-1)\rfloor,k)$ edges, then $|E(G)|\le g(n,k,s)$ .

Significance

The proposition settles, for every color-critical $H$ and large parameters, the Turán problem with a bounded matching number, and identifies the extremal graph $G(n,k,s)$ , which does not depend on $H$ beyond its chromatic number. For $H=K_{k+1}$ it agrees with the large- $n$ case of Theorem 1.1 of the same paper. The structural steps (few high-degree vertices, the independence of the low-degree side) are reusable in other degree-based arguments under matching constraints.

The result is proved in the paper; none of it is formalized. The mission produces, besides the goal, two classical theorems absent from Mathlib in the forms needed here: the matching-number consequence of Vizing's theorem (milestone 3) and Simonovits' exact Turán theorem for color-critical graphs (milestone 7). Milestone 7 is a cited classical theorem, not a result of Alon and Frankl; it is posed because the proof rests on it. Mathlib currently has Turán's theorem for cliques and the Erdős–Stone–Simonovits density theorem, but not the exact result for color-critical graphs.

Difficulty

Milestones 1, 2, 4, 5, 6 and 8 are elementary counting arguments, though each requires building matchings or explicit counts in Lean. Milestone 8 contains the paper's "easy to see" isomorphism, which in Lean is an identity between two edge counts, $t(s+m,k)+(n-s-m)s=g(n,k,s)$ with $m=\lfloor s/(k-1)\rfloor$ .

Milestone 3 needs Vizing's edge-coloring theorem (a graph of maximum degree $\Delta$ is properly $(\Delta+1)$ -edge-colorable). A naive greedy edge coloring gives only $2\Delta-1$ colors, which bounds the edge count by about $(4s-1)s$ and is too weak for the comparison in milestones 4 and 5.

Milestone 7 is the hardest item. The density version (Erdős–Stone–Simonovits) gives $t(N,k)+o(N^2)$ edges only; the exact bound for color-critical $H$ requires Simonovits' stability method, an argument that an almost-extremal $H$ -free graph is close to $T(N,k)$ followed by a cleaning step that uses the critical edge.

Formalization scope

Graphs are SimpleGraph (Fin n) with decidable adjacency; edges are counted by #G.edgeFinset. The matching number is the supremum, in $\mathbb N$ , of the edge counts of matching subgraphs; the set is nonempty and bounded, so this is the true maximum and not a junk value. $g(n,k,s)$ is defined as the edge count of the graph $G(n,k,s)$ , not by a closed formula. Chromatic numbers live in $\mathbb N\cup\{\infty\}$ (Mathlib's chromaticNumber), both in the definition of color-critical and in the hypothesis $\chi(H)=k+1$ . $H$ -freeness is Mathlib's SimpleGraph.Free (no subgraph copy). The vertex type of $H$ is any finite type in the lowest universe.

Conventions committed to:

$k\ge 2$ is the page's $k+1>2$ ; it is needed because $G(n,k,s)$ has $k-1$ classes and the proof divides by $k-1$ .
Quantifier order is the page's: $n_0$ is a function of $s$ alone and is chosen before $H$ ; $s_0$ depends on $H$ only.
Milestone 1 states $k$ -colorability for the page's " $k$ chromatic", and carries $2s\le n$ , which the page leaves implicit.
Milestone 3 bounds edges where the page writes "the number of vertices"; the vertex count is not bounded.
Milestone 5 uses the threshold $n>3s^2+2s$ . The page's " $n$ exceeding, say, $3s^2$ " is too small: for $k=2$ , $s=2$ , $n=13$ one has $(s-1)n+2(s+1)s=25>22=g(13,2,2)$ . The goal is unaffected, since $n_0(s)$ is unspecified.
Milestone 4 carries $s\ge 1$ so that $s-1$ is honest natural-number subtraction.

A formalization that states only the upper bound, without an attaining graph, or that places the existential $n_0$ after $s$ is fixed as a constant independent of $s$ , or that defines $\nu$ or $g$ so that they take junk values, is a different and weaker statement and is ruled out.

Infrastructure that would be reusable beyond this mission: a matching-number API on Mathlib's Subgraph.IsMatching (in particular $\nu(G)\le\nu(G')$ for $G\le G'$ and the behaviour under induced subgraphs); Vizing's theorem; and Simonovits' theorem. Contributions of any of these, and of partial results toward milestone 7 (for example the case $H=C_{2\ell+1}$ ), are welcome.

Selected references

N. Alon and P. Frankl, Turán graphs with bounded matching number, arXiv:2210.15076v1, 2022; J. Combin. Theory Ser. B, 2024. https://arxiv.org/abs/2210.15076, https://doi.org/10.1016/j.jctb.2023.12.002
M. Simonovits, A method for solving extremal problems in graph theory, stability problems, in: Theory of Graphs (Proc. Colloq., Tihany, 1966), Academic Press, 1968, pp. 279–319.
P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959), 337–356. https://doi.org/10.1007/BF02024498
P. Turán, On an extremal problem in graph theory (in Hungarian), Mat. Fiz. Lapok 48 (1941), 436–452.
V. G. Vizing, On an estimate of the chromatic class of a p-graph, Diskret. Analiz 3 (1964), 25–30.

11 thms1 active userReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Competitive Equilibrium with Indivisible Goods and Generic Budgets 1: Two Additive Agents with Almost Equal but Unequal Budgets Have a Competitive Equilibrium Giving Each Agent Her Truncated ShareResearch Paper

Motivation

Many allocation problems divide indivisible goods among agents who are entitled to different shares but cannot pay with real money: course seats among students, shifts among workers, inherited items among heirs. A standard mechanism gives each agent a budget of artificial currency and lets a market run. When budgets are equal this is the competitive equilibrium from equal incomes (CEEI) of Varian (1974), the basis of the course-allocation mechanism of Budish (2011). With indivisible items, however, an equilibrium can fail to exist: one item and two agents with equal budgets already admit none, because whoever does not get the item could afford it at any price the owner can pay.

Babaioff, Nisan and Talgam-Cohen (arXiv 2017; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) ask whether this failure is robust or a knife edge, and answer for two agents with additive preferences: an arbitrarily small, strict inequality between the budgets restores existence. Budish's approximate CEEI perturbs budgets randomly for the same reason; this mission formalizes the exact two-agent result.

Setting

A discrete Fisher market has a set $M$ of $m$ indivisible items and two agents. Agent $i$ has a valuation $v_i$ assigning a real value to every bundle $S\subseteq M$ , and a budget $b_i>0$ . Valuations are additive ( $v_i(S)=\sum_{j\in S}v_i(\{j\})$ ), normalized ( $v_i(M)=1$ ), non-negative, monotone ( $v_i(S)<v_i(T)$ when $S\subsetneq T$ ) and strict (different bundles have different values). Budgets are normalized, $b_1+b_2=1$ ; money has no value to the agents.

An allocation $\mathcal S=(\mathcal S_1,\mathcal S_2)$ is a partition of all items between the agents. Item prices $p_j\ge 0$ give bundle prices $p(S)=\sum_{j\in S}p_j$ . Agent $i$ demands $S$ if $p(S)\le b_i$ and $p(T)>b_i$ for every bundle $T$ with $v_i(T)>v_i(S)$ . A competitive equilibrium (CE) is a pair $(\mathcal S,p)$ in which each agent demands her own bundle. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent.

Agent $i$ 's budget-proportional share is $b_i$ (her budget times $v_i(M)=1$ ). Her truncated share is the best value she gets in a PO allocation that gives her at most that share:

b_i^-=\max\{v_i(\mathcal S_i):\ \mathcal S\ \text{PO},\ v_i(\mathcal S_i)\le b_i\}.

The Lean development uses the same names: bundle σ i for $\mathcal S_i$ , price, IsCE, IsPO, IsStandardValuation, GetsTruncatedShare.

Formalization targets

Goal: Theorem 7.1 (p. 17)

For every two-agent additive market there is $\epsilon>0$ such that every budget pair with

b_2<b_1\le b_2+\epsilon

admits a CE $(\mathcal S,p)$ in which $v_j(\mathcal S_j)\ge b_j^-$ for both agents. The goal fixes no value of $\epsilon$ ; it asserts only that one exists for each market.

Milestones

Proposition 4.1 (p. 10): for a PO allocation with non-empty bundles and budget-exhausting prices, CE is equivalent to a pairwise swap condition, Condition (1).
Lemma 4.3 (p. 11): a budget-exhausting combination pricing $p_j=\alpha v_1(\{j\})+\beta v_2(\{j\})$ ( $\alpha,\beta\ge0$ , $\max\{\alpha,\beta\}>0$ ) at a PO allocation is a CE.
Proposition 5.1 (p. 12): budget-proportional and anti-proportional PO allocations are supported in a CE.
Lemma 5.5 (p. 14): without budget-proportional or PO anti-proportional allocations, agent $i$ 's augmented-share minimizer is agent $k$ 's truncated-share maximizer.
Lemma 6.3 (p. 15): if the budgets avoid the finite exceptional set $R_i$ and the rectangle of allocations $T_i$ is empty, a CE with truncated shares exists.
Case 1 of the proof (p. 18): a CE at budgets $(\tfrac12,\tfrac12)$ remains a CE, after rescaling prices, when agent 1's budget is raised slightly.
$R_i$ avoidance (p. 19): almost equal but unequal budgets lie outside $R_i$ .

Two companion statements are drafted without being milestones: Theorem 4.4 (second welfare theorem) and Theorem 5.2 (a budget-proportional allocation implies a CE).

Significance

The result. Theorem 7.1 shows that the non-existence of CEEI with indivisible goods is a measure-zero phenomenon for two additive agents: equal budgets are the only bad point near equality, and the equilibrium obtained is also fair in the truncated-share sense. It justifies tie-breaking by tiny budget differences in practice. It is the two-agent base case of the paper's main open question (§9.1, p. 20), whether generic almost-equal budgets guarantee a CE for more than two agents; the paper also leaves open two agents with arbitrary generic budgets and non-identical preferences (p. 21). For arbitrary, not almost-equal, budgets, Segal-Halevi (AAMAS 2018) shows that genericity does not guarantee existence for four additive agents.

Formalizing it. No machine-checked proof of any result of this paper is known. The paper's own argument for one case of the goal is incomplete: in Case 2(b) of the proof of Theorem 7.1 (p. 19) it asserts that the two candidate allocations are mirror images of each other and that the rectangles $T_1,T_2$ are empty. Both claims fail on an explicit three-item market. Theorem 7.1 itself held in every one of 6000 markets checked numerically during planning, including that one, where a CE with truncated shares exists at prices proportional to one agent's valuation. A formal proof therefore has to supply an argument the paper does not contain; the two false steps are not posed as milestones.

Difficulty

The milestones 1–5 are finite combinatorics on the Pareto frontier with sign bookkeeping. The difficulty sits in Case 2(b) of the goal: every allocation gives one agent more than $\tfrac12$ and the other less. The natural route, invoking Lemma 6.3, needs some $T_i$ to be empty, and in that case both can be non-empty. Lemma 6.3 does not cover it, and the paper's symmetry argument cannot be repaired by choosing $\epsilon$ smaller, since in the counterexample the two candidate allocations stay the same for every small $\epsilon$ . A complete proof must show directly that one of the two "as fair as possible" allocations is supported by suitable prices.

Formalization scope

Items are Fin m and agents Fin 2; the paper's agents 1, 2 are indices 0, 1, so " $b_1>b_2$ " reads b 1 < b 0. An allocation is a map σ : Fin m → Fin 2, which builds in that every item is allocated exactly once. All quantities are real numbers. Demand quantifies over every bundle, with strict inequality $p(T)>b_i$ . Prices are non-negative by definition of a CE. The truncated share is a maximum over PO allocations only.

Two conventions are disclosed restrictions or additions:

Strictness without identical items. The paper allows identical items as the single exception to strict preferences (p. 6). Here each valuation is injective on bundles, so markets with identical items are excluded.
Rescaled prices in Case 1. The page says the perturbed CE uses unchanged prices; at normalized budgets the prices must be divided by $1+\epsilon$ , and the milestone says so.

In the goal $\epsilon$ is chosen after the valuations and before the budgets. A formalization in which $\epsilon$ depends on the budgets, demand ranges over a restricted family of bundles, allocations need not allocate every item, prices may be negative, or the truncated share is a maximum over all allocations, would be a different and in several cases trivial statement; all of these are ruled out.

The definitions file GenericBudgets.AlmostEqual.Setting holds the market, CE, PO, the fairness notions, combination pricing, Condition (1), $T_i$ and $R_i$ , and is reusable for any two-agent indivisible-goods market with budgets. Proofs of the milestones, a repaired argument for Case 2(b), and general $n$ -agent versions of the CE and PO infrastructure are welcome.

Selected references

M. Babaioff, N. Nisan, I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, arXiv:1703.08150v2, 2018; Mathematics of Operations Research 46(1), 2021. https://arxiv.org/abs/1703.08150v2, https://doi.org/10.1287/moor.2020.1062
H. R. Varian, Equity, envy, and efficiency, Journal of Economic Theory 9(1), 1974. https://doi.org/10.1016/0022-0531(74)90075-1
E. Budish, The combinatorial assignment problem: approximate competitive equilibrium from equal incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
E. Segal-Halevi, Competitive equilibrium for almost all incomes, Proceedings of AAMAS 2018, pp. 1267–1275. https://arxiv.org/abs/1705.04212

9 thms1 active userReviewed

Analysis Differential Geometry Functional Analysis+1·Captain: mikedeng1

Bakry–Émery Curvature-Dimension Condition and Riemannian Ricci Curvature Bounds 2: The Dirichlet Form of an Energy Measure Space Is Twice the Cheeger Energy Iff It Is Upper-RegularResearch Paper

Motivation

There are two standard ways to do analysis on a non-smooth space. The first starts from an energy: a Dirichlet form $\mathcal E$ on $L^2(X,m)$ , its heat semigroup and its carré du champ $\Gamma$ . This is the setting of Bakry–Émery $\Gamma$ -calculus and of the curvature-dimension condition $BE(K,N)$ . The second starts from a metric measure space $(X,d,m)$ : slopes of Lipschitz functions, the Cheeger energy, Wasserstein distances, and the synthetic Ricci bounds $\mathrm{CD}(K,\infty)$ and $\mathrm{RCD}(K,\infty)$ of Lott–Villani and Sturm.

Moving between the two requires a dictionary. A Dirichlet form defines a distance, the intrinsic distance $d_{\mathcal E}$ (Biroli–Mosco, Sturm). That distance defines a Cheeger energy. The question is whether the energy rebuilt from $d_{\mathcal E}$ is the energy we started from. Ambrosio, Gigli and Savaré answer this in §3.3 of their paper on the Bakry–Émery condition and Riemannian Ricci bounds (arXiv:1209.5786, Ann. Probab. 2015). Their answer is the identification used in the main theorem of the paper, $BE(K,\infty)\Rightarrow\mathrm{RCD}(K,\infty)$ .

Timeline:

1991–1995: Biroli–Mosco and Sturm introduce the intrinsic distance of a strongly local regular Dirichlet form on a locally compact space and prove its length property there ([50, 52] of the paper).
1999: Cheeger defines the energy that now bears his name (GAFA 9).
2014: Ambrosio–Gigli–Savaré identify the minimal weak gradient with Cheeger's relaxed gradient on general metric measure spaces and introduce $\mathrm{RCD}(K,\infty)$ (Invent. Math. 195; Duke 163).
2015: the present paper sets up Energy measure spaces on Polish spaces, without local compactness, and proves Theorems 3.9–3.14.

Setting

Let $X$ be a set with a σ-additive measure $m$ . A Dirichlet form is a lower semicontinuous quadratic form $\mathcal E:L^2(X,m)\to[0,\infty]$ with $\mathcal E(\eta\circ f)\le\mathcal E(f)$ for every 1-Lipschitz $\eta$ with $\eta(0)=0$ , and with dense domain $\mathbb V=\{\mathcal E<\infty\}$ . It is strongly local when $\mathcal E(f,g)=0$ whenever $(f+a)g=0$ a.e. for a constant $a$ . A function $f\in\mathbb V$ belongs to $\mathbb G$ , with carré du champ $\Gamma(f)\in L^1_+$ , if $\mathcal E(f,f\varphi)-\frac12\mathcal E(f^2,\varphi)=\int\Gamma(f)\varphi\,dm$ for all bounded $\varphi\in\mathbb V$ .

Let $\mathbb L_C$ be the set of continuous $\psi\in\mathbb G$ with $\Gamma(\psi)\le1$ a.e. The intrinsic distance is

d_{\mathcal E}(x,y)=\sup_{\psi\in\mathbb L_C}|\psi(y)-\psi(x)|.

An Energy measure space $(X,\tau,m,\mathcal E)$ (Definition 3.6) is a strongly local Dirichlet form on a Polish space with a fully supported Borel measure such that $d_{\mathcal E}$ is a finite complete distance inducing $\tau$ , and a continuous $\theta\ge0$ has its truncations $S_k\circ\theta$ in $\mathbb L$ .

On the metric side, $|Df|(x)=\limsup_{y\to x}|f(y)-f(x)|/d(y,x)$ is the slope, and the Cheeger energy is

\mathrm{Ch}(f)=\inf\Big\{\liminf_n\tfrac12\int|Df_n|^2\,dm:\ f_n\in\mathrm{Lip}_b(X),\ f_n\to f\text{ in }L^2\Big\}.

Condition (MD) asks that $(X,d)$ be complete and separable, $\operatorname{supp}m=X$ , and balls have finite measure. Condition (ED) asks that every $\psi\in\mathbb L_C$ be 1-Lipschitz for $d$ (ED.a), and that every Lipschitz $\psi$ with $|D\psi|\le1$ and bounded support lie in $\mathbb L_C$ (ED.b). $\mathcal E$ is upper-regular (Definition 3.13) if every $f$ in a dense subset of $\mathbb V$ is an $L^2$ limit of bounded continuous $f_n\in\mathbb G$ with bounded upper semicontinuous $g_n\ge\sqrt{\Gamma(f_n)}$ and $\limsup_n\int g_n^2\le\mathcal E(f)$ .

Formalization targets

Goal: Theorem 3.14

For an Energy measure space,

\mathcal E(f)=2\,\mathrm{Ch}(f)\quad\forall f\in L^2(X,m)\qquad\Longleftrightarrow\qquad\mathcal E\text{ is upper-regular},

and in this case $\mathbb G=\mathbb V$ .

Milestones

Theorem 3.9: an Energy measure space satisfies (MD) and (ED) for $d_{\mathcal E}$ ; conversely, a distance with (MD) and (ED) makes the structure an Energy measure space and equals $d_{\mathcal E}$ .
Theorem 3.10: $(X,d_{\mathcal E})$ is a length space.
Proposition 3.11: if $f\in\mathbb G\cap C_b$ and $\Gamma(f)\le\zeta^2$ with $\zeta$ bounded upper semicontinuous, then $f$ is Lipschitz and $|D^*f|\le\zeta$ .
Theorem 3.12: under (MD), (ED.b) holds iff every Lipschitz $f$ of bounded support has $|Df|^2\ge\Gamma(f)$ ; then $2\mathrm{Ch}\ge\mathcal E$ and $|Dg|_w^2\ge\Gamma(g)$ .
The remaining assertions of Theorem 3.14: $\Gamma(f)=|Df|_w^2$ (3.41), density of $\mathbb V\cap\mathrm{Lip}_b$ in $\mathbb V$ , and mass preservation of $(P_t)$ under (MD.exp).

Significance

The identification $\mathcal E=2\mathrm{Ch}$ lets every metric notion be applied to an energy structure. Once it holds, the Wasserstein gradient flow of the entropy, the $\mathrm{EVI}_K$ formulation and $\mathrm{RCD}(K,\infty)$ all make sense for the energy. That is the route by which the paper proves that $BE(K,\infty)$ on a Riemannian Energy measure space implies $\mathrm{RCD}(K,\infty)$ , the converse of the earlier $\mathrm{RCD}\Rightarrow BE$ result. Theorem 3.12 gives the one-sided inequality $2\mathrm{Ch}\ge\mathcal E$ under the single condition (ED.b), and (3.41) says the energy density is the squared minimal weak gradient. Mass preservation is a standing hypothesis of several other results of the paper, and here it comes for free.

All of these results are proved in the paper, partly by citation: the mass-preservation clause rests on [6, Theorem 4.20], and the length property uses a midpoint criterion from Burago–Burago–Ivanov. None of them has a machine-checked proof. Mathlib has no Dirichlet forms, no Cheeger energy and no theory of length spaces built from curve length. This mission produces precise Lean statements of the paper's identification theorem and of the lemmas its proof uses, so that the metric–energy dictionary can be built up and proved one piece at a time.

Difficulty

The inequality $2\mathrm{Ch}\ge\mathcal E$ is the easy direction once (3.32) is available. Proving (3.32) means bounding the energy density of the Hopf–Lax inf-convolution $Q_tf$ pointwise by $D^+(x,t)^2/t^2$ . Only finite minima over a countable dense set lie in $\mathbb V$ , so the bound has to pass to the limit through the lower semicontinuity (2.10) of $\sqrt\Gamma$ .

The reverse inequality needs the opposite move: from an $m$ -a.e. bound $\Gamma(f)\le\zeta^2$ to a pointwise bound on the metric slope at every point. That step is Proposition 3.11. It needs $\zeta$ to be upper semicontinuous and $d_{\mathcal E}$ to be a length distance. Without upper semicontinuity, an a.e. bound says nothing about the slope at a given point. The obvious idea, testing $\mathcal E$ against the Lipschitz functions given by (ED.b), produces only lower bounds on $\mathcal E$ and cannot give $2\mathrm{Ch}\le\mathcal E$ . That is why upper regularity is the exact condition. The length property (Theorem 3.10) is itself proved by contradiction from a Lipschitz test function built from two disjoint balls. On a space that is not locally compact, this needs a completeness argument rather than Hopf–Rinow.

Formalization scope

Representation. Elements of $L^2(X,m)$ are functions $X\to\mathbb R$ . $\mathcal E$ is $\infty$ off $L^2$ , and every predicate is invariant under $m$ -a.e. equality. The σ-algebra is Borel (BorelSpace), standing in for its $m$ -completion. The topology $\tau$ is the topology of the metric of $X$ , and condition (b) of Definition 3.6 says that this metric equals $d_{\mathcal E}$ . Completeness and separability are typeclass binders. The carré du champ is a predicate on a density, never a chosen function. Slopes, $d_{\mathcal E}$ , $\mathrm{Ch}$ and curve lengths take values in $[0,\infty]$ . The curve length is the total variation, which agrees with $\int|\dot\gamma|$ . The truncation profile $S$ of (3.27) is a parameter with the properties the paper fixes. "Dense in $\mathbb V$ " means dense for the norm $(\|f\|_2^2+\mathcal E(f))^{1/2}$ . The minimal weak gradient is required to be nonnegative, which makes its two characterizing conditions determine it. Mass preservation is stated on $L^1\cap L^2$ , with $P_tf\in L^1$ part of the conclusion. In Theorem 3.9 the printed "distance on $X\times X$ " is read as a distance on $X$ .

Ruling out trivializations. The Cheeger energy is defined from slopes of bounded Lipschitz functions and never through $\mathcal E$ . Upper regularity is Definition 3.13 with a dense approximating set, not the identity $\mathcal E=2\mathrm{Ch}$ .

Infrastructure. A complete development needs carré du champ calculus for strongly local forms (chain rule, (2.9), (2.10)), the Hopf–Lax semigroup on metric spaces, relaxation and minimal weak gradients, and the midpoint characterization of length spaces. Mathlib has none of these, and all of them can be reused beyond this mission. Contributions of any of these pieces, and proofs of individual milestones, are welcome.

Selected references

L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. https://arxiv.org/abs/1209.5786 (v4 cited)
L. Ambrosio, N. Gigli, G. Savaré, Calculus and heat flow in metric measure spaces and applications to spaces with Ricci bounds from below, Invent. Math. 195, 289–391, 2014. https://doi.org/10.1007/s00222-013-0456-1
L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163, 1405–1490, 2014. https://doi.org/10.1215/00127094-2681605
J. Cheeger, Differentiability of Lipschitz functions on metric measure spaces, Geom. Funct. Anal. 9, 428–517, 1999. https://doi.org/10.1007/s000390050094
K.-T. Sturm, Analysis on local Dirichlet spaces I. Recurrence, conservativeness and L^p-Liouville properties, J. Reine Angew. Math. 456, 173–196, 1994. https://doi.org/10.1515/crll.1994.456.173
N. Bouleau, F. Hirsch, Dirichlet Forms and Analysis on Wiener Space, de Gruyter, 1991. https://doi.org/10.1515/9783110858389

12 thms1 active userReviewed

Linear Optimization Machine Learning Operations Research+1·Captain: mikedeng1

Strong Mixed-Integer Programming Formulations for Trained Neural Networks 2: Under Strict Activity Every Inequality of the Exponential Family (6b) Is Facet-DefiningResearch Paper

Motivation

Trained neural networks are increasingly embedded inside optimization models: to verify that a classifier is robust to small input perturbations, to optimize over a learned surrogate of an expensive system, or to choose decisions whose outcome is predicted by a network. When the network uses rectified linear units (ReLU), each neuron $y=\max\{0,\,w\cdot x+b\}$ is piecewise linear, and the whole network can be written exactly as a mixed-integer program (MIP) with one binary variable per neuron. How fast a branch-and-bound solver closes such a model depends on how tight the linear-programming relaxation of each neuron's formulation is.

Anderson, Huchette, Tjandraatmadja and Vielma (arXiv:1811.08359v2, the IPCO 2019 extended abstract) gave a formulation (6) of a single ReLU neuron over a box that uses only the original variables and one binary variable, and is ideal: its LP relaxation has integral extreme points (Proposition 1, p. 6). The price is an exponential family of inequalities (6b), one for every subset $I$ of the support of $w$ . The present mission formalizes their Proposition 2: each of these inequalities is facet-defining, so no member of the family can be dropped without weakening the relaxation. A longer journal version of the work, with different numbering, appeared later (arXiv:1811.01988); this mission follows the extended abstract.

Setting

Fix $\eta\in\mathbb N$ , a weight vector $w\in\mathbb R^\eta$ , a bias $b\in\mathbb R$ , and bounds $L,U\in\mathbb R^\eta$ with $L_i<U_i$ for every $i$ (§1.3, p. 4). Write $f(x)=w\cdot x+b$ and $[L,U]=\{x : L\le x\le U\}$ . The sign-adjusted bounds are

\breve L_i=\begin{cases}L_i & w_i\ge 0\\ U_i & w_i<0\end{cases},\qquad \breve U_i=\begin{cases}U_i & w_i\ge 0\\ L_i & w_i<0\end{cases},

so that $M^+(f)=w\cdot\breve U+b$ and $M^-(f)=w\cdot\breve L+b$ are the maximum and minimum of $f$ over $[L,U]$ . The support is $\operatorname{supp}(w)=\{i : w_i\neq 0\}$ . Strict activity means $M^-(f)<0<M^+(f)$ : the neuron is neither always off nor always on over the box. The paper assumes it throughout (§1.3).

Formulation (6) (p. 6) consists of the points $(x,y,z)$ with

\begin{aligned} &y\ge w\cdot x+b, &&\text{(6a)}\\ &y\le\sum_{i\in I}w_i\bigl(x_i-\breve L_i(1-z)\bigr)+\Bigl(b+\sum_{i\notin I}w_i\breve U_i\Bigr)z\quad\forall I\subseteq\operatorname{supp}(w), &&\text{(6b)}\\ &(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}. &&\text{(6c)} \end{aligned}

In Lean, form6 w b L U is this set, and relax6 w b L U is its LP relaxation ( $0\le z\le1$ in place of $z\in\{0,1\}$ ). The right-hand side of (6b) for the subset $I$ is rhs6b w b L U I x z.

An inequality $g\le0$ is facet-defining for a set $P$ when it holds on $P$ , its face $F=P\cap\{g=0\}$ is nonempty, and $\dim F=\dim P-1$ , the dimension of a set being that of its affine hull. The paper uses this standard notion without defining it.

Formalization targets

Goal: Proposition 2 (p. 6)

Under $L<U$ and strict activity, for every $I\subseteq\operatorname{supp}(w)$ , the inequality (6b) for $I$ is facet-defining for

P=\operatorname{conv}\{(x,y,z) : (x,y,z)\text{ satisfies (6a)–(6c)}\}.

The page states the result as "Each inequality in (6b) is facet-defining", and adds right after the proof line: "We require the assumption of strict activity above, as introduced in Section 1.3."

Milestones (App. A.2, p. 15)

For some $\varepsilon>0$ , the $\eta+2$ points $p^0=(\breve L,0,0)$ , $p^1=(\breve U,f(\breve U),1)$ , $\tilde p^i=(\breve L+\varepsilon\sigma_ie^i,0,0)$ for $i\notin I$ , and $\tilde p^i=(\breve U-\varepsilon\sigma_ie^i,f(\breve U-\varepsilon\sigma_ie^i),1)$ for $i\in I$ are feasible with respect to (6) and satisfy (6b) for $I$ at equality; here $\sigma_i=\pm1$ is the sign of $w_i$ (with $\sigma_i=1$ when $w_i=0$ ).
For every $\varepsilon>0$ these $\eta+2$ points are affinely independent.

Significance

The result. Proposition 1 shows that (6) is ideal; Proposition 2 shows it cannot be made smaller: removing any single inequality (6b) produces a strictly weaker relaxation. Since the family has $2^{|\operatorname{supp}(w)|}$ members, this is what justifies the paper's practical recommendation to start from the big- $M$ formulation and separate inequalities of (6b) on demand (Proposition 3, p. 7) rather than to search for a smaller ideal description in the same variables. The facet structure also gives the geometric picture the paper describes after Proposition 2: each facet is the convex combination of an $(\eta-|I|)$ -dimensional face at $z=0$ and an $|I|$ -dimensional face at $z=1$ .

Formalizing it. The result is proved in the paper, in a half-page appendix; it has not been machine-checked. The formalization adds two things. First, the proof is written for $w\ge0$ "without loss of generality by appropriately interchanging $+$ and $-$ "; the Lean statements are for every sign pattern, including zero weights. Second, the appendix exhibits $\eta+2$ affinely independent points on the face, which bounds the face dimension from below; the statement that the face has dimension exactly one less than the polyhedron also needs the polyhedron to be full-dimensional and the face to lie in a proper hyperplane, steps the extended abstract leaves implicit and a complete proof must supply.

Difficulty

The arithmetic in each step is elementary. The work lies in the bookkeeping: choosing a single $\varepsilon$ that keeps every perturbed point inside the box and on the correct side of $f=0$ (this is exactly where strict activity enters), checking the perturbed points against all $2^{|\operatorname{supp}(w)|}$ inequalities of (6b) and not only the one for $I$ , and turning a row-reduction argument on an $(\eta+1)\times(\eta+2)$ matrix into a statement about AffineIndependent and finrank of a vectorSpan in Lean. The natural shortcut, proving only that $\eta+2$ affinely independent tight points exist, is not Proposition 2: it says nothing about the dimension of the polyhedron itself.

Formalization scope

Inputs are Fin η → ℝ (indices $0,\dots,\eta-1$ for the paper's $1,\dots,\eta$ ); a point $(x,y,z)$ is p : (Fin η → ℝ) × ℝ × ℝ with p.1 = x, p.2.1 = y, p.2.2 = z. $M^\pm(f)$ are given by their closed forms $w\cdot\breve U+b$ and $w\cdot\breve L+b$ . In (6b), " $i\notin I$ " ranges over all indices outside $I$ , zero weights included; $I$ ranges over subsets of $\operatorname{supp}(w)$ , as on the page.

Every goal and milestone keeps the standing assumptions of §1.3, $L_i<U_i$ for all $i$ and strict activity, except the affine-independence milestone, which holds without them and is stated without them (a stronger statement). No other hypothesis is added. Strict activity excludes $\eta=0$ , so no nonemptiness assumption on the index set is needed.

IsFacetDefining P g is the standard notion: validity, a nonempty face, and $\dim F+1=\dim P$ with dimensions the finrank of the vectorSpan. The equation is written with $+1$ on the left so that no natural-number subtraction can make the empty set or a point a facet. The polyhedron is the convex hull of the points of (6), not the set form6 itself (which is not convex, since $z\in\{0,1\}$ ); by Proposition 1 it equals the LP relaxation relax6, but the statement does not depend on that.

The shared objects of this paper (the ReLU graph, $\breve L$ , $\breve U$ , $M^\pm$ , support, strict activity, formulation (6), ideality) come from the shared definitions module ReluMIP.Ideal.Setting, common to the companion mission on Proposition 1; this mission's own definitions module adds form6, IsFacetDefining, the sign inward, and the indexed family facetPts of the $\eta+2$ points. The facet notion and the affine-independence argument are reusable for other facet proofs of polyhedra in product spaces. Proofs of the milestones, of the goal, and of the full-dimensionality step are all welcome.

Selected references

R. Anderson, J. Huchette, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, IPCO 2019, LNCS 11480, pp. 27–42; preprint arXiv:1811.08359v2, 2019. https://arxiv.org/abs/1811.08359v2
R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, Mathematical Programming 183 (2020), 3–39. https://doi.org/10.1007/s10107-020-01474-5
G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0
J. P. Vielma, Mixed integer linear programming formulation techniques, SIAM Review 57 (2015), 3–57. https://doi.org/10.1137/130915303

5 thms1 active userReviewed

Differential Geometry Functional Analysis Probability·Captain: mikedeng1

Bakry–Émery Curvature-Dimension Condition and Riemannian Ricci Curvature Bounds 5: A Product of Riemannian Energy Measure Spaces with BE(K,N_X) and BE(K,N_Y) Satisfies BE(K,N_X+N_Y)Research Paper

Motivation

A lower bound $K$ on the Ricci curvature of a Riemannian manifold and an upper bound $N$ on its dimension can be expressed without coordinates in two ways. The Bakry–Émery condition $\mathrm{BE}(K,N)$ is a property of the heat semigroup and its generator: the iterated carré du champ $\Gamma_2$ dominates $K\Gamma+\frac1N(\Delta f)^2$ (Bakry–Émery 1985). The Riemannian curvature-dimension conditions $\mathrm{RCD}(K,\infty)$ and $\mathrm{RCD}^*(K,N)$ are properties of a metric measure space, defined through optimal transport (Ambrosio–Gigli–Savaré 2014). A basic test for any notion of "Ricci curvature at least $K$ , dimension at most $N$ " is its behaviour under products: on a product of manifolds, Ricci curvature bounds combine and dimensions add.

The paper of Ambrosio, Gigli and Savaré (arXiv:1209.5786) proves that $\mathrm{BE}(K,\infty)$ and $\mathrm{RCD}(K,\infty)$ coincide on a natural class of Dirichlet-form spaces, and draws from it, in its §5.1, two tensorization results. The first (Theorem 5.1) is the stability of $\mathrm{RCD}(K,\infty)$ under products. This had been proved in Ambrosio–Gigli–Savaré 2014 only under a nonbranching assumption on the factors; the equivalence removes that assumption. The second (Theorem 5.2) is the dimensional statement: the product of two Riemannian Energy measure spaces satisfying $\mathrm{BE}(K,N_X)$ and $\mathrm{BE}(K,N_Y)$ satisfies $\mathrm{BE}(K,N_X+N_Y)$ , the bound on the dimension of the product that the smooth case predicts.

Setting

Let $X$ be a complete separable metric space with a Borel measure $\mathfrak m$ . A Dirichlet form is a quadratic, $L^2$ -lower semicontinuous, Markovian functional $\mathcal E:L^2(X,\mathfrak m)\to[0,\infty]$ with dense domain $\mathbb V$ . Its generator $\Delta_{\mathcal E}$ is defined by $\mathcal E(f,g)=-\int g\,\Delta_{\mathcal E}f\,d\mathfrak m$ for all $g\in\mathbb V$ , and its heat flow $\mathsf P_t$ solves $\frac{d}{dt}\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$ . The carré du champ $\Gamma(f)$ is the density of $\varphi\mapsto\mathcal E(f,f\varphi)-\frac12\mathcal E(f^2,\varphi)$ . For $\nu=1/N\ge0$ , $\mathrm{BE}(K,N)$ is the weak form (2.33) of $\Gamma_2\ge K\Gamma+\nu(\Delta f)^2$ , written through the functional $\mathsf A_t[f;\varphi](s)=\frac12\int(\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,d\mathfrak m$ .

The intrinsic distance is $\mathsf d_{\mathcal E}(x,y)=\sup\{|\psi(y)-\psi(x)|:\psi\text{ continuous},\ \Gamma(\psi)\le1\}$ . An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a space whose metric is $\mathsf d_{\mathcal E}$ , with full-support measure and an exhausting function; a Riemannian Energy measure space (Definition 3.16) is in addition upper regular, and every $\psi$ with $\Gamma(\psi)\le1$ has a continuous version. An $\mathrm{RCD}(K,\infty)$ space (Definition 3.1) is a length metric measure space with the growth bounds (MD.b) and (MD.exp) on which the relative entropy has an $\mathrm{EVI}_K$ gradient flow in $(\mathscr P_2(X),W_2)$ .

The product (5.1) of $(X,\mathsf d_X,\mathfrak m_X)$ and $(Y,\mathsf d_Y,\mathfrak m_Y)$ is $Z=X\times Y$ with

\mathsf d((x,y),(x',y'))=\sqrt{\mathsf d_X^2(x,x')+\mathsf d_Y^2(y,y')},\qquad\mathfrak m=\mathfrak m_X\times\mathfrak m_Y,

and the Cartesian Dirichlet form (5.2) is

\mathcal E(f)=\int_Y\mathcal E^X(f^y)\,d\mathfrak m_Y(y)+\int_X\mathcal E^Y(f^x)\,d\mathfrak m_X(x),

where $f^y=f(\cdot,y)$ and $f^x=f(x,\cdot)$ .

Formalization targets

Goal: Theorem 5.2

If $(X,\mathcal E^X,\mathfrak m_X)$ and $(Y,\mathcal E^Y,\mathfrak m_Y)$ are Riemannian Energy measure spaces satisfying (MD.exp), $\mathrm{BE}(K,N_X)$ and $\mathrm{BE}(K,N_Y)$ , then

(Z,\mathcal E,\mathfrak m)\ \text{is a Riemannian Energy measure space with}\ \mathsf d_{\mathcal E}=\mathsf d\ \text{and}\ \mathrm{BE}(K,N_X+N_Y).

In the parametrization $\nu=1/N$ the product satisfies $\mathrm{BE}$ with $\nu_Z=\nu_X\nu_Y/(\nu_X+\nu_Y)$ .

Milestones

Corollary 4.18 (i), p. 58: under (MD+exp) and a quadratic Cheeger energy, the length property together with the gradient bound

|\mathrm D\mathsf P_tf|^2\le e^{-2Kt}\mathsf P_t(|\mathrm Df|_w^2)\tag{4.30}

implies $\mathrm{RCD}(K,\infty)$ . 2. Theorem 5.1, p. 60: the product of two $\mathrm{RCD}(K,\infty)$ spaces is $\mathrm{RCD}(K,\infty)$ . 3. The elementary inequality of p. 62: $\nu_Xa^2+\nu_Yb^2\ge\frac{\nu_X\nu_Y}{\nu_X+\nu_Y}(a+b)^2$ for positive $\nu_X,\nu_Y$ and nonnegative $a,b$ . 4. Lemma 5.3, p. 62: $\Delta_Zf(x,y)=\Delta_Xf^y(x)+\Delta_Yf^x(y)$ under the fibrewise regularity (5.9), for the RCD factors and their Cheeger forms fixed in §5.1.

Significance

Theorem 5.1 shows that $\mathrm{RCD}(K,\infty)$ is closed under products with no nonbranching condition on the factors, the hypothesis under which Ambrosio–Gigli–Savaré 2014 had obtained it. Theorem 5.2 gives the dimensional version for Dirichlet-form spaces, $\mathrm{BE}(K,N_X)\times\mathrm{BE}(K,N_Y)\Rightarrow\mathrm{BE}(K,N_X+N_Y)$ : a product of spaces of finite dimension has finite dimension, with the bound $N_X+N_Y$ of the smooth case, while the condition $\mathrm{BE}(K,\infty)$ alone loses all dimensional information.

Both results are proved in the paper; none of them, nor the objects they are stated for, has a machine-checked proof. The mission produces a Lean statement of the Cartesian Dirichlet form and of the product structure, the statements of the two tensorization theorems, and the characterization of $\mathrm{RCD}(K,\infty)$ that drives Theorem 5.1. A formal proof would also check the measure-theoretic steps that the paper takes for granted: the measurability of $y\mapsto\mathcal E^X(f^y)$ , the Fubini arguments of Lemma 5.3, and the identification of the domain of the Cartesian form (cited from [Ambrosio–Gigli–Savaré 2014], Theorem 6.18).

Difficulty

The obvious argument works fibre by fibre: apply $\mathrm{BE}(K,N_X)$ to each section $f^y$ and $\mathrm{BE}(K,N_Y)$ to each $f^x$ , and add. This fails as stated, because $\mathsf P_t$ on $Z$ does not act on the sections separately: $(\mathsf P_tf)^y$ is an average over $y'$ of the semigroup of $X$ applied to $f^{y'}$ , weighted by the heat kernel of $Y$ , so fibrewise gradient and Laplacian bounds have to be transported through this average. For Theorem 5.2 a second step is not fibrewise at all: before any dimensional estimate, the product has to be shown to be a Riemannian Energy measure space whose intrinsic distance is the product distance, which in the paper goes through Theorem 5.1 and hence through the equivalence $\mathrm{BE}(K,\infty)\Leftrightarrow\mathrm{RCD}(K,\infty)$ of Theorem 4.17.

Formalization scope

Functions on $X$ are X → ℝ, and $L^2$ membership is MemLp f 2 m; every object is invariant under $\mathfrak m$ -a.e. equality. Dirichlet forms take values in $[0,\infty]$ and are $+\infty$ off $L^2$ . Heat flows are passed as functions pinned by the predicate IsHeatSemigroup. $\Gamma(f)$ is a predicate on a density. $\mathrm{BE}(K,N)$ is parametrized by $\nu=1/N\ge0$ ; $\nu_Z=\nu_X\nu_Y/(\nu_X+\nu_Y)$ is $0$ when either factor has $N=\infty$ . The product $Z$ is WithLp 2 (X × Y), whose metric is the $\ell^2$ distance (5.1); the plain type X × Y would carry the max-metric. The second term of (5.2) uses $\mathcal E^Y$ , correcting the printed $\mathcal E^X(f^x)$ . Factors are σ-finite.

Theorem 5.2 assumes (MD.exp) for both factors: its proof invokes Theorem 5.1, whose factors must be $\mathrm{RCD}(K,\infty)$ , which a Riemannian Energy measure space with $\mathrm{BE}(K,\infty)$ is only under (MD.exp). In Corollary 4.18, the minimal weak gradient is written as $|\mathrm Df|_w^2=\Gamma(f)$ , the identity that (QCh) asserts. Lemma 5.3 carries the RCD and Cheeger-form assumptions established at the opening of §5.1. The elementary inequality retains the printed $a,b\ge0$ ; applying it to signed Laplacians requires its all-real extension.

The goal is not met by stating $\mathrm{BE}$ on the product with $\nu_Z=0$ : that is $\mathrm{BE}(K,\infty)$ , a strictly weaker claim; nor by defining the product form through the Cheeger energy of $Z$ instead of (5.2).

A complete development needs the Cartesian form's domain theorem, a pointwise version of the heat semigroups, Theorem 4.17 of the paper and the converse $\mathrm{RCD}(K,\infty)\Rightarrow\mathrm{BE}(K,\infty)$ from [Ambrosio–Gigli–Savaré 2014]. The product layer (sections, Cartesian form, Lemma 5.3) is reusable for any tensorization argument on Dirichlet forms. Proofs of the elementary inequality and of Lemma 5.3 are the natural first contributions.

Selected references

L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. arXiv:1209.5786v4
L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163(7), 1405–1490, 2014. arXiv:1109.0222
D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123, 177–206, 1985. doi:10.1007/BFb0075847

7 thms1 active userReviewed

Differential Geometry Functional Analysis Optimal Transport+1·Captain: mikedeng1

Bakry–Émery Curvature-Dimension Condition and Riemannian Ricci Curvature Bounds 6: BE(K,N) on Riemannian Energy Measure Spaces Is Stable Under Sturm–Gromov–Hausdorff ConvergenceResearch Paper

Motivation

Curvature bounds on a smooth Riemannian manifold control diffusion and the behavior of probability measures. Metric measure spaces extend these questions to limits that need not be smooth. A useful curvature condition must continue to hold when a sequence of spaces converges. Ambrosio, Gigli, and Savaré prove that their analytic Bakry–Émery curvature-dimension condition has this stability property for Riemannian energy measure spaces under Sturm–Gromov–Hausdorff convergence Ambrosio–Gigli–Savaré, Theorem 5.8. The result connects a condition stated through heat flow and Dirichlet forms with convergence stated through distances between probability measures.

The article's §5.2 first defines the convergence of spaces and of functions living in different $L^2$ spaces, then states the stability theorem. This order matters: the measure changes with the space, so ordinary convergence of functions on one fixed measured space cannot express the claim Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6.

Setting

A metric measure space $(X,d,m)$ consists of a complete separable metric space $(X,d)$ and a measure $m$ . The class $\mathcal P_2(X)$ contains probability measures with finite second moment. The squared Wasserstein distance $W_2^2(\mu,\nu)$ is the infimum of the mean squared transport cost $d(x,y)^2$ over couplings of $\mu$ and $\nu$ .

A sequence $(X_n,d_n,m_n)$ Sturm–Gromov–Hausdorff converges to $(X_\infty,d_\infty,m_\infty)$ when there is a complete separable ambient metric space $Z$ and distance-preserving embeddings $\iota_n:X_n\to Z$ , including $\iota_\infty$ , such that $W_2((\iota_n)_\#m_n,(\iota_\infty)_\#m_\infty)\to0$ . The embeddings need not be onto. This definition compares measures on different spaces after placing them in one ambient space; it does not assume that the original spaces coincide Ambrosio–Gigli–Savaré, Definition 5.4.

An energy measure space has a strongly local Dirichlet form $\mathcal E$ , its associated heat flow $P_t$ , a carré du champ $\Gamma$ , and an intrinsic distance $d_{\mathcal E}$ agreeing with $d$ . The Cheeger energy $\operatorname{Ch}_m$ is the relaxed integral of one half the squared local slope. A Riemannian energy measure space also has the upper-regularity and continuous-representative properties of Definition 3.16. The paper writes $\mathcal E=2\operatorname{Ch}_m$ in this situation Ambrosio–Gigli–Savaré, Definitions 3.6 and 3.16 and Theorem 3.14.

The Bakry–Émery condition $\mathrm{BE}(K,N)$ bounds a second-order expression involving the heat flow, the carré du champ, curvature parameter $K$ , and dimension parameter $N$ . The formalization uses the paper's weak distributional form (2.33), writing $\nu=1/N\ge0$ ; $\nu=0$ represents $N=\infty$ . This is the same $K$ and $N$ for every source space and for the limit Ambrosio–Gigli–Savaré, Definition 2.4 and (2.33).

Formalization targets

Supporting convergence results

Remark 5.5 asserts that the Cheeger energy is invariant under an isometric embedding. Lemma 5.7 supplies two criteria (squared norms, or entropies of bounded densities) for convergence of scalar functions across changing measures and shows that continuous maps of linear growth preserve this convergence. Lemma 5.9 says that, in the RCD setting, both heat-flow outputs and their generators converge. These are the mission's formal milestones Ambrosio–Gigli–Savaré, pp. 63–66.

Stability goal

For Riemannian energy measure spaces $(X_n,d_n,m_n,\mathcal E_n)$ with $m_n\in\mathcal P_2(X_n)$ and $\mathrm{BE}(K,N)$ , Theorem 5.8 asks for

(X_n,d_n,m_n)\xrightarrow{\mathrm{SGH}}(X_\infty,d_\infty,m_\infty) \quad\Longrightarrow\quad (X_\infty,d_\infty,m_\infty,2\operatorname{Ch}_{m_\infty}) \text{ is Riemannian and satisfies }\mathrm{BE}(K,N).

The goal includes the assertion that the limit energy is a Dirichlet form; quadraticity is part of the conclusion. It covers finite $N$ and $N=\infty$ with the same statement Ambrosio–Gigli–Savaré, Theorem 5.8.

Significance

The theorem permits analytic curvature-dimension bounds to survive convergence even when the carrier spaces, measures, and $L^2$ spaces vary. Without a stability statement, a bound verified separately on approximating spaces would give no such bound for their metric measure limit. The theorem also ensures that the limit Cheeger energy retains the quadratic structure required for the Riemannian theory Ambrosio–Gigli–Savaré, Theorem 5.8 and its proof.

The result is proved in the cited paper. The remaining work here is a machine-checked development of its definitions and proof, including the convergence of heat flows and generator terms across changing measures. The statements in this proposal are proof targets; they are not presented as already machine-checked. The definitions of SGH convergence and graph-law convergence can also support other stability questions for metric measure spaces.

Difficulty

The difficulty is that each $P_t^n$ acts on a different $L^2(X_n,m_n)$ , while $\mathrm{BE}(K,N)$ is an inequality involving the semigroup, its generator, and integrals against $m_n$ . Convergence of the underlying measures alone does not imply convergence of those functions or of their squared terms. In particular, pointwise convergence on a common carrier is not even a statement available before choosing embeddings and representatives. The paper's separate notion of function convergence addresses this gap Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6 and Lemma 5.9.

Formalization scope

Lean keeps the spaces indexed by $n$ : Xn n, m n, E n, and P n. The goal uses SGH convergence as an existential ambient realization, rather than assuming the paper's common-space reduction (5.10). The source heat flows and the truncation profile $S$ are named by their defining properties; they are the paper's determined objects. The limit heat flow is not assumed to exist: the $\mathrm{BE}(K,N)$ conclusion is stated for every family satisfying the heat-flow characterization of $2\operatorname{Ch}_{m_\infty}$ . Functions represent $L^2$ classes, and the common Setting layer records almost-everywhere invariance. The measurable spaces are Borel; the paper's completed measurable structures are represented through measurable versions and almost-everywhere relations.

The formal goal assumes that $m_\infty$ has full support on $X_\infty$ . Definition 3.6 requires this, while §5.2 explicitly warns that the ambient SGH limit may fail to be fully supported. The full-support condition makes the theorem refer to the intended limit carrier. The goal does not assume that the limit already is a Riemannian energy measure space or satisfies $\mathrm{BE}(K,N)$ .

Function convergence uses graph laws on $X\times\mathbb R^k$ . The chosen product metric is Mathlib's max metric; any fixed finite product metric yields the same $W_2$ convergence in this setting. The squared Wasserstein distance is extended nonnegative, so a missing finite coupling does not turn into a false real value. The limit energy is defined as $2\operatorname{Ch}_{m_\infty}$ , with no free energy parameter. Measurable representatives are explicit when forming pushforwards. Lemma 5.9 is stated on a common, fully supported RCD carrier; this narrows its ambient application and is recorded for review. Contributions to the Cheeger-energy invariance, changing-measure function convergence, heat-flow stability, and final BE passage are all within scope.

Selected references

Luigi Ambrosio, Nicola Gigli, Giuseppe Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Annals of Probability 43(1), 2015, 339–404. arXiv:1209.5786v4, DOI:10.1214/14-AOP907.

7 thms1 active userReviewed

Mathematical Physics Quantum Information·Captain: Lucas

Chiribella–D'Ariano–Perinotti 2011: Informational Derivation of Quantum TheoryResearch Paper

Motivation

Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.

Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).

Setting

An operational-probabilistic theory (OPT) has systems $A,B,\dots$ , a composite system $AB$ for every pair, and, for each pair $(A,B)$ , tests: finite families $\{\mathcal C_i\}_{i\in X}$ of transformations from $A$ to $B$ . Tests with no input are preparation tests (families of states $\rho_i$ ), tests with no output are observation tests (families of effects $a_j$ ). Composing a preparation test with an observation test yields a joint probability distribution $p(i,j)=(a_j|\rho_i)$ , and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of $A$ span a real vector space $\mathrm{St}_{\mathbb R}(A)$ of finite dimension $D_A$ , effects are linear functionals on it, and transformations are linear maps. $\mathrm{St}_1(A)$ denotes the normalized (deterministic) states.

Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face $F_\rho$ of a state, and perfectly distinguishable families $\{\rho_i\}_{i=1}^N$ (there is an observation test with $(a_j|\rho_i)=\delta_{ij}$ ). The informational dimension $d_A$ is the common size of all maximal perfectly distinguishable families of pure states.

Formalization targets

Goal (Theorem 20)

For every theory satisfying the six principles and every system $A$ , there is a real-linear isomorphism $S:\mathrm{St}_{\mathbb R}(A)\to\mathrm{Herm}_n(\mathbb C)$ with

S\big(\mathrm{St}_1(A)\big)=\{M\in M_n(\mathbb C):\ M\succeq 0,\ \operatorname{tr}M=1\},

and $n=d_A$ , the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on $\mathbb C^{d_A}$ .

Milestones

In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 ( $d_{AB}=d_Ad_B$ ), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 ( $D_A=d_A^2$ ), Theorem 13 (the Bloch ball and $G_A\cong SO(3)$ for $d_A=2$ ), Theorem 16 (superposition principle).

Significance

The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula $D_A=d_A^2$ (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.

The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.

Difficulty

The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of $O(3)$ ), then projections on faces, the superposition principle and finally a coordinate system on $d$ -level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.

Formalization scope

Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: $\mathrm{St}_{\mathbb R}(A)$ is modelled as $\mathbb R^{D_A}$ , effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.

Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.

Selected references

G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311 (2011). https://doi.org/10.1103/PhysRevA.84.012311
G. Chiribella, G. M. D'Ariano, P. Perinotti, Probabilistic theories with purification, Phys. Rev. A 81, 062348 (2010). https://doi.org/10.1103/PhysRevA.81.062348
L. Hardy, Quantum theory from five reasonable axioms (2001). https://arxiv.org/abs/quant-ph/0101012
Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001 (2011). https://arxiv.org/abs/1004.1483

13 thms1 active userReviewed

Algorithmic Game Theory Control Theory Probability·Captain: mikedeng1

On the Convergence of Closed-Loop Nash Equilibria to the Mean Field Game Limit 3: Under Convexity Every Markovian ε-Nash Equilibrium Is a Closed-Loop ε-Nash EquilibriumResearch Paper

Two notions of equilibrium in stochastic differential games

In an $n$ -player stochastic differential game each player controls the drift of its own diffusion and is rewarded through a running and a terminal payoff that depend on its own state and on the empirical distribution of all states. A player's strategy can be closed-loop (path-dependent), reacting to the whole observed history of all states, or Markovian (in the engineering literature, "feedback perfect state"), reacting only to the current states and the time. The two lead to two equilibrium notions. A Markovian equilibrium is the object produced by the classical PDE approach (a Nash system of $n$ parabolic equations), and it is the natural object for mean field game approximations. A closed-loop equilibrium is the economically more convincing notion, because it rules out profitable deviations to any strategy a player could actually implement.

D. Lacker's paper On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020, doi:10.1214/19-AAP1541) proves limit theorems for closed-loop equilibria as $n\to\infty$ . Its Proposition 2.2, the subject of this mission, shows that under a convexity condition going back to Filippov and Roxin, the Markovian equilibria form a subset of the closed-loop ones. The limit theorems for closed-loop equilibria then apply to Markovian ones as well.

Setting

Fix a horizon $T>0$ , a dimension $d$ , a number of players $n\ge1$ , a control set $A$ in a real normed space, an initial law $\lambda$ on $\mathbb R^d$ , and functions

b:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R^d,\quad f:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R,\quad g:\mathbb R^d\times\mathcal P(\mathbb R^d)\to\mathbb R.

Assumption A: $A$ is compact and convex, and $b,f,g$ are bounded and jointly continuous. Assumption B: for each $(t,x,m)$ the set $K(t,x,m)=\{(b(t,x,m,a),z): a\in A,\ z\le f(t,x,m,a)\}$ is convex; this holds, for instance, if $b$ is affine and $f$ concave in $a$ .

Write $\mathcal C^d=C([0,T];\mathbb R^d)$ . An admissible control is a Borel, non-anticipative map $\alpha:[0,T]\times(\mathcal C^d)^n\to A$ ; the set of these is $\mathcal A_n$ . A Markovian control is a Borel map $\tilde\alpha:[0,T]\times(\mathbb R^d)^n\to A$ , used as $\alpha(t,\boldsymbol x)=\tilde\alpha(t,\boldsymbol x_t)$ ; the set is $\mathcal{AM}_n$ . A profile $\boldsymbol\alpha=(\alpha^1,\dots,\alpha^n)$ drives the states

dX^i_t=b(t,X^i_t,\mu^n_t,\alpha^i(t,\boldsymbol X))\,dt+dW^i_t,\qquad \mu^n_t=\frac1n\sum_{k=1}^n\delta_{X^k_t},

with independent Brownian motions $W^i$ and i.i.d. initial states of law $\lambda$ . Player $i$ receives

J^n_i(\boldsymbol\alpha)=\mathbb E\Big[\int_0^T f(t,X^i_t,\mu^n_t,\alpha^i(t,\boldsymbol X))\,dt+g(X^i_T,\mu^n_T)\Big].

For $\epsilon\ge0$ , a closed-loop $\epsilon$ -Nash equilibrium is a profile in $\mathcal A_n^n$ with $J^n_i(\boldsymbol\alpha)\ge\sup_{\beta\in\mathcal A_n}J^n_i(\alpha^{-i},\beta)-\epsilon$ for all $i$ ; a Markovian $\epsilon$ -Nash equilibrium is a profile in $\mathcal{AM}_n^n$ with the same inequality, the supremum taken over $\beta\in\mathcal{AM}_n$ only.

Formalization targets

Goal: Proposition 2.2

Under Assumptions A and B, for every $\epsilon\ge0$ ,

\boldsymbol\alpha\ \text{Markovian }\epsilon\text{-Nash}\quad\Longrightarrow\quad\boldsymbol\alpha\ \text{closed-loop }\epsilon\text{-Nash}.

Milestones

Theorem 2.14 (Markovian projection; Gyöngy, Brunick–Shreve). If $X_t=X_0+\int_0^t b_s\,ds+W_t$ with $b$ bounded and progressively measurable, there is a bounded Borel $\widehat b$ with $\widehat b(t,X_t)=\mathbb E[b_t\mid X_t]$ , and the strong solution of $dY_t=\widehat b(t,Y_t)\,dt+dW_t$ , $Y_0=X_0$ , has $Y_t\overset d=X_t$ for each $t$ .
(4.6)–(4.7). When player $i$ deviates to a closed-loop $\beta$ against Markovian opponents, producing states $\boldsymbol Y$ , there is a Borel $\widetilde\beta:[0,T]\times(\mathbb R^d)^n\to A$ with $b(t,Y^i_t,\nu^n_t,\widetilde\beta(t,\boldsymbol Y_t))=\mathbb E[b(t,Y^i_t,\nu^n_t,\beta(t,\boldsymbol Y))\mid\boldsymbol Y_t]$ and $f(t,Y^i_t,\nu^n_t,\widetilde\beta(t,\boldsymbol Y_t))\ge\mathbb E[f(t,Y^i_t,\nu^n_t,\beta(t,\boldsymbol Y))\mid\boldsymbol Y_t]$ .
Payoff comparison. With such a $\widetilde\beta$ , $J^n_i(\beta,\alpha^{-i})\le J^n_i(\widetilde\beta,\alpha^{-i})$ .

Significance

The proposition makes the two equilibrium notions comparable: since a priori a Markovian equilibrium is tested only against Markovian deviations, there is no reason for it to survive path-dependent deviations, and without convexity it need not. Under Assumption B, every result about closed-loop equilibria (in the paper: tightness of the empirical measure flows and identification of their limits as weak mean field equilibria, Theorem 2.7) covers Markovian equilibria too, and in particular those built from classical solutions of the Nash system.

The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it is formalized. The mission produces a machine-checked formulation of the $n$ -player game with weak solutions, both equilibrium notions, and the comparison; the Markovian projection theorem is a general result of stochastic analysis, used well beyond game theory (local volatility calibration, mimicking theorems), with no formal proof in any proof assistant that we know of.

Difficulty

The obvious attempt is to replace a closed-loop deviation $\beta$ by its "Markovian average", the conditional expectation of the control given the current state. This fails twice. First, $b$ and $f$ are nonlinear in the control, so averaging the control changes both drift and reward; the convexity of $K$ is what allows a single Markovian control to reproduce the conditional drift exactly while not losing reward, and producing it requires a measurable selection that is jointly measurable in time and state. Second, replacing the drift changes the law of the whole state process, so it is not clear that the payoff can be compared at all. Only the one-dimensional time marginals are preserved, and proving that requires the Markovian projection theorem, whose proof rests on uniqueness for a Fokker–Planck equation with merely bounded measurable drift. Neither ingredient is in Mathlib, which has no stochastic differential equations, Girsanov theorem, or Itô formula.

Formalization scope

State equations are pathwise. The volatility is the identity (footnote 4), so every SDE is written $X_t=X_0+\int_0^t(\text{drift})_s\,ds+W_t$ for all $t\in[0,T]$ , a.s., with a Lebesgue integral; no Itô integral occurs.
Weak solutions are quantified, not chosen. A solution of the $n$ -player system (NSol) bundles its own probability space (in Type), filtration, $n$ independent Brownian motions jointly forming an $nd$ -dimensional $\mathbb F$ -Brownian motion, adapted continuous states, i.i.d. initial states of law $\lambda$ independent of the noise, and the empirical flow. $J^n_i$ is evaluated on a given solution, and each $\epsilon$ -Nash condition is required for every solution of the equilibrium profile and every solution of the deviated profile. This equals the paper's definition because solutions exist and are unique in law (Girsanov, p. 6); proving the goal therefore requires constructing solutions where needed.
Brownian motion is the platform's EthierKurtz.IsStandardBrownian on $[0,\infty)$ , made an $\mathbb F$ -Brownian motion by adaptedness and independent increments; $\mathbb R^d$ is EthierKurtz.SDEState d.
Spaces. $\mathcal P(\mathbb R^d)$ carries the weak topology and its Borel $\sigma$ -field; paths and flows are continuous maps on $[0,T]$ with the compact-open (= uniform) topology and Borel $\sigma$ -field.
Explicit hypotheses: $n\ge1$ (NeZero n), $T>0$ , $\epsilon\ge0$ , measurability of every process and control, and the completed filtration of $(X_0,W)$ for the strong solution in Theorem 2.14 (platform EthierKurtz.completedBrownianPast). Coefficients and controls take a real time argument, constrained only on $[0,T]$ .
Player index. The paper's proof is written for player 1; milestones 2 and 3 are stated for an arbitrary player $i$ .
Direction. The hypothesis tests only Markovian deviations, the conclusion all admissible closed-loop deviations. A formalization with the classes swapped, or one in which the solution sets are empty, would be trivially true; a sorry-free check in the workspace shows that solutions, Assumptions A–B and the hypothesis are all satisfiable.

Needed infrastructure: weak solutions of SDEs with bounded drift (Girsanov), strong existence for bounded measurable drift (Veretennikov), Fokker–Planck uniqueness, measurable selection, and disintegration of measures depending measurably on a parameter. The Markovian projection theorem and the Girsanov existence of $n$ -player solutions are reusable beyond this mission. Contributions toward any of these are welcome.

Selected references

D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020. https://arxiv.org/abs/1808.02745
I. Gyöngy, Mimicking the one-dimensional marginal distributions of processes having an Itô differential, Probab. Theory Related Fields 71, 1986. https://doi.org/10.1007/BF00699039
G. Brunick, S. Shreve, Mimicking an Itô process by a solution of a stochastic differential equation, Ann. Appl. Probab. 23(4), 2013. https://doi.org/10.1214/12-AAP881
A. Yu. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39, 1981. https://doi.org/10.1070/SM1981v039n03ABEH001522

9 thms1 active userReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Supplier Centrality and Auditing Priority in Socially Responsible Supply Chains II: A Stable Joint-Auditing Coalition Audits the Common Supplier and Shares Costs FairlyResearch Paper

Motivation

Brands that sell consumer goods are held responsible by the public for the labour and safety practices of their suppliers. After the 2013 Rana Plaza collapse in Bangladesh, about 200 clothing brands and retailers signed the Accord on Fire and Building Safety and inspect roughly 1,600 factories jointly; pharmaceutical companies such as Pfizer and GSK audit their suppliers jointly through the Pharmaceutical Supply Chain Initiative (both examples from the paper, pp. 4 and 14). Two features of such supply bases matter for auditing. Competing brands often share a common supplier, so a scandal at that supplier hurts both of them. And brands compete downstream, so a scandal that hurts only a rival can help a brand.

Chen, Qi and Dawande (MSOM 2020; accepted manuscript SSRN 2889889) model two competing buyers with one common and two independent suppliers. Their Proposition 2 shows that, when each buyer audits on his own, competition drives the buyers away from the common supplier: in every equilibrium it is left unaudited. This mission formalizes their Proposition 3. It shows that a coalition that audits jointly, and splits the cost by a Shapley-value rule, does audit the common supplier and is stable. A companion mission (Supplier Centrality … I) covers Proposition 2.

Setting

Two buyers $B_1, B_2$ source from three suppliers: $B_i$ from its independent supplier $S_i$ , and both from the common supplier $S_c$ . Each supplier is compliant with probability $e\in(0,1)$ . A non-compliant supplier that passes an audit of effort $x\in[0,1]$ (probability $1-x$ ) is exposed in public with probability $r\in(0,1]$ . An independent supplier audited with effort $x$ therefore causes damage with probability $\lambda_I(x)=r(1-e)(1-x)$ . The three suppliers offend independently.

If buyer $B_i$ has $n_i\in\{0,1,2\}$ exposed suppliers, its demand intercept falls from $\alpha$ to $\alpha-d_M$ (by $d_M>0$ once, however many offend). Each exposed supplier also raises its unit input cost from $w$ to $\hat w\ge w$ . The buyers then play a Cournot game with differentiated products (substitution $\beta\in(0,1]$ ). Buyer $B_1$ 's equilibrium profit is $\pi^b_1(n_1,n_2)=(q^*_1)^2$ , where

q^*_1=\frac{2(A_1-c_1)-\beta(A_2-c_2)}{4-\beta^2},\qquad A_i=\alpha-d_M\mathbf 1\{n_i\ge1\},\quad c_i=(2-n_i)w+n_i\hat w.

The aggregate ex post profit is $\pi^b(i\,d_M,j\,d_M)=\pi^b_1(i,j)+\pi^b_2(i,j)$ . Auditing a supplier with effort $x$ costs $K\mathbf 1\{x>0\}+\tfrac a2x^2$ .

Unilateral auditing. Each buyer audits at most one of his two suppliers. $\Pi^b_i$ is buyer $B_i$ 's expected profit net of his own audit costs. An equilibrium is a pair of mutual best responses in which, by the paper's tie-breaking rule, a buyer who audits strictly prefers it to not auditing. The effort $\hat e_I$ of eq. (2) is a buyer's optimal effort on his own supplier when the rival does not audit.

Joint auditing. The coalition chooses efforts $x=(e_{c1},e_{cc},e_{c2})\in[0,1]^3$ on $S_1,S_c,S_2$ , auditing at most two suppliers, and pays each audited supplier's cost once. The buyers still compete downstream. With $R^b_i(x)$ the buyers' expected profits excluding audit costs, the coalition's profit is

\Pi^b(x)=R^b_1(x)+R^b_2(x)-\sum_{j\in\{1,c,2\}}\Big[K\mathbf 1\{e_{cj}>0\}+\tfrac a2e_{cj}^2\Big].

The difference of the buyers' profits is $\Delta\Pi=R^b_1-R^b_2$ . The cost shares are $\Gamma_{1,2}=\tfrac12[\text{total cost}\pm\Delta\Pi]$ (eq. (3)). The analysis assumes the scenario

\pi^b(0,0)\ge\pi^b(d_M,0)\ge\pi^b(d_M,d_M)\ge\pi^b(2d_M,d_M)\ge\pi^b(2d_M,2d_M).

Formalization targets

Goal: Proposition 3

There are thresholds $K^L_c\le K^H_c$ such that, for every $K\ge0$ , an optimal joint plan

\begin{cases}\text{audits } S_1 \text{ and } S_c,\ \Delta\Pi>0, & K<K^L_c,\\ \text{audits only } S_c,\ \Delta\Pi=0, & K^L_c\le K<K^H_c,\\ \text{audits nothing}, & K\ge K^H_c.\end{cases}

The coalition is also stable. At an optimal plan its aggregate profit is at least the buyers' aggregate profit in any unilateral equilibrium. After paying $\Gamma_i$ , each buyer earns at least his profit in a symmetric unilateral equilibrium.

Milestones

The coalition's profit as a sum of unilateral profits (proof of Lemma OA9). Lemma OA9: $S_c$ beats one independent supplier, and beats no audit for $K<\hat K$ . Lemma OA10: $S_c$ with $S_1$ beats $S_1$ with $S_2$ . Lemma OA11: $S_1$ with $S_c$ beats $S_c$ alone for $K<\tilde K$ . The fair shares (3). The case analysis with $K^L_c=\min\{\frac{\hat K+\tilde K}2,\tilde K\}$ and $K^H_c=\max\{\frac{\hat K+\tilde K}2,\hat K\}$ . Stability.

Significance

The result separates two effects of downstream competition on responsible sourcing. Under unilateral auditing, a buyer gains nothing private from auditing the shared supplier: the reduction in risk accrues equally to his rival. The joint coalition removes this free-riding. The common supplier is audited whenever anything is, and the Shapley-type split (3) charges the buyer who also has his own supplier audited for the competitive advantage this gives him ( $\Gamma_1>\Gamma_2$ exactly when $\Delta\Pi>0$ ). The paper's welfare comparison (Proposition 4) builds on this proposition and on Proposition 2.

The proof in the e-companion argues through four comparisons of candidate plans and short cost-sharing algebra. None of it is machine-checked. A formal proof fixes the model (in particular which costs the coalition pays and what "at most two suppliers" excludes) and checks each comparison. In one place it also corrects the printed claim: the per-firm stability argument is given only for the symmetric unilateral equilibrium, and it does not extend to the asymmetric one (see Formalization scope).

Difficulty

All objects are explicit polynomials in the efforts. The difficulty is in the comparisons. Lemmas OA9 and OA10 compare different audit plans through the scenario ordering of aggregate ex post profits, an assumption on the stage-2 closed form that is not implied by the standing conditions. The obvious attempt, comparing first-order conditions, fails because the coalition's profit is discontinuous at zero effort (the fixed cost) and the feasible set is not convex: "at most two of three" is a union of faces of the cube. The thresholds $\hat K$ , $\tilde K$ are differences of maxima, so the case analysis has to handle ties and the boundary $K=K^H_c$ with weak inequalities. Stability needs the unilateral equilibria of Proposition 2, so the full goal reaches into the companion mission's game.

Formalization scope

Model. Params holds $\alpha,\beta,w,\hat w,d_M,e,r,a$ with $\beta\in[0,1]$ , $w\le\hat w$ , $d_M>0$ , $e\in(0,1)$ , $r\in(0,1]$ , $a>0$ and the three positivity conditions of p. 8. Every statement adds $\beta>0$ (Sec. 4.3 continues the competing case) and the p. 13 scenario as five inequalities between piAgg values. Their arguments count exposed suppliers: $\pi^b(2d_M,d_M)$ is a label, not a damage of $2d_M$ .
Expected profits are 8-outcome expectations of the closed-form stage-2 profit. The coalition's profit charges each audited supplier once, and the common supplier's damage probability under a joint audit is $r(1-e)(1-e_{cc})$ .
Thresholds $\hat K,\tilde K$ are the maxima at $K=0$ written as sSup over $[0,1]$ and $[0,1]^2$ . At $K=0$ the profit is a polynomial, so these suprema are attained.
"Yields the highest aggregate profit" is read as "some maximizer over the feasible plans has this pattern"; uniqueness is not claimed. $\Delta\Pi$ is evaluated at that maximizer (its mirror image, which audits $S_2$ , has $\Delta\Pi<0$ ).
Cost shares use the total cost of the plan. For plans with $e_{c2}=0$ they are the printed formulas (3).
Unilateral benchmark. The equilibrium includes the tie-breaking rule of p. 10, and the interior-effort assumption of p. 10 is encoded as $\hat e_I<1$ , with $\hat e_I$ given by eq. (2).
Stability, corrected. Condition (b) of Sec. 4.3 (each firm earns more) is stated against symmetric unilateral equilibria only, the case the paper's proof treats. Against the asymmetric equilibrium, where one buyer audits with $\hat e_I$ and the other audits nothing, it fails. Take $\alpha=10$ , $\beta=1$ , $w=1$ , $\hat w=3$ , $d_M=\tfrac12$ , $e=\tfrac1{10}$ , $r=1$ , $a=50$ , $K=0.2$ : the coalition optimally audits nothing, yet the auditing buyer earns more unilaterally than half of the coalition's profit. Condition (a) is stated against every equilibrium. "Higher" is stated as $\ge$ .
The goal's thresholds are existential and come before $\forall K$ . Choosing $K^L_c=K^H_c$ does not trivialize it, because the three cases must cover every $K\ge0$ . The milestone on part (2) fixes the thresholds explicitly.
The source is the authors' SSRN accepted manuscript. Main-text page numbers equal PDF pages, and e-companion page ec $k$ is PDF page $28+k$ .

Contributions welcome: proofs of Lemmas OA9–OA11, which are self-contained polynomial inequalities; existence of maximizers on the non-convex feasible set (upper semicontinuity); and the link to the unilateral equilibria needed for stability.

Selected references

F. Chen, A. Qi, M. Dawande, Supplier Centrality and Auditing Priority in Socially-Responsible Supply Chains, Manufacturing & Service Operations Management, 2020; accepted manuscript, SSRN 2889889. https://ssrn.com/abstract=2889889
E. L. Plambeck, T. A. Taylor, Supplier evasion of a buyer's audit: Implications for motivating supplier social and environmental responsibility, Manufacturing & Service Operations Management 18(2):184–197, 2016. https://doi.org/10.1287/msom.2015.0550
N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4):546–554, 1984. https://doi.org/10.2307/2555525

10 thms1 active userReviewed

Combinatorics Complexity Theory Linear Optimization+1·Captain: mikedeng1

Promise Constraint Satisfaction: Algebraic Structure and a Symmetric Boolean Dichotomy 2: The LP Algorithm Decides PCSPs with Majority or Alternating-Threshold Polymorphisms of All Odd AritiesResearch Paper

Motivation

A constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint of a given instance holds. Feder and Vardi conjectured, and Bulatov and Zhuk proved in 2017, that every CSP over a finite set of relations is either polynomial-time solvable or NP-complete, and that the answer is governed by the polymorphisms of the relations: the functions that map tuples of satisfying assignments, coordinate by coordinate, to a satisfying assignment.

A promise CSP (PCSP) relaxes the question. Each constraint comes as a pair of relations $P \subseteq Q$ ; the input is promised to be satisfiable with every constraint read as $P$ , or unsatisfiable even with every constraint read as $Q$ , and the task is to tell which. Approximate graph colouring ("is this 3-colourable graph 100-colourable?") and $(2+\varepsilon)$ -SAT are of this kind. Austrin, Guruswami and Håstad (2017, doi:10.1137/15M1006507) showed that $(2+\varepsilon)$ -SAT is NP-hard via polymorphisms; Brakensiek and Guruswami extended the polymorphism view to general Boolean PCSPs and proved a dichotomy for symmetric Boolean families (arXiv:1704.01937v2, SODA 2018, SIAM J. Comput. 2021). Later work by Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) built the general algebraic theory of PCSPs on this foundation.

This mission takes one ingredient of the dichotomy: the tractable side for two polymorphism families that have no counterpart among tractable CSPs, the Majority and the Alternating-Threshold functions. The paper solves both with the same linear programming test.

Setting

The domain is $\{0,1\}$ . A finite family of promise relations is $\Gamma = \{(P_R, Q_R) : R \in \tau\}$ , with $\tau$ finite and $P_R \subseteq Q_R \subseteq \{0,1\}^{k_R}$ . An instance $\Psi = (\Psi_P, \Psi_Q)$ has variables $x_1, \dots, x_n$ and clauses $R_j(x_{j_1}, \dots, x_{j_k})$ ; a variable may occur several times in a clause. $\Psi_P$ reads each clause with $P_{R_j}$ , and $\Psi_Q$ with $Q_{R_j}$ . Since $P \subseteq Q$ , satisfiability of $\Psi_P$ implies that of $\Psi_Q$ .

A function $f : \{0,1\}^L \to \{0,1\}$ is a polymorphism of $\Gamma$ if for every $R$ and all $x^{(1)}, \dots, x^{(L)} \in P_R$ the tuple $\big(f(x^{(1)}_1, \dots, x^{(L)}_1), \dots, f(x^{(1)}_k, \dots, x^{(L)}_k)\big)$ lies in $Q_R$ . For odd $L$ ,

\mathrm{Maj}_L(x) = 1 \iff \sum_{i=1}^L x_i > \frac L2, \qquad \mathrm{AT}_L(x) = 1 \iff \sum_{i=1}^L (-1)^{i-1} x_i > 0 .

The LP relaxation of $\Psi$ has one unknown $v_j \in [0,1]$ per variable, and for every clause $R_j(x_{j_1}, \dots, x_{j_k})$ of $\Psi_P$ it requires $(v_{j_1}, \dots, v_{j_k})$ to lie in the convex hull of $P_{R_j}$ . The §3.2 algorithm loops over the variables: it fixes $v_j = 0$ and re-solves the LP, then, if that is infeasible, fixes $v_j = 1$ and re-solves, and outputs "unsatisfiable" if both are infeasible. If every variable passes, it outputs "satisfiable". In Lean the answer is the predicate LPAlgAccepts 𝔸 X: the LP is feasible and, for each $j$ , it has a solution with $v_j = 0$ or one with $v_j = 1$ .

Formalization targets

Goal: correctness of the §3.2 algorithm

If $\mathrm{Maj}_L \in \mathrm{Pol}(\Gamma)$ for every odd $L$ , or $\mathrm{AT}_L \in \mathrm{Pol}(\Gamma)$ for every odd $L$ , then for every instance $\Psi$

\Psi_P \text{ satisfiable} \;\Longrightarrow\; \texttt{LPAlgAccepts}(\Psi) \;\Longrightarrow\; \Psi_Q \text{ satisfiable}.

No symmetry of the relations is assumed.

Milestones, in the order of the proof (pp. 14–15)

Completeness. If $\Psi_P$ is satisfiable, the algorithm accepts; no polymorphism is needed.
Convexity. A convex combination of LP solutions is an LP solution.
Case 1 claim. If $M \in ([0,1]\cap\mathbb Q)^{n\times n}$ has $M_{ii} \in \{0,1\}$ , some rational probability vector $v$ has $(Mv)_i \ne 1/2$ for all $i$ .
Case 1 rounding. With $\mathrm{Maj}_L$ for all odd $L$ , an LP solution $w$ with no coordinate $1/2$ rounds to a satisfying assignment $x^*_i = \lfloor w_i \rceil$ of $\Psi_Q$ .
Case 2 perturbation. For such $M$ and any rational $\hat w$ , some $v$ has $(Mv)_i \ne \hat w_i$ wherever $\hat w_i \notin \{0,1\}$ .
Case 2 rounding. With $\mathrm{AT}_L$ for all odd $L$ , two LP solutions $w, \hat w$ that agree only where $\hat w_i \in \{0,1\}$ give the satisfying assignment $x^*_i = [w_i > \hat w_i \text{ or } w_i = \hat w_i = 1]$ of $\Psi_Q$ .

Significance

The theorem shows that the Majority and Alternating-Threshold cases of Theorem 3.2 are tractable. Since $\Gamma$ is fixed, the LP has size linear in the instance, so linear programming decides $\mathrm{PCSP}(\Gamma)$ in polynomial time. Unlike the Zero, One, AND, OR and Parity cases of §3.1, these families cannot be handled by sandwiching a tractable CSP between $P$ and $Q$ : footnote 12 of the paper observes that the closure of $\{\mathrm{Maj}_L\}$ or $\{\mathrm{AT}_L\}$ under identification of variables is not a clone. The tractable half of the paper's symmetric Boolean dichotomy (Theorem 2.16) depends on this result. Later work replaced this LP by the Basic LP and BLP+Affine relaxations (Brakensiek–Guruswami 2019, Barto et al. 2021).

The result is proved in the paper; to our knowledge it has no machine-checked proof. The formal content is a finite-dimensional rational convexity argument plus a counting argument on columns of polymorphism inputs. Related platform work: the published PCSPBLPAff.Symmetric.theorem_2 and theorem_3 concern the BLP+Affine algorithm with symmetric or block-symmetric polymorphisms. That is a different relaxation, and $\mathrm{AT}_L$ is not symmetric.

Difficulty

Completeness is immediate. Soundness is where the difficulty lies. The obvious approach, rounding an arbitrary LP solution, fails. For Majority, a coordinate equal to $1/2$ has no nearest integer, and the LP may admit no solution without such coordinates unless one uses the per-variable solutions the algorithm found. For Alternating-Threshold, there is no fixed threshold at all, and a single LP solution gives no rule for rounding a fractional coordinate. Two further points need care. Getting from a fractional point back to a polymorphism application needs a polymorphism of an arity that depends on the denominators of the hull weights, so a single fixed arity does not suffice. In the Alternating-Threshold case, as printed, the paper pads the inputs with an arbitrary point of $P$ , and that step fails at coordinates where both solutions equal $0$ or $1$ ; the padding point has to come from the support of the hull weights.

Formalization scope

The domain $\{0,1\}$ is Bool. $\Gamma$ is a pair 𝔸 𝔹 : RelStruct τ ar Bool with [Fintype τ] and 𝔸.rel R ⊆ 𝔹.rel R, and instances, satisfiability and polymorphisms come from the published PCSPBLPAff_Symmetric_Setting. Coordinates are 0-based (Fin L), so the sign of $\mathrm{AT}_L$ is $(-1)^i$ . The LP is stated over $\mathbb Q$ ; an LP with rational data is feasible over $\mathbb R$ exactly when it is feasible over $\mathbb Q$ . The hull condition uses $P_R$ , never $Q_R$ . The acceptance predicate also requires the LP itself to be feasible, which matters only for instances without variables. The hypothesis is a disjunction of two universal statements (" $\mathrm{Maj}_L$ for all odd $L$ , or $\mathrm{AT}_L$ for all odd $L$ "), not "for every odd $L$ , one of the two". A formalization that drops the hull constraint, replaces $P$ by $Q$ in the LP, or lets the acceptance predicate be satisfied without solving the LP would make the theorem trivial or different, and is ruled out by the definitions here.

Out of scope: polynomial running time and the printed conclusion "PCSP(Γ) is polynomial-time tractable" of Theorem 3.2; the polynomial-time solvability of linear programs; the Zero/One/AND/OR/Parity cases (Lemma 3.1, which invokes Schaefer's theorem); and the non-idempotent ("anti-") cases, which go through the reduction of Lemma 2.13(2). The Remark on p. 15 says the algorithm decides but does not find a solution. Only the decision is formalized.

Infrastructure needed: finite convex combinations over $\mathbb Q$ , a perturbation lemma for avoiding finitely many hyperplanes in the rational simplex, and counting identities for $\mathrm{Maj}_L$ and $\mathrm{AT}_L$ on block inputs. The perturbation lemma and the counting identities are reusable beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the affine-hull algorithm in the Remark on p. 14), are welcome.

Selected references

J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Algebraic Structure and a Symmetric Boolean Dichotomy, arXiv:1704.01937v2, 2021; SIAM J. Comput. 50(6), 2021. https://arxiv.org/abs/1704.01937v2
P. Austrin, V. Guruswami, J. Håstad, (2+ε)-Sat Is NP-Hard, SIAM J. Comput. 46(5), 2017. https://doi.org/10.1137/15M1006507
L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic Approach to Promise Constraint Satisfaction, J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970
J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019. https://arxiv.org/abs/1807.05194
T. J. Schaefer, The Complexity of Satisfiability Problems, STOC 1978. https://doi.org/10.1145/800133.804350

10 thms1 active userReviewed

Bandit Algorithms Machine Learning·Captain: mikedeng1

An Optimal Algorithm for Stochastic and Adversarial Bandits II: α-Tsallis-INF With Symmetric Regularization Has Anytime Adversarial Pseudo-Regret 2√(min{1/(α−α²), log K/α, log T/(1−α)}·KT) + 1Research Paper

Motivation

In the adversarial multi-armed bandit problem a learner repeatedly picks one of $K$ arms and observes only the loss of the arm it picked, while an adversary chooses the losses, possibly reacting to the learner's past choices. The minimax pseudo-regret of this problem is of order $\sqrt{KT}$ after $T$ rounds, and the classical algorithm Exp3 achieves only $\sqrt{KT\log K}$ (Auer et al., 2002). Online mirror descent with a Tsallis-entropy regularizer interpolates between Exp3 (negative Shannon entropy) and the log-barrier, and the choice of the Tsallis parameter $\alpha$ decides which logarithmic factor appears in the bound.

Timeline:

2002: Auer, Cesa-Bianchi, Freund and Schapire, Exp3, pseudo-regret $O(\sqrt{KT\log K})$ .
2009: Audibert and Bubeck, the Poly-INF algorithm, the first $O(\sqrt{KT})$ adversarial bound (COLT 2009).
2015: Abernethy, Lee and Tewari analyse gradient-based prediction with Tsallis regularization for $\alpha\in(0,1]$ with a horizon-dependent learning rate (NeurIPS 2015).
2017: Agarwal, Luo, Neyshabur and Schapire analyse the log-barrier ( $\alpha=0$ ) (COLT 2017).
2019/2021: Zimmert and Seldin give a single anytime analysis covering every $\alpha\in[0,1]$ , Theorem 3 of arXiv:1807.07623v6 (JMLR 22(28), 2021).

Setting

There are $K\ge1$ arms and rounds $t=1,2,\dots$ . At round $t$ the learner draws an arm $I_t$ from a probability vector $w_t$ in the simplex $\Delta^{K-1}$ , the adversary fixes a loss vector $\ell_t\in[0,1]^K$ , which may depend on $I_1,\dots,I_{t-1}$ and on the adversary's internal randomization, and the learner observes $\ell_{t,I_t}$ . The pseudo-regret is

\overline{Reg}_T=\mathbb E\Big[\sum_{t=1}^T\ell_{t,I_t}\Big]-\min_i\mathbb E\Big[\sum_{t=1}^T\ell_{t,i}\Big],

with the expectation over both sources of randomness.

The importance-weighted (IW) estimator is $\hat\ell_{t,i}=\mathbb 1(I_t=i)\,\ell_{t,i}/w_{t,i}$ and $\hat L_{t}=\sum_{s\le t}\hat\ell_s$ . For $\alpha\in(0,1)$ and $\xi_i>0$ the α-Tsallis regularizer is

\Psi(w)=-\sum_i\frac{w_i^\alpha-\alpha w_i}{\alpha(1-\alpha)\xi_i},\qquad\Psi_t=\Psi/\eta_t ,

with symmetric regularization $\xi_i=1$ . α-Tsallis-INF is online mirror descent:

w_t=\arg\max_{w\in\Delta^{K-1}}\ \langle w,-\hat L_{t-1}\rangle-\Psi_t(w),

and the potential is $\Phi_t(Y)=\max_{w\in\Delta^{K-1}}\langle w,Y\rangle-\Psi_t(w)$ . The pseudo-regret splits into a stability term $\mathbb E[\sum_t\ell_{t,I_t}+\Phi_t(-\hat L_t)-\Phi_t(-\hat L_{t-1})]$ and a penalty term $\mathbb E[\sum_t\Phi_t(-\hat L_{t-1})-\Phi_t(-\hat L_t)-\ell_{t,i^*_T}]$ , where $i^*_T$ is a best arm in expectation in hindsight. Theorem 3 uses the learning rate

\eta_t=\sqrt{\frac{K^{1-2\alpha}-K^{-\alpha}}{1-\alpha}\cdot\frac{1-t^{-\alpha}}{\alpha t}} .

Formalization targets

Goal: Theorem 3, $\alpha\in(0,1)$

\overline{Reg}_T\le2\sqrt{\min\Big\{\frac{1}{\alpha-\alpha^2},\frac{\log K}{\alpha},\frac{\log T}{1-\alpha}\Big\}KT}+1\qquad\text{for every }T\ge1 .

The goal fixes the constants of the paper; it holds against every randomized adaptive adversary.

Milestones

Lemma 11 part 1: the per-round stability is at most $\min\{\sum_i\frac{\eta_t\xi_i}{2}\mathbb E[w_{t,i}]^{1-\alpha},1\}$ .
The maximum of $\sum_i z_i^{1-\alpha}$ over the simplex is $K^\alpha$ .
Lemma 20: the penalty is bounded by increments of the inverse learning rate times differences of $\Psi$ , plus $\langle u-e_{i^*_T},L_T\rangle$ .
Lemma 12 part 1: for non-increasing positive learning rates the penalty is at most $\frac{(K^{1-\alpha}-1)(1-T^{-\alpha})}{(1-\alpha)\alpha\eta_T}+1$ .
Lemma 14: $(1-y^{-x})/x$ is non-increasing on $x>0$ , tends to $\log y$ , and is at most $\min\{x^{-1},\log y\}$ .

Companions

Theorem 3 at the boundaries: $\alpha=1$ (negative-entropy regularizer, rate $\lim_{\alpha\to1}\eta_t=\sqrt{\log(K)(1-t^{-1})/(Kt)}$ , bound $2\sqrt{\log(K)KT}+1$ ) and $\alpha=0$ (log-barrier, rate $\sqrt{(K-1)\log(t)/t}$ , bound $2\sqrt{\log(T)KT}+1$ ).

Significance

Theorem 3 gives one anytime bound for the whole Tsallis family. At $\alpha=\tfrac12$ it is $O(\sqrt{KT})$ , the minimax rate, without knowledge of $T$ ; at $\alpha\to1$ it recovers the Exp3 rate and at $\alpha\to0$ the log-barrier rate, with constants matching Abernethy et al. without tuning the learning rate to the horizon. It is the adversarial half of the paper's study of α-Tsallis-INF, whose stochastic half (Theorem 4) shows why $\alpha=\tfrac12$ is the only value that is optimal in both regimes.

The result is proved in the paper. As far as is known, no machine-checked proof of any Tsallis-INF or Poly-INF regret bound exists. The mission produces a formal model of randomized adaptive adversaries together with online mirror descent for bandits, and formal stability and penalty lemmas for the Tsallis family, which are the standard building blocks of later best-of-both-worlds analyses.

Difficulty

The obvious route, bounding the regret of each fixed seed and action sequence and averaging, fails: the IW estimates have second moments of order $1/w_{t,i}$ , which are unbounded, and only their expectation under the learner's own sampling is controlled. The stability term therefore has to be bounded in expectation, for a regularizer whose convex conjugate has no closed form for general $\alpha$ . The penalty term involves a learning rate that changes every round, so the potentials of consecutive rounds are not directly comparable. The expectation of the run is over a law that couples the adversary's seed with the learner's random actions, so every step that the paper writes as "take expectations" has to be carried out over that law.

Two features of the printed proof need care. Theorem 3's learning rate is $0$ at $t=1$ , where $\Psi_1=\Psi/\eta_1$ is undefined, and for small $\alpha$ it increases between $t=2$ and $t=3$ , while Lemma 12 part 1 assumes a non-increasing sequence of positive learning rates. A complete proof of the goal has to handle these first rounds.

Formalization scope

Arms are Fin K with $K\ge1$ ; action sequences are maps $h:\mathbb N\to$ Fin K with $h(t)=I_t$ and $h(0)$ unused. The adversary is a seed $\omega$ drawn from a probability measure $\mu$ together with one published RegretBandits.Adversarial.Adversary K per seed (losses in $[0,1]$ , depending on past actions only), with losses measurable in the seed. The expectation of a quantity at horizon $T$ is $\int\sum_{a}(\prod_{t\le T}w_{t,a_t})F\,d\mu$ . The learner's weights are an argmax predicate on a weight function: for every round, the objective $\eta_t\langle w,-\hat L_{t-1}\rangle-\Psi(w)$ is maximized over the simplex. This is the paper's rule whenever $\eta_t>0$ , and at $\eta_1=0$ it makes $w_1$ the minimizer of $\Psi$ , the uniform vector, which is the initialisation of online mirror descent. No hypothesis on the weights is added beyond this rule. $\Phi_t$ is a real supremum over the simplex, attained because the simplex is compact and nonempty. Powers are real powers; $\log$ is the natural logarithm.

The goal and the milestones take $\alpha\in(0,1)$ (the page: $\alpha\in[0,1]$ ); the boundary values are separate companion theorems, with the limiting regularizers of §3.2 and the limiting learning rates of p. 12, and the log-barrier companion restricts the weights to the open simplex. Lemmas 12 and 20 are stated, as on the page, for any loss estimator that is conditionally unbiased given the seed and the past, depends on the actions through its own round only, and is measurable and integrable under the run law. The page prints the $\alpha\to1$ limit of the learning rate as $\sqrt{\log(K)(1-t^{-1})/t}$ ; the true limit carries an extra factor $1/K$ under the root, and the $\alpha=1$ companion uses the true limit. In Lemma 20 the term $\langle u-e_{i^*_T},L_T\rangle$ sits inside the expectation, since $L_T$ is random under an adaptive adversary.

A trivializing formalization is ruled out: the weights are not chosen by a choice function, and an algorithm whose weights are arbitrary at $\eta_1=0$ is excluded because the predicate pins $w_1$ .

A complete development needs: convex conjugates of separable regularizers on the simplex, the stability argument via a second-order bound, telescoping of potentials, unbiasedness of IW estimators under the run law, and elementary real-analysis estimates (Lemma 14, the simplex maximum). The run law, the IW estimator and the potential are reusable in the companion missions on Theorem 1 and Theorem 4. Contributions to any milestone, and to reusable lemmas about the run law, are welcome.

Selected references

J. Zimmert, Y. Seldin, Tsallis-INF: An Optimal Algorithm for Stochastic and Adversarial Bandits, J. Mach. Learn. Res. 22(28), 2021; arXiv:1807.07623v6. https://arxiv.org/abs/1807.07623
J. Abernethy, C. Lee, A. Tewari, Fighting Bandits with a New Kind of Smoothness, NeurIPS 2015. https://arxiv.org/abs/1505.00340
A. Agarwal, H. Luo, B. Neyshabur, R. E. Schapire, Corralling a Band of Bandit Algorithms, COLT 2017. https://arxiv.org/abs/1612.06246
J.-Y. Audibert, S. Bubeck, Minimax Policies for Adversarial and Stochastic Bandits, COLT 2009. https://www.learningtheory.org/colt2009/papers/024.pdf
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375

9 thms1 active userReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

A Block Successive Upper-Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization 2: Randomized BSUM-M Converges to Primal-Dual Optimal Solutions Almost SurelyResearch Paper

Motivation

Many large convex problems in signal processing, networking and statistics have a separable objective coupled by linear constraints: $K$ blocks of variables, each with its own nonsmooth regularizer and its own feasible set, tied together by $\sum_k E_kx_k=q$ . The alternating direction method of multipliers (ADMM) is the standard tool for such problems when $K=2$ . For $K\ge3$ the direct extension of ADMM can diverge, as shown by Chen, He, Ye and Yuan (2016), and convergence guarantees for multi-block variants typically require strong convexity or extra correction steps.

Hong, Chang, Wang, Razaviyayn, Ma and Luo propose the block successive upper-bound minimization method of multipliers (BSUM-M), which updates each primal block by minimizing a local upper bound of the augmented Lagrangian, followed by a dual gradient step, and prove that it converges for any number of blocks without strong convexity of the objective. They also analyse a randomized version, RBSUM-M, in which each iteration updates a single randomly chosen block, primal or dual. Randomized block selection matters when data or computation are distributed and not every block is available at every step. This mission formalizes the randomized half of their main theorem; the cyclic half is a separate mission.

Setting

Let $x=(x_1,\dots,x_K)$ with $x_k\in\mathbb R^{n_k}$ , and consider

\min_x\ f(x)=g(x)+\sum_{k=1}^K h_k(x_k)\quad\text{s.t.}\quad Ex=\sum_{k=1}^K E_kx_k=q,\quad x_k\in X_k. \tag{1.1}

The standing assumptions (Assumption A) are: $g(x)=\ell(Ax)+\langle x,b\rangle$ with $\ell$ strictly convex and continuously differentiable; $h_k(x_k)=\lambda_k\|x_k\|_1+\sum_J w_J\|x_{k,J}\|_2$ with nonnegative weights; each $X_k=\{x_k\mid C_kx_k\le c_k\}$ is a compact polyhedron; the problem is feasible and its primal and dual optimal values are attained.

For $\rho>0$ the augmented Lagrangian and augmented dual function are

L(x;y)=f(x)+\langle y,q-Ex\rangle+\frac\rho2\|q-Ex\|^2,\qquad d(y)=\min_{x\in X}L(x;y),

and $X(y)$ is the set of minimizers of $L(\cdot;y)$ over $X=\prod_kX_k$ . The method works with approximation functions $u_k(v_k;x)$ (Assumption B): $u_k(\cdot;x)$ majorizes $g+\frac\rho2\|E\cdot-q\|^2$ in block $k$ , touches it with matching gradient at $x_k$ , is strongly convex with modulus $\gamma_k$ and has an $L_k$ -Lipschitz gradient.

RBSUM-M. Fix probabilities $p_0,\dots,p_K>0$ summing to 1. At iteration $t\ge1$ draw $k$ with probability $p_k$ . If $k=0$ , take a dual step $y^{t+1}=y^t+\alpha^t(q-Ex^t)$ ; otherwise replace block $k$ by

x_k^{t+1}=\arg\min_{x_k\in X_k}\ u_k(x_k;x^t)-\langle y^t,E_kx_k\rangle+h_k(x_k),

leaving the other blocks and $y$ unchanged. The analysis uses the block steps $\hat x_k^{t+1}$ (the minimizer above, computed for every $k$ ), the dual step $\hat y^{t+1}=y^t+\alpha^t(q-Ex^t)$ , the gaps $\Delta_d^t=d^*-d(y^t)$ , $\Delta_p^t=L(x^t;y^t)-d(y^t)$ , and the proximal gradient $\tilde\nabla_xL(x;y)=x-\operatorname{prox}_{h+\iota_X}\big(x-\nabla_x(L(x;y)-h(x))\big)$ . The error bound with constant $\tau$ is $\operatorname{dist}(x,X(y))\le\tau\|\tilde\nabla_xL(x;y)\|$ for all $y$ and $x\in X$ .

Formalization targets

Goal: Theorem 2.1, part 2

Under Assumptions A and B and the error bound, if the stepsizes are either constant and sufficiently small, or satisfy $\sum_t\alpha^t=\infty$ , $\alpha^t\to0$ , then with probability 1

\|Ex^t-q\|\to0,\qquad\|x^t-x^{t+1}\|\to0,\qquad\|x^t-\bar x^t\|\to0,

where $\bar x^t$ is the point of $X(\hat y^t)$ nearest to $x^t$ , and every limit point of $(x^t,y^t)$ is a primal and dual optimal pair. The threshold for "sufficiently small" is existential and depends only on the problem data, the $u_k$ , the error-bound constant and $p$ .

Milestones

In the order of the paper: Lemma 2.1 (differentiability of $d$ , $\nabla d(y)=q-Ex(y)$ , the $1/\rho$ -Lipschitz bound); Lemma 2.3(2) (expected decrease of $L$ ); Lemma 2.4(2) (proximal gradient bounded by the block and dual steps); Lemmas 2.5(2) and 2.6(2) (expected change of the dual and primal gaps); and from the proof of Theorem 2.1, (2.24)–(2.25) (expected change of $\Delta_p+\Delta_d$ ), (2.28) (constraint violation), (2.29) (the descent estimate with explicit coefficients) and (2.40) (one-step change of $\|E\bar x^t-q\|$ ).

Significance

The result shows that a randomized, single-block-per-iteration primal-dual method converges almost surely to primal-dual optimal solutions of a multi-block linearly constrained problem, under assumptions that allow a rank-deficient $A$ , nonsmooth group-sparse regularizers, and inexact (majorized) block subproblems. The potential function $\Delta_p+\Delta_d$ and the way the error bound converts it into a supermartingale estimate are reused in later analyses of multi-block and randomized ADMM-type methods.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a checked convergence proof for a randomized augmented-Lagrangian method, a reusable formal treatment of the augmented dual function of a convex program with compact polyhedral constraints, and a precise record of the conventions under which the published statements hold (see the scope section).

Difficulty

The obvious route is to show that $L(x^t;y^t)$ decreases. It does not: a dual step increases $L$ by $\alpha^t\|q-Ex^t\|^2$ , and without strong convexity there is no direct control of the distance to the solution set. The argument has to combine the primal and dual gaps into one potential, bound the residual term $\|Ex^t-E\bar x^{t+1}\|$ through an error bound that holds without strong convexity, and then pass from a conditional-expectation inequality to almost-sure convergence. Under diminishing stepsizes the supermartingale argument only yields $\liminf\|E\bar x^t-q\|=0$ , and upgrading this to a limit needs a separate pathwise argument on how fast $\nabla d(\hat y^t)$ can move.

Formalization scope

Blocks are EuclideanSpace ℝ (Fin (n k)) and the full vector lives in PiLp 2, so norms are Euclidean. $\ell$ is real-valued on all of $\mathbb R^p$ . The augmented dual function is $d(y)=\min_{x\in X}L(x;y)$ (the page's (1.9) prints an unconstrained minimum of $g$ plus penalty; the constrained reading is the one Lemma 2.1 and (2.19) use). The prox in the proximal gradient includes the constraint set $X$ , which is what the proof of Lemma 2.4 needs; the error bound of Lemma 2.2 is a hypothesis of the goal, in its global form on $X$ , and is not derived. Lemma 2.2 itself is not part of the mission.

Conditional expectations given $z^t=(x^t,y^t)$ are written as the explicit average $p_0F(x,\hat y)+\sum_kp_kF((\hat x_k,x_{-k}),y)$ over the random index, at every state; this is $\mathbb E[F(z^{t+1})\mid z^t]$ because the index drawn at iteration $t$ is independent of $z^t$ . The goal is stated on an arbitrary probability space carrying mutually independent indices with law $p$ , for every run from a deterministic start $x^1\in X$ , $y^1$ . Iterations are indexed from $t=1$ as on the page.

Two printed statements are corrected and labelled in their items: Lemma 2.1 asserts $Ax$ (not each $A_kx_k$ ) constant over $X(y)$ , and Lemma 2.6(2) uses $\alpha^t$ where the page prints $\alpha^r$ . Statements are not trivialized: the setting is satisfiable (for instance $K=1$ , $g\equiv0$ , $h=0$ , $E=0$ , $X=[-1,1]$ , $u(v;x)=(v-x_1)^2/2$ ), the stepsize threshold precedes the probability space and the run, and the solution sets entering distances are nonempty under Assumption A. A formalization in which the error bound or the gap bounds are assumed in a form that already contains the conclusion would not count.

A complete development needs: Danskin-type differentiability of $d$ and the $1/\rho$ -smoothness of the augmented dual; first-order optimality and nonexpansiveness of the prox of $h+\iota_X$ ; and the Robbins–Siegmund almost-supermartingale convergence theorem in Mathlib's conditional expectation framework, together with a bridge from the explicit index average to condExp. The last two are reusable well beyond this mission. Contributions to any of the milestones, or to these general lemmas, are welcome.

Selected references

M. Hong, T.-H. Chang, X. Wang, M. Razaviyayn, S. Ma, Z.-Q. Luo, A Block Successive Upper Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization, arXiv:1401.7079v1, 2014; Mathematics of Operations Research 45(3), 2020. https://arxiv.org/abs/1401.7079, https://doi.org/10.1287/moor.2019.1010
M. Hong, Z.-Q. Luo, On the linear convergence of the alternating direction method of multipliers, Mathematical Programming 162, 2017. https://doi.org/10.1007/s10107-016-1034-2
C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155, 2016. https://doi.org/10.1007/s10107-014-0826-5
H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
M. Razaviyayn, M. Hong, Z.-Q. Luo, A unified convergence analysis of block successive minimization methods for nonsmooth optimization, SIAM Journal on Optimization 23(2), 2013. https://doi.org/10.1137/120891009

Theorem numbers, equation numbers and page numbers in this mission refer to arXiv:1401.7079v1 (printed page = PDF page − 1); the journal version renumbers them.

12 thms1 active userReviewed

Machine Learning Optimal Transport Optimization·Captain: mikedeng1

Computational Optimal Transport XII: The Entropic Barycenter Scalings Are (e^{f_s/ε}, e^{g_s/ε}) for the Solutions of a Dual Program with Σ_s λ_s f_s = 0Textbook

Why barycenters of histograms matter

A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.

The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.

Finite histogram setting

There are $S$ input histograms. Source $s$ has $n_s$ bins and a probability vector $b_s$ , while the barycenter has $n$ bins. The real matrix $C_s\in\mathbb R^{n\times n_s}$ gives the cost of transporting a unit of mass from barycenter bin $i$ to input bin $j$ . A weight vector $\lambda\in\Sigma_S$ has nonnegative entries summing to one; $\Sigma_k$ denotes the probability simplex on $k$ bins. The unregularized barycenter problem (9.10) minimizes $\sum_s\lambda_s L_{C_s}(a,b_s)$ over $a\in\Sigma_n$ , where $L_{C_s}$ is the minimum transport cost with marginals $a$ and $b_s$ .

For a regularization parameter $\varepsilon>0$ , the entropic transport cost $L^\varepsilon_{C_s}(a,b_s)$ minimizes $\langle C_s,P_s\rangle-\varepsilon H(P_s)$ over nonnegative coupling matrices $P_s$ with row marginal $a$ and column marginal $b_s$ . Here $\langle C_s,P_s\rangle=\sum_{i,j}C_{s,ij}P_{s,ij}$ and $H(P_s)=\sum_{i,j}(-P_{s,ij}\log P_{s,ij}+P_{s,ij})$ , with $0\log0=0$ . The Gibbs kernel is $K_{s,ij}=e^{-C_{s,ij}/\varepsilon}$ .

The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices $(P_s)_s$ ; each matrix has column marginal $b_s$ , and every matrix has the same row marginal. That shared row marginal is $a$ , so the optimization can be expressed without carrying $a$ as a separate variable. The generalized matrix divergence is $\mathrm{KL}(P_s\mid K_s)=\sum_{i,j}[P_{s,ij}\log(P_{s,ij}/K_{s,ij})-P_{s,ij}+K_{s,ij}]$ , using the continuous value at $P_{s,ij}=0$ . See (9.15)–(9.17) in Peyré and Cuturi.

Formalization targets

The goal is Proposition 9.1 on p. 530. The dual variables are row potentials $f_s\in\mathbb R^n$ and column potentials $g_s\in\mathbb R^{n_s}$ . They maximize

\sum_s\lambda_s\left[\langle g_s,b_s\rangle-\varepsilon\sum_{i,j}e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon}\right] \quad\text{subject to}\quad \sum_s\lambda_s f_s=0.

The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy

P_{s,ij}=e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon},

and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one $g_s$ block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.

What the result supplies

The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.

Where the difficulty lies

The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.

Formalization scope

Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires $S,n,n_s>0$ , $\varepsilon>0$ , strictly positive weights $\lambda_s$ that sum to one, and strictly positive input histograms $b_s$ that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses $0\log0=0$ on nonnegative couplings. The shared row marginal is constructed by the constraints on the $P_s$ ; it is not a free histogram unrelated to them.

The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on $K$ in (9.17); the Lean statements use the dimensions specified by $P_s\in\mathbb R^{n\times n_s}$ . The optional cost-gradient Proposition 9.2 on pp. 519–520 and the $f_s$ block update (9.19)–(9.20) lie outside this proposal.

Selected references

Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. DOI: 10.1561/2200000073.

6 thms1 active userReviewed

Operations Research Partial Differential Equations Probability+1·Captain: mikedeng1

Global C¹ Regularity of the Value Function in Optimal Stopping Problems 2: In Finite Horizon, Probabilistic Regularity of the Boundary Makes the Time Derivative of the Value Function ContinuousResearch Paper

Motivation

In an optimal stopping problem the value function $V$ and the gain function $G$ agree on the stopping set $D=\{V=G\}$ , and $V>G$ on the continuation set $C$ . The smooth fit principle says that, at the boundary $\partial C$ between them, $V$ meets $G$ with matching first derivatives. Smooth fit is one of the boundary conditions in the free-boundary problems that characterise optimal stopping boundaries. It is behind the integral equations for the early-exercise boundary of the American put and for many problems in sequential analysis and finance (Peskir & Shiryaev, 2006). On a finite horizon the value depends on the remaining time, and continuity of the time derivative $\partial_tV$ across $\partial C$ is the step that justifies the local time-space calculus applied to $V$ (Peskir, 2005).

Before De Angelis & Peskir (2020) such continuity results were proved problem by problem, or under sign conditions that the main examples do not satisfy: $G=0$ on the stopping set and $H<0$ globally, which fails for the American put. Their paper gives two general results. Theorem 8 covers the space derivative, and Theorem 15, the subject of this mission, covers the time derivative on a finite horizon. Both are stated for a strong Markov process realised as a stochastic flow, and both rest on probabilistic regularity of the boundary.

Setting

Fix a horizon $T>0$ and $d=m+1\ge1$ . The process is the time-space process $X^{t,x}_s=(t+s,X^x_s)$ . Its first coordinate is time, and $(X^x_s)_{s\ge0,\,x\in\mathbb R^{d-1}}$ is a stochastic flow on a probability space $(\Omega,\mathcal F,P)$ with a right-continuous filtration $(\mathcal F_s)$ , adapted to it, with $X^x_0=x$ . Its paths are right-continuous with left limits, it is left-continuous over stopping times, and it is strong Markov. The flow is continuous in the space variable if, outside one null set, $x\mapsto X^x_s(\omega)$ is continuous for every $s$ .

Given continuous functions $\lambda\ge0$ , $G$ and $H$ of $(t,x)$ , write $\Lambda^{t,x}_s=\int_0^s\lambda(t+u,X^x_u)\,du$ . The value function is

V(t,x)=\sup_{0\le\tau\le T-t}\mathsf E\Big[e^{-\Lambda^{t,x}_\tau}G(t+\tau,X^x_\tau)+\int_0^\tau e^{-\Lambda^{t,x}_s}H(t+s,X^x_s)\,ds\Big]

over stopping times $\tau$ bounded by the remaining time $T-t$ . The sets are $C=\{V>G\}$ and $D=\{V=G\}$ inside $[0,T]\times\mathbb R^{d-1}$ , and $\partial C=D\cap\overline C$ . The problem is well posed if the expected payoffs are integrable and the first entry time $\tau_D$ into $D$ is optimal.

The first hitting time of a set $A$ is $\sigma^{t,x}_A=\inf\{s\in(0,T-t]:X^{t,x}_s\in A\}$ . A point $z$ is probabilistically regular for $A$ if $P(\sigma^z_A=0)=1$ . The generator $\mathbb L_X$ (2.14) acts in the space variable, with diffusion matrix $\sigma_{ij}$ , drift $\mu_i$ , killing rate $\lambda$ and jump measure $\nu$ . Its coefficient formula is tied to the flow by the right derivative at zero of the killed spatial semigroup applied to $G(t,\cdot)$ . The function $\tilde H=G_t+\mathbb L_XG+H$ appears in the hypotheses.

Formalization targets

Goal: Theorem 15, global form (p. 20)

Assume well-posedness, (5.9) ( $V$ continuous on $[0,T]\times\mathbb R^{d-1}$ and $C^1$ on $C$ ), (5.10) ( $G\in C^{1,2}$ ) and (5.11) (Lipschitz continuity of $\tilde H$ and $\lambda$ in $t$ , uniformly in $x$ ), and a continuous flow. Assume the local conditions (5.12)–(5.13) and probabilistic regularity for $D^\circ$ at every $z\in\partial C$ . Then

\partial_tV\ \text{exists and is continuous on }[0,T]\times\mathbb R^{d-1}.

Milestones

(5.17): along every sequence $(t_n,x_n)\in C$ with $(t_n,x_n)\to z$ , $\displaystyle\liminf_{n}V_t(t_n,x_n)\ge G_t(z)$ .
(5.20): along the same sequences, $\displaystyle\limsup_{n}V_t(t_n,x_n)\le G_t(z)$ .
Theorem 15, (5.14): at a single regular $z\in\partial C$ ,

\partial_tV(z)=\partial_tG(z)\quad\text{and}\quad\lim_{C\ni(t,x)\to z}\partial_tV(t,x)=\partial_tG(z).

Significance

The result. Theorem 15 turns a probabilistic property of the boundary, which can be checked through sample-path arguments, into the analytic smooth-fit condition in time. Continuity of $\partial_tV$ across $\partial C$ is the hypothesis that the change-of-variable formula with local time on curves and surfaces requires. That formula yields the free-boundary integral equations for optimal stopping boundaries. The theorem needs no sign condition on $G$ or $H$ and no strong Feller property. The time-space process is never strong Feller, which is exactly why the earlier strong Feller route to boundary regularity does not apply here.

Formalizing it. The result is proved in the paper; nothing here is open mathematics. As far as is known no part of it has been machine-checked. Mathlib has stopping times and conditional expectation, but no stochastic flows, no generators of jump diffusions and no optimal stopping in continuous time. A complete development formalizes the proof on pp. 20–23 together with the upper semicontinuity of hitting times of open sets (Lemma 4 and Corollary 6 of the paper, posed in the companion mission on the space derivative).

Difficulty

The infinite-horizon argument (Theorem 13, via Theorem 8) perturbs the starting point and reuses the optimal stopping time of the unperturbed problem. On a finite horizon this fails in the time variable. Shifting the start from $t_n$ to $t_n+\varepsilon_n$ shortens the remaining horizon, so the stopping time optimal for $V(t_n,x_n)$ is no longer admissible for $V(t_n+\varepsilon_n,x_n)$ . A first-order comparison of payoffs therefore cannot be used. The proof truncates the stopping time and controls the truncated part, which is the role of the identity (5.12) and of the window $[T-t-\varepsilon,T-t]$ in (5.13). The convergence $\tau_n\to0$ of the optimal stopping times has to come from regularity of $z$ for the interior $D^\circ$ and continuity of the flow, not from the strong Feller property.

Formalization scope

Space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin m) with $d=m+1$ . Time is ℝ≥0. Points of the time-space domain are pairs in ℝ × EuclideanSpace ℝ (Fin m), and $[0,T]\times\mathbb R^{d-1}$ is Set.Icc 0 T ×ˢ univ.
$P_x$ and $\mathsf E_x$ are $P$ and $\mathsf E$ of the flow started at $x$ . All stopping times are for one common right-continuous filtration and are finite valued. Admissible times for $(t,x)$ satisfy $\tau\le T-t$ .
Hitting and entry times take values in $[0,\infty]$ (WithTop ℝ≥0) with $\inf\emptyset=\infty$ , and are capped by the horizon.
Expectations are Bochner integrals. Well-posedness carries integrability of every admissible payoff and optimality of a stopping time equal to $\tau_D$ almost surely, so $V$ is attained and is not a junk supremum.
$\partial C:=D\cap\overline C$ . " $C\ni(t,x)\to z$ " is the filter $\mathcal N_C(z)$ , and $\partial_tV$ is the derivative of $s\mapsto V(s,x)$ within $[0,T]$ . The pointwise clause "continuous at $z$ " means convergence along $C$ ; the global clause is ContinuousOn on $[0,T]\times\mathbb R^{d-1}$ .
(5.13) is an integrable majorant valid simultaneously for all points of the window. The ball $b(z,\varepsilon)$ is the max-metric ball, which is equivalent because $\varepsilon$ is existential. (5.12) includes integrability of both sides.
$D^\circ$ is the interior in $\mathbb R\times\mathbb R^{d-1}$ . No point with $t=T$ is probabilistically regular, so the global hypothesis requires $\overline C$ to avoid $t=T$ . This is the paper's scope, not an addition.
The model is not specialized: any $d\ge1$ , general $\lambda$ , jumps allowed, càdlàg paths, unbounded $G$ , $H$ and $V$ . A formalization that takes $\Lambda\equiv0$ , $d=1$ , continuous paths, or the strong Feller property is a different theorem.

Contributions welcome: the hitting-time lemmas (upper semicontinuity of $\sigma_{D^\circ}$ under a continuous flow), dominated-convergence lemmas for the truncated stopping times, and the two halves (5.17) and (5.20).

Selected references

T. De Angelis, G. Peskir, Global C¹ regularity of the value function in optimal stopping problems, Ann. Appl. Probab. 30(3), 2020. Preprint arXiv:1812.04564v2. https://arxiv.org/abs/1812.04564v2
G. Peskir, A. Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser, 2006. https://doi.org/10.1007/978-3-7643-7390-0
G. Peskir, A change-of-variable formula with local time on curves, J. Theoret. Probab. 18, 2005. https://doi.org/10.1007/s10959-005-3517-6
R. M. Blumenthal, R. K. Getoor, Markov Processes and Potential Theory, Academic Press, 1968.

8 thms1 active userReviewed

Information Theory Machine Learning Optimal Transport+1·Captain: mikedeng1

Computational Optimal Transport IX: The Entropic Cost L^ε_C(a, b) Equals max ⟨f, a⟩ + ⟨g, b⟩ − ε⟨e^{f/ε}, K e^{g/ε}⟩, with Optimal Scalings (e^{f/ε}, e^{g/ε})Textbook

Motivation

Optimal transport compares two distributions by finding the least expensive way to move mass between them. For finite histograms, the resulting linear program is precise but its optimal coupling can be sparse. In applications where the coupling represents traffic, matching, or a differentiable loss, a sparse plan may be undesirable or expensive to compute repeatedly. Peyré and Cuturi describe how adding an entropy term selects a diffuse coupling and leads to matrix scaling algorithms that can be used on large finite problems (Peyré and Cuturi, 2019, Chapter 4).

The entropic dual gives a second view of the same regularized problem. Its variables are real vectors attached to the two marginal constraints. Unlike the ordinary Kantorovich dual, the objective has no explicit feasibility constraints and is smooth. This permits calculations in the log domain, which the book introduces because direct scaling with exponentials can suffer from numerical overflow or underflow when the regularization parameter is small relative to the costs (Peyré and Cuturi, 2019, §4.4). This mission targets the exact relationship between the regularized minimum, the smooth dual maximum, and the scaling factors.

Setting

Fix positive integers $n,m$ . A histogram $a\in\Sigma_n$ is a vector with nonnegative entries summing to one; $b\in\Sigma_m$ is defined similarly. Strict positivity is required for the attained dual maximum and log-domain updates; the primal scaling and Kantorovich-feasibility statements also cover zero-entry histograms. A coupling $P\in U(a,b)$ is an $n\times m$ matrix with nonnegative entries, row sums $a$ , and column sums $b$ . A real matrix $C$ assigns cost $C_{ij}$ to each transfer from row $i$ to column $j$ , and $\langle C,P\rangle=\sum_{i,j}C_{ij}P_{ij}$ is its transport cost.

The book uses the entropy $H(P)=-\sum_{i,j}P_{ij}(\log P_{ij}-1)$ , with $0\log0=0$ . For $\varepsilon>0$ , the regularized cost is $L_C^\varepsilon(a,b)=\min_{P\in U(a,b)}\{\langle C,P\rangle-\varepsilon H(P)\}$ . The Gibbs kernel has entries $K_{ij}=\exp(-C_{ij}/\varepsilon)$ . Given potentials $f\in\mathbb R^n$ and $g\in\mathbb R^m$ , the smooth dual objective is $Q(f,g)=\langle f,a\rangle+\langle g,b\rangle-\varepsilon\sum_{i,j}e^{f_i/\varepsilon}K_{ij}e^{g_j/\varepsilon}$ . These are the finite-dimensional objects of (4.1), (4.2), and (4.30) in the source (Peyré and Cuturi, 2019, pp. 425, 428, 448).

Formalization targets

Attained entropic duality

The goal is Proposition 4.4. There are an optimal coupling $P$ and potentials $(f,g)$ at which the dual reaches its maximum, with the common value

L_C^\varepsilon(a,b) =\langle C,P\rangle-\varepsilon H(P) =\max_{f',g'} Q(f',g').

For every maximizing pair $(f',g')$ , the same optimal coupling satisfies

P_{ij}=e^{f'_i/\varepsilon}K_{ij}e^{g'_j/\varepsilon}.

Thus the dual potentials determine the scaling vectors $u=e^{f'/\varepsilon}$ and $v=e^{g'/\varepsilon}$ in (4.12). The maximum is an attained maximum of a real function, as stated in the book, rather than an unrestricted real infimum or supremum that might take a default value on a bad input (Peyré and Cuturi, 2019, Proposition 4.4).

Supporting results

The milestones follow the source's statements. Proposition 4.3 gives existence, uniqueness, and the Gibbs scaling of the primal optimizer. Remark 4.21 gives the two partial-gradient formulas and the closed log-domain block updates. Proposition 4.5 states that an entropic dual maximizer is a feasible pair of ordinary Kantorovich potentials, so its linear objective is bounded above by the unregularized cost $L_C(a,b)$ (Peyré and Cuturi, 2019, pp. 432, 449, 452–453).

Significance

The equality establishes that the matrix scaling variables and the dual potentials describe the same optimal coupling. It lets a computation based on scaling be interpreted as maximizing a smooth objective, and it gives exact marginal-error expressions through the dual gradients. Feasible Kantorovich potentials obtained at the optimum also provide a lower bound on the ordinary transport cost. These statements explain why log-domain updates represent the same mathematical problem as entropic transport, even when direct exponentiation is numerically fragile (Peyré and Cuturi, 2019, §§4.4–4.5).

The results are established in the textbook; the open work here is their Lean formalization. A completed development would provide reusable finite coupling, entropy, Gibbs-kernel, and smooth-dual interfaces, together with the existence and differentiability results needed to connect them. It would also distinguish a primal optimum, a dual maximum, and a feasible potential without relying on informal convention. The mission does not assert that these textbook results are new, and no machine-checked proof of these exact statements is claimed here.

Difficulty

The unconstrained dual objective has a symmetry: shifting every coordinate of $f$ by one constant and every coordinate of $g$ by its negative leaves the value unchanged. Consequently, the set of maximizers is not bounded in the ordinary product space. Positivity of the marginals matters for attaining a maximum with finite real potentials; if a marginal entry is zero, the corresponding potential can escape toward negative infinity. On the primal side, the entropy formula must be valid at zero entries even though optimality links it to strictly positive exponential scalings. The formal argument must connect these boundary conventions and the finite-dimensional optimization statements without turning the maximum into a junk real supremum (Peyré and Cuturi, 2019, Proposition 4.4 and Remark 4.21).

Formalization scope

The Lean development represents indices by Fin n and Fin m, matrices by Matrix (Fin n) (Fin m) ℝ, and histograms by Mathlib's stdSimplex. Positive dimensions and $\varepsilon>0$ appear throughout. Strictly positive marginal entries are required for the attained dual maximum and log-domain updates; the other statements permit zero entries. The book assumes positive weights for discrete measures in Remark 2.1; the marginal positivity is also required for the attained dual maximum and the logarithmic updates. The cost matrix itself may have arbitrary real entries. Entropy uses Real.negMulLog, which implements $0\log0=0$ on the nonnegative couplings where it is applied.

The primal optimum is a predicate on a coupling and its objective, rather than a chosen matrix. The unregularized $L_C$ is a real infimum used only when simplex marginals make its feasible set nonempty and bounded. The dual objective is a finite sum. Its gradients are stated as one-variable derivatives in each coordinate, and each block update is characterized as the unique maximizer with the other block fixed. The complete development needs Mathlib's finite sums, real exponential and logarithm, calculus, finite-dimensional topology, and optimization facts. Contributions that establish these shared interfaces or the four milestone statements are in scope.

Propositions 4.7 and 4.8 are excluded from this proposal because their printed bounds compare a dual linear objective with $L_C^\varepsilon$ where the accompanying arguments instead support a comparison with the unregularized $L_C$ ; (4.47) also has a sign discrepancy. The milestone list therefore avoids encoding a false inequality (Peyré and Cuturi, 2019, pp. 453–454).

Selected references

Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6), 2019, pp. 355–607. DOI: 10.1561/2200000073.

8 thms1 active userReviewed

Operations Research Partial Differential Equations Probability+1·Captain: mikedeng1

Global C¹ Regularity of the Value Function in Optimal Stopping Problems 1: Probabilistic Regularity of the Boundary Makes the Value Function Continuously DifferentiableResearch Paper

Why boundary regularity matters

An optimal stopping rule chooses when to end a stochastic process in order to collect a terminal reward, possibly after earning or paying a running reward. The resulting value function often solves a free-boundary problem: the state space splits into a region where stopping is optimal and one where continuing is better. Smoothness inside either region does not by itself say what happens where the regions meet. This mission concerns the global first spatial derivative of that value function at the optimal stopping boundary.

De Angelis and Peskir proved that a probabilistic condition on the boundary, together with regularity of the process as a spatial flow and explicit integrability bounds, gives continuous differentiability of the value function across the boundary. Their result applies to standard Markov processes with right-continuous paths and left limits, including jump processes; it is not restricted to diffusions or to a constant discount rate. The source is De Angelis and Peskir, arXiv:1812.04564v2, Theorem 8.

The stopping problem and its boundary

Let $d\ge1$ , let $E=\mathbb R^d$ , and let $X_t^x$ be a stochastic flow: the same probability space carries a path starting from every state $x\in E$ . Time is nonnegative. One right-continuous filtration makes every path adapted and is used for every stopping rule. The process is strong Markov, has right-continuous paths with left limits, is left continuous over stopping times, and starts from $X_0^x=x$ . Expectations and probabilities written $E_x$ and $P_x$ in the paper are the expectation and probability of the flow $X^x$ under one measure $P$ .

The continuous data are a nonnegative discount rate $\lambda:E\to[0,\infty)$ , a terminal reward $G:E\to\mathbb R$ , and a running reward $H:E\to\mathbb R$ . The discount accumulated along the path from $x$ is $\Lambda_t^x=\int_0^t\lambda(X_s^x)\,ds$ . For every finite-valued stopping time $\tau$ of the common filtration, define

J(x,\tau)=E\!\left[e^{-\Lambda_\tau^x}G(X_\tau^x)+\int_0^\tau e^{-\Lambda_t^x}H(X_t^x)\,dt\right], \qquad V(x)=\sup_\tau J(x,\tau).

This is the infinite-horizon problem (2.1). It is well posed here when all admissible payoffs are integrable and the first entry time into the stopping set is an almost surely finite optimal stopping time. These conditions ensure that $V$ is a real, attained supremum rather than a default value of Lean's real supremum or integral. Define the stopping set $D=\{x:V(x)=G(x)\}$ , the continuation set $C=\{x:V(x)>G(x)\}$ , and the boundary relevant to the theorem as $D\cap\overline C$ . For a state set $A$ , the first entry time is $\tau_A^x=\inf\{t\ge0:X_t^x\in A\}$ and the first strictly positive hitting time is $\sigma_A^x=\inf\{t>0:X_t^x\in A\}$ . Both may be infinite.

A boundary point $z$ is probabilistically regular for $A$ if $P_z(\sigma_A=0)=1$ . It is Green regular for $A$ when $P_x(\tau_A\ge\varepsilon)\to0$ as $x\to z$ through $C$ , for every $\varepsilon>0$ . The paper obtains Green regularity by either strong Feller continuity with probabilistic regularity for $D$ , or spatial continuity of the flow with probabilistic regularity for $D^\circ$ . Lemma 1 and Corollaries 2–3 give the first route; Lemma 4 and Corollaries 5–6 give the second. All six statements use an arbitrary closed $D$ , as in Section 3 of the source. Source: §§2–3, pp. 3–11.

Formalization targets

The milestone results first establish the two boundary regularity routes. In particular, approaching $z$ through $C$ , the first route gives $\tau_D^{x_n}\to0$ in probability; the second gives $\tau_{D^\circ}^{x_n}\to0$ and $\tau_D^{x_n}\to0$ almost surely. Equations (4.16) and (4.19) then bound, respectively, the lower and upper limits of each coordinate derivative $\partial_iV(x_n)$ by $\partial_iG(z)$ . The pointwise part of Theorem 8 concludes

D V(z)=D G(z),\qquad \lim_{C\ni x\to z}D V(x)=D G(z).

The mission goal is the final sentence of Theorem 8. If the theorem's local hypotheses hold at every $z\in D\cap\overline C$ , then

V\in C^1(\mathbb R^d).

The hypotheses include the discounted generator representation (2.14) from the problem setup, continuity and interior $C^1$ regularity of $V$ , global $C^1$ regularity of $G$ , one positive Lipschitz constant for both $H$ and $\lambda$ , a $C^1$ spatial flow, the four local bounds (4.4)–(4.7) with one radius at each boundary point, and one of the two probabilistic regularity alternatives. The goal retains all dimensions $d\ge1$ , all nonnegative continuous discount rates, and the source's full class of standard Markov flows. Source: §2.5 and Theorem 8, pp. 7, 11–12.

What the result gives

The conclusion identifies the derivative of the value function on both sides of the stopping boundary. It strengthens a derivative match along a single direction or a chosen sequence into continuous differentiability on the whole state space. This is relevant to free-boundary formulations of optimal stopping, where interior regularity can be available from a Dirichlet or Poisson problem while boundary regularity remains the missing step. The authors describe that distinction in their discussion of smooth fit and global differentiability. Source: §2.5, p. 8.

The mathematical theorem is proved in the 2020 paper. In this mission, the definitions and statements compile as Lean declarations, while the theorem proofs remain to be formalized. A complete development would supply reusable arguments about hitting times, semicontinuity of hitting probabilities, stochastic flows, and limits of derivatives near a stopping boundary. Those components would also support the paper's finite-horizon spatial and temporal results.

The central difficulty

The value is a supremum over stopping rules. Differentiating the reward for a fixed stopping time does not automatically differentiate that supremum, because the optimal time depends on the initial state. Near the boundary, even continuity of the value does not control the duration of the optimal rule from neighboring states. The paper's probabilistic regularity conditions address that duration, while (4.4)–(4.7) provide the integrability needed to pass to derivative limits. A direct appeal to interior differentiability leaves the boundary itself untreated. Source: §§3–4.1, pp. 9–15.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d) with $d\ge1$ ; Fin d indices are the paper's coordinates $1,\ldots,d$ shifted by one. Balls are open Euclidean balls. Time is $\mathbb R_{\ge0}$ , and the entry and hitting times live in $\mathbb R_{\ge0}\cup\{+\infty\}$ so an unattained hit has its intended value. The flow is the process; no separate family of measures $P_x$ is introduced. One common filtration is used for all initial states and is right-continuous. Its finite stopping times are the full admissible class, not only hitting times.

The value uses Bochner expectations and real Lebesgue time integrals. Well-posedness records integrability for every admissible payoff and optimality and almost sure finiteness of $\tau_D^x$ . The generator clause acts on smooth functions in the domain of the discounted transition semigroup; it retains the paper's diffusion, drift, killing, and jump terms. The boundary is $D\cap\overline C$ , and approach through continuation points is expressed by the within-set neighborhood filter. Pointwise continuous differentiability means a Fréchet derivative at $z$ equal to $D G(z)$ and convergence of $D V$ along $C$ ; the goal uses global ContDiff. The local bounds retain all independently indexed starting states and coordinates. Their uncountable suprema are represented by integrable common majorants, with timewise measurable envelopes for the suprema inside time integrals. This convention excludes default integral values from nonmeasurable or nonintegrable expressions.

A formalization restricted to Brownian motion, one dimension, zero or constant discount, continuous paths, bounded rewards, or only one boundary regularity branch would state a different theorem. Contributions toward measurable hitting-time events, the two Section 3 regularity chains, the envelope bounds, and the derivative comparison are welcome.

Selected references

De Angelis, T., and Peskir, G., Global C¹ Regularity of the Value Function in Optimal Stopping Problems, Annals of Applied Probability 30(3), 2020. arXiv:1812.04564v2; DOI:10.1214/19-AAP1517.

15 thms1 active userReviewed

Functional Analysis Optimal Transport Probability+1·Captain: mikedeng1

Computational Optimal Transport XI: For p = 1, 2 the p-Wasserstein Distance on ℝ^d with d ≥ 2 Is Not HilbertianTextbook

Why ask whether a Wasserstein distance is Hilbertian

Kernel methods, multidimensional scaling and low-distortion embeddings all work best on data whose distance comes from a Hilbert space. A distance $d$ on a set $\mathcal Z$ is Hilbertian when $\mathcal Z$ can be mapped into a Hilbert space so that $d$ becomes the norm distance; for such a $d$ , the kernel $e^{-d^p/t}$ is positive definite for $0\le p\le 2$ and $t>0$ (Berg, Christensen and Ressel, 1984), and the classical Euclidean toolbox applies. Optimal transport distances are popular for comparing probability measures, so it is natural to ask whether they are Hilbertian. In dimension one the answer is yes for $\mathcal W_2$ : the map sending a measure to its quantile function is an isometry into $L^2([0,1])$ , and between univariate Gaussians $\mathcal W_2$ is the Euclidean distance between (mean, standard deviation). Peyré and Cuturi, Computational Optimal Transport (FnT ML 2019), §8.3, show that this does not extend to the plane: for $p=1,2$ and $d\ge2$ the $p$ -Wasserstein distance on $\mathbb R^d$ is not Hilbertian (Proposition 8.2, p. 507).

The tool is a classical characterization. Schoenberg (1938) proved that a distance is Hilbertian exactly when its square is conditionally negative definite; Berg, Christensen and Ressel (1984, Prop. 3.2) give the modern form. The easy direction turns non-embeddability into a finite check, and the book's proof of Proposition 8.2 performs that check numerically on 35 measures supported on the four corners of the unit square (Figure 8.6, p. 508). Stronger, quantitative statements are known: planar $\mathcal W_1$ does not even embed into $L^1$ with bounded distortion (Naor and Schechtman, 2007), and Andoni, Naor and Neiman (2018) study which powers of Wasserstein distances embed.

Setting

Let $\mathcal Z$ be a set. A function $\varphi:\mathcal Z\times\mathcal Z\to\mathbb R$ is negative definite (Definition 8.3, p. 501, in the conditional form used in §8.3) if it is symmetric and, for every $n\ge0$ , every $x_1,\dots,x_n\in\mathcal Z$ and every $r\in\mathbb R^n$ with $\sum_ir_i=0$ ,

\sum_{i,j=1}^n r_ir_j\,\varphi(x_i,x_j)\le0 .

A function $d:\mathcal Z\times\mathcal Z\to\mathbb R$ is Hilbertian (Definition 8.4, p. 506) if there are a real Hilbert space $\mathcal H$ and a map $\phi:\mathcal Z\to\mathcal H$ with $d(z,z')=\|\phi(z)-\phi(z')\|_{\mathcal H}$ for all $z,z'$ .

On $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$ , let $\mathcal P_p(\mathbb R^d)$ be the Borel probability measures $\mu$ with $\int\|x\|_2^p\,d\mu<\infty$ . A coupling of $\mu$ and $\nu$ is a measure $\pi$ on $\mathbb R^d\times\mathbb R^d$ whose two marginals are $\mu$ and $\nu$ , and the $p$ -Wasserstein distance (2.18) is

\mathcal W_p(\mu,\nu)=\Big(\inf_{\pi}\int\|x-y\|_2^p\,d\pi(x,y)\Big)^{1/p},

finite on $\mathcal P_p(\mathbb R^d)$ . For points $x_1,\dots,x_n$ and a histogram $a\in\Sigma_n$ (nonnegative, summing to one) the discrete measure is $\sum_ia_i\delta_{x_i}$ ; for two histograms $a,b$ , $U(a,b)$ is the set of nonnegative matrices with row sums $a$ and column sums $b$ , and $L_C(a,b)=\min_{P\in U(a,b)}\sum_{i,j}C_{i,j}P_{i,j}$ (2.11).

The configuration of the book's proof consists of the corners $x^1=[0,0]$ , $x^2=[1,0]$ , $x^3=[0,1]$ , $x^4=[1,1]$ of the unit square, the 35 histograms of $\Sigma_4$ with entries in $\{0,\tfrac14,\tfrac12,\tfrac34,1\}$ , and the centering matrix $J=I_n-\tfrac1n\mathbb 1_{n,n}$ .

Formalization targets

Goal: Proposition 8.2

For $d\ge2$ and $p\in\{1,2\}$ ,

\mathcal W_p \text{ on } \mathcal P_p(\mathbb R^d) \text{ is not Hilbertian.}

Milestones

Proposition 8.1, proved direction (pp. 506–507): if $d$ is Hilbertian then $d^2$ is negative definite.
Squared distance (p. 507): $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$ is not negative definite, $d\ge2$ , $p=1,2$ .
Reduction to the plane (proof of Prop. 8.2): if $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$ , $d\ge2$ , were negative definite, so would be $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^2)$ .
Discrete measures (Remark 2.13, p. 375): $\mathcal W_p\big(\sum_ia_i\delta_{x_i},\sum_jb_j\delta_{x_j}\big)^p=L_C(a,b)$ with $C_{i,j}=\|x_i-x_j\|_2^p$ .
Centering criterion (proof of Prop. 8.2): a matrix $M$ admits a zero-sum $r$ with $r^\top Mr>0$ if and only if $JMJ$ has a positive eigenvalue.
The grid counterexample (proof of Prop. 8.2, Figure 8.6): for $p=1,2$ there are grid histograms $a^1,\dots,a^n$ and a zero-sum $r$ with

\sum_{i,j}r_ir_j\,\mathcal W_p^2\Big(\sum_k a^i_k\delta_{x^k},\sum_k a^j_k\delta_{x^k}\Big)>0.

Significance

A Hilbertian distance gives positive definite Gaussian and Laplace kernels, Euclidean multidimensional scaling and Johnson–Lindenstrauss dimension reduction for free. Proposition 8.2 says none of these can be obtained for $\mathcal W_1$ or $\mathcal W_2$ on $\mathbb R^d$ , $d\ge2$ , by an isometric embedding; this is why the literature turned to approximate embeddings, sliced distances and entropic surrogates (pp. 507–508). The negative-definiteness test of milestone 1 is a reusable certificate for non-embeddability of any finite metric.

The result is known, and the book's proof is a floating-point eigenvalue computation. The formal content of this mission is a machine-checked proof with an exact certificate: rational or algebraic Wasserstein distances between explicit discrete measures and an explicit zero-sum vector. As far as this mission is aware, no formal proof of the statement exists in Mathlib or on the platform. Schoenberg's converse is cited by the book and is not part of the mission.

Difficulty

The abstract part is short: expanding $\|\phi(z_i)-\phi(z_j)\|^2$ and using $\sum_ir_i=0$ gives milestone 1. The obstacle is the certificate. The book observes that $J\mathbf D_p^2J$ has a positive top eigenvalue (about $1.2$ for $p=1$ and $0.7$ for $p=2$ ), but a proof needs exact transport costs between the chosen measures, each the value of a small linear program whose optimality has to be established (for instance by a dual certificate), together with a vector $r$ for which the quadratic form is provably positive. For $p=1$ the costs involve $\sqrt2$ , the diagonal of the square. A second, separate difficulty is connecting the measure-theoretic $\mathcal W_p$ to the discrete program (milestone 4) and transporting a counterexample from $\mathbb R^2$ into $\mathbb R^d$ (milestone 3), both of which require working with couplings as measures on a product space.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\mathcal W_p$ is the published definition WassersteinDRO.Duality.wassersteinDistance (an $[0,\infty]$ -valued infimum over all measures with the two marginals, raised to $1/p$ ), converted to a real number. The distance is considered on $\mathcal P_p(\mathbb R^d)$ , the set where it is finite; outside it the real conversion is a junk $0$ . The book names no domain; since the counterexample consists of finitely supported measures, the finite computation gives non-Hilbertianity on $\mathcal P_p$ and on every smaller set containing those measures.
Negative definiteness is conditional. Definition 8.3 as printed quantifies over all $r$ ; under that reading no nonzero squared distance is negative definite, so Proposition 8.1 would be false and "not negative definite" trivially true. The zero-sum condition, used by the book in the proof of Proposition 8.1, is part of the definition; this rules out the trivial formalization.
Hilbert spaces are real, complete inner-product spaces in the universe of $\mathcal Z$ . Indices are 0-based (Fin n). Histograms are real vectors; the reduction milestone is stated for every $p\ge1$ .
Discrete transport objects ( $U(a,b)$ , $L_C$ ) are redefined in this mission's namespace CompOT.NotHilbertian, duplicating chunk II of the series.

Contributions welcome: the forward direction of Schoenberg's characterization, the discrete-measure bridge (reusable wherever discrete optimal transport meets measure-theoretic couplings), the isometric-embedding invariance of $\mathcal W_p$ , and exact certificates for the grid computation.

Selected references

G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073
I. J. Schoenberg, Metric spaces and positive definite functions, Transactions of the AMS 44(3):522–536, 1938. https://doi.org/10.1090/S0002-9947-1938-1501980-0
C. Berg, J. P. R. Christensen and P. Ressel, Harmonic Analysis on Semigroups, Graduate Texts in Mathematics 100, Springer, 1984. https://doi.org/10.1007/978-1-4612-1128-0
A. Naor and G. Schechtman, Planar earthmover is not in $L_1$ , SIAM Journal on Computing 37(3):804–826, 2007. https://doi.org/10.1137/05064206X
A. Andoni, A. Naor and O. Neiman, Snowflake universality of Wasserstein spaces, Annales scientifiques de l'École normale supérieure 51(3):657–700, 2018. https://arxiv.org/abs/1509.08677

10 thms1 active userReviewed

Combinatorics Linear Optimization Optimal Transport+1·Captain: mikedeng1

Computational Optimal Transport V: A Feasible Pair of Kantorovich Potentials Is Optimal or Strictly Improves Along a Direction (1_S, −1_S′)Textbook

Motivation

The discrete optimal transport problem between two histograms is a linear program, and much of the algorithmic theory of optimal transport is the theory of solving that linear program well. Chapter 3 of Peyré and Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019) surveys the classical combinatorial solvers: the network simplex, dual ascent methods, and the auction algorithm. Dual ascent methods work entirely with the dual variables, the Kantorovich potentials $(f, g)$ : they keep a feasible pair of potentials and improve it step by step until it is optimal. The specialisation of this idea to assignment problems is the Hungarian algorithm of Kuhn (1955), and its general form is the primal-dual method for network flow problems presented in Bertsimas and Tsitsiklis, Introduction to Linear Optimization (1997, §7.7), on which §3.6 of the book is modelled.

The mathematical engine of every dual ascent method is one alternative: a feasible pair of potentials is either already optimal, or it can be improved along a direction of a very special, combinatorial form. This mission formalizes that alternative (Proposition 3.6 of the book) together with the results it rests on.

Setting

Fix integers $n, m \ge 1$ , a cost matrix $C \in \mathbb{R}^{n\times m}$ , and two histograms $a \in \Sigma_n$ , $b \in \Sigma_m$ , where $\Sigma_n = \{a \in \mathbb{R}^n_+ : \sum_i a_i = 1\}$ is the probability simplex. Write $[\![n]\!] = \{1, \dots, n\}$ for the row indices and, following the book, $[\![m]\!]' = \{1', \dots, m'\}$ for the column indices.

The couplings between $a$ and $b$ form the transportation polytope

U(a,b) = \{P \in \mathbb{R}^{n\times m}_+ : P\mathbb{1}_m = a,\ P^{\mathsf T}\mathbb{1}_n = b\},

and the primal problem is $\mathrm{L}_C(a,b) = \min_{P\in U(a,b)} \langle C, P\rangle$ with $\langle C, P\rangle = \sum_{i,j} C_{i,j}P_{i,j}$ . A pair of vectors $(f, g) \in \mathbb{R}^n \times \mathbb{R}^m$ is dual feasible, written $(f,g) \in R(C)$ , when $f_i + g_j \le C_{i,j}$ for all $(i, j)$ . The dual problem (3.4) is

\mathrm{L}_C(a,b) = \max_{(f,g)\in R(C)} \langle f, a\rangle + \langle g, b\rangle .

For a feasible pair $(f, g)$ , a pair of indices $(i, j')$ is balanced if $f_i + g_j = C_{i,j}$ and inactive if $f_i + g_j < C_{i,j}$ . A matrix $P$ and a pair $(f, g)$ are complementary if $P_{i,j} > 0$ implies $C_{i,j} = f_i + g_j$ , that is, $P$ is supported on balanced pairs. For $S \subset [\![n]\!]$ the vector $\mathbb{1}_S \in \mathbb{R}^n$ has ones at the indices in $S$ and zeros elsewhere; likewise $\mathbb{1}_{S'} \in \mathbb{R}^m$ for $S' \subset [\![m]\!]'$ .

Formalization targets

Goal: Proposition 3.6 (p. 416)

For $a \in \Sigma_n$ , $b \in \Sigma_m$ and $(f,g) \in R(C)$ : either $(f, g)$ is optimal for (3.4), or there exist $S \subset [\![n]\!]$ , $S' \subset [\![m]\!]'$ and $\varepsilon_0 > 0$ such that for every $0 < \varepsilon \le \varepsilon_0$ ,

(\tilde f, \tilde g) = (f, g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C) \quad\text{and}\quad \langle \tilde f, a\rangle + \langle \tilde g, b\rangle > \langle f, a\rangle + \langle g, b\rangle .

Milestones

Proposition 3.3 (p. 405). If $P \in U(a,b)$ and $(f,g) \in R(C)$ are complementary, then $P$ is primal optimal and $(f,g)$ is dual optimal.
Proposition 3.5 (p. 415). If every balanced pair $(i, j')$ with $i \in S$ has $j' \in S'$ , then $(f,g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C)$ for all sufficiently small $\varepsilon > 0$ .
Objective change (proof of Proposition 3.6, pp. 416–417). The step changes the dual objective by exactly $\varepsilon(\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b)$ .
Labeled sets (proof of Proposition 3.6, pp. 416–417). If no coupling in $U(a,b)$ is complementary to $(f,g)$ , then there are $S, S'$ with every balanced pair leaving $S$ landing in $S'$ , and

\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b > 0 .

Significance

The result. Proposition 3.6 says that non-optimality of a feasible dual pair is always witnessed by a direction with entries in $\{0, \pm 1\}$ , determined by two index sets, which keeps the pair feasible for a positive step and strictly improves the objective. This is what makes dual ascent a finite combinatorial method rather than a generic linear-programming iteration: the search for an ascent direction reduces to a maximum-flow computation on the bipartite graph of balanced pairs. Combined with the step length of Proposition 3.5, it is the primal-dual method, which reduces to the Hungarian algorithm on assignment problems. Milestone 1 is the optimality certificate of complementary slackness, used throughout the book's chapter 3.

Formalizing it. These results are classical and proved in the book and in Bertsimas and Tsitsiklis; no machine-checked proof of them is known to exist. The mission produces a formal statement and proof of the optimality-or-ascent alternative for the discrete Kantorovich dual, together with the complementary-slackness certificate in the transport setting. Milestone 4 is a Hall-type statement (a supply–demand theorem on a bipartite graph) whose formal proof is reusable for other matching and transportation results.

Difficulty

Milestones 1–3 are short computations. The content of the goal is in milestone 4. The obvious argument is linear-programming duality: if $(f,g)$ is not optimal, some feasible direction improves the objective. But LP duality only produces an arbitrary real direction; the claim that a direction of the form $(\mathbb{1}_S, -\mathbb{1}_{S'})$ suffices is a combinatorial statement. The book obtains $S, S'$ as the labeled nodes of a maximal flow (Ford–Fulkerson) and argues through max-flow/min-cut; the flow bookkeeping printed on p. 417 is garbled, so the step from "no complementary coupling exists" to " $\mathbb{1}_S^{\mathsf T}a > \mathbb{1}_{S'}^{\mathsf T}b$ for a set closed under balanced edges" has to be supplied carefully. Separately, connecting "not optimal" to "no complementary coupling exists" needs the converse direction of complementary slackness or strong duality for the transport problem.

Formalization scope

Row and column indices are Fin n and Fin m (0-based); the primed column set $[\![m]\!]'$ is just Fin m. Cost matrices and couplings are Matrix (Fin n) (Fin m) ℝ; histograms and potentials are real functions on Fin n, Fin m; $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n). Index sets $S, S'$ are Finsets and $\mathbb{1}_S$ is indicatorVec S. "Optimal for Problem (3.4)" is the predicate IsDualOptimal: feasible, and no feasible pair has a larger objective (no real infimum or supremum is used, so no junk value can enter). The book's "for a small enough $\varepsilon > 0$ " is stated as "for every $\varepsilon \in (0, \varepsilon_0]$ ", which is equivalent because $R(C)$ is convex and the objective is linear.

Standing assumptions, all from the book: $(f, g)$ is dual feasible (p. 415, "In what follows, $(f,g)$ is a feasible dual pair in $R(C)$ "); $a, b$ are histograms in the simplex (used for the goal and milestone 4; without equal masses the dual is unbounded and optimality fails for every pair). Milestone 4 replaces the book's flow hypothesis "the throughput is strictly smaller than 1" by the equivalent flow-free statement "no coupling in $U(a,b)$ is complementary to $(f,g)$ "; flows, capacities and the labeling algorithm appear in no statement.

The goal admits a trivializing formalization: allowing an arbitrary direction $(u, v)$ instead of $(\mathbb{1}_S, -\mathbb{1}_{S'})$ turns Proposition 3.6 into plain non-optimality of a linear program. The statement here fixes the direction to $(\mathbb{1}_S, -\mathbb{1}_{S'})$ exactly as the book does.

A complete development needs finite LP duality or complementary slackness for the transportation problem, and a max-flow/min-cut or Hall-type theorem on bipartite graphs with vertex capacities. Both are reusable well beyond this mission. Contributions welcome: proofs of the milestones, a self-contained proof of milestone 4 by induction or by a max-flow argument, and alternative proofs of the goal through LP duality plus a vertex argument.

Selected references

G. Peyré, M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§3.1–3.3, §3.6, pp. 400–417)
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §7.7 (the primal-dual method) and pp. 305–308 (Ford–Fulkerson and the labeling algorithm).
H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2(1–2):83–97, 1955. https://doi.org/10.1002/nav.3800020109
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5

8 thms1 active userReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

A Mean Field Game of Optimal Portfolio Liquidation 2: The Value Functions of the Penalized Mean Field Games Converge in L¹ to the Value Function of the Liquidation-Constrained GameResearch Paper

Motivation

Optimal portfolio liquidation asks how a trader should unwind a position of $\mathcal X$ shares over a horizon $[0,T]$ when trading moves prices. Since Almgren and Chriss (2001) the standard model charges a quadratic cost $\eta_t\xi_t^2$ for trading at rate $\xi_t$ (temporary impact) and a risk penalty $\lambda_tX_t^2$ on the open position, and imposes the liquidation constraint $X_T=0$ . When many traders liquidate at once, each one's costs also depend on the others' aggregate trading rate $\mu_t$ through a permanent impact term $\kappa_t\mu_tX_t$ . Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and prove that, under a weak-interaction condition, the game has a unique equilibrium.

The liquidation constraint makes the problem singular: the value function blows up at $T$ , and the equilibrium is described by a forward-backward system whose decoupling field $A$ satisfies a Riccati BSDE with terminal value $A_T=+\infty$ . A natural question is whether the constraint can be replaced by a finite penalty $nX_T^2$ on the unliquidated position, a non-singular problem of the type studied in the MFG literature, and whether the penalized equilibria approach the constrained one as $n\to\infty$ . Section 4 of the paper answers this at the level of values. In the single-agent case, singular terminal conditions of this type were studied by Ankirchner, Jeanblanc and Kruse (SIAM J. Control Optim., 2014) and Graewe, Horst and Séré (Stochastic Process. Appl., 2018), references [3] and [28] of the paper.

Setting

Fix $T>0$ , an $m$ -dimensional Brownian motion $\widetilde W=(W^0,W)$ whose first coordinate $W^0$ is common noise, and an initial position $\mathcal X\in L^2$ independent of $\widetilde W$ . Let $\mathbb F^0$ be the filtration of $W^0$ and $\mathbb F$ that of $(\mathcal X,\widetilde W)$ , both augmented. The coefficients $\kappa,\lambda,\eta$ are bounded, nonnegative, $\mathbb F$ -progressive processes, with $\lambda$ and $\eta$ bounded below by positive constants. Write $\kappa_{\max}$ , $\eta_\star$ , $\lambda_\star$ for the essential supremum of $\kappa$ and the essential infima of $\eta$ and $\lambda$ , $\|\eta\|$ for the essential supremum of $|\eta|$ , and $\alpha=\eta_\star/\|\eta\|\in(0,1]$ . Assumption 2.3 adds the weak-interaction condition: some $\theta>0$ satisfies $\kappa_{\max}<4\eta_\star\theta$ and $\theta\kappa_{\max}<4\lambda_\star$ .

Given an aggregate rate $\mu$ , a trading rate $\xi\in L^2_{\mathbb F}$ yields the position $X^\xi_t=\mathcal X-\int_0^t\xi_s\,ds$ . The constrained problem minimizes

J(\mathcal X,\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_s\mu_sX^\xi_s+\eta_s\xi_s^2+\lambda_s(X^\xi_s)^2\big)ds\,\Big|\,\mathcal X\Big]

over $\xi$ with $\int_0^T\xi_s\,ds=\mathcal X$ ; its value is $V(\mathcal X;\mu)$ . The penalized problem (4.1) drops the constraint and minimizes

J^n(\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_t\mu_tX^\xi_t+\eta_t\xi_t^2+\lambda_t(X^\xi_t)^2\big)dt+n(X^\xi_T)^2\,\Big|\,\mathcal X\Big]

over all $\xi\in L^2_{\mathbb F}$ , with value $V^n(\mathcal X;\mu)$ . An equilibrium is a fixed point $\mu_t=\mathbb E[\xi^*_t|\mathcal F^0_t]$ .

The constrained equilibrium is given by the FBSDE (2.3), $dX_t=-\frac{Y_t}{2\eta_t}dt$ , $-dY_t=\big(\kappa_t\mathbb E[\frac{Y_t}{2\eta_t}|\mathcal F^0_t]+2\lambda_tX_t\big)dt-Z_t\,d\widetilde W_t$ , $X_0=\mathcal X$ , $X_T=0$ , decoupled as $Y=AX+B$ where

-dA_t=\Big(2\lambda_t-\frac{A_t^2}{2\eta_t}\Big)dt-Z^A_t\,d\widetilde W_t,\qquad A_T=+\infty .

The penalized equilibria are given by the FBSDE (4.2) with $Y^n_T=2nX^n_T$ , decoupled by $A^n$ , the solution of the same Riccati BSDE with $A^n_T=2n$ . The solutions live in weighted spaces: $\mathcal H_l$ with norm $\big(\mathbb E\sup_t|Y_t/(T-t)^l|^2\big)^{1/2}$ , and the penalized analogue $\mathcal H^n_l$ with weight $(T-t+\eta_\star/n)^{-l}$ . Assumption 4.1 requires a constant $C$ with $\exp\big(-\int_r^s\frac{A_u}{2\eta_u}du\big)\le C\frac{T-s}{T-r}$ for all $0\le r\le s<T$ , almost surely.

Formalization targets

Goal: Theorem 4.6

Under Assumptions 2.3 and 4.1, with $\mu^*=\mathbb E[Y/(2\eta)|\mathcal F^0]$ the constrained equilibrium and $\mu^n=\mathbb E[Y^n/(2\eta)|\mathcal F^0]$ the penalized ones,

\lim_{n\to\infty}\mathbb E\big|V^n(\mathcal X;\mu^n)-V(\mathcal X;\mu^*)\big|=0 .

Milestones

Lemma 4.2 (first condition). If $\eta$ is deterministic, Assumption 4.1 holds.
Lemma A.3. $A^n$ exists uniquely, $A^n_t\ge\big(\frac1{2n}+\mathbb E[\int_t^T\frac{ds}{2\eta_s}|\mathcal F_t]\big)^{-1}$ , $A^n\uparrow A$ , and $\|A^n\|_{\mathcal M_{-1}}+\|A^n\|_{\mathcal M^n_{-1}}\le\mathfrak C$ uniformly in $n$ .
Theorem 4.3. The FBSDE (4.4), with parameter $\mathfrak p\in[0,1]$ and data $f\in L^2$ , has a unique solution in $\mathcal H^n_\alpha\times\mathcal H^n_\gamma\times S^2\times L^2\times L^2$ .
Lemma 4.4. $\|X^n\|_{n,\alpha}+\|B^n\|_{n,\gamma}+\mathbb E\int_0^T|Y^n_t|^2dt\le\overline{\mathfrak C}$ uniformly in $n$ .
(4.8). Under Assumption 4.1 the constrained equilibrium position satisfies $\|X^*\|_1<\infty$ .
Lemma 4.5. $(X^n,B^n,Y^n)\to(X,B,Y)$ in $L^2(dt\otimes d\mathbb P)$ .

Significance

The result is a consistency statement between two models of liquidation. Penalized models are what a numerical scheme or a standard MFG solver can handle, since their FBSDEs have finite terminal data. Theorem 4.6 says that equilibrium values computed with a large penalty approximate the value of the hard-constrained game, and Lemma 4.5 says the same for positions and trading rates. Without it, a penalized model would be an unrelated object rather than an approximation of the constrained one.

The result is proved in the paper; it is not formalized anywhere. A machine-checked development would need, beyond the paper, the theory of quadratic BSDEs with finite and singular terminal values, conditional mean-field FBSDEs with common noise, and conditional essential infima of control problems. The milestones isolate reusable pieces: the monotone approximation of a singular Riccati BSDE (Lemma A.3) and uniform estimates in $n$ -dependent weighted spaces (Lemma 4.4).

Difficulty

The obvious argument compares the two problems control by control: the constrained optimizer is admissible for the penalized problem, so $V^n\le V$ up to the change of $\mu$ . The reverse inequality is where it fails. The penalized optimizer leaves a residual position $X^n_T\neq0$ , and its cost has to be compared with the singular one, whose weight $(T-t)^{-1}$ explodes at $T$ . Controlling this requires estimates uniform in $n$ in spaces whose weights $(T-t+\eta_\star/n)^{-l}$ degenerate as $n\to\infty$ , and the bare exponent $\alpha=\eta_\star/\|\eta\|<1$ of the constrained problem is not enough to make the boundary terms vanish. Assumption 4.1, which upgrades the state to $\mathcal H_1$ , is what closes the gap. In addition, the aggregate rate $\mu^n$ changes with $n$ , so both the controls and the cost functional move at once.

Formalization scope

Time is $\mathbb R_{\ge0}$ ; processes are real-valued functions of $(t,\omega)$ ; $W$ is the $m=k+1$ -dimensional $\widetilde W$ with coordinate $0$ the common noise. Stochastic integrals and BSDEs come from the published definition Peng1990.SMP.Stochastic. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$ , $\tau<T$ ; $A_T=+\infty$ is $\lim_{t\uparrow T}A_t=+\infty$ a.s. Conditional expectations inside drivers are $\mathbb F^0$ -progressive versions of integrable processes. Weighted norms are computed in $[0,\infty]$ . The explicit readings are:

$\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$ ; (2.4) is stated without division; " $1/\lambda,1/\eta\in L^\infty$ " is a positive essential lower bound.
Assumption 2.3 is a hypothesis of every statement, including Lemma A.3 (the appendix assumes only its boundedness part).
Assumption 4.1 holds almost surely with the constant chosen before $\omega$ (as restated on p. 32).
The penalty index is an integer $n\ge1$ ; constants in Lemma A.3 and Lemma 4.4 are chosen before $n$ .
The class of $A^n$ is $S^2\times L^2$ on $[0,T]$ (not printed in Lemma A.3).
The penalized control set is $L^2_{\mathbb F}$ , with no terminal constraint.
Values are conditional essential infima given $\sigma(\mathcal X)$ .
The equilibria $\mu^n,\mu^*$ of Theorem 4.6 are defined through the FBSDE solutions, as in the proof; uniqueness of penalized equilibria is not claimed.
The solution of Proposition 2.8 includes the relation $Y=AX+B$ on $[0,T)$ ; "Theorem 2.8" on pp. 25–29 means Proposition 2.8.
$L^1$ convergence means $\int|V^n-V|\,d\mathbb P\to0$ , not convergence of expectations.

A trivializing formalization would quantify over all solutions of the penalized MFG (claiming a uniqueness the paper does not state) or define $V$ by a pointwise infimum over all controls (which is $-\infty$ or junk); both are ruled out above. Contributions toward BSDE comparison principles and quadratic BSDE well-posedness on this stochastic-integral layer are welcome and reusable.

Selected references

G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, Math. Oper. Res. 46(4), 2021; preprint arXiv:1804.04911v3. https://arxiv.org/abs/1804.04911
R. Almgren, N. Chriss, Optimal execution of portfolio transactions, Journal of Risk 3, 2001. https://doi.org/10.21314/JOR.2001.041
S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2):893–913, 2014 (reference [3] of the paper).
P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stochastic Process. Appl. 128(3):979–1006, 2018 (reference [28] of the paper).
S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

11 thms1 active userReviewed

Linear Optimization Machine Learning Operations Research+1·Captain: mikedeng1

Strong Mixed-Integer Programming Formulations for Trained Neural Networks 1: A ReLU Neuron over a Box Has an Ideal Formulation with One Binary Variable and the Exponential Family (6b)Research Paper

Why optimize over a trained ReLU neuron

A trained feed-forward neural network with ReLU activations, $\mathrm{ReLU}(v)=\max\{0,v\}$ , is a piecewise linear function of its input. Many tasks ask for an optimization over such a network with its weights held fixed: verifying that no small perturbation of an image changes its classification, finding adversarial examples, or embedding a learned model of demand or cost inside a decision problem ("predict, then optimize"). The standard way to solve such problems exactly is mixed-integer programming (MIP): each neuron is written as a small set of linear constraints with one binary variable, and the network is the composition of these neuron formulations. How strong each neuron formulation is decides how fast branch-and-bound can close the gap.

The formulation used in the literature up to 2018 is the big-M formulation. It is valid but weak. This mission formalizes the main result of Anderson, Huchette, Tjandraatmadja and Vielma, IPCO 2019 extended abstract (arXiv:1811.08359v2), which gives the strongest possible formulation of a single ReLU neuron that uses the original variables and one binary variable only.

Timeline. Big-M formulations of ReLU networks were used by several groups in 2017–2018 for verification and adversarial analysis (see §1.2 of the paper). Balas's disjunctive programming (1985, 1998) and the multiple choice formulation of piecewise linear functions (Vielma and Nemhauser, Math. Program. 2011) give an ideal formulation of the neuron that needs a copy of the input variables. Anderson et al. (2019) project out that copy and obtain the formulation (6) below; a longer journal version (Math. Program. 2020, with W. Ma) develops the analysis further, including interactions between neurons.

Setting

Fix $\eta\in\mathbb N$ , a weight vector $w\in\mathbb R^\eta$ , a bias $b\in\mathbb R$ , and bounds $L,U\in\mathbb R^\eta$ with $L_i<U_i$ for every $i$ . The neuron computes $\mathrm{ReLU}(f(x))$ for the affine function $f(x)=w\cdot x+b$ on the box $[L,U]=\{x: L\le x\le U\}$ . Its graph is

\operatorname{gr}(\mathrm{ReLU}\circ f;[L,U])=\{(x,\mathrm{ReLU}(f(x))) : L\le x\le U\}.

The sign-adjusted bounds are $\breve L_i=L_i$ , $\breve U_i=U_i$ when $w_i\ge 0$ , and $\breve L_i=U_i$ , $\breve U_i=L_i$ when $w_i<0$ . Then $M^+(f)=w\cdot\breve U+b$ and $M^-(f)=w\cdot\breve L+b$ are the maximum and minimum of $f$ on $[L,U]$ , and $\operatorname{supp}(w)=\{i: w_i\ne 0\}$ . Strict activity means $M^-(f)<0<M^+(f)$ : the neuron is neither always off nor always on. The paper assumes throughout that $L_i<U_i$ and that strict activity holds.

A set $R$ of points $(x,y,z)$ with $z\in[0,1]$ , read together with the constraint $z\in\{0,1\}$ , is a formulation of the graph if $(x,y)$ lies on the graph exactly when $(x,y,z)\in R$ for some $z\in\{0,1\}$ ; $R$ is then its LP relaxation. The formulation is ideal if every extreme point of $R$ has $z\in\{0,1\}$ .

The big-M formulation (3) is $y\ge f(x)$ , $y\le f(x)-M^-(f)(1-z)$ , $y\le M^+(f)z$ , $(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}$ . The formulation of Proposition 1 is

\begin{aligned} &y\ge w\cdot x+b &&(6a)\\ &y\le\sum_{i\in I}w_i\bigl(x_i-\breve L_i(1-z)\bigr)+\Bigl(b+\sum_{i\notin I}w_i\breve U_i\Bigr)z\qquad\forall I\subseteq\operatorname{supp}(w) &&(6b)\\ &(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}. &&(6c) \end{aligned}

Formalization targets

Goal: Proposition 1 (p. 6)

\text{(6a)–(6c) is a formulation of }\operatorname{gr}(\mathrm{ReLU}\circ f;[L,U]),\ \text{and every extreme point of its LP relaxation has } z\in\{0,1\}.

Milestones (Appendix A.1 and §2.2)

The multiple choice formulation (5), with copies $x^0,x^1,y^0,y^1$ , has only integral $z$ at extreme points in its lifted space and formulates the graph; projected to $(x,y,z)$ , its LP relaxation is the convex hull of its points with $z\in\{0,1\}$ (§2.2, pp. 5–6).
Projecting the copies out of the LP relaxation of (5) gives the linear system (7): (6a), (6b), a second exponential family (7c), and the bounds (7d) (App. A.1, p. 14).
The family (7c) is implied by the other constraints (App. A.1, pp. 14–15).
The LP relaxation of (6) is the convex hull of its points with $z\in\{0,1\}$ (App. A.1, p. 14).

Companion results

$M^\pm(f)$ are the maximum and minimum of $f$ on $[L,U]$ (§1.3, p. 4).
Proposition 3 (p. 7): for $(\hat x,\hat y,\hat z)\in[L,U]\times\mathbb R_{\ge0}\times[0,1]$ , if some inequality of (6b) is violated, the one for $\hat I=\{i\in\operatorname{supp}(w): w_i\hat x_i<w_i(\breve L_i(1-\hat z)+\breve U_i\hat z)\}$ is the most violated.
The big-M formulation (3) is a formulation of the graph (p. 4); Examples 1 and 2 (p. 5) show that it is not ideal and that its gap grows like $\tfrac12\gamma\eta$ ; its inequalities (3b), (3c) are (6b) for $I=\operatorname{supp}(w)$ and $I=\emptyset$ (p. 7).

Significance

Proposition 1 says that the convex hull of the graph, lifted with one binary variable, is described by (6a), (6b) and the bounds, with no auxiliary continuous variables. Optimizing a linear function over the LP relaxation of (6) therefore gives the tightest convex relaxation available for a single neuron, and Proposition 3 gives a separation routine linear in $\eta$ , so the exponential family can be added on demand to a big-M model. The paper's experiments (§3, not formalized) report that separating over (6b) solves smaller MNIST verification instances faster than Gurobi's default cut generation by a factor of 7.

The result is proved in the paper; nothing here is open. To our knowledge none of these statements has a machine-checked proof. The work this mission asks for is the formalization of the known proof: an ideality statement for the multiple choice formulation, a Fourier–Motzkin projection carried out for an arbitrary index set with general-sign weights, and the passage from a hull identity to integrality of extreme points.

Difficulty

The formulation half of Proposition 1 is a short case analysis on $z\in\{0,1\}$ ; the content is ideality. The obvious attempt, characterizing the extreme points of the LP relaxation of (6) directly, is impractical: the polytope is cut out by $2^{|\operatorname{supp}(w)|}$ inequalities, and showing that every point with fractional $z$ is a proper convex combination of feasible points means handling all patterns of tight inequalities of (6b) at once. Ideality of the extended formulation (5) is classical and passes to its projection onto $(x,y,z)$ , but that only helps once the projection is known to be exactly the LP relaxation of (6): it has to be computed for an arbitrary index set, and every inequality it produces must be shown to be one of (6a), (6b), the bounds, or implied by them. Weights of both signs must be handled throughout: the page treats negative weights by a change of variables, and a formal development has to carry the sign-adjusted bounds $\breve L,\breve U$ through every step.

Formalization scope

Inputs $x\in\mathbb R^\eta$ are Fin η → ℝ, so indices are 0-based; points $(x,y,z)$ are (Fin η → ℝ) × ℝ × ℝ. A formulation is encoded by its LP relaxation $R$ (with $z\in[0,1]$ ) and the predicate " $(x,y)\in S$ iff $(x,y,z)\in R$ for some $z\in\{0,1\}$ "; ideality is ∀ p ∈ Set.extremePoints ℝ R, p.2.2 = 0 ∨ p.2.2 = 1. $M^\pm(f)$ are defined by their closed forms, and a companion theorem proves that they are the maximum and minimum. In (6b) and (7c), " $i\notin I$ " ranges over all indices outside $I$ , zero weights included. The system (7) is stated with $\breve L,\breve U$ , i.e. after undoing the page's substitution $\tilde x_i=-x_i$ ; for $w\ge 0$ it is the page's display. The LP relaxation of (5) is represented both in its lifted space and projected to $(x,y,z)$ , with the copies quantified existentially in the latter, and constant $b$ is scaled by $1-z$ in (5b) and by $z$ in (5c).

The goal carries both standing assumptions of §1.3 ( $L_i<U_i$ and strict activity) and nothing else. Milestones that do not need strict activity omit it, which makes them stronger. Example 2 includes the page's $\gamma=0$ boundary: although its box then violates $L_i<U_i$ when $\eta>0$ , the example's three stated claims remain true.

Ideality is a statement about the LP relaxation, not about the set with $z\in\{0,1\}$ : applied to the latter it would hold trivially, and a goal stating only that (6) is a formulation would omit the result's content. Both are ruled out by the statement of the goal.

A complete development needs: extreme points and convex hulls of polyhedra in product spaces (Mathlib), the hull of a union of two polytopes as a projection, Fourier–Motzkin elimination over an arbitrary finite index set, and finite-sum manipulations over subsets of $\operatorname{supp}(w)$ . The Fourier–Motzkin and disjunctive-hull lemmas are reusable well beyond this mission; contributions of either are welcome, as are proofs of the companion results.

Source: the IPCO 2019 extended abstract, arXiv:1811.08359v2 (28 Feb 2019); all labels and pages refer to that version.

Selected references

R. Anderson, J. Huchette, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, IPCO 2019 (LNCS 11480), extended abstract. arXiv:1811.08359v2
R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, Mathematical Programming 183 (2020) 3–39. doi:10.1007/s10107-020-01474-5, arXiv:1811.01988
J. P. Vielma, G. Nemhauser, Modeling disjunctive constraints with a logarithmic number of binary variables and constraints, Mathematical Programming 128 (2011) 49–72. doi:10.1007/s10107-009-0295-4
E. Balas, Disjunctive programming and a hierarchy of relaxations for discrete optimization problems, SIAM Journal on Algebraic and Discrete Methods 6(3) (1985) 466–486. doi:10.1137/0606047
E. Balas, Disjunctive programming: properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998) 3–44. doi:10.1016/S0166-218X(98)00136-X
J. P. Vielma, Mixed integer linear programming formulation techniques, SIAM Review 57(1) (2015) 3–57. doi:10.1137/130915303

7 thms1 active userReviewed

Convex Optimization Optimization·Captain: mikedeng1

A Block Successive Upper-Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization 1: Cyclic BSUM-M Converges to Primal-Dual Optimal SolutionsResearch Paper

Motivation

Many problems in signal processing, machine learning and power systems have the form of a convex objective that is a sum of a smooth coupled term and nonsmooth block-separable terms, minimized subject to linear equality constraints that couple $K$ blocks of variables: basis pursuit, demand response control in smart grids, and distributed estimation are the examples of Hong, Chang, Wang, Razaviyayn, Ma, Luo. The alternating direction method of multipliers (ADMM) handles two blocks well, but for $K\ge3$ blocks the directly extended Gauss–Seidel ADMM can diverge (Chen, He, Ye, Yuan, 2016), and convergence proofs for multi-block schemes usually need strong convexity or extra correction steps.

The block successive upper-bound minimization method of multipliers (BSUM-M) is the paper's answer: each block is updated by minimizing a local upper bound of the augmented Lagrangian, which makes the subproblems simple (for instance closed-form proximal steps), and the multiplier is updated by a dual gradient step with a small or diminishing stepsize. The main theorem shows that this scheme converges to primal and dual optimal solutions for any number of blocks without strong convexity, under an error bound.

Setting

The variable is $x=(x_1,\dots,x_K)$ , $x_k\in\mathbb R^{n_k}$ , with the Euclidean norm $\|x\|^2=\sum_k\|x_k\|^2$ . Problem (1.1) is

\min_x\ f(x)=g(x)+\sum_{k=1}^K h_k(x_k)\quad\text{s.t.}\quad Ex=\sum_{k=1}^KE_kx_k=q,\quad x_k\in X_k .

Under the standing Assumption A, $g(x)=\ell(Ax)+\langle x,b\rangle$ with $\ell$ strictly convex and continuously differentiable and $A$ any matrix; $h_k(x_k)=\lambda_k\|x_k\|_1+\sum_Jw_J\|x_{k,J}\|_2$ is a mixed $\ell_1/\ell_2$ norm with nonnegative weights; each $X_k=\{x_k\mid C_kx_k\le c_k\}$ is a compact polyhedron and $X=\prod_kX_k$ ; the problem is feasible and the dual optimal value is attained.

For $\rho>0$ , the augmented Lagrangian is $L(x;y)=f(x)+\langle y,q-Ex\rangle+\frac\rho2\|q-Ex\|^2$ , the augmented dual is $d(y)=\min_{x\in X}L(x;y)$ , and $X(y)=\arg\min_{x\in X}L(x;y)$ . For $x\in X$ , $\bar x$ denotes the point of $X(y)$ nearest to $x$ .

Assumption B concerns the approximation functions $u_k(v_k;x)$ : each upper-bounds $G(x)=g(x)+\frac\rho2\|Ex-q\|^2$ along block $k$ , is tight with matching gradient at $v_k=x_k$ , is continuous, strongly convex in $v_k$ with a uniform modulus $\gamma_k>0$ , and has an $L_k$ -Lipschitz gradient in $v_k$ .

BSUM-M (1.12). From $x^1\in X$ and any $y^1$ , for $r\ge1$ :

y^{r+1}=y^r+\alpha^r(q-Ex^r),\qquad x_k^{r+1}=\arg\min_{x_k\in X_k}u_k(x_k;w_k^{r+1})-\langle y^{r+1},E_kx_k\rangle+h_k(x_k),

for $k=1,\dots,K$ in order, with the Gauss–Seidel point $w_k^{r+1}=(x_1^{r+1},\dots,x_{k-1}^{r+1},x_k^r,\dots,x_K^r)$ .

The proximal gradient is $\tilde\nabla_xL(x;y)=x-\operatorname{prox}(x-\nabla_x(L(x;y)-h(x)))$ with $\operatorname{prox}(z)=\arg\min_{u\in X}h(u)+\frac12\|z-u\|^2$ . The error bound asks for $\tau>0$ with $\operatorname{dist}(x,X(y))\le\tau\|\tilde\nabla_xL(x;y)\|$ for all $x\in X$ and all $y$ .

Formalization targets

Goal: Theorem 2.1, part 1

Under Assumptions A and B and the error bound, there is $\bar\alpha>0$ such that for stepsizes $\alpha^r>0$ that are either constant with $\alpha^r=\alpha\le\bar\alpha$ , or satisfy $\sum_r\alpha^r=\infty$ and $\alpha^r\to0$ , every BSUM-M run satisfies

\lim_{r\to\infty}\|Ex^r-q\|=0,\qquad\lim_{r\to\infty}\|x^r-x^{r+1}\|=0,\qquad\lim_{r\to\infty}\|x^r-\bar x^r\|=0,

and every limit point of $\{(x^r,y^r)\}$ is a primal and dual optimal solution. The threshold $\bar\alpha$ is not specified; no rate is claimed.

Milestones

Lemma 2.3(1) (one sweep decreases $L(\cdot;y^{r+1})$ by $\gamma\|x^r-x^{r+1}\|^2$ ), Lemma 2.5(1) (dual gap decrease), Lemma 2.6(1) (primal gap bound), Lemma 2.4(1) (the proximal gradient at $x^r$ is $O(\|x^{r+1}-x^r\|)$ ) and Lemma 2.1 (differentiability of $d$ , $\nabla d(y)=q-Ex(y)$ , and Lipschitz continuity of $\nabla d$ on superlevel sets).

Significance

The theorem gives a convergent multi-block method of multipliers whose block subproblems may be replaced by any majorizer satisfying Assumption B, such as a linearized proximal step. It covers the cyclic Gauss–Seidel order, where the direct multi-block ADMM can fail, and it does not require strong convexity of $f$ (the matrix $A$ need not have full column rank). The paper's randomized variant (part 2 of the same theorem) is a separate mission.

The result is proved in the paper (the proof of part 1 is described as following the steps written out for part 2). It has not been machine-checked. Formalization adds a verified account of the potential-function argument for a primal-dual method with inexact block updates, and checks three printed statements that need correction (see the scope section): a formal proof settles them.

Difficulty

The obvious approach is to treat BSUM-M as an inexact dual gradient ascent on $d$ , but a single Gauss–Seidel sweep does not compute $x(y^{r+1})\in X(y^{r+1})$ , so the dual step uses a gradient at the wrong point. Controlling that error requires relating the primal step length to the distance from $X(y)$ , which fails without an error bound: $L(\cdot;y)$ is not strongly convex, $X(y)$ need not be a singleton, and the proximal gradient can be small far from $X(y)$ . The cyclic order adds a second gap: block $k$ is linearized at $w_k^{r+1}$ , not at $x^r$ . With a constant stepsize the dual ascent must not outrun the primal descent, which is where the smallness threshold enters.

Formalization scope

Citation basis: the arXiv preprint arXiv:1401.7079v1 (28 Jan 2014); every index refers to that version, not to the revised journal version (Mathematics of Operations Research, 2020).

Representation: blocks are indexed by Fin K with $K\ge1$ ; the block space is PiLp 2 of Euclidean spaces (the Euclidean norm, not the sup norm). $\ell$ is real valued and $C^1$ on all of $\mathbb R^p$ , which specializes the paper's extended-valued $\ell$ . $d$ , $d^*$ and $f^*$ are real infima and suprema over nonempty compact sets, where they are attained. The algorithm is a predicate on sequences indexed from $r=1$ ; argmin steps are minimality conditions, the minimizer being unique. The initial point is required to lie in $X$ . "Sufficiently small" is an existential threshold quantified before the stepsizes and the run. $\|x^r-\bar x^r\|$ is the distance from $x^r$ to $X(y^r)$ . Limit points are cluster points of the joint sequence; boundedness of $\{y^r\}$ is neither assumed nor concluded.

Interpretations and corrections, each labelled in the item's statement:

the proximity operator in (2.3) includes the constraint set $X$ , as the paper's optimality relation (2.14) requires;
$d(y)$ is $\min_{x\in X}L(x;y)$ ; (1.9) prints $g(x)$ and an unconstrained minimum;
(2.17) has $Ex^r$ where its proof (2.19) has $Ex^{r-1}$ ; the proved inequality is stated;
(2.12) evaluates the proximal gradient at $y^r$ and is false at $r=1$ ; it is stated at $y^{r+1}$ ;
Lemma 2.1's clause " $A_kx_k$ constant on $X(y)$ " fails for non-separable $\ell$ ; it is stated as " $Ax$ constant".

The error bound is a hypothesis of the goal, as in the paper, and is not derived from Assumption A: the paper's Lemma 2.2 does not hold under Assumption A alone. A formalization that makes the hypotheses unsatisfiable, drops the run's dependence on $y^{r+1}$ , or lets $\bar\alpha$ depend on the run is not this theorem. A sanity check that the hypotheses are satisfiable (a one-block instance with a constant run) is part of the drafting record.

Infrastructure needed: proximity operators of convex functions restricted to polyhedra and their nonexpansiveness; Danskin-type differentiability of a parametric minimum over a compact set; smoothness of the augmented dual; elementary convergence lemmas for nonnegative sequences with summable decrements. These pieces are reusable for other augmented Lagrangian and ADMM analyses. Proofs of the milestones are welcome independently of the goal.

Selected references

M. Hong, T.-H. Chang, X. Wang, M. Razaviyayn, S. Ma, Z.-Q. Luo, A Block Successive Upper Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization, arXiv:1401.7079v1, 2014; Mathematics of Operations Research 45(3), 2020. https://arxiv.org/abs/1401.7079 , https://doi.org/10.1287/moor.2019.1010
M. Hong, Z.-Q. Luo, On the linear convergence of the alternating direction method of multipliers, Mathematical Programming 162, 2017. https://doi.org/10.1007/s10107-016-1034-2
M. Razaviyayn, M. Hong, Z.-Q. Luo, A unified convergence analysis of block successive minimization methods for nonsmooth optimization, SIAM Journal on Optimization 23(2), 2013. https://doi.org/10.1137/120891009
C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155, 2016. https://doi.org/10.1007/s10107-014-0826-5

7 thms1 active userReviewed

Analysis Functional Analysis Probability·Captain: mikedeng1

Bakry–Émery Curvature-Dimension Condition and Riemannian Ricci Curvature Bounds 1: The Weak, Pointwise and Gradient Forms of the Bakry–Émery Condition BE(K,N) Are EquivalentResearch Paper

Motivation

On a Riemannian manifold, a lower bound $\mathrm{Ric}\ge K$ together with a dimension bound $N$ can be read off from the heat flow alone. This is the Bakry–Émery curvature-dimension condition $BE(K,N)$ : Bochner's inequality $\Gamma_2(f)\ge K\,\Gamma(f)+\tfrac1N(\Delta f)^2$ for the iterated carré du champ. The condition makes sense for any diffusion: weighted manifolds, infinite-dimensional Gaussian spaces, and limits of manifolds where no Ricci tensor exists. For this reason it is one of the two main routes to synthetic curvature bounds, the other being the optimal-transport conditions of Lott–Villani and Sturm. Bakry–Émery 1985; Bakry–Gentil–Ledoux 2014.

Ambrosio, Gigli and Savaré prove that, on metric measure spaces, $BE(K,\infty)$ for the Cheeger energy is equivalent to the transport condition $RCD(K,\infty)$ . Their first step (§2.2) is to state $BE(K,N)$ for an abstract Dirichlet form, in a weak form and under minimal regularity, and to show that the usual ways of writing it are equivalent. That equivalence, Corollary 2.3, is the subject of this mission. Every later section of the paper and the remaining missions of this series use one of its forms. arXiv:1209.5786v4, §2.2, pp. 14–20.

Setting

Let $(X,\mathcal B)$ be a measurable space with a $\sigma$ -additive measure $m$ .

A symmetric Dirichlet form is a functional $\mathcal E:L^2(X,m)\to[0,\infty]$ that is quadratic and $L^2$ -lower semicontinuous, satisfies $\mathcal E(\eta\circ f)\le\mathcal E(f)$ for every 1-Lipschitz $\eta$ with $\eta(0)=0$ , and has a dense domain $\mathbb V=\{f:\mathcal E(f)<\infty\}$ .
Write $\mathcal E(f,g)$ for its bilinear form and $\mathbb V_\infty=\mathbb V\cap L^\infty$ .
$\mathcal E$ is strongly local if $\mathcal E(f,g)=0$ whenever $(f+a)g=0$ a.e. for some constant $a$ .
The generator $\Delta_{\mathcal E}$ is defined by $\mathcal E(f,g)=-\int_X g\,\Delta_{\mathcal E}f\,dm$ for all $g\in\mathbb V$ , and the heat flow $\mathsf P_t$ solves $\partial_t\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$ with $\mathsf P_tf\to f$ in $L^2$ . By contraction, $\mathsf P_t$ extends to $L^1(X,m)$ .

For $f,g,\varphi\in\mathbb V_\infty$ set

\Gamma[f,g;\varphi]=\tfrac12\big(\mathcal E(f,g\varphi)+\mathcal E(g,f\varphi)-\mathcal E(fg,\varphi)\big),\qquad \Gamma[f;\varphi]=\Gamma[f,f;\varphi].

By continuity, this extends to $f,g\in\mathbb V$ , $\varphi\in\mathbb V_\infty$ . The set $\mathbb G$ consists of those $f\in\mathbb V$ for which $\varphi\mapsto\Gamma[f;\varphi]$ has a density $\Gamma(f)\in L^1_+(X,m)$ , the carré du champ. The iterated form is

\Gamma_2[f;\varphi]=\tfrac12\Gamma[f;\Delta_{\mathcal E}\varphi]-\Gamma[f,\Delta_{\mathcal E}f;\varphi].

Along the heat flow, for $t>0$ and $s\in[0,t]$ , set

\mathsf A_t[f;\varphi](s)=\tfrac12\!\int_X(\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,dm,\qquad \mathsf A^\Delta_t[f;\varphi](s)=\tfrac12\!\int_X(\Delta_{\mathcal E}\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,dm,

$\mathsf B_t[f;\varphi](s)=\Gamma[\mathsf P_{t-s}f;\mathsf P_s\varphi]$ and $\mathsf C_t[f;\varphi](s)=\Gamma_2[\mathsf P_{t-s}f;\mathsf P_s\varphi]$ . Finally $I_K(t)=\int_0^te^{Ks}ds$ , $I_{K,2}(t)=\int_0^tI_K(s)ds$ , and $\nu=1/N\ge0$ .

Formalization targets

Goal: Corollary 2.3

Let $K\in\mathbb R$ and $\nu\ge0$ . The following are equivalent:

(i) $\Gamma_2[f;\varphi]\ge K\Gamma[f;\varphi]+\nu\int_X(\Delta_{\mathcal E}f)^2\varphi\,dm$ for every $(f,\varphi)\in D(\Gamma_2)$ with $\varphi\ge0$ ;
(ii) $\mathsf C_t[f;\varphi](s)\ge K\mathsf B_t[f;\varphi](s)+2\nu\mathsf A^\Delta_t[f;\varphi](s)$ for $0\le s<t$ ;
(iii) the distributional inequality

\partial_s^2\mathsf A_t[f;\varphi]\ge2K\,\partial_s\mathsf A_t[f;\varphi]+4\nu\,\mathsf A^\Delta_t[f;\varphi]\quad\text{in }\mathscr D'(0,t);

(iv) $\mathsf P_tf\in\mathbb G$ and $I_{2K}(t)\Gamma(\mathsf P_tf)+2\nu I_{2K,2}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le\tfrac12\mathsf P_t(f^2)-\tfrac12(\mathsf P_tf)^2$ a.e.;
(v) $\mathbb G=\mathbb V$ and, for $f\in\mathbb V$ , $t>0$ , $\tfrac12\mathsf P_t(f^2)-\tfrac12(\mathsf P_tf)^2+2\nu I_{-2K,2}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le I_{-2K}(t)\mathsf P_t\Gamma(f)$ a.e.;
(vi) $\mathbb G$ is dense in $L^2$ , and for $f\in\mathbb G$ , $t>0$ ,

\Gamma(\mathsf P_tf)+2\nu I_{-2K}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le e^{-2Kt}\mathsf P_t\Gamma(f)\quad\text{a.e.}

Any of them implies $\mathbb G=\mathbb V$ . Condition (iii) is the paper's definition of $BE(K,N)$ (Definition 2.4).

Milestones

Lemma 2.1, in four parts:
- $\mathsf A$ is continuous, $\mathsf A^\Delta$ is continuous, and $\partial_s\mathsf A=\mathsf B$ (2.25);
- $\mathsf A$ and $\mathsf A^\Delta$ are monotone for $\varphi\ge0$ ;
- $\partial_s\mathsf B=2\mathsf C$ (2.26).
Lemma 2.2: four equivalent forms of the scalar inequality $a''\ge2Ka'+\nu g$ .
Its integrated consequences (2.30) and (2.31).

Significance

The result. Condition (i) is the classical Bochner inequality. (iii) is the form that survives limits and is used as a definition. (iv), (v) and (vi) are pointwise estimates for the heat flow: the reverse and the local Poincaré inequalities, and the Bakry–Émery gradient bound $\Gamma(\mathsf P_tf)\le e^{-2Kt}\mathsf P_t\Gamma(f)$ . Section 3 of the paper uses (vi) to obtain Lipschitz regularization and to identify the intrinsic distance. Section 4 uses (iii) with $\nu=0$ to prove the $RCD(K,\infty)$ property. The conclusion $\mathbb G=\mathbb V$ means that a $BE$ form automatically admits a carré du champ on its whole domain, so $\Gamma$ -calculus is available without extra assumptions.

Formalizing it. The equivalences are classical for smooth diffusions with an algebra of nice functions. The paper's contribution is to prove them for an arbitrary strongly local Dirichlet form, where no such algebra is assumed. The result is proved; it is not formalized. The mission produces a Lean interface for Dirichlet forms, their heat flows, the extended $\Gamma$ and $\Gamma_2$ , and the six conditions. Proofs of the milestones and of the goal are open.

Difficulty

The obvious argument differentiates $s\mapsto\mathsf A_t[f;\varphi](s)$ twice and reads off $\mathsf A''=2\Gamma_2$ . That requires $f$ , $\varphi$ and $\Delta_{\mathcal E}\varphi$ to be smooth enough for every term to be defined. For a general $f\in L^2$ only the first derivative exists, as $\Gamma[\cdot;\cdot]$ on $\mathbb V\times\mathbb V_\infty$ , and only through the continuity extension (2.20). The weak forms must therefore be reached by truncation and semigroup mollification.

The passage from the integrated inequality (iv) to the existence of the density $\Gamma(\mathsf P_tf)$ is not a computation either. It needs a Daniell-type construction of a measure from a positive functional on $\mathbb V_\infty$ . The converse directions, from (iv) or (vi) back to (iii), require a second-order Taylor expansion in time of quantities whose regularity is only that of Lemma 2.1.

Formalization scope

Representation. An element of $L^2$ is a function with MemLp f 2 m, and every predicate is invariant under a.e. equality. $\mathcal E$ takes values in $[0,\infty]$ , with $\infty$ off $L^2$ . The completion of $\mathcal B$ is not modelled.
Binders. The heat flow and its $L^1$ extension are binders, pinned by characterizing predicates. Generator values and carré du champ densities are witnesses, which are unique a.e.
Γ and Γ₂. They are predicates "the value is $c$ ": approximating sequences exist, and along each of them $\Gamma$ converges to $c$ . The paper defines $\Gamma$ only on $\mathbb V\times\mathbb V\times\mathbb V_\infty$ , so $\Gamma_2[f;\varphi]$ is undefined when $\Delta_{\mathcal E}\varphi\notin\mathbb V$ , and (i)–(ii) are required wherever it is defined.
Weak forms. Distributional inequalities are tested against nonnegative smooth functions compactly supported in $(0,t)$ , after integration by parts. This avoids derivatives at points where none exists.
Standing assumptions and constants. The strong locality and density assumptions of (2.1) are standing binders; there is no topology and no mass preservation. $K\in\mathbb R$ is free and $\nu\ge0$ . $I_K$ is defined by its integral, so $K=0$ needs no separate case.
Departures from the page.
- In condition (v) the coefficient of $\mathsf P_t\Gamma(f)$ is $I_{-2K}(t)$ . The page prints $I_{-2K,2}(t)$ , which makes (v) false for small $t$ already for the heat flow on $\mathbb R$ ; the paper's derivation of (v) from (2.31) gives $I_{-2K}(t)$ . (v) is stated for $t>0$ ; at $t=0$ both sides vanish.
- In Lemma 2.2 (iii), test functions are required to be nonnegative, since (2.27) fails for $-\zeta$ .
- In Lemma 2.2 (iv), $s_2<t$ is required.
Not a trivialization. The admissible test classes are nonempty, the conditions are not vacuous, and the hypotheses are satisfiable: the zero form with the identity flow satisfies them and $BE(K,\infty)$ for every $K$ , verified in Lean.
Shared layer. The setting module carries the paper's metric-measure definitions for the series and is reusable for any Dirichlet-form development, as is the interval lemma 2.2.

Proofs of any milestone are welcome. Each proved milestone is usable independently: Lemma 2.2, (2.30) and (2.31) are real-variable statements.

Selected references

L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. Pinned preprint arXiv:1209.5786v4, §2, pp. 10–20.
D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123, 1985. https://doi.org/10.1007/BFb0075847
D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators, Springer, 2014. https://doi.org/10.1007/978-3-319-00227-9

10 thms1 active userReviewed

Functional Analysis Partial Differential Equations Probability·Captain: mikedeng1

From Nonlinear Fokker-Planck Equations to Solutions of Distribution Dependent SDE: Density-Dependent McKean–Vlasov SDEs Have Weak Solutions Whose Marginals Solve the Nonlinear FPEResearch Paper

Motivation

A McKean–Vlasov stochastic differential equation, or distribution dependent SDE, is an SDE whose coefficients depend on the law of the solution itself:

dX(t) = b\big(t, X(t), \mathcal L_{X(t)}\big)\,dt + \sigma\big(t, X(t), \mathcal L_{X(t)}\big)\,dW(t),

where $\mathcal L_{X(t)}$ is the law of $X(t)$ . Such equations describe the limit of large systems of interacting particles (mean-field limits), and they are the probabilistic side of nonlinear Fokker–Planck equations: by Itô's formula the time marginals $\mu_t = \mathcal L_{X(t)}$ solve a Fokker–Planck equation whose coefficients depend on $\mu_t$ .

Most existence theory for McKean–Vlasov SDEs assumes that the coefficients are continuous, often Lipschitz, in the measure argument for a Wasserstein distance. That excludes the Nemytskii-type dependence $b(X(t), u(t, X(t)))$ , where $u(t,\cdot)$ is the density of $\mathcal L_{X(t)}$ evaluated at the current position. This dependence appears in models of nonlinear diffusion and porous media, where the diffusion speed depends on the local concentration. V. Barbu and M. Röckner (arXiv:1808.10706, Ann. Probab. 2020) reverse the usual direction: they first solve the nonlinear Fokker–Planck equation in $L^1$ by nonlinear semigroup theory and then construct the SDE from its solution.

Earlier results covered the case $a_{ij}(x,u) = \delta_{ij}\beta(u)$ , as recorded in Remark 4.2 of the paper. Benachour, Chassaing, Roynette and Vallois (Ann. Sc. Norm. Sup. Pisa, 1996) treated $d = 1$ , $b \equiv 0$ , $\beta(r) = r|r|^{m-1}$ . Blanchard, Röckner and Russo (Ann. Probab. 38, 2010) and Barbu, Röckner and Russo (Probab. Theory Relat. Fields, 2011) treated $d = 1$ , $b \equiv 0$ with irregular $\beta$ , the latter in the degenerate case. Barbu and Röckner (SIAM J. Math. Anal. 50, 2018) treated a maximal monotone $\beta$ with a drift $b(u)$ satisfying (H3)′.

Setting

Let $d \ge 1$ , $x \in \mathbb R^d$ , and let $a_{ij}, b_i : \mathbb R^d \times \mathbb R \to \mathbb R$ , $1 \le i,j \le d$ . The nonlinear Fokker–Planck equation (3.1) is

\frac{\partial u}{\partial t} - \sum_{i,j=1}^d D^2_{ij}\big(a_{ij}(x,u)u\big) + \operatorname{div}\big(b(x,u)u\big) = 0, \qquad u(0,\cdot) = u_0 .

Two sets of hypotheses are considered. (H1)–(H3) (nondegenerate): $a_{ij}$ is $C^2$ , bounded, with bounded $x$ -gradient, symmetric; $\sum_{i,j}(a_{ij} + u\,\partial_ua_{ij})\xi_i\xi_j \ge \gamma|\xi|^2$ for some $\gamma > 0$ ; $b_i$ is bounded, $C^1$ , and $b_i(x,0) = 0$ . (H1)′–(H3)′ (degenerate): the coefficients do not depend on $x$ , and the quadratic form above is only nonnegative.

The equation is written as an evolution equation $u' + Au = 0$ in $L^1(\mathbb R^d)$ , with the operator $Au = -\sum_{i,j}D^2_{ij}(a_{ij}(x,u)u) + \operatorname{div}(b(x,u)u)$ taken in the sense of distributions and domain $D(A) = \{u \in L^1 : Au \in L^1\}$ . An operator is m-accretive if $I + \lambda A$ is onto with a contractive inverse for every $\lambda > 0$ . A mild solution is the uniform limit of the implicit Euler scheme $u_h^i + hAu_h^i = u_h^{i-1}$ . The paper calls a mild solution a weak solution of (3.1).

The SDE of the main theorem is

dX(t) = b\big(X(t), u(t,X(t))\big)\,dt + \sqrt2\,\sigma\big(X(t), u(t,X(t))\big)\,dW(t), \quad 0 \le t \le T, \qquad u(t,\cdot) = \frac{d\mathcal L_{X(t)}}{dx}, \tag{4.1}

with $\sigma : \mathbb R^d \times \mathbb R \to L(\mathbb R^d;\mathbb R^d)$ measurable and $a = \sigma\sigma^T$ .

Formalization targets

Goal: Theorem 4.1

If $a = \sigma\sigma^T$ and $b$ satisfy (H1)–(H3) or (H1)′–(H3)′ and $u_0$ is a probability density, then (3.1) has a mild solution $u$ with $u(0) = u_0$ , and for every $T > 0$ there is a weak solution $X$ of (4.1) on $[0,T]$ with

P \circ X(t)^{-1}(dx) = u(t,x)\,dx, \qquad 0 \le t \le T .

Milestones

The PDE layer for (H1)–(H3): Lemmas 3.2 and 3.3 (approximate and $H^1$ solutions of the resolvent equation under the extra smoothness (K)), the $L^1$ contraction (3.22), Proposition 3.1 (the resolvent equation in $L^1$ , with contraction, positivity and mass conservation), density of $D(A)$ , m-accretivity of $A$ , and Theorem 3.4 (existence and uniqueness of the mild solution, properties (3.36)–(3.39)), including preservation of probability densities.
The cited Crandall–Liggett theorem: an m-accretive operator generates a contraction semigroup of mild solutions.
The PDE layer for (H1)′–(H3)′: Lemma 3.6, the resolvent properties (3.52)–(3.54), Theorem 3.7.
The general scheme of §2: a weakly continuous probability solution of a linear Fokker–Planck equation with bounded coefficients is the marginal flow of a weak solution of the corresponding SDE.

Significance

The theorem gives weak existence for a class of distribution dependent SDEs whose coefficients are not continuous in the measure for any weak or Wasserstein topology: they are defined only on measures with a density and read that density at one point. The same construction gives a probabilistic representation of the nonlinear Fokker–Planck equation, which identifies its solutions as one-dimensional time marginals of a stochastic process and is the starting point for particle approximations.

The proofs are written in the literature. This mission formalizes them: the $L^1$ theory of a quasilinear elliptic operator in divergence form, the Crandall–Liggett generation theorem, and the passage from a Fokker–Planck solution to an SDE through the superposition principle. None of these is in Mathlib. The m-accretive operator layer and the superposition step are reusable well beyond this paper.

Difficulty

The natural first idea, a fixed point on the measure argument as in the Lipschitz McKean–Vlasov theory, fails: the map $\mu \mapsto b(x, \frac{d\mu}{dx}(x))$ is not continuous in any topology for which the law map of an SDE is compact, and it is not even defined at measures without density. The paper therefore solves the PDE first. There the obstacle is that $A$ is nonlinear in the highest-order term and, under (H1)′–(H3)′, degenerate. Its resolvent has to be built from $H^1$ solutions on balls under extra smoothness. Its $L^1$ contraction comes from a sign-function argument that needs the monotonicity of $u \mapsto a_{ij}(x,u)u$ . Approximation arguments then remove (K) and the nondegeneracy. On the SDE side, the superposition principle needs a solution of the linear equation that is weakly continuous and consists of probability measures. Mass conservation and positivity of the semigroup supply exactly that.

Formalization scope

$\mathbb R^d$ is EthierKurtz.SDEState d, with indices Fin d (0-based) and Lebesgue measure volume. $L^1$ is MeasureTheory.Lp ℝ 1 volume. Coefficients are functions $a_{ij}(x,r)$ , $b_i(x,r)$ of the point and of a real number. The degenerate case uses coefficients constant in $x$ , and the operator $A_1$ of (3.42) is then literally $A$ . Operators are graphs X → X → Prop, and no resolvent is ever chosen. Mild solutions require that the Euler scheme can be run for all small steps, so the notion is not vacuous. Distributional derivatives are always moved onto smooth compactly supported test functions. $H^1$ uses the published weak derivative HunterPDE.Shared.HasWeakDeriv, and $H^1_0(B_N)$ means "in $H^1(\mathbb R^d)$ and zero outside $B_N$ ". The SDE is the published EthierKurtz.IsWeakSDESolution on $[0,\infty)$ with coefficients switched off after $T$ . Its coefficients are evaluated on a jointly measurable version $\tilde u(t,x)$ of the density, which must equal the law of $X(t)$ .

Deviations from the page, all disclosed in the statements:

$a = \sigma\sigma^T$ , not the printed $2\sigma\sigma^T$ . With noise $\sqrt2\sigma$ the printed factor makes the theorem false (for $d = 1$ , $\sigma \equiv 1/\sqrt2$ , $b \equiv 0$ the PDE has variance $2t$ and the SDE variance $t$ ).
In Lemmas 3.2 and 3.3 the explicit $\lambda_0 = \gamma(b_\infty^2 + c_\infty^2)^{-1}$ is replaced by the existence of some $\lambda_0 > 0$ ; (3.22) keeps the printed $\lambda_0$ , read as $+\infty$ when $b_\infty = c_\infty = 0$ .
In §2 the coefficients are bounded instead of satisfying the integrability Hypothesis 2.1 (ii), and any measurable $\bar\sigma$ with $\bar\sigma\bar\sigma^T = \bar a$ is allowed.
The typos " $C_b(\mathbb R^d\times\mathbb R^d)$ " in (H1) and " $C^1(\mathbb R^d)$ " in (H3)′ are read as $C_b(\mathbb R^d\times\mathbb R)$ and $C^1(\mathbb R)$ .

A trivializing formalization is ruled out: the goal asserts the existence of the mild solution as well as the SDE for every mild solution, a mild solution must come from a run of the scheme, and the constant $C$ of Lemma 3.3 is fixed before the data. Contributions are welcome at every layer, especially general results on m-accretive operators and the Crandall–Liggett theorem, $L^1$ estimates for quasilinear elliptic equations, and the superposition principle.

Selected references

V. Barbu, M. Röckner, From nonlinear Fokker–Planck equations to solutions of distribution dependent SDE, Ann. Probab. 48(4), 2020; arXiv:1808.10706v4. https://arxiv.org/abs/1808.10706
V. Barbu, M. Röckner, Probabilistic representation for solutions to nonlinear Fokker–Planck equations, SIAM J. Math. Anal. 50, 2588–2607, 2018.
Ph. Blanchard, M. Röckner, F. Russo, Probabilistic representation for solutions of an irregular porous media type equation, Ann. Probab. 38, 1870–1900, 2010.
V. Barbu, Nonlinear Differential Equations of Monotone Type in Banach Spaces, Springer, 2010. https://doi.org/10.1007/978-1-4419-5542-5
M. G. Crandall, T. M. Liggett, Generation of semi-groups of nonlinear transformations on general Banach spaces, Amer. J. Math. 93, 1971. https://doi.org/10.2307/2373376
D. Trevisan, Well-posedness of multidimensional diffusion processes with weakly differentiable coefficients, Electron. J. Probab. 21, 2016. https://doi.org/10.1214/16-EJP4453
D. W. Stroock, S. R. S. Varadhan, Multidimensional Diffusion Processes, Springer, 1979. https://doi.org/10.1007/3-540-28999-2

22 thms1 active userReviewed

Algebra Combinatorics Discrete Geometry+1·Captain: mikedeng1

Generalising the Scattered Property of Subspaces 5: For h ≥ 2, Two h-Scattered Linear Sets Are PΓL(r, qⁿ)-Equivalent iff Their Subspaces Are ΓL(r, qⁿ)-EquivalentResearch Paper

Motivation

Linear sets are point sets of a finite projective space defined by a subspace over a subfield. They appear throughout finite geometry, for instance in the study of semifields and, through the correspondence studied by Sheekey and Van de Voorde (arXiv:1806.05929), maximum rank distance (MRD) codes; see Polverino's survey (doi:10.1016/j.disc.2009.04.007). In these applications one needs to decide when two linear sets are the same up to a collineation, which can be difficult (Csajbók–Zanella, arXiv:1501.03441; Csajbók–Marino–Polverino, arXiv:1607.06962). The natural candidate answer, "when their defining subspaces are in the same orbit of the semilinear group", is only a sufficient condition: on the projective line $\mathrm{PG}(1,q^n)$ there are maximum scattered subspaces in different $\Gamma\mathrm L(2,q^n)$ -orbits defining equivalent linear sets (the two papers just cited).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590, Combinatorica 41 (2021)) introduced $h$ -scattered subspaces, a generalisation of scattered subspaces, and showed in their §4 that for $h \ge 2$ the sufficient condition is also necessary. This mission formalizes that result, Theorem 4.5.

Setting

Let $\mathbb F_q \subseteq \mathbb F_{q^n}$ be finite fields and let $V$ be an $r$ -dimensional vector space over $\mathbb F_{q^n}$ ; it is also a vector space over $\mathbb F_q$ . The projective space $\mathrm{PG}(V,\mathbb F_{q^n}) = \mathrm{PG}(r-1,q^n)$ has as points the one-dimensional $\mathbb F_{q^n}$ -subspaces $\langle u\rangle_{\mathbb F_{q^n}}$ , $u \ne 0$ .

For an $\mathbb F_q$ -subspace $U$ of $V$ , the $\mathbb F_q$ -linear set of $U$ is

L_U = \{\langle u\rangle_{\mathbb F_{q^n}} : u \in U\setminus\{0\}\},

of rank $\dim_{\mathbb F_q} U$ .

For $0 < h \le r-1$ , the subspace $U$ is $h$ -scattered (Definition 1.1) if $\langle U\rangle_{\mathbb F_{q^n}} = V$ and every $h$ -dimensional $\mathbb F_{q^n}$ -subspace $S$ of $V$ satisfies $\dim_{\mathbb F_q}(S\cap U) \le h$ . The linear set $L_U$ of an $h$ -scattered $U$ is called $h$ -scattered (Definition 4.1); for $h = 2$ it is scattered with respect to lines.

The group $\Gamma\mathrm L(r,q^n)$ consists of the bijective additive maps $f$ of $V$ that are semilinear: $f(av) = a^\sigma f(v)$ for some field automorphism $\sigma$ of $\mathbb F_{q^n}$ . Each $f$ induces a collineation $\varphi_f$ of $\mathrm{PG}(V,\mathbb F_{q^n})$ , $\langle u\rangle \mapsto \langle f(u)\rangle$ , and these collineations form $\mathrm P\Gamma\mathrm L(r,q^n)$ . Two linear sets are $\mathrm P\Gamma\mathrm L$ -equivalent if $\varphi_f(L_U) = L_W$ for some $f$ ; two subspaces are $\Gamma\mathrm L$ -equivalent if $f(U) = W$ for some $f$ .

Formalization targets

Goal: Theorem 4.5 (p. 14)

For $h \ge 2$ and $h$ -scattered $\mathbb F_q$ -subspaces $U$ , $W$ of $V(r,q^n)$ ,

L_U \sim_{\mathrm P\Gamma\mathrm L(r,q^n)} L_W \iff U \sim_{\Gamma\mathrm L(r,q^n)} W .

Milestones (in the order of the proof)

Proposition 2.1 (p. 3): an $h$ -scattered subspace is $i$ -scattered for every $0 < i < h$ .
Proposition 4.2 (p. 13, quoted from Bonoli–Polverino [5]): on a projective line $\mathrm{PG}(1,q^n)$ , (1) a linear set with $q+1$ points has rank $2$ ; (2) two subspaces defining the same linear set of size $q+1$ and sharing a nonzero vector coincide.
Proposition 4.3 (p. 13): if $U$ is $2$ -scattered and $L_W = L_U$ , then $\dim_{\mathbb F_q} W = \dim_{\mathbb F_q} U$ .
Lemma 4.4 (p. 13): if $U$ is $2$ -scattered and $L_U = L_W$ , then $U = \lambda W$ for some $\lambda\in\mathbb F_{q^n}^*$ .

Significance

The result. Theorem 4.5 says that, for $h\ge2$ , an $h$ -scattered linear set remembers its defining subspace up to a scalar and up to the semilinear group. The equivalence problem for such linear sets, a geometric question about point sets, becomes the equivalence problem for subspaces, which is algebraic and can be attacked with linearized polynomials. Through the correspondence of Sheekey and Van de Voorde between maximum $(r-1)$ -scattered subspaces and MRD codes, the paper derives from it (Theorem 4.10, not part of this mission) that two $\mathbb F_q$ -linear MRD codes with minimum distance $n-r+1$ , $r>2$ , and left idealiser isomorphic to $\mathbb F_{q^n}$ are equivalent if and only if their associated linear sets in $\mathrm{PG}(r-1,q^n)$ are $\mathrm P\Gamma\mathrm L$ -equivalent. Lemma 4.4 and Proposition 4.3 are of independent use: they say that the rank and, up to scalars, the subspace of any linear set scattered with respect to lines are invariants of the point set.

The formalization. The theorem is proved in the paper; no part of it, nor any statement about linear sets over a field extension, is machine-checked in Mathlib. The mission produces a formal model of linear sets, of the semilinear group and of its induced collineations that later finite-geometry missions can reuse, together with formal proofs of the four milestones. Proposition 4.2 is quoted from [5] without proof in the paper, so formalizing it means formalizing Bonoli and Polverino's argument.

Difficulty

The "if" direction is a direct computation, $L_{U^f} = L_U^{\varphi_f}$ . The obvious approach to the converse, reconstructing $U$ from $L_U$ point by point, fails because a point $\langle u\rangle$ of $L_U$ determines $U\cap\langle u\rangle$ only up to a scalar of $\mathbb F_{q^n}^*$ , and these scalars can a priori differ from point to point. Without the condition $h \ge 2$ they really do differ: for $h = 1$ the theorem is false. The step that needs $h\ge2$ is the rigidity of the intersections of $U$ with two-dimensional $\mathbb F_{q^n}$ -subspaces, which is where the quoted result on linear sets of size $q+1$ on a projective line enters. Proposition 4.2 itself is a counting statement about point weights on $\mathrm{PG}(1,q^n)$ and is not available in any library.

Formalization scope

$\mathbb F_q$ and $\mathbb F_{q^n}$ are arbitrary finite fields F, K with [Algebra F K]; $q$ is Fintype.card F. $V$ is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]), and $r$ is Module.finrank K V.
IsHScattered F K h U includes the range $0 < h < r$ and the spanning condition $\langle U\rangle_{\mathbb F_{q^n}} = V$ , as in Definition 1.1. With $h\ge2$ this forces $r\ge3$ .
A point is the K-submodule K ∙ u; linearSet F K U is a Set (Submodule K V) and $|L_U|$ is its Set.ncard.
$\Gamma\mathrm L$ is the set of f : V ≃+ V for which some σ : K ≃+* K gives f (a • v) = σ a • f v. The collineation $\varphi_f$ sends a subspace $P$ to Submodule.span K (f '' P). The image $U^f$ is the set f '' U, and $\lambda W$ is (λ • ·) '' W with $\lambda\ne0$ .
Two trivializing readings are excluded. Restricting to linear maps (GL, PGL) would prove a different, weaker statement; taking $\mathrm{P}\Gamma\mathrm{L}$ -equivalence to mean "some bijection of points maps $L_U$ to $L_W$ " would make the "only if" direction false. Both equivalences quantify over the full semilinear group, and the collineation is the one induced by the same $f$ .
Proposition 4.2 is a result the paper numbers but quotes from [5] (Bonoli–Polverino, $\mathbb F_q$ -linear blocking sets in $\mathrm{PG}(2,q^4)$ ). It is a milestone with its own proof obligation and is not assumed. The two parts are separate items.
Proposition 2.1's "for any $i < h$ " is read as $0 < i < h$ , the range on which Definition 1.1 defines $i$ -scattered.

Welcome contributions: the general theory of linear sets (point weights, $|L_U| \le (q^k-1)/(q-1)$ with equality iff $U$ is scattered), the fact that a semilinear map of $V$ maps $\mathbb F_q$ -subspaces to $\mathbb F_q$ -subspaces, and the counting argument behind Proposition 4.2. These are reusable for every linear-set mission.

Selected references

B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, Combinatorica 41 (2021); arXiv:1906.10590v2 (2020). https://arxiv.org/abs/1906.10590
G. Bonoli, O. Polverino, $\mathbb F_q$ -linear blocking sets in $\mathrm{PG}(2,q^4)$ , Innov. Incidence Geom. 2 (2005), 35–56. https://doi.org/10.2140/iig.2005.2.35
B. Csajbók, G. Marino, O. Polverino, Classes and equivalence of linear sets in $\mathrm{PG}(1,q^n)$ , J. Combin. Theory Ser. A 157 (2018), 402–426. https://arxiv.org/abs/1607.06962
B. Csajbók, C. Zanella, On the equivalence of linear sets, Des. Codes Cryptogr. 81 (2016), 269–281. https://arxiv.org/abs/1501.03441
O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2009.04.007
J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://arxiv.org/abs/1806.05929

9 thms1 active userReviewed