All missions

Motivation

For bipartite graphs, Kőnig's theorem says that the minimum number of vertices needed to meet every edge equals the maximum number of pairwise disjoint edges: $\tau=\nu$. For hypergraphs whose edges have $r$ vertices, the ratio $\tau/\nu$ can be as large as $r$ in general, and the bound $\tau\le r\nu$ is trivial. Ryser's conjecture asserts that for $r$-partite $r$-uniform hypergraphs, the natural generalisation of bipartite graphs, the trivial bound can be improved by one:

$$\tau(\mathcal H)\le (r-1)\,\nu(\mathcal H).$$

For $r=2$ it is Kőnig's theorem. Truncated projective planes show that the factor $r-1$ cannot be lowered when $r-1$ is a prime power. The conjecture is a central problem on matchings and covers in hypergraphs (Aharoni 2001, Haxell–Scott 2012).

Timeline.

• 1931 — Kőnig proves $\tau=\nu$ for bipartite graphs, the case $r=2$.
• 1971 — The conjecture appears in the thesis of Ryser's student Henderson; the case $\nu=1$ is attributed to Lovász.
• 1983 — Tuza proves the intersecting case $\nu=1$ for $r\le 5$ (Tuza 1983).
• 2001 — Aharoni proves the case $r=3$ using the topological Hall theorem of Aharoni and Haxell (Aharoni 2001).
• 2012 — Haxell and Scott prove $\tau\le (r-\varepsilon)\nu$ for $r=4,5$ and some $\varepsilon>0$ (Haxell–Scott 2012).
• 2017–2021 — Francetić, Herke, McKay and Wanless, then Abu-Khazneh, Barát, Pokrovskiy and Szabó, construct families of extremal hypergraphs; Bishnoi, Das, Morris and Szabó settle the $t$-intersecting case (Abu-Khazneh et al. 2019, Bishnoi et al. 2021).

The case $r=4$ is open.

Setting

A hypergraph $\mathcal H$ has a finite vertex set $V(\mathcal H)$ and a set $E(\mathcal H)$ of edges, each a subset of $V(\mathcal H)$. It is $r$-uniform if every edge has exactly $r$ vertices, and $r$-partite if $V(\mathcal H)$ is the disjoint union of parts $P_1,\dots,P_r$ such that every edge meets every part in exactly one vertex. A vertex cover is a set $C\subseteq V(\mathcal H)$ meeting every edge; the cover number $\tau(\mathcal H)$ is the least size of a vertex cover. A matching is a set of pairwise disjoint edges; the matching number $\nu(\mathcal H)$ is the largest size of a matching. For $r\in\mathbb N$ let $\mathrm{Ry}(r)$ be the statement

$$r\ge 2 \implies \text{every } r\text{-partite } r\text{-uniform hypergraph } \mathcal H \text{ satisfies } \tau(\mathcal H)\le (r-1)\,\nu(\mathcal H).$$

Formalization targets

Goal

$$\forall r\in\mathbb N:\quad \mathrm{Ry}(r).$$

Rungs

$\mathrm{Ry}(2)$ is Kőnig's theorem, $\mathrm{Ry}(3)$ is Aharoni's theorem, and $\mathrm{Ry}(4)$ is the first open rung. For $r\le 1$ the statement is vacuous.

Significance

Ryser's conjecture is the hypergraph form of Kőnig's theorem and one of the standard open problems in the matching theory of hypergraphs. Its intersecting case ($\nu=1$) is equivalent to a question about the covering number of Latin-square-like structures and is open for $r\ge 6$; its fractional version, $\tau\le (r-1)\nu^*$, was proved by Füredi. A proof for $r=4$ would be the first progress on the full conjecture since Aharoni's theorem.

Formalizing the known rungs gives a theory of finite hypergraphs, covers and matchings on top of Mathlib's Finset, which currently has Kőnig's theorem only in graph form (Hall's marriage theorem is in Mathlib). Aharoni's proof for $r=3$ goes through the topological Hall theorem, so a formalization would need the connectivity of independence complexes, a sizeable but reusable piece of topological combinatorics. None of the rungs has a machine-checked proof in the hypergraph formulation; $\mathrm{Ry}(4)$ and the goal are open.

Difficulty

The bound $\tau\le r\nu$ comes from taking all vertices of a maximum matching; improving it by a factor $(r-1)/r$ requires exploiting the partition, and no inductive or greedy argument is known to do so beyond $r=3$. Aharoni's proof for $r=3$ is non-constructive and topological, and the topological Hall theorem gives for general $r$ only $\tau\le r\nu$-type bounds; the $\varepsilon$-improvements of Haxell and Scott already require long case analyses. The conjecture is tight for infinitely many $r$, so no slack is available.

Formalization scope

A hypergraph is the structure FinHypergraph α with vertices : Finset α, edges : Set (Finset α) and the axiom that every edge is a subset of vertices; since edges are finite subsets of a finite set, there are finitely many. IsUniform r, IsPartite r (parts indexed by Fin r, covering the vertex set, pairwise disjoint, each meeting each edge in exactly one vertex), IsVertexCover C (a subset of the vertices meeting every edge) and IsMatching M (a Finset of edges, pairwise disjoint) are as in the Setting. coverNumber is the infimum sInf of the sizes of vertex covers, and matchingNumber the supremum sSup of the sizes of matchings; both are natural numbers, with the conventions $\inf\emptyset=0$ and $\sup$ of an unbounded set $=0$, which never arise since the vertex set covers every edge whenever edges are nonempty and matchings are bounded by the number of edges. RyserConjectureFor H r is $\tau\le(r-1)\nu$ under the uniformity and partiteness hypotheses, statement_08 r adds the guard $2\le r$ and quantifies over all vertex types with decidable equality in a universe u, and the goal is ∀ r, statement_08 r.

No trivialising reading: $r=0$ and $r=1$ are excluded by the guard, uniformity with $r\ge 2$ makes edges nonempty, and for an edgeless hypergraph both sides are $0$. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: the basic inequalities $\nu\le\tau\le r\nu$, finiteness of the edge set, Kőnig's theorem in this formulation, and decompositions of Aharoni's theorem.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 8).
• R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica 21 (2001), 1–4. https://doi.org/10.1007/s004930170001
• Z. Tuza, Ryser's conjecture on transversals of r-partite hypergraphs, Ars Combin. 16 (1983), 201–209.
• P. E. Haxell, A. D. Scott, On Ryser's conjecture, Electron. J. Combin. 19 (2012), P23. https://doi.org/10.37236/1175
• A. Abu-Khazneh, J. Barát, A. Pokrovskiy, T. Szabó, A family of extremal hypergraphs for Ryser's conjecture, J. Combin. Theory Ser. A 161 (2019), 164–177. https://doi.org/10.1016/j.jcta.2018.07.011
• A. Bishnoi, S. Das, P. Morris, T. Szabó, Ryser's conjecture for t-intersecting hypergraphs, J. Combin. Theory Ser. A 179 (2021), 105366. https://doi.org/10.1016/j.jcta.2020.105366
• N. Francetić, S. Herke, B. D. McKay, I. M. Wanless, On Ryser's conjecture for linear intersecting multipartite hypergraphs, European J. Combin. 61 (2017), 91–105. https://doi.org/10.1016/j.ejc.2016.10.004
• Z. Füredi, Maximum degree and fractional matchings in uniform hypergraphs, Combinatorica 1 (1981), 155–162. https://doi.org/10.1007/BF02579271

Motivation

A family of finite sets is union-closed if the union of any two members is again a member. The union-closed sets conjecture, attributed to Frankl (1979), asserts that every such family, other than the two degenerate ones $\emptyset$ and $\{\emptyset\}$, has an element that lies in at least half of its members. Despite its elementary statement the conjecture resisted all attempts for over forty years; it is equivalent to statements about lattices and about intersection-closed families, and the first constant-fraction bound was found only in 2022 (Bruhn–Schaudt 2015).

Timeline.

• 1979 — Frankl poses the conjecture.
• 1994 — Knill proves that some element lies in at least $(|\mathcal F|-1)/\log_2|\mathcal F|$ members (Knill 1994).
• 2015 — Bruhn and Schaudt survey the partial results: families with few members, few elements, or special structure (Bruhn–Schaudt 2015).
• 2022 — Gilmer proves the first constant bound, density at least $0.01$, by an entropy argument (Gilmer 2022).
• 2022 — Within weeks, Sawin, Chase and Lovett, Alweiss, Huang and Sellke, and Pebody independently push Gilmer's method to density at least $\frac{3-\sqrt5}{2}\approx 0.38197$ (Chase–Lovett 2022, Sawin 2022, Alweiss–Huang–Sellke 2022, Pebody 2022).
• 2023 — Further refinements improve the constant slightly beyond $0.382$ but stay below $0.39$ (Liu 2023).

Setting

Let $\mathcal F$ be a finite family of finite subsets of a set $U$. It is union-closed if $A\cup B\in\mathcal F$ for all $A,B\in\mathcal F$, and nondegenerate if $\mathcal F\ne\emptyset$ and $\mathcal F\ne\{\emptyset\}$. The density of an element $x\in U$ in $\mathcal F$ is

$$\delta_{\mathcal F}(x) := \frac{|\{A\in\mathcal F: x\in A\}|}{|\mathcal F|}.$$

The conjecture says that some $x$ has $\delta_{\mathcal F}(x)\ge\tfrac12$. The challenge scales the bound: for $r\in\mathbb N$ let $\mathrm{UC}(r)$ be the statement

$$\text{every nondegenerate union-closed } \mathcal F \text{ has an element } x \text{ with } \delta_{\mathcal F}(x)\ \ge\ \frac12-\frac1{r+2}.$$

The bounds $\tfrac12-\tfrac1{r+2}$ increase to $\tfrac12$, so $\mathrm{UC}(r)$ for all $r$ is the full conjecture, and each $\mathrm{UC}(r)$ follows from the next.

Formalization targets

Goal

$$\text{every nondegenerate union-closed } \mathcal F \text{ has an element } x \text{ with } \delta_{\mathcal F}(x)\ \ge\ \tfrac12,$$

the union-closed sets conjecture itself. It is equivalent to $\mathrm{UC}(r)$ for all $r$: the densities in a fixed finite family $\mathcal F$ take finitely many values, so an element of density at least $\tfrac12-\tfrac1{r+2}$ for every $r$ is an element of density at least $\tfrac12$.

Rungs

$\mathrm{UC}(0)$ is trivial. $\mathrm{UC}(r)$ for $1\le r\le 6$ follows from the bound $\frac{3-\sqrt5}{2}\approx 0.382$, since $\tfrac12-\tfrac18=0.375$. $\mathrm{UC}(7)$ asks for density $\tfrac12-\tfrac19\approx 0.3889$ and is the first open rung.

Significance

The conjecture is one of the best-known open problems in extremal set theory, with equivalent forms for lattices (every finite lattice has a join-irreducible element in at most half of the elements) and for intersection-closed families. The entropy method of 2022 changed its status from "no constant known" to "within $0.118$ of the truth", and the remaining gap is exactly what the rungs $r\ge 7$ measure: the constant $\frac{3-\sqrt5}{2}$ is the limit of the known method, as shown by examples of Sawin and others, so $\mathrm{UC}(7)$ needs a new idea.

Formalizing the entropy argument is a self-contained project: Gilmer's proof is a few pages of entropy inequalities on top of Mathlib's probability and information theory, and the $\frac{3-\sqrt5}{2}$ refinement adds one optimisation. Neither has a machine-checked proof in Mathlib. The rungs $r\le 6$ would follow; the rungs $r\ge 7$ and the goal are open.

Difficulty

The entropy argument bounds the density of the best element through the entropy of a random union $A\cup B$ of two independent random members; the constant $\frac{3-\sqrt5}{2}$ is where this inequality becomes tight, and the "approximate" families constructed by Sawin and by Chase and Lovett show that the one-step entropy method cannot pass it. Elementary approaches (induction on $|U|$ or $|\mathcal F|$, averaging over pairs) are known to fail even for a constant bound. The naive idea, that the most frequent element of the largest set works, is false.

Formalization scope

Families are Finset (Finset U) for a type U with decidable equality, in an arbitrary universe. IsUnionClosed F says $A\cup B\in F$ for all $A,B\in F$; occurrences F x counts the members containing $x$; density F x : ℚ is occurrences F x / max 1 F.card, so the division is by $|F|$ when $F$ is nonempty and by $1$ otherwise; Nondegenerate F is $F\ne\emptyset\wedge F\ne\{\emptyset\}$. The rung statement_09 r states that for every union-closed nondegenerate $F$ there is an element $x$ of U with density F x ≥ 1/2 - 1/((r : ℚ) + 2) in the rationals. The goal states the conjecture directly, ∃ x, density F x ≥ 1/2 for every union-closed nondegenerate F; it is equivalent to ∀ r, statement_09 r, the universal form of the benchmark.

No trivialising reading: nondegeneracy excludes exactly the two families for which the conjecture fails, the density is a genuine quotient for nonempty $F$, and an empty type U admits no nondegenerate family. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: the equivalence of density with the real-valued density of the Mathlib archive, monotonicity of the rungs in $r$, the trivial rung $r=0$, the singleton and power-set special cases, and a formalization of the entropy bound giving the rungs $r\le 6$.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 9).
• H. Bruhn, O. Schaudt, The journey of the union-closed sets conjecture, Graphs Combin. 31 (2015), 2043–2074. https://doi.org/10.1007/s00373-014-1515-0
• E. Knill, Graph generated union-closed families of sets, 1994. https://arxiv.org/abs/math/9409215
• J. Gilmer, A constant lower bound for the union-closed sets conjecture, 2022. https://arxiv.org/abs/2211.09055
• Z. Chase, S. Lovett, Approximate union closed conjecture, 2022. https://arxiv.org/abs/2211.11689
• W. Sawin, An improved lower bound for the union-closed set conjecture, 2022. https://arxiv.org/abs/2211.11504
• R. Alweiss, B. Huang, M. Sellke, Improved lower bound for the union-closed sets conjecture, 2022. https://arxiv.org/abs/2211.11731
• L. Pebody, Extension of a method of Gilmer, 2022. https://arxiv.org/abs/2211.13139
• J. Liu, Improving the lower bound for the union-closed sets conjecture via conditionally IID coupling, 2023. https://arxiv.org/abs/2306.08824
• N. Nagel, Notes on the union closed sets conjecture, 2023. https://arxiv.org/abs/2208.03803

Motivation

A partition of the vertices of a graph into two classes is unfriendly if every vertex has at least as many neighbours in the other class as in its own. Every finite graph has one: a partition with the maximum number of crossing edges. For infinite graphs the question is the unfriendly partition conjecture of Cowan and Emerson: does every countable graph have an unfriendly partition? Shelah and Milner showed that uncountable graphs need not, and the countable case has been open since the 1980s, with positive answers for locally finite graphs, graphs with finitely many vertices of infinite degree, and rayless graphs (Aharoni–Milner–Prikry 1990, Shelah–Milner 1990, Bruhn–Diestel–Georgakopoulos–Sprüssel 2010).

This challenge scales the conjecture through a game. The parameter is an ordinal $r$, the clock: Challenger repeatedly names a vertex and lowers the clock, and Partitioner must extend a finite partial partition so that the named vertex becomes unfriendly. An unfriendly partition of the whole graph gives Partitioner a winning strategy for every clock, so the full conjecture implies every rung, and the rungs with transfinite clocks measure how much of an unfriendly partition can be built on demand.

Timeline.

• 1980s — Cowan and Emerson pose the conjecture.
• 1990 — Aharoni, Milner and Prikry prove it for graphs with only finitely many vertices of infinite degree, in particular for locally finite graphs (Aharoni–Milner–Prikry 1990).
• 1990 — Shelah and Milner construct uncountable graphs without unfriendly partitions (Shelah–Milner 1990).
• 2010 — Bruhn, Diestel, Georgakopoulos and Sprüssel prove it for rayless graphs of any cardinality (Bruhn–Diestel–Georgakopoulos–Sprüssel 2010).
• 2017 — Berger proves it for graphs containing no subdivision of an infinite clique (Berger 2017).

Setting

Let $G$ be a graph with vertex set $V$. A partial partition is a partial function $f\colon V\rightharpoonup\{0,1\}$; it is finite if its domain is finite, and a partition if it is total. Write $N(v)$ for the neighbourhood of $v$. A partial partition $f$ is unfriendly at $v$ if $f(v)$ is defined and

$$\big|N(v)\cap f^{-1}[1-f(v)]\big|\ \ge\ \big|N(v)\cap f^{-1}[f(v)]\big|,$$

as cardinal numbers; neighbours outside the domain of $f$ are not counted. A partition is unfriendly if it is unfriendly at every vertex.

The $r$-partitioning game. For an ordinal $r$, a position is a pair $(f,\alpha)$ of a partial partition and an ordinal, the initial position is $(\emptyset,r)$. In each turn from $(f,\alpha)$, Challenger names a vertex $v$ and an ordinal $\beta<\alpha$; Partitioner must answer with a finite partial partition $g$ extending $f$ (preserving all assignments of $f$) that is unfriendly at $v$; the new position is $(g,\beta)$. A player unable to move loses; since ordinals have no infinite descending sequences, the game ends after finitely many turns, and Partitioner wins if Challenger runs out of moves. For an ordinal $r$ let

$$\mathrm{UP}(r):\quad \text{Partitioner has a winning strategy in the } r\text{-partitioning game on every countable graph.}$$

Formalization targets

Goal

$$\text{every countable graph has an unfriendly partition,}$$

the unfriendly partition conjecture of Cowan and Emerson. A partial partition that is unfriendly at every vertex is total, so the goal is stated with the same notion of unfriendliness as the game.

The scaled form

$$\forall r\in\mathrm{Ord}:\quad \mathrm{UP}(r),$$

Partitioner wins the $r$-partitioning game on every countable graph for every ordinal clock. An unfriendly partition yields a winning strategy for every clock, so the goal implies the scaled form; the rungs are the scaled form for particular clocks and particular classes of graphs.

Rungs

Any graph with an unfriendly partition yields a winning strategy for every clock: Partitioner reveals the partition on a finite set containing the named vertex and the finitely many coloured neighbours needed. Hence every finite graph, every countable locally finite graph, and every countable rayless graph satisfies all rungs. For finite clocks $r=n$ the statement is an exercise; the rung $r=\omega$ is the first with an infinite clock.

Significance

The unfriendly partition conjecture is the basic open question about majority colourings of infinite graphs, and its scaled form isolates how the difficulty grows with the "transfinite length" of the commitment required: with clock $\omega$, Challenger must announce in advance how many more vertices will be challenged, with clock $\omega\cdot 2$ once more, and so on. The full statement is implied by the conjecture; how much of the conjecture the game recovers in return is part of what the scaled version is designed to probe.

Nothing about unfriendly partitions is formalized; Mathlib has simple graphs on arbitrary types and cardinals, but neither majority conditions nor the compactness argument for locally finite graphs. The finite-clock rungs, the finite-graph case and the locally finite case are reachable formalization projects; the infinite-clock rungs are open.

Difficulty

The max-cut argument of the finite case has no infinite analogue: a vertex of infinite degree can be unfriendly only through a cardinality comparison, and attempts to build a partition by transfinite induction run into vertices whose status is changed by later decisions. The known positive results use a careful ordering of the vertices of infinite degree or a structural decomposition (rayless graphs); none of them gives any information about graphs with infinitely many vertices of infinite degree and infinite paths. In the game, the naive strategy of colouring only the challenged vertex fails because Challenger can later challenge a coloured vertex all of whose finitely many neighbours have already been coloured badly.

Formalization scope

Graphs are Mathlib's SimpleGraph V with V in a universe u and the hypothesis Countable V; partial partitions are functions V → Option Bool, with none for undefined and some b for class $b$. NeighColored G f v b is the type of neighbours of $v$ with value $b$, and UnfriendlyAt G f v requires some b with f v = some b and the cardinal inequality #(neighbours coloured b) ≤ #(neighbours coloured !b) (Mathlib's Cardinal.mk). emptyPartition V is the constant none; HasFiniteDomain, Extends and IsLegalResponse G f g v (extends, finite domain, unfriendly at $v$) are as in the Setting. PartitionerWins G f α is defined by well-founded recursion on the ordinal α : Ordinal.{v}: for every vertex $v$ and every $\beta<\alpha$ there is a legal response $g$ with PartitionerWins G g β. The rung statement_10 r is PartitionerWins G (emptyPartition V) r for every countable V and every G; the scaled form is ∀ r, statement_10 r. The goal is ∃ f : V → Option Bool, ∀ v, UnfriendlyAt G f v for every countable V and every G: since UnfriendlyAt requires f v to be defined, such an f assigns a class to every vertex and is an unfriendly partition in the usual sense.

No trivialising reading: with clock $0$ Partitioner wins vacuously, which is the intended base case; responses must be finite, so Partitioner cannot reveal a whole infinite partition at once; and the cardinal comparison is exactly the majority condition on coloured neighbours. The universes of V and of the ordinal are independent parameters. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: the lemma that an unfriendly partition yields PartitionerWins for every clock, monotonicity of PartitionerWins in the clock, the finite-graph and locally finite cases, the finite-clock rungs, and the relation between winning for all countable clocks and the existence of an unfriendly partition.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 10).
• R. Aharoni, E. C. Milner, K. Prikry, Unfriendly partitions of a graph, J. Combin. Theory Ser. B 50 (1990), 1–10. https://doi.org/10.1016/0095-8956(90)90092-E
• S. Shelah, E. C. Milner, Graphs with no unfriendly partitions, in: A Tribute to Paul Erdős, Cambridge University Press, 1990, 373–384.
• H. Bruhn, R. Diestel, A. Georgakopoulos, P. Sprüssel, Every rayless graph has an unfriendly partition, Combinatorica 30 (2010), 521–532. https://doi.org/10.1007/s00493-010-2590-3
• E. Berger, Unfriendly partitions for graphs not containing a subdivision of an infinite clique, Combinatorica 37 (2017), 157–166. https://doi.org/10.1007/s00493-015-3261-1
• R. Diestel, Graph Theory, 5th ed., Springer, 2017, Chapter 8. https://doi.org/10.1007/978-3-662-53622-3

Portfolio choice when the market regime is hidden

The distribution of stock returns is not constant: drifts and volatilities change with economic conditions that are not directly observed, and drift parameters in particular are notoriously hard to estimate. A standard way to model this in discrete time is to let the return distribution depend on an unobservable Markov chain, the hidden state or regime, while the investor sees only prices. Chapter 6 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) treats two classical portfolio problems in this setting, terminal wealth maximization and the dynamic mean–variance problem, by reducing them, through the Bayes filter of Chapter 5, to fully observed Markov Decision Problems whose state is the wealth together with the conditional law of the hidden regime. The book notes that partially observable portfolio problems in discrete time had been sparsely studied, with binomial models with an unknown up-probability (Runggaldier et al. 2002, Favero 2001) and a hidden-Markov model with unknown drift and volatility (Taksar and Zeng 2007) as earlier examples.

Setting

A bond earns the interest rate $i_{n+1}\ge0$ in period $[n,n+1)$, with price $S^0_n=\prod_{k\le n}(1+i_k)$. There are $d$ stocks with relative risk $R_{n+1}\in\mathbb R^d$, every component above $-1$. A hidden process $(Y_n)$ lives on a standard Borel space $E_Y$, and $(R_n,Y_n)$ is a Markov process with

$$\mathbb P(R_{n+1}\in B,\ Y_{n+1}\in C\mid Y_n=y,R_n)=Q^R(B\mid y)\,Q^Y(C\mid y),$$

where $Q^R$ and $Q^Y$ have densities $q^R$, $q^Y$ with respect to $\sigma$-finite measures and $Y_0$ has the prior $Q_0$. The investor's strategy $\varphi_n$ (the amounts in the stocks) may depend only on $R_1,\dots,R_n$; wealth evolves as $X_{n+1}=(1+i_{n+1})(X_n+\varphi_n\cdot R_{n+1})$.

The Bayes operator maps a belief $\rho\in\mathbb P(E_Y)$ and an observed return $z$ to

$$\Phi(\rho,z)(C)=\frac{\int_C\int q^R(z\mid y)q^Y(y'\mid y)\rho(dy)\,\nu(dy')}{\int_{E_Y}\int q^R(z\mid y)q^Y(y'\mid y)\rho(dy)\,\nu(dy')},$$

and the filter is $\mu_0=Q_0$, $\mu_{n+1}=\Phi(\mu_n,R_{n+1})$.

In the terminal wealth problem (6.2) the investor has a utility function $U$ (strictly increasing, strictly concave, continuous) on $\operatorname{dom}U=[0,\infty)$ or $(0,\infty)$, a constant rate $i$, and maximizes $\mathbb E_xU(X_N)$ over adapted strategies with $X_N\in\operatorname{dom}U$ almost surely. The admissible investments at wealth $x$ are $D(x)=\{a:(1+i)(x+a\cdot R(y))\in\operatorname{dom}U\text{ a.s.}\}$. The filtered model has state $(x,\rho)$; from it, $z$ is drawn from $\int Q^R(\cdot\mid y)\rho(dy)$ and the state moves to $((1+i)(x+a\cdot z),\Phi(\rho,z))$. Its value functions with $n$ stages to go are $J_n(x,\rho)$.

Formalization targets

Goal: Theorem 6.1.1

Under the no-arbitrage, common-support and moment assumption (FM), and with $D(x)$ independent of the hidden state:

1. $x\mapsto J_n(x,\rho)$ is finite, strictly increasing, strictly concave and continuous on $\operatorname{dom}U$;
2. $J_0(x,\rho)=U(x)$ and

$$J_n(x,\rho)=\sup_{a\in D(x)}\int\!\!\int J_{n-1}\big((1+i)(x+a\cdot z),\Phi(\rho,z)\big)Q^R(dz\mid y)\rho(dy);$$

3. the value of (6.2) from wealth $x>0$ is $J_N(x,Q_0)$;
4. maximizers $f^*_n$ of $J_{n-1}$ exist when $\operatorname{dom}U=[0,\infty)$, $D(x)$ is closed, or $U'(0+)=\infty$, and for any maximizers $f_n(h_n)=f^*_{N-n}(x_n,\mu_n(\cdot\mid h_n))$ is optimal for (6.2).

Theorem 6.1.2 (power utility)

For $U(x)=x^\gamma/\gamma$, $0<\gamma<1$: $J_n(x,\rho)=(xS^0_n)^\gamma d_n(\rho)$ with $d_0\equiv1/\gamma$ and

$$d_n(\rho)=\sup_{\alpha\in\tilde A}\int\!\!\int d_{n-1}(\Phi(\rho,z))(1+\alpha\cdot z)^\gamma Q^R(dz\mid y)\rho(dy),$$

and the optimal amounts are $\alpha^*_n(\rho)x$.

Theorem 6.2.3 (mean–variance)

For $\operatorname{Var}(X_N)\to\min$ subject to $\mathbb E X_N\ge\mu$, with $x_0S^0_N<\mu$: the strategy $f^*_n(x,\rho)=\big(\tfrac{\mu-d_0(Q_0)x_0S^0_N}{1-d_0(Q_0)}\tfrac{S^0_n}{S^0_N}-x\big)C^{-1}_{n+1}(\rho)\ell_{n+1}(\rho)$ applied to the filter is optimal, and the minimal variance is

$$\frac{d_0(Q_0)}{1-d_0(Q_0)}\big(\mu-x_0S^0_N\big)^2,$$

with $d_n,\ell_n,C_n$ given by the backward recursion (6.7).

Significance

Theorem 6.1.1 is the structural result of the chapter: it says that a hidden regime costs no more than one extra state variable, the filter, and that the investor who uses the whole price history does no better than one who uses only current wealth and current belief. Theorems 6.1.2 and 6.2.3 turn this into explicit recursions: for power utility the wealth dependence factors out and only a function of the belief remains; for mean–variance the efficient frontier keeps the same shape as under full observation, with the constant $d_0(Q_0)$ computed from the filter. The comparison results of the chapter (Theorem 6.1.5, partial versus complete observation in the binomial model) and the logarithmic case (Theorem 6.1.7) build on these.

The results are proved in the book by combining the general reduction of Chapter 5 (Theorems 5.3.2, 5.3.3) with the structure theorems of Chapter 4. Those general POMDP theorems are formalized on the platform for models whose observable transition has a density; the financial model here does not (the next wealth is a deterministic function of the return), so this mission states the financial results directly on the market, with no reduction built into the definitions. None of the three theorems is formalized yet; earlier platform statements of them were retired as unfaithful.

Difficulty

The value of (6.2) is a supremum over strategies that are arbitrary measurable functions of the observed history, computed under the law of the hidden chain; $J_N$ is defined from a different process, the filtered model, in which returns are drawn from predictive laws. Equality of the two requires the filter property: the conditional law of $Y_n$ given $R_1,\dots,R_n$ is $\mu_n$, and the conditional law of $R_{n+1}$ is the predictive mixture. On top of this, the Bellman equation needs measurability of the value functions on the space of probability measures and the existence of measurable maximizers, which the book obtains from compactness of $D(x)$ under no arbitrage and the upper bounding function $1+x$. Applying the one-period existence theorem pointwise in $\rho$ does not give a measurable selection by itself.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ; $E_Y$ is a standard Borel space and beliefs are ProbabilityMeasure E_Y with the Giry $\sigma$-algebra. Return paths are 0-indexed vectors. Strategies are measurable functions of the return path; the market law of the returns is built recursively from (6.1). $J_n$ is a supremum over Markov policies of measurable decision rules on $\mathbb R\times\mathbb P(E_Y)$ of the expected utility under the filtered model's law of returns. Expectations of utilities are extended reals, $\int f^+-\int f^-$. The Bayes operator returns $\rho$ on the null set where its normalizing constant is $0$ or $\infty$.

The hypothesis that $D(x)$ does not depend on $y$ is part of the goal: for $\operatorname{dom}U=(0,\infty)$ it does not follow from equal supports, and without it part 4 fails. The existence of maximizers is also corrected: for $\operatorname{dom}U=(0,\infty)$ with $U(0+)$ and $U'(0+)$ finite, for instance $U(x)=\log(1+x)$, the set $D(x)$ can be open with the supremum approached at its boundary, so part 4 asserts existence only under the stated conditions, which cover $[0,\infty)$, logarithmic and negative power utility. For the mean–variance theorem the first-moment condition is used in its uniform $L^2$ form, which the book's covariance matrices for every belief require. A formalization in which competitors are restricted to filter-based Markov rules would make part 3 trivial and is not used.

Needed infrastructure: filtering for hidden Markov models (conditional laws of $Y_n$ under the recursive path law), Markov Decision Processes on Borel spaces with measurable selection, and the one-period no-arbitrage existence theorem; all of these are reusable beyond this mission. Contributions of lemmas on the filter, the predictive law and the compactness of $D(x)$ are welcome.

Selected references

• N. Bäuerle, U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011; Chapter 5 (pp.147–174) and Chapter 6 (pp.175–189). https://doi.org/10.1007/978-3-642-18324-9
• W. Runggaldier, B. Trivellato, T. Vargiolu, A Bayesian adaptive control approach to risk management in a binomial model, in Seminar on Stochastic Analysis, Random Fields and Applications III (Ascona, 1999), Birkhäuser, 2002, 243–258 (as cited in the book's bibliography).
• G. Favero, Shortfall risk minimization under model uncertainty in the binomial case: adaptive and robust approaches, Mathematical Methods of Operations Research 53, 2001, 493–503 (as cited in the book's bibliography).
• M. Taksar, X. Zeng, Optimal terminal wealth under partial information: both the drift and the volatility driven by a discrete-time Markov chain, SIAM Journal on Control and Optimization 46, 2007, 1461–1482 (as cited in the book's bibliography).

Motivation

Convexity and concavity of trace functions of matrices are a basic tool of mathematical physics and quantum information. Lieb's concavity theorem (Lieb 1973), that $(A,B)\mapsto\operatorname{Tr}K^*A^pKB^{1-p}$ is jointly concave for $0<p\le1$, settled the Wigner–Yanase–Dyson conjecture on the concavity of skew information and underlies the strong subadditivity of quantum entropy. Ando's convexity theorem (Ando 1979) is its counterpart for $-1\le p<0$.

In quantum information the same functions govern the data processing inequality for Rényi-type divergences. The $\alpha$-$z$ Rényi relative entropies of Audenaert–Datta 2015 are monotone under completely positive trace preserving maps exactly when a two-variable trace function of the form below is jointly convex or concave with exponent $s=1/(p+q)$.

Timeline:

• 1973: Epstein proves concavity of $A\mapsto\operatorname{Tr}(K^*A^pK)^{1/p}$ for $0<p\le1$ by complex analysis; Lieb proves joint concavity of $\operatorname{Tr}K^*A^pKB^{1-p}$.
• 1979: Ando proves the joint convexity for $-1\le p<0$.
• 2008: Carlen and Lieb prove convexity of $\operatorname{Tr}(K^*A^pK)^{1/p}$ for $1\le p\le2$ by a variational method (arXiv:0710.4167).
• 2013: Hiai proves convexity of $\operatorname{Tr}(K^*A^pK)^s$ for $-1\le p<0$, $0<s\le1$.
• 2015: Audenaert and Datta conjecture the range of $(\alpha,z)$ for monotonicity.
• 2018: Carlen, Frank and Lieb survey the area and pose a stronger conjecture covering all $s\ge1/(p+q)$ (arXiv:1806.03985).
• 2018–2020: Zhang proves the full range (arXiv:1811.01205), the paper of this mission.

Setting

Fix a finite index type $n$, so matrices are elements of $\mathbb C^{n\times n}$. A matrix $A$ is positive definite if it is Hermitian with strictly positive eigenvalues; for such $A$ and real $p$, the real power $A^p$ is defined by applying $x\mapsto x^p$ to the eigenvalues (Lean: OgawaNagaoka.matPow A p). Fix an invertible matrix $K$ and real numbers $p,q,s$. The trace function of the paper is

$$\Psi_{p,q,s}(A,B)=\operatorname{Tr}\big(B^{q/2}K^*A^pKB^{q/2}\big)^s$$

on pairs $(A,B)$ of positive definite matrices (Lean: ZhangCFL.Psi p q s K A B). Its one-variable specialization is $\Upsilon_{p,s}(A)=\operatorname{Tr}(K^*A^pK)^s$ (Lean: ZhangCFL.Upsilon p s K A). For any matrix $X$, write $|X|=(X^*X)^{1/2}$ and $\operatorname{Tr}|X|^r=\operatorname{Tr}(X^*X)^{r/2}$ (Lean: ZhangCFL.trAbsPow r X).

$\Psi_{p,q,s}$ is jointly concave if for all pairs $(A_1,B_1),(A_2,B_2)$ and $\lambda\in[0,1]$, $\Psi(\lambda A_1+(1-\lambda)A_2,\lambda B_1+(1-\lambda)B_2)\ge\lambda\Psi(A_1,B_1)+(1-\lambda)\Psi(A_2,B_2)$, and jointly convex with the inequality reversed.

Formalization targets

Goal: Theorem 1.1

Assume $p\ge q$ and $s>0$. Then $\Psi_{p,q,s}$ is

$$\begin{aligned} &\text{(1) jointly concave if } 0\le q\le p\le1,\ 0<s\le\tfrac1{p+q};\\ &\text{(2) jointly convex if } -1\le q\le p\le0,\ s>0;\\ &\text{(3) jointly convex if } -1\le q\le0,\ 1\le p\le2,\ (p,q)\ne(1,-1),\ s\ge\tfrac1{p+q}. \end{aligned}$$

The normalization $p\ge q$, $s>0$ loses nothing by symmetry, and the ranges are sharp (Proposition 2.3 of the paper, cited).

Milestones, in attack order

1. Lemma 3.1 (Lieb, Ando): joint concavity of $\operatorname{Tr}K^*A^pKB^{1-p}$ for $0<p\le1$, joint convexity for $-1\le p<0$.
2. Lemma 3.2: pointwise suprema of convex functions are convex, partial infima of jointly convex functions are convex, and the concave analogues.
3. Theorem 3.3: the variational formulas

$$\operatorname{Tr}|XY|^{r_0}=\min_{Z}\Big\{\tfrac{r_0}{r_1}\operatorname{Tr}|XZ|^{r_1}+\tfrac{r_0}{r_2}\operatorname{Tr}|Z^{-1}Y|^{r_2}\Big\},\quad \operatorname{Tr}|XY|^{r_1}=\max_{Z}\Big\{\tfrac{r_1}{r_0}\operatorname{Tr}|XZ|^{r_0}-\tfrac{r_1}{r_2}\operatorname{Tr}|Y^{-1}Z|^{r_2}\Big\}$$

for $\frac1{r_0}=\frac1{r_1}+\frac1{r_2}$, $Z$ ranging over invertible matrices. 4. $Z\mapsto\operatorname{Tr}Z^r$ is convex on positive definite matrices for every $r<0$ (used in the proof of Theorem 3.7). 5. Theorem 3.7 (Epstein, Hiai, Carlen–Lieb): concavity of $\Upsilon_{p,1/p}$ for $0<p\le1$; convexity of $\Upsilon_{p,s}$ for $-1\le p<0$, $0<s\le1$; convexity of $\Upsilon_{p,1/p}$ for $1\le p\le2$. 6. Theorem 3.5 (Carlen–Frank–Lieb): $\Upsilon_{p,s}$ is concave for $0<p\le1$, $0<s\le1/p$; convex for $-1\le p\le0$, $s>0$; convex for $1\le p\le2$, $s\ge1/p$. 7. The identity $\Psi_{p,q,s}(A,B)=\operatorname{Tr}|A^{p/2}KB^{q/2}|^{2s}$ that opens the proof of Theorem 1.1.

Significance

Theorem 1.1 gives the complete region of $(p,q,s)$ in which $\Psi_{p,q,s}$ is jointly concave or convex for every invertible $K$. Part (3) confirms the conjecture of Carlen, Frank and Lieb, and its case $s=1/(p+q)$ the Audenaert–Datta conjecture; together with known necessity results this yields the exact set of $(\alpha,z)$ for which the $\alpha$-$z$ Rényi relative entropy satisfies the data processing inequality (Theorem 1.2 of the paper, not part of this mission). The same theorem recovers the concavity results of Lieb and Epstein and the convexity results of Ando, Carlen–Lieb and Hiai as special cases.

The result is proved; as far as is recorded on the platform, none of it is formalized. A machine-checked development would supply real powers of positive definite matrices with their calculus, trace Hölder and Young inequalities for Schatten quasi-norms, the variational formulas of Theorem 3.3, and Lieb's concavity theorem, all of which are reusable throughout quantum information theory (relative entropies, recoverability, entropy inequalities).

Difficulty

The variational reduction itself is short once its inputs exist; the weight lies in the inputs. Lemma 3.1 is Lieb's concavity theorem and Ando's convexity theorem, which rest on operator concavity and convexity of $A\mapsto A^p$ and are absent from Mathlib. Theorem 3.3 requires Hölder's inequality for Schatten $r$-quasi-norms with $r$ possibly below $1$, together with polar decompositions to exhibit the extremizers. The tempting shortcut of proving convexity separately in $A$ and in $B$ does not work: separate convexity does not imply joint convexity, and the theorem is about the pair.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type n : Type with decidable equality; the dimension is arbitrary, including $0$. Positive definite means Matrix.PosDef (with open scoped ComplexOrder), and invertibility of $K$ is IsUnit K. Real powers are the published OgawaNagaoka.matPow (continuous functional calculus with Real.rpow), and traces are the real part of Matrix.trace, which is the trace itself on the positive definite matrices involved. Joint concavity and convexity are ConcaveOn ℝ/ConvexOn ℝ on the set of pairs of positive definite matrices. In Theorem 1.1 the bound $s\le1/(p+q)$ is written $s(p+q)\le1$, so that at $p=q=0$ the clause is not vacuous; Lemma 3.2 takes suprema and infima in EReal, with no boundedness hypothesis; minima and maxima in Theorem 3.3 are IsLeast/IsGreatest, so they are attained.

Positive semidefinite inputs are not a substitute for positive definite ones: on singular matrices matPow at a negative exponent is a generalized inverse power, and the statements change meaning.

Contributions welcome: proofs of the milestones in any order; Lieb's concavity theorem and the trace Hölder inequality are the reusable cores.

Selected references

• H. Zhang, From Wigner-Yanase-Dyson conjecture to Carlen-Frank-Lieb conjecture, Adv. Math. 365 (2020); arXiv:1811.01205v2. https://arxiv.org/abs/1811.01205
• E. A. Carlen, R. L. Frank, E. H. Lieb, Inequalities for quantum divergences and the Audenaert–Datta conjecture, J. Phys. A 51 (2018). https://arxiv.org/abs/1806.03985
• E. H. Lieb, Convex trace functions and the Wigner-Yanase-Dyson conjecture, Adv. Math. 11 (1973). https://doi.org/10.1016/0001-8708(73)90011-X
• T. Ando, Concavity of certain maps on positive definite matrices and applications to Hadamard products, Linear Algebra Appl. 26 (1979). https://doi.org/10.1016/0024-3795(79)90179-4
• E. A. Carlen, E. H. Lieb, A Minkowski type trace inequality and strong subadditivity of quantum entropy II, Lett. Math. Phys. 83 (2008). https://arxiv.org/abs/0710.4167
• K. M. R. Audenaert, N. Datta, α-z-Rényi relative entropies, J. Math. Phys. 56 (2015). https://doi.org/10.1063/1.4906367

Selling with few price changes

Network revenue management studies a firm that sells several products made from shared, limited resources over a finite season: airline seats on connected legs, hotel room nights, retail items that share inventory. In the blind version the firm does not know how demand responds to price and has to learn it while selling. Besbes and Zeevi (2012) posed this problem, and later work reached regret of order $\sqrt T$ over $T$ periods (Agrawal and Devanur 2014, Badanidiyuru, Kleinberg and Slivkins 2013). Almost all of those algorithms change prices order-$T$ times, which retailers usually cannot do. Simchi-Levi, Xu and Zhao ask how much regret a limit on the number of price changes costs, and how that cost depends on the number of resources.

Setting

A BNRM problem has a horizon of $T$ periods, $d$ resources with inventories $B_i$, $n$ products, a consumption matrix $A=(a_{ij})$ and $K$ price vectors $\mathbf p_k=(p_{j,k})_j$. Each period the firm posts one price vector $z_t$. Under price vector $k$ the demand of product $j$ is a random variable $Q_{j,k}\in[0,1]$ with an unknown law, independent across products and fresh each period. A unit of demand for product $j$ earns $p_{j,k}$ and uses $a_{ij}$ of resource $i$. Selling stops as soon as the cumulative consumption of some resource exceeds its inventory.

A switch is a period with $z_t\ne z_{t+1}$. A non-anticipating policy $\phi$ picks $z_t$ from a probability kernel on the past actions and demands. $\Phi[s]$ is the set of policies with at most $s$ switches almost surely under every demand law, and $\Pi_Q[s]$ is the set of policies with at most $s$ switches under the law $Q$. The $s$-switch regret and the regret are

$$R^\phi_s(T)=\sup_Q\Big(\sup_{\pi\in\Pi_Q[s]}\mathrm{Rev}_Q(\pi)-\mathrm{Rev}_Q(\phi)\Big),\qquad R^\phi(T)=\sup_Q\Big(\sup_{\pi}\mathrm{Rev}_Q(\pi)-\mathrm{Rev}_Q(\phi)\Big).$$

The deterministic LP $J^{\mathrm{DLP}}$ maximizes $\sum_{k,j}p_{j,k}q_{j,k}x_k$ subject to $\sum_{k,j}a_{ij}q_{j,k}x_k\le B_i$, $\sum_k x_k\le T$, $x\ge0$, where $q_{j,k}=\mathbb E[Q_{j,k}]$. Its role is that of the benchmark. The rate is governed by the integer

$$\nu(s,d)=\Big\lfloor\frac{s-d-1}{K-1}\Big\rfloor .$$

Formalization targets

Goal: the optimal rate

With $B_i/T\in[b,1]$, $K\ge2(d+1)$, $n\ge d+1$ and $T\ge2$, there is a problem with these $T$ and $\mathbf B$ (entries of $P$ at most $1$, of $A$ at most $2$) such that, for every $s$, the minimax regret over $\Phi[s]$ satisfies

$$\min\{c_Lb,c_L'\}\,\frac{K^{-\frac32-a}}{(d+1)^{3}(\log T)^{5/2}}\,T^{a}\ \le\ \inf_{\phi\in\Phi[s]}R^\phi_s(T),\qquad a=\frac1{2-2^{-\nu(s,d)}},$$

while on every problem with these $T$ and $\mathbf B$ and entries bounded by $p_{\max}$, $a_{\max}$, the algorithm LS-2SLP exists, is in $\Phi[s]$, and, when $n\le(d+1)\log[(d+1)KT](\log T)^2$,

$$R^\phi(T)\le\max\{c_U/b,c_U'\}\,\sqrt{n^3(d+1)\log[(d+1)KT]}\,K^{1-a}\log T\;T^{a}.$$

$c_L,c_L'$ are numerical; $c_U,c_U'$ depend only on $a_{\max},p_{\max}$. This is the $\tilde\Theta(T^{1/(2-2^{-\nu(s,d)})})$ of §4.3.

Milestones

• Theorem 3 (upper bound) with its preparations: Lemma EC.1 on the epoch grid, and the DLP bound of §3.1.
• Theorem 4 (lower bound) with its preparations: Lemmas EC.3–EC.7, the comparator bound (EC.46), and the bandit bound $C_{\mathrm{MAB}}\sqrt{KT}$.

Significance

The result. The optimal regret is a step function of $s$. Roughly $\log\log T$ switches suffice for $\tilde\Theta(\sqrt T)$, and with $s\le d+1$ the regret is linear. Each extra resource costs one more switch, the first result, according to the authors, that shows how the dimension of the constraints makes a stochastic online learning problem harder. Theorem 3 also shows that a small number of LPs replaces the elimination over mixtures of Badanidiyuru et al.

Formalizing it. The result is proved on paper and, to the extent we could determine, has no machine-checked proof. The platform has switching-limited bandits without resources (BwSC.LowerBound.theorem_2) and bandits with knapsacks without switch limits, but nothing with both. Formalization also records corrections to the printed statements. Theorem 3 fails at $T=1$, and its proof hides epoch-1 consumption of order $n\,a_{\max}t_1$, so the printed bound fails for $n$ growing like $(\log T)^5$. For fixed $n$ the rate in $T$ is untouched. The DLP does not bound revenue exactly under the paper's stopping rule, so a factor $1+\max_i\sum_ja_{ij}/B_i$ appears. Lemmas EC.1, EC.3, EC.4 and EC.7 carry smaller corrections, each with a counterexample in its item.

Difficulty

For the upper bound, single-arm elimination and uniform exploration both fail, because the optimal play is a mixture of arms. The epoch lengths are fixed, but the number of plays $n_k$ of each arm comes out of LPs with data-dependent values and has no closed form. The natural analysis, which plugs a confidence radius into a fixed sample count, therefore does not apply.

For the lower bound, the argument for bandits with limited switches tracks the cover times of an arbitrary policy and gives $\lfloor(s-1)/(K-1)\rfloor$. Moving to $\lfloor(s-d-1)/(K-1)\rfloor$ requires instances whose LP optimum has $d+1$ non-zeros at every shift, such that any policy that neglects a family of arms loses linear revenue, under a benchmark that itself has at most $s$ switches.

Formalization scope

Periods, arms and products are $0$-based in Lean. Actions are Option (Fin K), where none is an absorbing stop, as Algorithm 2 stops once it has run. The history law is built period by period from Markov kernels. Demand vectors have the product law of their marginals. A period earns revenue exactly when cumulative consumption through it is within every inventory. LearningClass quantifies over all DemandLaw, and clairvoyant classes over all history-dependent policies with the switch bound under that law.

Regrets are real suprema of nonempty bounded families, with integrable revenue, and the verification file proves these facts, so no statement holds through a junk value. $T\ge2$ excludes $(\log T)^{-5/2}$ at $T=1$, where Lean's $0^{-5/2}=0$ would trivialize the lower bound. The goal asserts that LS-2SLP exists, so its upper clause cannot hold vacuously. IsLS2SLP fixes what Algorithm 2 overlooks: rounding by $\lceil\gamma N_k\rceil$, sparse LP solutions, empty samples and the order of arms within an epoch.

A complete development needs the DLP layer, Hoeffding and maximal concentration for the clean events, a change-of-measure bound for the Bernoulli history laws, a measurable selection of LP solutions, and the bandit lower bound in this model. The DLP bound and the history law are reusable for other network revenue management missions. Proofs of Lemmas EC.4 and EC.1 and of the DLP bound are the natural starting points, and direct proofs of the theorems are welcome too.

Selected references

• D. Simchi-Levi, Y. Xu, J. Zhao, Blind Network Revenue Management and Bandits with Knapsacks Under Limited Switches, arXiv:1911.01067v5, 2025; Operations Research. https://arxiv.org/abs/1911.01067
• O. Besbes, A. Zeevi, Blind Network Revenue Management, Operations Research 60(6), 2012. https://doi.org/10.1287/opre.1120.1103
• A. Badanidiyuru, R. Kleinberg, A. Slivkins, Bandits with Knapsacks, FOCS 2013. https://arxiv.org/abs/1305.2545
• S. Agrawal, N. Devanur, Bandits with Concave Rewards and Convex Knapsacks, EC 2014. https://arxiv.org/abs/1402.5758
• D. Simchi-Levi, Y. Xu, Phase Transitions in Bandits with Switching Constraints, Management Science 69(12), 2023. https://doi.org/10.1287/mnsc.2023.4755