Missions · Prove2Me

Machine Learning Reinforcement Learning Statistics·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making III: E2D with Hellinger Confidence Sets Has Regret at Most Σ_t sup dec_γ(M_εt(M̄), M̄) + γ·Est_H(T,δ)Research Paper

Motivation

Interactive decision making covers bandits, contextual bandits and reinforcement learning: a learner repeatedly chooses a decision, observes a reward and an observation drawn from an unknown model, and tries to accumulate nearly as much reward as the best decision for that model. Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) introduced the Decision-Estimation Coefficient (DEC), a single quantity that gives lower bounds on the regret of every algorithm and, through the Estimation-to-Decisions (E2D) meta-algorithm, matching upper bounds. This mission formalizes the upper-bound side in its strongest form: E2D run with Hellinger confidence sets (Option II of Algorithm 1) has regret controlled by the localized DEC, the same quantity that appears in the paper's lower bounds (Theorems 3.1 and 3.2).

The basic E2D guarantee (33) in terms of the global DEC is already posed on Prove2Me as an open goal (FoundationsRL.GeneralDM.e2d_general_regret_bound_v2, the restatement in Foster and Rakhlin's lecture notes, arXiv:2312.16730, Proposition 26). It is not posed again here.

Setting

A decision space $\Pi$ is a finite set. An outcome $y = (r, o)$ consists of a reward and an observation and ranges over a finite set $Y$ , and $\mathrm{rew}(y) \in [0,1]$ is its reward. A model $M$ assigns to every decision $\pi$ a probability distribution $M(\pi)$ on $Y$ . Its mean reward is $f^M(\pi) = \mathbb E_{y\sim M(\pi)}[\mathrm{rew}(y)]$ , and $\pi_M$ is a decision maximizing $f^M$ . The learner knows a model class $\mathcal M$ that contains the true model $M^\star$ . At round $t$ it plays a distribution $p^{(t)}$ on $\Pi$ , and its regret is

\mathrm{Reg}_{\mathrm{DM}} = \sum_{t=1}^T \mathbb E_{\pi\sim p^{(t)}}\big[f^{M^\star}(\pi_{M^\star}) - f^{M^\star}(\pi)\big].

Write $D^2_{\mathrm H}(P,Q) = \sum_y (\sqrt{P(y)} - \sqrt{Q(y)})^2$ for the squared Hellinger distance. For a reference model $\bar M$ and $\gamma > 0$ the DEC is

\mathrm{dec}_\gamma(\mathcal M, \bar M) = \inf_{p\in\Delta(\Pi)} \sup_{M\in\mathcal M} \mathbb E_{\pi\sim p}\big[f^M(\pi_M) - f^M(\pi) - \gamma\, D^2_{\mathrm H}(M(\pi), \bar M(\pi))\big].

The localized class $\mathcal M_\varepsilon(\bar M) = \{M\in\mathcal M : f^{\bar M}(\pi_{\bar M}) \ge f^M(\pi_M) - \varepsilon\}$ keeps only the models whose optimal value exceeds that of $\bar M$ by at most $\varepsilon$ .

E2D with Option II receives at each round an estimate $\widehat M^{(t)}$ from an online estimation oracle. It keeps the confidence set $\mathcal M^{(t)}$ of models whose accumulated Hellinger error against past estimates, $\sum_{i<t}\mathbb E_{\pi\sim p^{(i)}}[D^2_{\mathrm H}(M(\pi), \widehat M^{(i)}(\pi))]$ , is at most $R^2$ . It plays a minimizer $p^{(t)}$ of the DEC problem over $\mathcal M^{(t)}$ at $\widehat M^{(t)}$ . Assumption D.1 asks that, with probability $1-\delta$ , the oracle's Hellinger error on the rounds where $M^\star \in \mathcal M^{(t)}$ is at most a known bound $\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)$ . It also asks that $\widehat M^{(t)} \in \mathrm{co}(\mathcal M^{(t)})$ .

Formalization targets

Goal: Theorem 4.1, (35) (in the form (137) of Theorem 4.1a)

With $R^2 = \widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)$ , rewards in $[0,1]$ and $\gamma > 0$ , with probability at least $1-\delta$ ,

\mathrm{Reg}_{\mathrm{DM}} \le \sum_{t=1}^T \sup_{\bar M\in\mathrm{co}(\mathcal M)} \mathrm{dec}_\gamma\big(\mathcal M_{\varepsilon_t}(\bar M), \bar M\big) + \gamma\, \widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta),

\varepsilon_t = 6\frac{\gamma}{t}\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta) + \sup_{\bar M\in\mathrm{co}(\mathcal M)}\mathrm{dec}_\gamma(\mathcal M,\bar M) + (2\gamma)^{-1}.

Milestones (the steps of the proof in App. D.1)

(138): the per-round step. At a minimizer $p^{(t)}$ , the instantaneous regret minus $\gamma$ times the Hellinger error of $M^\star$ is at most $\mathrm{dec}_\gamma(\mathcal M^{(t)}, \widehat M^{(t)})$ .
Lemma D.1: on the event of Assumption D.1, $M^\star \in \mathcal M^{(t)}$ for every $t$ , and the total Hellinger error is at most $\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)$ .
Lemma D.2: if $M\in\mathcal M^{(i)}$ for all $i\le t$ , then for any model $\bar M$ , $f^M(\pi_M) - f^{\bar M}(\pi_{\bar M})$ is bounded by $(2\gamma)^{-1}$ plus the average over $i\le t$ of the DEC values and Hellinger errors.
Containment: $\mathcal M^{(t)} \subseteq \mathcal M_{\varepsilon_t}(\widehat M^{(t)})$ for every round, with the radius derived on p. 99 using $2\sup\mathrm{dec}$ .

Companion results

Theorem 4.3, (47): E2D for a general divergence $D \ge 0$ and randomized estimators $\nu^{(t)}$ satisfies $\mathrm{Reg}_{\mathrm{DM}} \le \sup_{\nu\in\Delta(\widehat{\mathcal M})}\mathrm{dec}^D_\gamma(\mathcal M,\nu)\cdot T + \gamma\,\mathrm{Est}_D$ almost surely. With $D = D^2_{\mathrm H}$ and point estimates it contains (33), so it is a generalization of the open goal above, not the same statement.
Theorem 8.1, (87): contextual E2D with arbitrary contexts satisfies $\mathrm{Reg}_{\mathrm{DM}} \le \sup_{x}\mathrm{dec}^D_\gamma(\mathcal M|_x, \widehat{\mathcal M}|_x)\cdot T + \gamma\,\mathrm{Est}_D$ .

Significance

The bound is the paper's most general upper bound. Together with the lower bounds of §3, it shows that the localized DEC characterizes the regret of interactive decision making up to the estimation term. With an aggregating estimator satisfying $\widehat M^{(t)}\in\mathrm{co}(\mathcal M^{(t)})$ (App. A.3), it recovers the finite-class guarantee of Theorem 3.3. The companions extend E2D to general divergences, randomized estimators and adversarially chosen contexts. That last setting contains SquareCB for contextual bandits.

All results of this mission are proved in the paper. None was machine-checked before. Formalizing them produces a checked reduction from decision making to estimation for finite decision and outcome spaces, stated against the published DEC and localized-class definitions, so that later bounds on the DEC of specific classes (bandits, tabular RL) can be combined with it.

Difficulty

The non-localized bound follows from the per-round step (138) by summation. The localized bound does not: the per-round DEC is taken over the confidence set $\mathcal M^{(t)}$ , and replacing it by a localized class requires that every model surviving in $\mathcal M^{(t)}$ have optimal value close to that of the current estimate $\widehat M^{(t)}$ . The confidence set constrains Hellinger errors against past estimates, not optimal values, and the estimate itself is in general not a member of the class. Bridging these is the content of Lemma D.2 and the containment. The first round is a boundary case: there the confidence set is the whole class, so the containment holds only if the radius $\varepsilon_1$ is at least the full range of the rewards.

Formalization scope

Finite alphabets. The paper works over measurable spaces. This mission takes a finite decision set $\Pi$ (a Fintype), a finite outcome set $Y$ , and models m : S → Y → ℝ with every m π a probability vector. Expectations are finite sums. Contexts in Theorem 8.1 range over an arbitrary type.
Published layer. Hellinger distance, $f^M$ , regret, the DEC (decGf, and dec for the supremum over $\mathrm{co}(\mathcal M)$ ) and the localized class are the published FoundationsRL.GeneralDM definitions, referenced and not redefined.
Pathwise statements. A run is a realized sequence of estimates, distributions and confidence sets tied to Algorithm 1 by IsOptionIIRun (lines 7 and 8 and $\widehat M^{(t)}\in\mathrm{co}(\mathcal M^{(t)})$ ). "With probability at least $1-\delta$ " becomes the hypothesis EventD1, the event of Assumption D.1. Line 8's arg min is relaxed to "certifies the minimax value from above", as Remark 4.1 permits. Rounds are 0-based, and $\varepsilon_t$ is evaluated at the paper's index.
Added hypothesis $R^2 \ge 1/12$ in the goal and the containment. Without it the goal is false. With $R^2 = 0$ , two decisions, two Bernoulli models and $\gamma = 10$ , the first round has positive regret while the right side is $0$ . In applications $\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)\ge 2\log(1/\delta)$ .
Radius. The goal uses the printed theorem radius with $1\cdot\sup\mathrm{dec}$ . The containment milestone uses the p. 99 proof radius with $2\cdot\sup\mathrm{dec}$ . Averaging the DEC terms over the $t-1$ earlier rounds gives the goal's sharper factor.
Junk values. When a localized class is empty, its Lean DEC is $0$ instead of $-\infty$ , which only weakens the bound. All other suprema are over nonempty bounded sets.
Ruled out. Leaving the confidence sets, estimates or distributions unconstrained would make the goal false or trivial; they are tied to the algorithm by IsOptionIIRun. The open bound (33) is not restated.
Welcome contributions. Convexity and the triangle inequality for $D^2_{\mathrm H}$ , the bound $|f^M - f^{\bar M}| \le D_{\mathrm H}$ for rewards in $[0,1]$ , and monotonicity of decGf in the class are reusable beyond this mission.

Selected references

D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, v3, 2023. https://arxiv.org/abs/2112.13487
D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. https://arxiv.org/abs/2312.16730
D. J. Foster, A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML 2020. https://arxiv.org/abs/2002.04926

13 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Potential Games Are Necessary to Ensure Pure Nash Equilibria in Cost Sharing Games 1: Every Game Has a Pure Nash Equilibrium Iff the Distribution Rules Are Generalized Weighted Shapley ValuesResearch Paper

Motivation

In a cost sharing game (or, symmetrically, a revenue sharing game) self-interested players each pick a set of resources, every resource generates a welfare that depends on who uses it, and a distribution rule splits that welfare among the users. Network formation, atomic routing, coverage and distributed-control problems all fit this model (Anshelevich et al. 2004; Marden and Wierman, Distributed welfare games, 2013; see §2 of the paper). The designer controls only the distribution rule, and the first requirement on a rule is that the games it induces have a pure Nash equilibrium; without one, equilibrium-based efficiency guarantees say nothing.

Which rules guarantee equilibria? The Shapley value and its weighted and generalized-weighted versions do, because they induce potential games (Hart and Mas-Colell 1989). Chen, Roughgarden and Valiant (2010) and Marden and Wierman (Overcoming the limitations of utility design for multiagent systems, 2013) showed that, among budget-balanced rules, these are the only ones that work for every welfare function, by exhibiting one worst-case welfare function (Proposition 1 of the paper, p. 9). Marden and Wierman (Distributed welfare games) also showed that when players may choose only one resource, other budget-balanced rules can work. That left open what happens when the designer knows the welfare functions in advance, and whether dropping budget-balance enlarges the set of good rules. Gopalakrishnan, Marden and Wierman 2014 answered both questions: for any fixed set of welfare functions, with or without budget-balance, the equilibrium-guaranteeing rules are exactly generalized weighted Shapley values on suitable ground welfare functions.

Setting

Players are $N=\{1,\dots,n\}$ with $n>1$ ; resources are $R=\{r_1,\dots,r_m\}$ with $m>1$ . A local welfare function is $W:2^N\to\mathbb R$ and a distribution rule is $f:N\times2^N\to\mathbb R$ , where $f(i,S)$ is the share of player $i$ when sharing with the coalition $S$ (and $f(i,S)=0$ for $i\notin S$ ). Each player $i$ has a nonempty action set $\mathcal A_i\subseteq 2^R$ . In an allocation $a$ , the users of $r$ are $\{a\}_r=\{i:r\in a_i\}$ and player $i$ receives

U_i(a)=\sum_{r\in a_i}f^{W_r}\bigl(i,\{a\}_r\bigr).

Resources with equal welfare functions use the same rule. For a nonempty set $\mathbb W$ of welfare functions, $\mathcal G(N,f^{\mathbb W},\mathbb W)$ is the class of all such games with every $W_r\in\mathbb W$ , any number of resources and any action sets. A rule is budget-balanced for $W$ if $\sum_{i\in S}f(i,S)=W(S)$ .

A weight system $\omega=(\lambda,\Sigma)$ consists of positive weights $\lambda_i$ and an ordered partition $\Sigma=(S_1,\dots,S_K)$ of $N$ into priority classes. For nonempty $T$ , $\overline T=T\cap S_k$ with $k$ the first class meeting $T$ . With the basis coefficients $q^W_T=\sum_{R\subseteq T}(-1)^{|T|-|R|}W(R)$ , the generalized weighted Shapley value is

f^W_{GWSV}[\omega](i,S)=\sum_{T\subseteq S:\,i\in\overline T}\frac{\lambda_i}{\sum_{j\in\overline T}\lambda_j}\,q^W_T .

The distributed welfare of a rule is $W'(S)=\sum_{i\in S}f^W(i,S)$ , display (10).

Formalization targets

Goal: Theorem 1

\text{all games in }\mathcal G(N,f^{\mathbb W},\mathbb W)\text{ have a pure Nash equilibrium}\iff\exists\,\omega\ \forall W\in\mathbb W:\ f^W=f^{W'}_{GWSV}[\omega]\text{ on }\{(i,S):i\in S\},

with $W'$ the distributed welfare of $f^W$ . One weight system serves all of $\mathbb W$ .

Milestones

The "if" direction (Appendix A, p. 16). For a single $W$ and a budget-balanced $f$ guaranteeing equilibria: $f(i,S)=0$ when $S$ contains no contributing coalition (Lemma 1) and for non-contributing $i$ (Lemma 2); $f(i,S)=f(i,N(S))$ (Lemma 3). The basis rules $f^T$ of the recursion (27) are budget-balanced for the inclusion functions (Lemma 5), recover $f=\sum_Tq_Tf^T$ (Lemma 7), obey an inclusion–exclusion principle (Corollary 1), and are generalized weighted Shapley basis rules $f^T_{GWSV}[\omega^T]$ (Lemma 8). Across welfare functions the basis shares are consistent pairwise (Lemma 9) and around cycles (Lemma 10); the induced relation on players is a partial order modulo equivalence (Lemma 11), and one universal weight system replaces all $\omega^{W,T}$ (Lemma 13).

Companions

Proposition 2: for welfare functions normalized by $W'(\emptyset)=W''(\emptyset)=0$ , $f^{W'}_{GWSV}[\omega]=f^{W''}_{GWMC}[\omega]$ iff $\mathcal T'=\mathcal T''$ and $q'_T=(\sum_{j\in\overline T}\lambda_j)q''_T$ . Theorem 2: the same characterization with generalized weighted marginal contributions on $W''=h(W')$ .

Significance

The theorem settles the design space completely: a designer who wants equilibria in every game over known welfare functions must use a generalized weighted Shapley value, and the only freedom is the weight system and the ground welfare functions, which control budget-balance. Since these rules induce (generalized weighted) potential games, potential games are necessary for guaranteed equilibrium existence in this model, and computing shares inherits the exponential cost of Shapley values. Theorem 2 gives the marginal-contribution form, which needs one marginal contribution per share.

The paper proves Theorem 1 with a full appendix of counterexample constructions; none of it has a published machine-checked proof. The mission asks for a Lean proof of the characterization, of the reusable structure behind it (necessary conditions, basis decomposition, inclusion–exclusion for basis rules, consistency of weight systems), and of the Shapley–marginal-contribution correspondence.

Difficulty

The "if" direction is a potential argument. The "only if" direction is not: every necessary condition is proved by building, from a hypothetical violation, a specific game with no equilibrium, and the games grow more elaborate as the conditions do. Lemma 8 needs the inclusion–exclusion principle to isolate a single basis share, using many weighted copies of resources; Lemma 10's proof combines best-response cycles over $k$ welfare functions and is partly omitted on the page ("We omit the proof for brevity", p. 51), so it is the hardest milestone. A tempting shortcut, applying the worst-case result of Chen et al. and Marden–Wierman (Proposition 1, p. 9), fails: it uses one worst-case welfare function, while here $\mathbb W$ is arbitrary and may not contain it.

Formalization scope

Players are Fin n, resources Fin m, an action is a Finset (Fin m) (the empty action is allowed). The family of rules is one function f : Welfare n → Rule n, which encodes that equal welfare functions get equal rules. GuaranteesPNE 𝕎 f quantifies over every m > 1, every assignment Fin m → 𝕎 (repetitions allowed: the counterexamples rely on many copies of one welfare function) and every family of nonempty action sets. A weight system stores a block index Fin K per player (empty blocks allowed) and positive weights. Rules are compared only at $i\in S$ . Contributing coalitions exclude $\emptyset$ (Appendix A's normalization $W(\emptyset)=0$ ). The recursion (27) divides by $q_T$ and is used only for contributing $T$ ; where it reads $f(i,T)$ with $i\notin T$ , the paper's convention $f(i,S)=0$ off $S$ is a hypothesis.

The ground welfare in Theorem 1 is the distributed welfare (10), written out, never an arbitrary function: an existentially quantified ground welfare would make the right side easier and the theorem a different one. The weight system is quantified before the welfare functions, and empty action sets are excluded; with them no game would have an equilibrium and the theorem would claim that no rule is a Shapley value.

Disclosed readings: Lemma 11's "partial order" is antisymmetry modulo the equivalence $=^+_\Omega$ , as the proof states; in (74) the first block $S_1^{W,T}$ is read on $T$ as its positive-share block $\overline T$ . Proposition 2 carries $W'(\emptyset)=W''(\emptyset)=0$ so that the paper's basis support, which ranges over all coalitions, agrees with the local support of nonempty coalitions.

A complete development needs: finite games and pure equilibria on resource-selection models, Möbius inversion on Finset lattices, the potential argument for generalized weighted Shapley values (shared with the companion mission on generalized weighted potential games), and counterexample games built from copies of resources. The game model and the basis-rule recursion are reusable for other cost-sharing results. Proofs of any milestone, and alternative arguments for the necessary conditions, are welcome.

Selected references

R. Gopalakrishnan, J. R. Marden, A. Wierman, Potential Games are Necessary to Ensure Pure Nash Equilibria in Cost Sharing Games, Math. Oper. Res. 39(4), 2014; preprint arXiv:1402.3610v1, 2014. https://arxiv.org/abs/1402.3610v1
S. Hart, A. Mas-Colell, Potential, Value, and Consistency, Econometrica 57(3), 589–614, 1989. https://doi.org/10.2307/1911054
H.-L. Chen, T. Roughgarden, G. Valiant, Designing Network Protocols for Good Equilibria, SIAM J. Comput. 39(5), 1799–1832, 2010 (reference [8] of arXiv:1402.3610v1).
J. R. Marden, A. Wierman, Overcoming the Limitations of Utility Design for Multiagent Systems, IEEE Trans. Autom. Control, 2013 (reference [30] of arXiv:1402.3610v1).
J. R. Marden, A. Wierman, Distributed Welfare Games, Oper. Res., 2013 (reference [29] of arXiv:1402.3610v1).
E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, FOCS 2004, 295–304 (reference [3] of arXiv:1402.3610v1).
L. S. Shapley, A Value for n-Person Games, Contributions to the Theory of Games II, Princeton University Press, 1953 (reference [43] of arXiv:1402.3610v1).

17 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Information Sharing in Competing Supply Chains with Production Cost Reduction: Under Cournot Competition Both Chains Share Below k_N, Both or Neither Between k_N and k_S, and Neither Above k_SResearch Paper

Motivation

Retailers observe demand signals (point-of-sale data, local forecasts) that their suppliers do not. Whether a retailer should pass such a signal upstream is a central question of the supply chain information-sharing literature. In a single chain, sharing helps the manufacturer plan, but the retailer may lose from it. Competition between chains adds a second effect: sharing in one chain changes how the rival chain responds to its own signal.

Ha, Tian and Tong (MSOM 2017) study this question when the manufacturer's planning decision is production cost reduction: a manufacturer that knows more about demand can invest in lowering its unit cost more efficiently. They find that the equilibrium of the information-sharing game between two competing chains depends on a single efficiency parameter $k$ in a three-regime pattern. This mission formalizes that pattern for quantity (Cournot) competition.

Earlier work on information sharing in competing chains (for example Ha, Tong and Zhang, Management Science 2011, on production diseconomies of scale) found related threshold structures under different upstream technologies. The present paper replaces the production cost with a cost-reduction investment.

Setting

There are two identical supply chains $i=1,2$ , each with one manufacturer and one retailer. Retailer $i$ faces the inverse demand

p_i=a+\theta-q_i-\gamma_C q_j,

where $\theta$ is a demand shock with mean $0$ and variance $\sigma^2$ , and $\gamma_C\in(0,1)$ is the competition intensity. Manufacturer $i$ has unit production cost $c$ and lowers it by $x_i$ at effort cost $\tfrac12 kx_i^2$ ; a small $k$ means efficient cost reduction. Retailer $i$ observes a signal $Y_i$ with accuracy $t$ ; under the linear information structure, $E[\theta\mid Y_i]=E[Y_j\mid Y_i]=\tfrac{t\sigma^2}{1+t\sigma^2}Y_i$ .

In stage one, each chain fixes its arrangement $X_i\in\{S,N\}$ : the retailer shares its signal with the manufacturer ( $S$ ) or not ( $N$ ). Then the manufacturer sets a wholesale price and a cost reduction, and the retailer a quantity. For each arrangement profile $(X_i,X_j)$ the quantity stage has a linear equilibrium $q_i=\bar q+C^{X_iX_j}Y_i$ with explicit response coefficients $C^{X_iX_j}(k,\gamma_C,t,\sigma^2)$ (Lemma 2(a)). These give closed-form ex-ante profits $\Pi^{X_iX_j}_{R_i,C}$ , $\Pi^{X_iX_j}_{M_i,C}$ and $\Pi^{X_iX_j}_{i,C}$ for the retailer, the manufacturer and the chain.

The value of information sharing to chain $i$ is $V^{X_j}_{i,C}=\Pi^{SX_j}_{i,C}-\Pi^{NX_j}_{i,C}$ . In stage one, manufacturer $i$ offers retailer $i$ the smallest side payment $\hat m^{X_j}$ that makes sharing acceptable to the retailer, and chooses $S$ or $N$ . The result is a symmetric $2\times2$ game between the two manufacturers (Table 1). Manufacturer $i$ 's payoff is $\Pi^{SX_j}_{M_i,C}-\hat m^{X_j}$ for $S$ and $\Pi^{NX_j}_{M_i,C}$ for $N$ . The standing assumptions are $k>a/(4c)$ , $k>1/3$ and $a>c$ .

Formalization targets

Goal: Proposition 7(a)

For fixed $\gamma_C\in(0,1)$ , $t>0$ and $\sigma^2>0$ there are thresholds

\tfrac12<k^N_C<k^S_C<\tfrac{3+\sqrt5}{4}

such that the set $\mathcal E$ of pure-strategy equilibria of the stage-one game is

\mathcal E=\{(S,S)\}\ (k<k^N_C),\qquad \mathcal E=\{(S,S),(N,N)\}\ (k^N_C<k<k^S_C),\qquad \mathcal E=\{(N,N)\}\ (k>k^S_C).

In the middle regime, both manufacturers are strictly better off at $(S,S)$ than at $(N,N)$ .

Milestones

the linear strategies solve the best responses (proof of Lemma 2(a));
$C^{X_jX_i}_j<1$ and the four coefficient differences in closed form with their signs (proof of Lemma 3);
the retailer gains from sharing if and only if $k\le1/2$ , and for $k\le1/2$ free information strictly raises the manufacturer's profit (§5.3);
$V^S_{i,C}>0\iff g>0$ and $V^N_{i,C}>0\iff h>0$ for two explicit polynomials $g,h$ (proof of Proposition 6(a));
Proposition 6(a): $V^S_{i,C}>0\iff k<k^S_C$ , $V^N_{i,C}>0\iff k<k^N_C$ , the bounds above, and both thresholds strictly decreasing in $t$ and in $\gamma_C$ .

A companion item states the Cournot half of Proposition 7(c): for $k<1/2$ no side payment is needed and $(S,S)$ is the unique equilibrium.

Significance

Proposition 7(a) separates three regimes of cost-reduction efficiency. When cost reduction is efficient ( $k<k^N_C$ ), sharing is dominant. At intermediate efficiency the stage-one game is a coordination game: both chains sharing is Pareto-better for the manufacturers, but both not sharing is also an equilibrium. When cost reduction is inefficient, no chain shares. Competition matters through the gap $k^N_C<k^S_C$ : a chain whose rival shares tolerates a less efficient cost reduction before it stops sharing, and the thresholds fall as signals become more accurate or competition more intense.

The paper proves these facts by hand-checked algebra, often stated as "we can verify". The formalization turns each such step into a checked statement: the fixed-point identities behind Lemma 2(a), the closed forms of Lemma 3, the reduction of the sign of $V$ to the polynomials $g$ and $h$ , and the monotonicity and location of their roots. None of these results has a machine-checked proof yet. The definitions (response coefficients, profits, side payment, stage-one game) are reusable for the Bertrand half of the paper and for other two-chain information-sharing models.

Difficulty

The obvious approach expands $V^S$ and $V^N$ as rational functions of $(k,\gamma_C,t,\sigma^2)$ and tries to read off their signs. That does not finish by itself. After cancelling positive factors, the signs are those of $g$ and $h$ , which are quadratics in $\xi=t^2\sigma^4\gamma_C^2/(t\sigma^2+1)^2\in(0,1)$ with coefficients polynomial in $k$ . The thresholds are defined implicitly by a root of each quadratic crossing $\xi$ . Showing that $\{g>0\}$ and $\{h>0\}$ are initial intervals of $(1/3,\infty)$ needs the relevant root to be strictly decreasing in $k$ , to exceed $1$ below $k=1/2$ and to change sign at $(3+\sqrt5)/4$ . The strict ordering $k^N_C<k^S_C$ needs a comparison of two roots involving $\sqrt{k^3(6k-1)}$ and $\sqrt{k(6k-1)}$ on $(1/2,(3+\sqrt5)/4)$ . The equilibrium analysis then needs the retailer comparison, to know when the side payment is positive. Table 1's payoff entries are valid only in that case.

Formalization scope

Everything is over $\mathbb R$ , in the namespace CompetingChains.Cournot. A general definition TwoPlayerGame gives pure-strategy Nash equilibria of a two-player normal-form game. The definition Setting records the paper's reduced form: the standing assumptions, the response coefficients $C^{X_iX_j}$ of Lemma 2(a), the best responses (7) and (9), the ex-ante profit functions of p. 17, the equilibrium profits $\Pi^{X_iX_j}=\pi^{X_i}(C_j^{X_jX_i})$ , $V$ , $\hat m$ , the stage-one payoff and its set of pure equilibria. The Bayesian stages enter only through these closed forms. The arrangements are an inductive type {S, N}. Manufacturer 2's payoff at $(X_1,X_2)$ is manufacturer 1's payoff at $(X_2,X_1)$ . The chain profit is defined as retailer plus manufacturer profit. The stage-one payoff uses $\hat m$ as printed on p. 21, and agrees with Table 1 whenever the side payment is positive.

Conventions and added hypotheses, each disclosed in the items:

$\gamma_C>0$ wherever the result needs it; at $\gamma_C=0$ the chains do not interact and the middle regime is empty. Positivity of $c$ , $t$ and $\sigma^2$ is part of the standing assumptions.
The goal's "otherwise" is read as $k>k^S_C$ , because both profiles are equilibria at $k=k^N_C$ and $k=k^S_C$ .
Only pure-strategy equilibria are counted. "Unique equilibrium" is equality of the equilibrium set with a singleton, not membership.
The thresholds depend on $(\gamma_C,t,\sigma^2)$ only and are chosen before $a,c,k$ .
"Decreasing" means strictly decreasing.
Every division is real division by a quantity positive under $k>1/3$ , $\gamma_C\ge0$ , $t\sigma^2>0$ . These hypotheses are carried in every theorem, so no statement is about Lean's value $x/0=0$ .

The coefficients, profits, $V$ and payoffs are definitions, never free parameters. A statement with free coefficients, a goal whose thresholds lack $k^N_C<k^S_C$ , or one that only asserts membership of $(S,S)$ would be trivial or weaker, and is not what is posed. No published platform definition states this model, so none is referenced.

Not in scope: Lemma 2's uniqueness (delegated by the paper to earlier work), the wholesale-price and cost-reduction lines of Lemma 2(a), the Bertrand half (Propositions 6(b), 7(b)), the single-chain analysis of §4, Proposition 8 and the numerical study. Proofs of any item are welcome. The polynomial root analysis behind Proposition 6(a) is the main open piece of work.

Selected references

A. Y. Ha, Q. Tian and S. Tong, Information Sharing in Competing Supply Chains with Production Cost Reduction, Manufacturing & Service Operations Management 19(2), 2017. https://doi.org/10.1287/msom.2016.0607
A. Y. Ha, S. Tong and H. Zhang, Sharing Imperfect Demand Information in Competing Supply Chains with Production Diseconomies, Management Science 57(3), 566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295

12 thms2 active usersReviewed

Harmonic Analysis Machine Learning Probability·Captain: mikedeng1

Approximation Bounds for Random Neural Networks and Reservoir Systems I: Random ReLU Networks with Sampled Inner Weights Approximate Fourier-Represented Functions on a Hilbert Space (Theorem 1)Research Paper

Motivation

In random-feature models, also called extreme learning machines or random neural networks, the inner weights of a one-hidden-layer network are drawn at random and only the linear readout is trained. Training is then a least-squares problem, which is why such models, and their dynamic counterparts reservoir computing and echo state networks, are used in practice. The question is how well such a network can approximate a target when it is not allowed to choose its inner weights. Gonon, Grigoryeva and Ortega (Ann. Appl. Probab. 33 (2023) 28–69) answer it with explicit, non-asymptotic $L^2$ bounds. Their first result, Theorem 1, covers static ReLU networks on an arbitrary separable Hilbert space. The later results of the paper, on finite-dimensional inputs and on echo state networks, are built on it.

Timeline:

1993: Barron (IEEE Trans. Inf. Theory 39) proves $O(N^{-1/2})$ approximation rates for functions with a finite first Fourier moment, using networks whose inner weights are optimized.
2008: Rahimi and Recht (NeurIPS 2008) prove random kitchen-sink bounds for random features sampled from a fixed law.
2023: Gonon, Grigoryeva and Ortega prove bounds with explicit constants for ReLU units with importance-sampled inner weights, on infinite-dimensional input spaces, under weak conditions on the sampling law.

Setting

$\mathcal X$ is a separable real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ , and $\sigma(x)=\max(x,0)$ is the rectifier. The inner weights $\theta_i=(A_i,\zeta_i)\in\mathcal X\times\mathbb R$ , $i=1,\dots,N$ , are i.i.d. with law $\pi$ . For a readout matrix $W\in\mathbb M_{m,N}$ the random ReLU network is

H_W^{A,\zeta}(z)=W\sigma(Az+\zeta),\qquad (Az+\zeta)_i=\langle A_i,z\rangle+\zeta_i .

The target $H^*:\mathcal X\to\mathbb R^m$ is assumed to have a Fourier representation on the ball of radius $M$ : $H^*_j(z)=\int e^{i\langle w,z\rangle}\hat\mu_j(dw)$ for $\|z\|\le M$ , with complex measures $\hat\mu_j$ whose total variations $|\hat\mu_j|$ have finite second moments (condition (15)). The sampling law has the product form $\pi=\pi_{\mathcal X}\otimes(\pi_{\mathbb R}(x)dx)$ . Two further quantities enter: $F_\pi(x)=2\int_{-x}^0\pi_{\mathbb R}(u)^{-1}du$ , and the density $g_j=d(|\hat\mu_j|+|\hat\mu_j|^-)/d\pi_{\mathcal X}$ , where $\nu^-(\cdot)=\nu(-\cdot)$ . The input $Z$ is an $\mathcal X$ -valued random variable with law $\mu_Z$ and $\|Z\|\le M$ , independent of the inner weights.

Formalization targets

Goal: Theorem 1 (pp. 37–38)

If $|\hat\mu_j|+|\hat\mu_j|^-\ll\pi_{\mathcal X}$ , condition (i) or (ii) on $\pi_{\mathbb R}$ holds, and the integrals (16) of $F_\pi(M\|w\|)\|w\|^2g_j^2$ and $\max(\|w\|^2,1)g_j^2$ are finite, then there is a readout $W$ , a measurable function of $(A,\zeta)$ , with

\mathbb E\big[\|H_W^{A,\zeta}(Z)-H^*(Z)\|^2\big]\le\frac{C^*}{N},

and for every $\delta\in(0,1)$ , with probability at least $1-\delta$ , $\|H_W^{A,\zeta}-H^*\|_{L^2(\mu_Z)}\le\sqrt{C^*}/(\delta\sqrt N)$ . Here $C^*=\sum_jC^*_j$ and

C^*_j=M^2\!\int F_\pi(M\|w\|)\|w\|^2g_j^2\,d\pi_{\mathcal X}+32\max(M^2,1)\big(F_\pi(1)-F_\pi(-1)\big)\!\int\max(\|w\|^2,1)g_j^2\,d\pi_{\mathcal X}.

Milestones

Lemma 1 (p. 37): $(\omega,z)\mapsto H_{W(\omega)}^{A(\omega),\zeta(\omega)}(z)$ is product-measurable.
Step 1 (p. 39): $\int i\langle v,w\rangle\hat\mu(dw)$ is real, and the identity (19).
(20) (p. 40): $H^*(v)=\int\sigma(\langle v,w\rangle+u)\,\alpha(dw,du)$ for $\|v\|\le M$ , for an explicit signed measure $\alpha$ .
(21) (p. 40): $\alpha\ll\pi$ , with $|d\alpha/d\pi(w,u)|\le(\mathbb 1_{(-M\|w\|,0]}(u)+2\sqrt2\,\mathbb 1_{[-1,1]}(u))\,g(w)/\pi_{\mathbb R}(u)$ .
(25) (p. 40): the mean-square error of the i.i.d. average is $\frac1N\operatorname{Var}$ , which is at most $\frac1N$ times the second moment.
(26) (p. 41): that second moment is at most $C^*$ .

Milestones 2–6 are stated for a single output component ( $m=1$ ), to which the proof reduces.

Significance

Theorem 1 says that only the readout has to be trained. With inner weights drawn from an essentially arbitrary product law satisfying (i) or (ii), a least-squares readout achieves $L^2$ error $O(N^{-1/2})$ with a constant computable from the Fourier data of $H^*$ and the sampling law (Remark 3, p. 38). The finite-dimensional rates of Section 4.2 (Proposition 3, Corollary 1) follow from it, and so do, through the reservoir functional's Fourier representation, the echo state network bounds of Sections 5–6.

The result is proved on paper but has no machine-checked proof. A formal proof needs integral representations of Fourier-type functions by ReLU units, Radon–Nikodym arguments for signed measures on product spaces, and the variance identity for i.i.d. averages. A side product of formalizing it is a correction: the printed constant $32M^2$ is false for small $M$ and has to be replaced by $32\max(M^2,1)$ , which agrees with it for $M\ge1$ .

Difficulty

There is an obvious argument: sample features from $|\hat\mu|$ and use Maurey's empirical method. It does not apply, because the features here are ReLU ridge functions of a real-valued bias drawn from $\pi_{\mathbb R}$ , not complex exponentials. The proof must first rewrite the oscillatory representation as an integral of rectifiers, (18)–(20). That step uses the realness of $\int i\langle v,w\rangle\hat\mu(dw)$ , which is not given and follows only from $H^*$ being real near $0$ . The signed measure $\alpha$ obtained this way must then be absolutely continuous with respect to the sampling law $\pi$ , with a density whose second moment is controlled by (16). In case (ii), $\pi_{\mathbb R}$ may vanish outside a bounded interval, and the support of $\alpha$ has to be matched to it.

Formalization scope

Space. $\mathcal X$ is a complete, separable real inner product space with its Borel $\sigma$ -algebra.
Complex measures. Each $\hat\mu_j$ is given in polar form $h_j\,\nu_j$ , with $\nu_j=|\hat\mu_j|$ a finite measure and $h_j$ measurable with $|h_j|=1$ . This loses no generality (Rudin, Thm 6.12).
Randomness. The inner weights live on $(\mathcal X\times\mathbb R)^N$ with law $\pi^{\otimes N}$ , and $Z$ has its own law $\mu_Z$ . Expectations are iterated lower integrals; this is the standing independence of §4.1. "With probability $1-\delta$ " bounds the $\pi^{\otimes N}$ -measure of the bad set.
Readout. The readout is a measurable function of the inner weights only. A readout allowed to depend on the input $Z$ would make the statement trivial, and it is ruled out.
Norms and normalisation. Norms on $\mathbb R^m$ are Euclidean, as a sum of squares. $\pi_{\mathcal X}$ is a probability measure and $\int\pi_{\mathbb R}=1$ ; rescaling $\pi_{\mathcal X}$ by $c$ and $\pi_{\mathbb R}$ by $1/c$ changes neither $\pi$ nor $C^*$ .
Encodings. " $|F_\pi(x)|<\infty$ " is integrability of $1/\pi_{\mathbb R}$ on the interval between $-x$ and $0$ , and $F_\pi$ is an oriented interval integral. (15) is a finite lower integral and (16) is integrability, so none of them holds vacuously.
Departures from the print. The page's " $C^*>0$ " is dropped in favour of the explicit value. The constant uses $32\max(M^2,1)$ .

A complete development needs the following:

the rectifier integral identity (18), which is identity (8) of Proposition 2 and is posed in the companion mission on echo state networks;
the Radon–Nikodym and Fubini arguments of Step 1;
the variance of i.i.d. averages under product measures;
Markov's inequality.

The variance identity (25) and the bound (26) are independent of the Fourier setting and reusable. Contributions to any milestone are welcome, and so are alternative proofs of (19) and (20).

Selected references

L. Gonon, L. Grigoryeva, J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, Ann. Appl. Probab. 33(1), 2023, 28–69. https://doi.org/10.1214/22-AAP1806
A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inf. Theory 39(3), 1993, 930–945. https://doi.org/10.1109/18.256500
A. Rahimi, B. Recht, Weighted sums of random kitchen sinks: replacing minimization with randomization in learning, NeurIPS 2008. https://papers.nips.cc/paper/2008/hash/0efe32849d230d7f53049ddc4a4b0c60-Abstract.html
W. Rudin, Real and Complex Analysis, 3rd ed., McGraw-Hill, 1987 (Chapter 6, Theorem 6.12).

8 thms2 active usersReviewed

Dynamical Systems Machine Learning Probability·Captain: mikedeng1

Approximation Bounds for Random Neural Networks and Reservoir Systems III: Echo State Networks with Output Feedback and Random Weights Approximate Contracting Reservoirs (Theorem 4)Research Paper

Motivation

An echo state network with output feedback is a recurrent model whose previous output is fed back into its next hidden-state update. In reservoir computing only the linear output weights are trained, while the internal weights are fixed, typically after being drawn at random. This raises a quantitative question: if the internal rows are sampled from a fixed law, can a network with $N$ blocks of random rows and a suitable linear readout approximate a given input–output rule, and at what rate in $N$ ? Gonon, Grigoryeva and Ortega answer this for targets generated by contracting reservoir systems. Their Theorem 4 (p. 63) gives, with explicit constants, a probability bound and an excess-risk bound of order $1/\sqrt N$ , plus a term decaying geometrically in the length $T$ of the observation window. The input set is not required to be bounded: the bound depends on the input process only through $\mathbb E[\max_{t}\|Z_t\|]$ over the window.

Setting

Inputs are vectors in a set $D_d\subseteq\mathbb R^d$ and an input history is $z=(z_t)_{t\in\mathbb Z_-}$ , with $\mathbb Z_-=\{0,-1,-2,\dots\}$ . A target reservoir is a map $F^*:\mathbb R^{N^*}\times D_d\to B_M$ , with $B_M$ the closed Euclidean ball of radius $M$ , such that $F^*(\cdot,v)$ is an $r$ -contraction for every $v\in D_d$ , with $r\in(0,1)$ . Its reservoir functional is $H^*(z)=x^*_0$ , where $x^*_t=F^*(x^*_{t-1},z_t)$ for all $t\in\mathbb Z_-$ . The output dimension is $m=N^*$ .

The approximating network has $N$ blocks of $N^*$ rows. Each row is a vector $\omega=(a,c,\zeta)\in\mathbb R^{N^*+d+1}$ , and the $\bar N=NN^*$ rows $U_j^{(i)}$ of $[A,C,\zeta]$ are i.i.d. with law $\pi$ . With an activation $\sigma$ and a readout matrix $W\in\mathbb M_{m,\bar N}$ , the system is

x_t=\sigma(Ay_{t-1}+Cz_t+\zeta),\qquad y_t=Wx_t,\qquad t=-T,\dots,0,\qquad y_{-T-1}=\Xi,

with $T\ge1$ and $\|\Xi\|\le M$ ; its functional is $H^{A,C,\zeta}_W(z)=y_0$ . For each $k\ge1$ and $j=1,\dots,N^*$ a signed measure $\pi_j^k\ll\pi$ defines the integral map

F_j^{*,N}(x,v)=\int\sigma((x,v,1)\cdot\omega)\,\pi_j^N(d\omega).

The constant $C_*=4\sqrt3L_\sigma\sup_{k}\sum_j(\int\|\omega\|^2(d\pi_j^k/d\pi)^2d\pi)^{1/2}$ measures the size of these densities, and $s_N=\mathbb E[\max_{t\in\{0,\dots,-T\}}\sup_{x\in B_{M+1}}\|F^{*,N}(x,Z_t)-F^*(x,Z_t)\|]$ is the approximation error of $F^{*,N}$ . The input process $Z$ is independent of $(A,C,\zeta)$ , $Y_0$ is an integrable target, and the loss $L\ge0$ is Lipschitz with constant $L_L$ . The echo state event $\Omega_{\mathrm{ESP}}$ of (87) is the event that $\|WF^{A,C,\zeta}(x,Z_t)\|\le M+1$ for all $x\in B_{M+1}$ and $t\in\{0,\dots,-T\}$ , where $F^{A,C,\zeta}(x,v)=\sigma(Ax+Cv+\zeta)$ .

Formalization targets

Steps of the proof

The milestones are the displayed estimates of the proof, in attack order:

(89): one step of the error recursion on $\Omega_{\mathrm{ESP}}$ , $\mathbb E[\|Y_t-X^*_t\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]\le\mathbb E[\sup_{y}\|\cdots\|]+s_N+r\,\mathbb E[\|Y_{t-1}-X^*_{t-1}\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]$ ;
(90): splitting into coordinates and symmetrization of the uniform error of the random map;
(91): a deterministic bound on Rademacher averages,

\mathbb E_\varepsilon\sup_{y\in B_{M+1}}\Big|\sum_{i=1}^N v_i\varepsilon_i\sigma((y,z,1)\cdot u_i)\Big|\le2L_\sigma\Big((M+1)\big(\textstyle\sum_iv_i^2\|a_i\|^2\big)^{1/2}+\|z\|\big(\sum_iv_i^2\|c_i\|^2\big)^{1/2}+\big(\sum_iv_i^2\zeta_i^2\big)^{1/2}\Big);

(92)–(93): for each fixed input $z\in D_d$ ,

\mathbb E\sup_{y\in B_{M+1}}\Big\|\frac1N\sum_{i=1}^NW_i\sigma(A^{(i)}y+C^{(i)}z+\zeta^{(i)})-F^{*,N}(y,z)\Big\|\le\frac{(M+2+\|z\|)C_*}{\sqrt N};

(96): $\mathbb P(\Omega\setminus\Omega_{\mathrm{ESP}})\le2(M+2+\mathbb E[\max_t\|Z_t\|])C_*/\sqrt N+2s_N$ .

Goal: Theorem 4

There is a readout $W$ , a function of $(A,C,\zeta)$ alone, such that for every $\delta\in(0,1)$ and every $\|\Xi\|\le M$ , with probability at least $\max(1-\delta-2C_*(M+2+\mathbb E[\max_t\|Z_t\|])/\sqrt N-2s_N,0)$ , the event $\Omega_{\mathrm{ESP}}$ holds and

|\mathcal R(H^{A,C,\zeta}_W)-\mathcal R(H^*)|\le \frac{L_L}{\delta}\Big[\frac{(M+2+\max_t\mathbb E\|Z_t\|)C_*}{(1-r)\sqrt N}+\frac{s_N}{1-r}+2(M+1)r^{T+1}\Big],

where $\mathcal R(H)=\mathbb E[L(H(Z),Y_0)]$ is evaluated at fixed network weights.

Significance

The bound separates three sources of error: sampling $N$ blocks of random rows (rate $1/\sqrt N$ ), the approximation of $F^*$ by the integral map $F^{*,N}$ ( $s_N$ ), and the finite initialization of the feedback recursion ( $r^{T+1}$ ). Only the readout depends on the target; the internal weights are generated without it. The theorem also bounds the probability that the random feedback map leaves the state ball on which the recursion is controlled, which is the form in which the echo state property enters. Via Theorem 3 (p. 62), which specializes the densities through the paper's Proposition 2, it gives approximation rates for ReLU output-feedback networks.

The paper proves the result on pp. 63–68. No part of it is formalized. A complete development would give machine-checked Rademacher symmetrization and contraction estimates for random features, uniform-over-a-ball bounds for sampled integral maps, and a treatment of finite feedback recursions on product probability spaces, all reusable outside reservoir computing.

Difficulty

A pointwise approximation of $F^*$ by the sampled map does not control the feedback system, because the next feedback value is itself the random output of the previous update. The comparison must hold uniformly over the state ball $B_{M+1}$ and over the whole input window, and the event that the recursion leaves the ball must be charged to an explicit probability. The uniform bound requires symmetrization and the Ledoux–Talagrand contraction principle for a supremum over a continuum of states, with per-index contractions; Lipschitz continuity of $\sigma$ alone does not supply the vanishing at zero that principle needs. The input is unbounded, so the input dependence must be tracked through $\|z\|$ and integrated at the end.

Formalization scope

States, inputs, outputs and rows are Euclidean spaces (EuclideanSpace); a row is indexed by $(\{1..N^*\}\sqcup\{1..d\})\sqcup\{\ast\}$ and the rows by $\{1..N\}\times\{1..N^*\}$ . Time $t\in\mathbb Z_-$ is the index $-t\in\mathbb N$ ; the equation (78) is the published ReservoirESN.IsSolution. The rows have law $\pi^{\otimes NN^*}$ on their own space and $(Z,Y_0)$ lives on a separate probability space; the probability is under the product law, which encodes the independence of §6.1. Signed measures $\pi_j^k$ are their Radon–Nikodym densities with respect to $\pi$ , with integrability and first-moment hypotheses. $C_*$ , $s_N$ and $\mathbb E[\max_t\|Z_t\|]$ are extended nonnegative integrals and suprema, converted to reals only under their finiteness hypotheses; the risk integrals are finite under the loss Lipschitz bound, integrable target and input-moment assumption; the supremum in (87) is unfolded. $F^*$ is assumed jointly measurable, the standing convention that makes $s_N$ and $H^*(Z)$ random variables; the standing assumptions $d,N^*\ge1$ and $M>0$ (p. 30) and $T\ge1$ (§6.1) are hypotheses.

Trivialization ruled out. The readout is a measurable function of the rows only and is chosen before $\delta$ and $\Xi$ . A readout allowed to look at the input $Z$ would make the claim a different and much weaker statement.

Correction of the print. The goal and milestones (91), (93), (96) assume $\sigma(0)=0$ : the contraction principle cited at (91) needs contractions vanishing at zero, while the printed theorem states only that $\sigma$ is Lipschitz. ReLU, the paper's application, satisfies it. The goal retains the printed full risk difference. Its proof passes through (88), where an indicator depending on $Z$ is moved inside a risk integral; this step needs further justification. The milestone quotations keep the printed text.

Contributions are welcome on each milestone, on general Rademacher symmetrization and contraction lemmas for suprema over compact parameter sets, on measurability of suprema of continuous random fields, and on the printed form of the risk bound.

Selected references

L. Gonon, L. Grigoryeva and J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, The Annals of Applied Probability 33(1), 2023, 28–69. https://doi.org/10.1214/22-AAP1806
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991 (Theorem 4.12, the contraction principle). https://doi.org/10.1007/978-3-642-20212-4

8 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Cycle Lengths in Expanding Graphs 1: Every α-Expander on n Vertices Has a Cycle of Length in [ℓ, ℓ+O(1/α)] for Every Integer ℓ from O(1/α)·log n up to 2^(−O(log(1/α)/α))·nResearch Paper

Motivation

Which cycle lengths a graph must contain is a long-standing theme of extremal graph theory, studied for graphs of given minimum degree, chromatic number or density. A natural class in which to ask it is that of expanders: graphs in which every not-too-large vertex set has many neighbours outside it (Hoory, Linial and Wigderson). It is known that an $\alpha$ -expander on $n$ vertices has a cycle of length $\Omega_\alpha(n)$ and a cycle of length $O_\alpha(\log n)$ (Krivelevich's survey, Corollary 3.2 and Theorem 7.4, arXiv:1812.11562); the question is what happens between these extremes.

One cannot hope for a full interval of cycle lengths: the complete bipartite graph $K_{\alpha n/2,(1-\alpha/2)n}$ is an $\alpha$ -expander without odd cycles, and subdividing every edge of a bounded-degree expander $m$ times gives an $\Omega(\alpha/m)$ -expander all of whose cycle lengths are divisible by $m+1$ . L. Friedman and M. Krivelevich (Cycle lengths in expanding graphs, Combinatorica 41 (2021); arXiv:1912.11011v2) show that this is the only obstruction: the cycle lengths of an $\alpha$ -expander are well spread, in the sense that every window of $O(1/\alpha)$ consecutive integers between logarithmic and linear length contains one. This mission formalizes that theorem (Theorem 1 of the paper) together with the lemmas of its §2.

Setting

Let $G=(V,E)$ be a finite simple graph on $n$ vertices. For $U\subseteq V$ , the external neighbourhood is $N_G(U)=\{v\in V\setminus U : v\text{ has a neighbour in }U\}$ .

For reals $k>0$ , $\alpha>0$ , $G$ is a $(k,\alpha)$ -expander if $|N_G(U)|\ge\alpha|U|$ for every $U\subseteq V$ with $|U|\le k$ .
$G$ is an $\alpha$ -expander if $|N_G(U)|\ge\alpha|U|$ for every $U$ with $|U|\le\lceil n/2\rceil$ .
A cycle of length $\ell\ge3$ is a closed walk with $\ell$ edges and no repeated vertex; $L(G)$ is the set of lengths of cycles of $G$ .
$B_G(v,r)$ is the ball of radius $r$ : the vertices at distance at most $r$ from $v$ .
For a tree $T\subseteq G$ rooted at $v_0$ , the level of a vertex is one plus its distance from $v_0$ in $T$ , so $L_1=\{v_0\}$ , and $T_{[j_1,j_2]}=\bigcup_{i=j_1}^{j_2}L_i$ .
Contracting the parts $V_1,\dots,V_r$ of a partition of $V$ gives the graph on $\{1,\dots,r\}$ in which $i\ne j$ are adjacent when some edge of $G$ joins $V_i$ and $V_j$ .

All logarithms are base $2$ . In Lean these objects are extNbhd, IsKAlphaExpander, IsAlphaExpander, cycleLengths, ball, contract, level and levelSet, in the namespace CycleLengthsExp.WellSpread.

Formalization targets

Goal: Theorem 1 (p. 3)

For every $0<\alpha\le1$ there are positive constants $A=O(1/\alpha)$ , $a_1=O(1/\alpha)$ and $a_2=2^{-O(\log(1/\alpha)/\alpha)}$ such that for all large $n$ , every $\alpha$ -expander $G$ on $n$ vertices satisfies

\forall\,\ell\in\mathbb Z\cap[a_1\log n,\ a_2n]\quad\exists\,L\in L(G):\ \ell\le L\le\ell+A .

The goal fixes only the shape of the dependence on $\alpha$ , not the constants, so an improvement of the constants does not invalidate it.

Milestones (§2, in the order the proof uses them)

Ball growth (p. 4): in a $(k,\alpha)$ -expander, $|B_G(v,r)|\ge\min\{k,(1+\alpha)^r\}$ .
Lemma 2.1 (p. 4): a component of a $(\delta n,\alpha)$ -expander ( $0<\delta<1$ , $0<\alpha\le1$ ) has diameter at most $\frac7{\delta\alpha}\log n$ .
Lemma 2.2 (p. 5): removing $\epsilon n$ vertices, $0<\epsilon\le\alpha^2k/(8n)$ , from a $(k,\alpha)$ -expander leaves an induced $(k,\alpha/2)$ -expander on $(1-3\epsilon/\alpha)n$ vertices.
Lemma 2.3 (p. 5): an $\alpha$ -expander has $t\alpha/(1+\alpha)$ vertex-disjoint paths between any two sets of size at least $t$ .
Lemma 2.4 (p. 6): contracting parts of size at most $C$ yields a $(k/C,\alpha/C)$ -expander on $r\ge n/C$ vertices.
Lemma 2.5 (p. 6): if every $k$ -set has at least $\ell$ external neighbours, a path of length $\ell$ starts at every vertex whose component has at least $k$ vertices.
Lemma 2.6 (p. 6): a set $W$ with $|W|>n/2$ and $|N_G(W)|\le\alpha\epsilon n$ contains an induced $((\tfrac12-2\epsilon)n,\alpha/2)$ -expander on more than $(\tfrac12-2\epsilon)n$ vertices.
Lemma 2.7 (p. 7): a tree rooted at any $v_0$ with levels $k_0\le C_0\log n$ , $k_1-k_0\le C_1$ , $k_2-k_1\le C_2$ , bounded degree $\Delta$ on $T_{[k_1,k_2]}$ , and an $(n/10,\alpha/5)$ -expander on at least $n/10$ vertices inside $T_{[k_1,k_2]}$ .

Significance

The result. Theorem 1 says that, up to an additive error of order $1/\alpha$ , an $\alpha$ -expander contains every cycle length from $O(\log n/\alpha)$ up to a constant fraction of $n$ . The additive error is optimal in its dependence on $\alpha$ by the subdivision example, and the logarithmic lower end is necessary because expanders can have logarithmic girth. It implies that $|L(G)|$ is linear in $n$ for every $\alpha$ -expander; the companion mission of this series (Theorem 2 of the paper) improves the dependence on $\alpha$ in that count. The lemmas of §2, especially the robust sub-expander lemmas 2.2 and 2.6, the disjoint-paths lemma 2.3 and the depth-first-search lemma 2.5, are general-purpose statements about vertex expanders that do not depend on the cycle-length question.

Formalizing it. The theorem is proved on paper; none of it is machine-checked. Mathlib has walks, paths, cycles, distances and induced subgraphs, but no vertex expansion, no Menger theorem, no depth-first-search path lemma and no breadth-first-tree construction. This mission produces formal statements of all of these at the level of generality the paper uses, and a complete development would supply reusable lemmas about vertex expanders on finite simple graphs.

Difficulty

The obvious argument fails at the step of hitting a prescribed length. Expansion easily gives long paths and long cycles, but controlling the length of a cycle to within an additive $O(1/\alpha)$ requires a structure with many cycles whose lengths differ by small, controlled amounts. The paper builds it from two breadth-first trees joined by many short disjoint paths, a long path routed through bounded-size subtrees, and a pigeonhole selection that avoids spoiling too many subtrees; the explicit constants of Lemma 2.7 then have to be propagated through Theorem 1. Lemma 2.3 additionally needs Menger's theorem, which is not in Mathlib, and Lemma 2.5 is a depth-first-search argument whose formal invariant is not short.

Formalization scope

Graphs are SimpleGraph (Fin n); the ball-growth milestone uses any finite vertex type. Sizes are Set.ncard; inequalities involving $\alpha$ , $\epsilon$ , $\delta$ or logarithms are stated in ℝ. $\lceil n/2\rceil$ is (n + 1) / 2. Logarithms are Real.logb 2.
$O(\cdot)$ constants: one absolute $K>0$ quantified before $\alpha$ . In Theorem 1, $A\le K/\alpha$ , $a_1\le K/\alpha$ , $a_2\ge2^{-K\log_2(2/\alpha)/\alpha}$ ; in Lemma 2.7, $\Delta,C_1\le K/\alpha^5$ and $C_0,C_2\le K/\alpha$ . Inside the $O$ , $\log(1/\alpha)$ is read as $\log_2(2/\alpha)$ , which agrees up to a constant for $\alpha\le1/2$ and avoids the value $0$ at $\alpha=1$ .
Thresholds: Theorem 1's "for large enough $n$ " is $n\ge n_0$ with $n_0$ depending on $\alpha$ only. Lemma 2.7 is also stated for $n\ge n_0(\alpha)$ : an addition, disclosed in the item, because the paper's proof suppresses rounding and needs $n$ large against $1/\alpha$ , and Theorem 1 uses the lemma only for large $n$ .
Induced subgraphs: " $G[U]$ is an expander" and "contains an expander" use G.induce U, the edges of $G$ , never the edges of a tree.
Lemma 2.1 is stated in its "In particular" form, as a bound on G.dist u v for $u,v$ in one component. The first inequality of the lemma is false as printed (the path $P_n$ with $k=1$ ) and is not posed. Lemma 2.7, item 4, is posed with $\alpha/5$ as printed, although its proof gives $\alpha/2$ .
Trivializing readings are ruled out: the $O$ -constants are bounded by one $K$ fixed before $\alpha$ ; cycles are Walk.IsCycle, never closed walks; Lemma 2.1 never uses G.diam, which is $0$ for a disconnected graph; and no statement divides by $\log(1/\alpha)$ .
Welcome contributions: Menger's theorem for vertex sets in finite simple graphs; the depth-first-search long-path lemma; breadth-first trees with level bookkeeping; and proofs of the milestones in any order.

Selected references

L. Friedman, M. Krivelevich, Cycle lengths in expanding graphs, Combinatorica 41 (2021). arXiv:1912.11011v2, doi:10.1007/s00493-020-4434-0
M. Krivelevich, Expanders — how to find them, and what to find in them, Surveys in Combinatorics 2019, LMS Lecture Note Series 456, 115–142. arXiv:1812.11562
S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bulletin of the AMS 43 (2006), 439–561. doi:10.1090/S0273-0979-06-01126-8

10 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space 1: SA[p ± 1] Is Recovered From the Sample at the Phrase Start Preceding SA[p] − 1Research Paper

Motivation

Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length $n$ , not with the amount of distinct content. The number $r$ of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in $O(r)$ words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to $n/s$ for a sampling step $s$ , which defeats the purpose on repetitive data.

Timeline.

1994: Burrows and Wheeler introduce the transform (DEC SRC Research Report 124).
2000–2005: Ferragina and Manzini build the FM-index, with backward search and the LF mapping (J. ACM 52(4), 2005).
2005: Mäkinen and Navarro give the run-length FM-index, which counts occurrences in $O(r)$ words (Nordic J. Computing 12(1), 2005).
2016–2018: Prezza (PhD thesis, Udine, 2016) and Policriti and Prezza (Algorithmica 80(7), 2018) keep one known suffix-array cell, a "toehold", during backward search.
2017–2020: Gagie, Navarro and Prezza show that $O(r)$ words suffice to locate every occurrence (arXiv:1705.10382; arXiv:1809.02792; J. ACM 67(1), 2020). This mission formalizes the combinatorial core of that result.

Setting

A text $T[1..n]$ is a sequence over the alphabet $[1..\sigma]$ whose last symbol $T[n]=\$ =1 $is the smallest symbol and occurs nowhere else. The **suffix array**$ SA[1..n] $is the permutation of$ [1..n] $that lists the suffixes$ T[SA[p]..n] $in strictly increasing lexicographic order, and the **inverse suffix array** satisfies$ SA[ISA[i]]=i $. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\$ \ (SA[p]=1),$$ so that $T[0]$ is read as $T[n]$ . The LF mapping is the counting formula $LF(p)=C[BWT[p]]+\operatorname{rank}[p]$ , where $C[c]$ counts BWT symbols smaller than $c$ and $\operatorname{rank}[p]$ counts copies of $BWT[p]$ in $BWT[1..p]$ .

A run is a maximal block of equal consecutive BWT symbols, and $r$ is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most $2r$ positions are sampled. Definition 3 cuts $T$ into phrases that begin exactly at the sampled positions. For a text position $k$ , the phrase head $i$ of $T[k]$ is the greatest sampled position $\le k$ . The permutation $\phi(i)=SA[ISA[i]-1]$ (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are $DSA[p]=SA[p]-SA[p-1]$ and $DISA[i]=ISA[i]-ISA[i-1]$ . A text position starts a phrase of $ISA$ when $ISA[i]$ is the first position of a run.

Formalization targets

Goal: the identity in the proof of Lemma 3

Let $SA[p]=k+1$ , let $i$ be the phrase head of $T[k]$ , let $q=ISA[i+1]$ , and let $N[i]=\langle x,y\rangle=\langle SA[q-1],SA[q+1]\rangle$ be the sample stored at $i$ . Then

SA[p-1]=x+k-i\quad(p\ge 2),\qquad SA[p+1]=y+k-i\quad(p<n),

and $q\ge 2$ , $q<n$ respectively, so that $N[i]$ is defined.

Milestones

§2.4, p. 9. $SA[LF(p)]=SA[p]-1$ for $SA[p]>1$ , with $LF(p)\in[1..n]$ .
Lemma 12, p. 20. If $BWT[p-1]=BWT[p]$ , then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$ .
Run-free claim, proof of Lemma 3, pp. 12–13. For $0\le t<k-i$ , the cells $LF^t(p-1),LF^t(p),LF^t(p+1)$ are contiguous and lie in one BWT run.
Lemma 14, p. 23. If $i$ does not start a phrase of $ISA$ , then $\phi(i-1)=\phi(i)-1$ and $DISA[i]=DISA[\phi(i)]$ .

A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both $c$ and a non- $c$ symbol contains an occurrence of $c$ at the first or last position of a run.

Significance

The goal says that the $O(r)$ numbers $N[i]$ , one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval $SA[sp..ep]$ of a pattern, it lets an index list all occurrences in $O(r)$ space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to $s$ neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for $SA$ and $ISA$ in §5.

The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the $r$ -index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.

Difficulty

The obvious argument follows the three cells $p-1,p,p+1$ backwards under LF for $k-i$ steps. It rests on two facts that are easy to state and not routine to prove. First, $SA[LF(p)]=SA[p]-1$ must be derived from the counting formula $C[c]+\operatorname{rank}[p]$ : this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of $\$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from$ T[k] $back to$ T[i+1] $. This is where the choice of$ i $as the *greatest* sampled position$ \le k $matters, and also where the case of no sampled position in$ [1..k] $needs care. Finally, one more LF step from$ T[i+1] $to$ T[i] $produces the cell$ q $, and the shift by$ k-i$ must be tracked through natural-number arithmetic.

Formalization scope

Positions are 1-based natural numbers, as in the paper. $T$ and $SA$ are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$ . $SA$ is a hypothesis, IsSuffixArray: it maps $[1..n]$ injectively into $[1..n]$ and sorts the suffixes strictly in Lean's lexicographic order on lists. Since $\$ =1 $is unique and smallest, this order agrees with the paper's. BWT and LF are defined by the formulas of p. 8, never by the properties the milestones assert.$ ISA[i] $is$ 0 $if no cell holds$ i $. Sampled positions follow the first sentence of Definition 1 (first or last in its run); the paper's "That is" clause omits the last character of the final run.$ DSA $and$ DISA$ are integer-valued.

Pins and guards:

Wrap-around phrase. If no sampled position lies in $[1..k]$ , the phrase containing $T[k]$ began at $T[n]=\$$, which is always sampled. Its head is encoded as$ 0 $($ T[0]\equiv T[n] $), so that$ q=ISA[1] $is the cell holding$ $ $. The goal covers this case; it does not assume a sampled position$ \le k$.
Neighbours. Each half of the goal and of the run-free claim is guarded by the existence of the neighbour ( $p\ge 2$ , $p<n$ ).
SA[LF(p)]. The identity is stated for $SA[p]>1$ ; for $SA[p]=1$ it holds only cyclically.
Lemma 14. " $[i-1..i]$ within a phrase of $ISA$ " means that $i$ does not start a phrase of $ISA$ , which begin only at run-first cells. Definition 3's phrases begin at run-first and run-last cells; the two parses are kept apart.

The space and time claims of Lemmas 2–3 and Theorem 1 ( $O(r)$ words, $O(\log\log_w(n/r))$ time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding $SA[p]-1$ ", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions $\le k$ .

A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and $\phi$ for the left half of the goal.

Selected references

T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv:1809.02792v2, 2019. https://arxiv.org/abs/1809.02792
T. Gagie, G. Navarro, N. Prezza, Fully Functional Suffix Trees and Optimal Text Searching in BWT-Runs Bounded Space, J. ACM 67(1), 2020. https://doi.org/10.1145/3375890
T. Gagie, G. Navarro, N. Prezza, Optimal-Time Text Indexing in BWT-runs Bounded Space, arXiv:1705.10382, 2017 (SODA 2018). https://arxiv.org/abs/1705.10382
P. Ferragina, G. Manzini, Indexing Compressed Text, J. ACM 52(4):552–581, 2005. https://doi.org/10.1145/1082036.1082039
A. Policriti, N. Prezza, LZ77 Computation Based on the Run-Length Encoded BWT, Algorithmica 80(7):1986–2011, 2018. https://doi.org/10.1007/s00453-017-0327-z
V. Mäkinen, G. Navarro, Succinct Suffix Arrays Based on Run-Length Encoding, Nordic Journal of Computing 12(1):40–66, 2005 (no DOI).
M. Burrows, D. J. Wheeler, A Block Sorting Lossless Data Compression Algorithm, Technical Report 124, Digital Equipment Corporation, 1994 (no DOI).

8 thms2 active usersReviewed

Machine Learning Reinforcement Learning Statistics·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making II: Every Algorithm Has Expected Regret at Least (1/6)·dec_γ(M^∞_ε̄γ(M̄), M̄)·T, the Localized DEC Lower BoundResearch Paper

Why expected regret needs a lower bound

In interactive decision making, an algorithm chooses actions while learning which model governs its observations. A low-regret guarantee for one algorithm does not by itself say whether every algorithm could do better. The Decision-Estimation Coefficient (DEC) was introduced to express the cost of choosing useful decisions while distinguishing plausible models. Foster, Kakade, Qian and Rakhlin's Theorem 3.2 gives the corresponding lower bound: when a localized model class has large DEC, an adaptive algorithm must incur expected regret under at least one model in the class. This mission formalizes that result for finite decision and outcome alphabets.

The paper's protocol covers bandits, partial monitoring, and reinforcement-learning examples through a common model that maps each decision to a distribution over rewards and observations. Its lower bound concerns the protocol itself, rather than any one algorithm or application. The theorem therefore gives a common test for the limits of learning in several interactive settings. The finite-alphabet representation here retains adaptive decision kernels, which are central to the theorem.

Models, algorithms and the coefficient

Let $\Pi$ be the set of decisions, $Y$ the set of joint reward–observation outcomes, and $r:Y\to\mathbb R$ the reward map. A model $M$ assigns a probability distribution $M(\pi)$ on $Y$ to each $\pi\in\Pi$ . Its mean reward is $f^M(\pi)=\mathbb E_{y\sim M(\pi)}r(y)$ , and $\pi_M$ is a maximizing decision. The gap function is $g^M(\pi)=f^M(\pi_M)-f^M(\pi)$ .

At round $t$ , an adaptive algorithm assigns a distribution $p^{(t)}(\cdot\mid H^{(t-1)})$ on decisions using the full preceding history. It samples a decision from that distribution and receives an outcome drawn from $M(\pi^{(t)})$ . The joint law of the length- $T$ history is $P^{M,p}$ . Following equation (1) of the paper, regret sums the gaps averaged under the algorithm's chosen distribution at each round. Thus its expectation is over the history law, while the inner gap is averaged under $p^{(t)}$ . This formulation retains the algorithm's dependence on earlier outcomes.

For probability distributions $P,Q$ on $Y$ , write $D_H^2(P,Q)=\sum_y(\sqrt{P(y)}-\sqrt{Q(y)})^2$ for squared Hellinger distance. For a reference model $\bar M$ and $\gamma>0$ , the DEC of a class $\mathcal N$ is

\operatorname{dec}_\gamma(\mathcal N,\bar M)= \inf_{q\in\Delta(\Pi)}\sup_{M\in\mathcal N} \mathbb E_{\pi\sim q}\left[g^M(\pi)-\gamma D_H^2(M(\pi),\bar M(\pi))\right].

The uniformly localized class $\mathcal M^\infty_\varepsilon(\bar M)$ contains those $M\in\mathcal M$ for which $|g^M(\pi)-g^{\bar M}(\pi)|\le\varepsilon$ for every decision. The density-ratio bound $V(\mathcal M)$ is the supremum of event likelihood ratios $M(A\mid\pi)/M'(A\mid\pi)$ over both models, decisions and events, with a lower cutoff of $e$ . It may be infinite. These conventions are equations (2), (5), and (12), and the definition immediately before Theorem 3.1 in the source.

Formalization targets

Localized DEC lower bound

Suppose $\mathcal M$ is nonempty, every model is a probability kernel, and $f^M(\pi)\in[0,1]$ for every $M\in\mathcal M$ and $\pi\in\Pi$ . For $T\ge1$ , set $C(T)=2^{11}\log(2T\wedge V(\mathcal M))$ and $\bar\varepsilon_\gamma=\gamma/(C(T)T)$ . The goal is the following supremum form of Theorem 3.2, equation (13):

\sup_{M\in\mathcal M}\mathbb E^{M,p}[\operatorname{Reg}_{\rm DM}] \ge \frac{T}{6}\operatorname{dec}_\gamma \bigl(\mathcal M^\infty_{\bar\varepsilon_\gamma}(\bar M),\bar M\bigr) \qquad(\gamma>0,\ \bar M\in\mathcal M).

The paper writes the result with a maximum over $\gamma$ and a supremum over $\bar M$ , and says that one model attains the resulting bound. Its proof explicitly permits a limit sequence when the inner supremum is not attained. The displayed statement records exactly the resulting bound on the supremum of expected regret. It implies an arbitrarily close model-specific bound for each fixed $\gamma$ and $\bar M$ .

Supporting targets

The milestones follow the statements the paper's proof (App. C.1.3, pp. 90–91) uses, in attack order: the multiplicative Hellinger comparison of Lemma A.11; the difference comparison of Lemma A.12; the Hellinger bound on adaptive history laws, $D_H^2(P^M,P^{\bar M})\le C_T\,T\,\mathbb E_{\pi\sim p_{\bar M}}[D_H^2(M(\pi),\bar M(\pi))]$ with $C_T=2^8\log(2T\wedge(V^{\bar M}(\mathcal M)\vee e))$ ; the DEC comparison at the reference model's average play $p_{\bar M}$ , (129); the localized gap comparison (132); and the final inequality $\mathbb E_{p_M}[g^M]+\mathbb E_{p_{\bar M}}[g^{\bar M}]\ge\frac13\operatorname{dec}_\gamma$ for $\varepsilon\le\gamma/(8C_TT)$ . Their source wording and page citations are preserved in the milestone list.

What the result supplies

The theorem supplies a quantitative obstruction to uniformly small expected regret. It uses the same coefficient that appears in the paper's upper-bound framework, so a model class with matching upper and lower DEC estimates can have its regret scale characterized through one object. In particular, the coefficient is sensitive to the model neighborhood relevant at horizon $T$ ; replacing it by a global coefficient would lose the theorem's stated localization. The paper applies this framework to bandit and reinforcement-learning classes.

The goal and milestone declarations here are open Lean statements with checked syntax and types. A complete formalization would supply proofs of the Hellinger comparisons, the history-law inequality, and the lower bound itself. The history and density-ratio definitions are reusable for other adaptive finite-alphabet lower bounds; the published FoundationsRL mean reward, Hellinger distance and DEC definitions are reused directly.

Where the difficulty lies

A fixed sequence of decision distributions does not describe the theorem's algorithms: later decisions depend on outcomes produced by the unknown model. The comparison must therefore use two different laws on entire histories generated by the same adaptive kernels under two models. A bound on a single round's divergence cannot simply be multiplied by $T$ without accounting for the dependence of future decision distributions on past observations. The DEC itself involves a minimum over decision distributions and a supremum over models, which need not be attained.

Formalization scope

The Lean representation uses finite $\Pi$ and $Y$ ; probability laws and expectations are finite vectors and sums. This is a finite-alphabet specialization of the paper's measurable-space setting. Histories are functions from round indices to decision–outcome pairs. The algorithm is a family of kernels from every possible past history to a decision distribution. Its law is the product of its decision probabilities and the model's outcome probabilities. Rounds are indexed from zero in Lean, corresponding to the paper's rounds $1,\ldots,T$ .

Every model in $\mathcal M$ and every algorithm kernel is normalized and nonnegative. The mean reward range $[0,1]$ , nonempty model class, maximizing selector, and positive horizon are explicit hypotheses. They keep the real-valued supremum and infimum in the published DEC from taking Lean's default values on empty or unbounded sets. An event with positive numerator and zero denominator has infinite likelihood ratio; $V(\mathcal M)=+\infty$ remains allowed because the theorem uses $2T\wedge V(\mathcal M)$ . Its logarithm therefore has a finite, positive argument for $T\ge1$ . The goal uses the exact constants $2^{11}$ and $1/6$ . The proof's constant $C_T$ is printed on p. 90 as $2^8(\log(2T)\wedge\log V^{\bar M}(\mathcal M))$ ; the formalization uses $V^{\bar M}(\mathcal M)\vee e$ , the hypothesis $V\ge e$ of Lemma A.13 (98) from which $C_T$ is derived. Without it the history bound fails for two nearly equal models, and with it $8C_T\le C(T)$ still holds, so the goal is unaffected. The intermediate results that select a model approaching a supremum carry an arbitrary slack $\eta>0$ , the paper's "limit sequence".

Contributions should preserve the adaptive history law and equation (1)'s decision-distribution regret. A statement restricted to predetermined decisions would leave out the central quantifier of Theorem 3.2. The published FoundationsRL definitions of $f^M$ , $D_H^2$ and $\operatorname{dec}_\gamma$ provide the shared finite model interface; the new history and density-ratio layer can support further lower bounds in this series.

Selected references

Dylan J. Foster, Sham M. Kakade, Jian Qian, and Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, version 3, 2023. arXiv:2112.13487v3.
Dylan J. Foster and Alexander Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv preprint, 2023. arXiv:2312.16730v1.

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research+1·Captain: mikedeng1

Online Contention Resolution Schemes with Applications to Bayesian Selection Problems 4: Intersecting the Families of (b, c₁)- and (b, c₂)-Selectable Greedy OCRSs Is (b, c₁c₂)-SelectableResearch Paper

Motivation

Online selection problems ask an algorithm to accept or reject elements as they arrive, while keeping the accepted set feasible. The decisions are irrevocable, and the arrival order can be chosen after the random activity of the elements is known. A guarantee for one constraint is therefore useful only if it remains meaningful when several constraints apply at once. In Feldman, Svensson and Zenklusen's paper, the constraints include matroid independence, matching, and knapsack capacity. A set satisfying two such requirements lies in the intersection of their feasible families. Theorem 1.9 establishes how their online guarantees combine: the two selectability factors multiply.

The result belongs to a sequence of statements in the paper. The authors first define greedy online contention resolution schemes and their selectability guarantee in Definitions 1.3–1.5. They then state the combination theorem in the introduction and identify the intersection construction in Definition 2.10. Lemma 2.11 supplies the precise selectability assertion for that construction. This mission isolates those claims so that later formalizations of specific constraints can reuse them without repeating the probability argument.

Setting

Let $N$ be a finite ground set and $\mathcal F\subseteq 2^N$ a family of feasible sets. A fractional point $x\in[0,1]^N$ determines a random active set $R(x)$ : each $e\in N$ belongs to $R(x)$ independently with probability $x_e$ . Thus a particular set $A\subseteq N$ has weight

\Pr[R(x)=A]=\prod_{e\in A}x_e\prod_{e\notin A}(1-x_e).

A greedy online contention resolution scheme, or greedy OCRS, chooses a down-closed family $\mathcal G_x\subseteq\mathcal F$ . As active elements arrive, it accepts an element when adding that element to those already accepted remains in $\mathcal G_x$ . In a randomized scheme, the choice of $\mathcal G_x$ is random and independent of $R(x)$ . The family contains the empty set, as the procedure begins with no accepted elements.

An element $e$ is selectable for a realized active set $A$ and family $\mathcal G_x$ if every $I\subseteq A$ with $I\in\mathcal G_x$ still permits $e$ : $I\cup\{e\}\in\mathcal G_x$ . This condition covers every possible set that might have been accepted before $e$ arrives. A greedy OCRS is $(b,c)$ -selectable for a relaxation $P$ when the probability of this event is at least $c$ for every $x\in bP$ and every $e\in N$ . The probability includes both draws when the family is randomized. Here $b,c\in[0,1]$ and $bP=\{by:y\in P\}$ .

For two feasible families $\mathcal F_1,\mathcal F_2$ , the combination of their greedy OCRSs independently draws $\mathcal G_{1,x}$ and $\mathcal G_{2,x}$ , then uses $\mathcal G_x=\mathcal G_{1,x}\cap\mathcal G_{2,x}$ . This is a family of sets satisfying both constraints. The proof also uses $\chi_e(A,F,F')$ , the indicator that $I\cup\{e\}\in F$ for every $I\subseteq A$ lying in $F'$ . For selectability itself, $F'=F$ .

Formalization targets

Goal: Theorem 1.9

For $P_1,P_2\subseteq[0,1]^N$ , let the first scheme be $(b,c_1)$ -selectable and the second $(b,c_2)$ -selectable. The mission asks for a greedy OCRS on the intersection with

\Pr[e\text{ selectable at }x]\ge c_1c_2 \quad\text{for all }x\in b(P_1\cap P_2),\ e\in N.

The target records existence of the combined scheme, independent of a particular proof of its selectability. The paper also claims preservation of polynomial-time efficiency; the finite mathematical model here does not assign a complexity measure to a family sampler or membership oracle, so that clause is outside this target.

Construction: Lemma 2.11

The lemma names the combined scheme: independently draw both greedy families and use their intersection. It asserts the same $(b,c_1c_2)$ bound for that specific scheme. The earlier milestones record the two order properties of $\chi_e$ and the finite product-measure correlation inequality appearing in the lemma's proof. Their statements keep the original quantifiers over active sets and families visible.

Significance

The theorem turns guarantees for individual constraints into a guarantee for simultaneous constraints. If a matroid scheme and a matching scheme meet the same scale parameter $b$ , their intersection is governed by the product of their selectability factors. The factor loss is explicit, which lets subsequent algorithmic results track it without redefining the combined scheme. The lemma additionally fixes the actual distribution over intersected families, avoiding ambiguity about how two randomized procedures are coupled.

Mathlib already provides a general finite FKG inequality, but it does not state the paper's OCRS objects, the selectable event, or the intersection theorem. This mission adds those interfaces and the specialized correlation statement. The source results are proved in the cited paper; the local theorem files in this proposal are statements for later machine-checked proofs. A complete formalization would connect the finite active-set weights to Mathlib's lattice correlation theorem and then establish the randomized family bookkeeping. The finite probability definitions can also serve other OCRS results in the same paper.

Difficulty

The obvious argument would multiply the two probabilities that $e$ is selectable for the separate families. Both events depend on the same active set $R(x)$ , so they are not independent even when the families are drawn independently. Moreover, selectability for the intersection checks only sets belonging to both families, whereas the original bounds check each family separately. The formal statements must keep these two dependencies distinct. The paper's two monotonicity claims and its FKG display identify the needed intermediate assertions, but their use with an arbitrary random choice of families still requires careful finite-sum reasoning.

Formalization scope

The ground set is a finite Lean type and subsets are Finsets. Feasibility is a predicate on those finite sets. Fractional points are real-valued functions, and each input relaxation is represented as a set of such functions with an explicit coordinate bound $0\le y_e\le1$ . The scale and selectability parameters belong to $[0,1]$ . The point $x$ ranges over $b(P_1\cap P_2)$ , not over an independently chosen intersection of scaled sets, so the case $b=0$ retains the paper's meaning. The finite products define the law of $R(x)$ ; no measure-theoretic integral is used.

A randomized scheme is a probability weight on possible greedy families for every input point. The combined weight is the product of the two original weights summed over pairs with the required intersection, expressing independent draws. The family distribution is independent of the active-set draw. This sampling convention is necessary for the stated product guarantee and is made explicit here although Definition 2.10 does not spell it out. Each greedy family contains $\varnothing$ and lies in its own feasible family. These requirements exclude the empty-family and unconstrained-family encodings that would make selectability trivial. The unit-cube bounds prevent negative active-set weights.

The Lean declarations focus on the finite selectability guarantee. They abstract a polytope by its set of fractional points and use the paper's unit-cube condition; they do not formalize a polyhedral representation or test that its binary points equal the feasible sets. A full development of the paper's algorithmic setting would additionally represent online arrival orders, family sampling algorithms, membership oracles, and polynomial running time. Contributions establishing the finite probability lemmas, the specialized FKG statement, and Lemma 2.11 are directly useful here. The general active-set and selectability definitions are reusable across the paper's other missions.

Selected references

Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes, arXiv preprint, 2015, arXiv:1508.00142v2. Definitions 1.3–1.5, Theorem 1.9, Definition 2.10 and Lemma 2.11.
Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing 50(2), 2021, DOI:10.1137/18M1226130. The mission's statement indices follow the arXiv version above.

15 thms2 active users

Information Theory Probability Quantum Information·Captain: mikedeng1

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization II: De Finetti Without Symmetry — Random Subsystems Are 3k^{3/2}d_B³ log d_B/√(n−k+1)-Close to Product in ExpectationResearch Paper

Motivation

Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.

The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.

Setting

Let $B$ be a quantum system of dimension $d_B$ , and let $\rho$ be an arbitrary density operator on $n$ copies of $B$ . Choose a uniformly random permutation of these copies. Its first $k$ positions form an ordered tuple $\vec i=(i_1,\ldots,i_k)$ of systems to retain; the remaining $r=n-k$ positions form an ordered tuple $\vec j=(j_1,\ldots,j_r)$ available for measurement. There is no symmetry condition on $\rho$ .

A measurement on $B$ has finitely many outcomes $z$ and positive operators $M_z$ whose sum is the identity. Measure the first $m$ systems $j_1,\ldots,j_m$ , where $0\le m\le r$ , and condition the retained state on the observed outcomes. Write $\rho_{\vec i\mid z}$ for that conditional state and $\rho_{i_s\mid z}$ for its marginal on the $s$ th retained system. The trace norm $\|X\|_1=\operatorname{Tr}\sqrt{X^\dagger X}$ measures the error between $\rho_{\vec i\mid z}$ and $\rho_{i_1\mid z}\otimes\cdots\otimes\rho_{i_k\mid z}$ . The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.

The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its $B$ factor. The input ranges over Hermitian operators on $A\otimes B$ , over every finite-dimensional side system $A$ , with zero partial trace on both $A$ and $B$ . The paper's $f(B\mid\cdot)$ is the infimum of this distortion over all measurements on $B$ equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most $d_B^2(d_B+1)$ .

Formalization targets

The principal target is the explicit form of Theorem 2.5. For $1\le k\le n$ , put $r=n-k$ . With the two-design measurement, some $m\in\{0,\ldots,r\}$ satisfies

\mathbb E_{\vec i,\vec j,z}\left\|\rho_{\vec i\mid z}-\bigotimes_{s=1}^k\rho_{i_s\mid z}\right\|_1 \le k d_B^2(d_B+1)\sqrt{\frac{(2\ln 2)(k-1)\log_2 d_B}{r+1}} \le \frac{3k^{3/2}d_B^3\log_2 d_B}{\sqrt{r+1}}.

Here the $z$ in the expectation is the outcome string for the first $m$ members of $\vec j$ . The same $m$ is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.

The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum $f(B\mid\cdot)$ as if every measurement attained it.

Significance

For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in $d_B$ and $k$ and decays as $1/\sqrt{n-k+1}$ . It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.

The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.

Difficulty

Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.

The printed theorem leaves the measurement $M_B$ unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with $d_B^2(d_B+1)$ replacing $f(B\mid\cdot)$ ; that is the measurement used in the goal proof of Theorem 2.5, p. 10.

Formalization scope

The $B$ system has basis Fin dB; $n$ copies have basis Fin n → Fin dB. The formalization writes $n=k+r$ , assumes $k\ge1$ , and ranges over $m\le r$ . A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.

The fixed-measurement distortion and $f(B\mid\cdot)$ take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for $\ln 2$ . The definitions use the paper's unnormalized trace norm, with no factor $1/2$ . No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.

Selected references

M. Berta, F. Borderi, O. Fawzi and V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3.

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Functional Analysis Operations Research·Captain: mikedeng1

Stochastic Graphon Games: I. The Static Case 2: Under Condition (17) the Unique Nash Equilibrium of a Graphon Game Moves by at Most κ‖W − W′‖ When the Graphon ChangesResearch Paper

Motivation

Large network games can be described by a graphon, a measurable kernel that assigns an interaction weight to each pair of players in a continuum. This representation is useful when a finite network is viewed as an approximation to a limiting network. A basic question is whether a small change in interaction weights can cause a large change in equilibrium behavior. Carmona, Cooney, Graves, and Laurière answer this question for a static game with real actions, noisy player states, and costs coupled through an aggregate state. Their static graphon games paper establishes existence and uniqueness under different hypotheses, and Theorem 3.20 gives an explicit stability estimate under its contraction condition.

The mission isolates that stability estimate and the results on which it depends. It belongs to the same development as the paper's existence theorem, but has a narrower question: how sensitively does the equilibrium respond when one graphon is replaced by another? The paper later studies finite-player approximations, for which understanding the limiting graphon game's equilibrium is useful. Those later approximation theorems are outside this mission.

Setting

The player set is $I=[0,1]$ with Lebesgue probability measure. Every player chooses a real action. A strategy profile $\alpha$ assigns an action $\alpha(x)$ to almost every player and belongs to $L^2(I)$ . Profiles that differ only on a null set represent the same strategy.

A graphon is a symmetric, real-valued, measurable, square-integrable function $w$ on $I\times I$ . It defines an integral operator $W$ on $L^2(I)$ by

[Wg](x)=\int_I w(x,y)g(y)\,dy.

Its norm $\|W\|$ is the $L^2$ -to- $L^2$ operator norm. In particular, interaction weights are allowed to be negative and are not restricted to $[0,1]$ . A second graphon $w'$ has operator $W'$ , and $\|W-W'\|$ is the operator norm of their difference.

A player's state is $X_{a,z,\xi}=b(a,z)+\xi$ , where $a$ is the player's action, $z$ is an aggregate state, and $\xi$ has a common centered probability law $\mu_0$ with finite second moment. Assumption 1 bounds squared changes in $b$ by $c_\alpha$ times the squared action change plus $c_z$ times the squared aggregate change. For a profile $\alpha$ , its aggregate $Z\alpha$ is the $L^2$ solution of

[Z\alpha](x)=\int_I w(x,y)b(\alpha(y),[Z\alpha](y))\,dy \quad\text{for almost every }x\in I.

Proposition 3.1 states that this aggregate exists and is unique when $\sqrt{c_z}\|W\|<1$ . This equation is the deterministic aggregate obtained from the paper's continuum model.

The expected cost of action $a$ at aggregate $z$ is $J(a,z)=\int f(b(a,z)+\xi,a,z)\,\mu_0(d\xi)$ . Assumption 4 says that $J(\cdot,z)$ is continuously differentiable and uniformly $\ell_c$ -strongly convex, and its action derivative changes at most $\ell_J|z-z'|$ when the aggregate changes. The best response $Bz$ minimizes this cost pointwise. A Nash equilibrium is an $L^2$ profile $\alpha$ whose action minimizes $J(\cdot,[Z\alpha](x))$ for almost every player. Assumption 5 adds the uniform bound $|b(a,z)|\leq c_0$ .

Formalization targets

The first targets are the unique aggregate of Proposition 3.1, the best-response bound of Lemma 3.7, and the $L^2$ aggregate bound (15) of Lemma 3.16. Together these support the uniqueness condition in Proposition 3.17:

\frac{\ell_J}{\ell_c} \frac{\sqrt{c_\alpha}\|W\|}{1-\sqrt{c_z}\|W\|}<1. \tag{17}

Lemma 3.19 then bounds the change of aggregate when the same profile is placed in two graphons. The goal, Theorem 3.20, concerns an equilibrium $\alpha$ for $w$ and any equilibrium $\alpha'$ for $w'$ :

\|\alpha-\alpha'\|_{L^2(I)}\leq\kappa\|W-W'\|, \qquad \kappa=\frac{c_0\ell_J(1-\sqrt{c_z}\|W\|)} {(1-\sqrt{c_z}\|W\|) [\ell_c(1-\sqrt{c_z}\|W\|)-\ell_J\sqrt{c_\alpha}\|W\|]}.

Here $w$ satisfies both $\sqrt{c_z}\|W\|<1$ and (17), while $w'$ is required only to satisfy $\sqrt{c_z}\|W'\|<1$ . The displayed coefficient is the paper's expression, including its common factor.

Significance

The theorem gives a quantitative guarantee: as long as the original game's contraction condition holds, the distance between equilibria is controlled by the operator distance between graphons. The bound identifies how state sensitivity $c_\alpha,c_z$ , cost sensitivity $\ell_J$ , strong convexity $\ell_c$ , and the state bound $c_0$ enter that guarantee. The result also separates two questions: whether an equilibrium exists for a changed graphon, and how far any such equilibrium can lie from the original one.

The mathematical theorem is proved in the paper; the Lean goal is open. A complete formal development would establish the $L^2$ integral-operator estimates, the aggregate and best-response regularity results, the unique equilibrium under (17), and finally the stability inequality. The definitions of real-valued graphons, aggregates, and their extended-valued operator norm can support later work on graphon games beyond this particular estimate. The paper's §4 finite-player results, including Theorems 4.3, 4.7, and 4.9, are not posed here.

Difficulty

An equilibrium is a fixed point of a response to an aggregate, so changing the graphon changes both the aggregate and the equilibrium profile. A direct comparison of costs at two equilibria does not by itself separate these effects or yield the printed constant. The aggregate is defined only as an $L^2$ equivalence class, while its equation and pointwise best responses use representatives. The formalization must keep those almost-everywhere statements aligned with the operator norm estimate. It must also retain the paper's asymmetric hypotheses: (17) is assumed for the original graphon, while the second graphon is allowed to have any Nash equilibrium under its own aggregate condition.

Formalization scope

Lean uses unitInterval with its volume measure for $I$ , real actions, functions with MemLp for $L^2$ profiles, and almost-everywhere equality for profiles and aggregates. IsGraphon includes measurability, symmetry, and square integrability. IsAggregate records equation (6) and membership in $L^2$ . The integral cost is computed from $b$ , $f$ , and $\mu_0$ rather than supplied as an unrelated function. Assumptions 1, 4, and 5 are explicit; the centered noise law is part of the standing model. Lemma 3.7 is stated for an arbitrary cost satisfying Assumption 4, as on the page.

The paper defines equilibrium through a best-response map on a rich Fubini extension. Proposition 3.6 identifies that with the almost-everywhere pointwise minimization condition under Assumption 4. The mission uses that equivalent condition as its equilibrium predicate. This is a disclosed model choice because the Fubini extension itself is not formalized. A best response is selected by classical choice; Assumption 4 gives the minimizer that makes the selection meaningful.

Norm inequalities use extended nonnegative reals. For a square-integrable graphon, its operator norm is finite, and real hypotheses use that finite value. The operator norm is never a real supremum with a default value for unbounded inputs; an equilibrium always includes an aggregate; and an infinite left-side norm is never converted to zero. These choices prevent the stability claim from becoming empty at a bad input. Contributions to the integral-operator infrastructure, the existence and uniqueness of aggregates, and the five named milestones are all within scope.

Selected references

René Carmona, Daniel B. Cooney, Christy V. Graves, and Mathieu Laurière, Stochastic Graphon Games: I. The Static Case, arXiv:1911.10664v1, 2019; published in Mathematics of Operations Research, 2022. arXiv

8 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness III: Adaptive Restarts Take at Most ⌈2C(q+2)/(αβ)⌉ Inner Steps and Converge Linearly on Sharp ProblemsResearch Paper

Motivation

First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to $1/t$ after $t$ steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4

Setting

Let $X\subseteq\mathbb R^n$ and $Y\subseteq\mathbb R^m$ be closed convex sets. The primal–dual problem is $\min_{x\in X}\max_{y\in Y}L(x,y)$ , where $L$ is differentiable, convex in $x$ and concave in $y$ . A point $z=(x,y)$ is feasible when $z\in Z=X\times Y$ . Its saddle-point set $Z^\star$ contains the feasible pairs satisfying $L(x,y')\le L(x,y)\le L(x',y)$ for every $x'\in X$ and $y'\in Y$ . Distances and balls use a chosen seminorm $\|\cdot\|_p$ ; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3

For $r>0$ , put $W_r(z)=\{\hat z\in Z:\|z-\hat z\|_p\le r\}$ . The normalized duality gap is $\rho_r(z)=\sup_{\hat z\in W_r(z)}[L(x,\hat y)-L(\hat x,y)]/r$ . At $r=0$ it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is $\alpha$ -sharp on $S\subseteq Z$ when $\alpha\operatorname{dist}_p(z,Z^\star)\le\rho_r(z)$ for every $z\in S$ and every $0<r\le\operatorname{diam}_p(S)$ . This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1

The base algorithm begins at $z^0\in Z$ and supplies averaged outputs $\bar z^t$ for positive inner times $t$ . Property 3 requires constants $q,C>0$ , uniform over every feasible start and output run, for which $\bar z^t\in Z$ , $\rho_{\|\bar z^t-z^0\|_p}(\bar z^t)\le2C\|\bar z^t-z^0\|_p/t$ , and $\|\bar z^t-z^0\|_p\le(q+2)\operatorname{dist}_p(z^0,Z^\star)$ . An outer run starts at $z^{k,0}$ , runs its inner algorithm for $\tau^k$ steps, and sets $z^{k+1,0}=\bar z^{k,\tau^k}$ . Its first length $\tau^0\ge1$ is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below $\beta$ times the gap at the previous outer transition, with $0<\beta<1$ . Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)

Formalization targets

The goal is both parts of Theorem 2. Assume all outer starts lie in one set $S$ on which the problem is $\alpha$ -sharp, with $\alpha>0$ . Define the ceiling time $t^\star=\left\lceil2C(q+2)/(\alpha\beta)\right\rceil$ . For every $k\ge1$ the target is

\tau^k\le t^\star, \qquad \operatorname{dist}_p(z^{k,0},Z^\star) \le\beta^k\frac{t^\star}{\tau^0}\operatorname{dist}_p(z^{0,0},Z^\star).

The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at $k=1$ : the first interval is free and need not be at most $t^\star$ . Applegate et al., arXiv:2105.12715v4, pp. 17–18

Significance

The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know $\alpha$ can have the same characteristic restart scale as one using a fixed frequency chosen from $\alpha$ . The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5

Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4

Difficulty

The restart test uses a gap evaluated at the moving radius $\|\bar z^{k,t}-z^{k,0}\|_p$ , whereas sharpness relates a gap at the radius of the previous outer transition to distance from $Z^\star$ . This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18

Formalization scope

Lean represents $x$ and $y$ by finite-dimensional Euclidean spaces and $z$ by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. $Z^\star$ is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires $Z^\star\ne\varnothing$ , a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to $Z^\star$ cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4

The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes $q,C$ before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor $t^\star/\tau^0$ is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18

Selected references

D. Applegate, O. Hinder, H. Lu and M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Mathematical Programming, 2022; mission citation basis: arXiv:2105.12715v4.

8 thms2 active usersReviewed

Completed

Machine Learning Optimization·Captain: mikedeng1

Certifying Some Distributional Robustness with Principled Adversarial Training 3: The Softmax Loss of a Smooth Deep Network Has a (√2·β_L(θ)+α_L(θ)²)-Lipschitz Input GradientResearch Paper

Motivation

Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) train classifiers against adversarial perturbations by solving a Lagrangian relaxation of a Wasserstein distributionally robust problem. The inner problem, $\sup_z \{\ell(\theta;z)-\gamma\, c(z,z_0)\}$ , is strongly concave, and hence solvable by gradient ascent with the paper's certificates, exactly when the penalty $\gamma$ exceeds the input-smoothness constant $L_{zz}$ of the loss: the Lipschitz constant of $z\mapsto\nabla_z\ell(\theta;z)$ . For a deep network this constant is not given; §4 of the paper ("Bounds on smoothness of neural networks") supplies an explicit upper bound in terms of the weights' spectral norms and per-layer constants of the activations. The bound tells a practitioner how large $\gamma$ must be for the robustness guarantees to apply, and it is of the same type as the spectral-norm Lipschitz bounds used for adversarial robustness and generalization of deep networks (Szegedy et al. 2014; Bartlett, Foster, Telgarsky 2017), but at the level of the derivative rather than the function.

Setting

A layered network of depth $L$ has widths $d_{l,I}$ (pre-activation of layer $l$ ) and $d_{l,O}$ (output of layer $l$ ), with $d_{0,O}=p$ the input dimension and $d_{L,O}=K$ the number of classes. Its parameters are weight matrices $\theta_l:\mathbb R^{d_{l-1,O}}\to\mathbb R^{d_{l,I}}$ , and each linear layer is followed by a nonlinear operation $\sigma_l:\mathbb R^{d_{l,I}}\to\mathbb R^{d_{l,O}}$ (an activation, possibly combined with pooling). The output of the first $l$ layers is

F_0(\theta;x)=x,\qquad F_l(\theta;x)=\sigma_l\big(\theta_l\cdot F_{l-1}(\theta;x)\big),

and its Jacobian in $x$ is $J_xF_l(\theta;x)$ . All spaces carry the Euclidean norm $\|\cdot\|_2$ , and $\|\cdot\|_{\mathrm{op}}$ is the $\ell_2$ -operator (spectral) norm.

Assumption E. For $l=1,\dots,L$ , the map $\sigma_l$ is $L^0_l$ -Lipschitz for $\|\cdot\|_2$ , its Jacobian $J\sigma_l$ is $L^1_l$ -Lipschitz from $\|\cdot\|_2$ to $\|\cdot\|_{\mathrm{op}}$ , and $L^0_l>0$ . From these constants define

\alpha_l(\theta)=\prod_{j=1}^{l}L^0_j\,\|\theta_j\|_{\mathrm{op}},\qquad \beta_l(\theta)=\alpha_l(\theta)\sum_{j=1}^{l}\frac{L^1_j}{(L^0_j)^2}\,\alpha_j(\theta).

The classification loss is the softmax loss $\ell(\theta;(x,y))=-\log p_y(\theta;x)$ with $p_y(\theta;x)=\exp(F_{L,y}(\theta;x))/\sum_{k=1}^K\exp(F_{L,k}(\theta;x))$ , for a class $y\in\{1,\dots,K\}$ .

Formalization targets

Goal: Corollary 4

Under Assumption E, for every class $y$ and all inputs $x,x'$ ,

\big\|\nabla_x\ell(\theta;(x,y))-\nabla_x\ell(\theta;(x',y))\big\|_2\le\big(\sqrt2\,\beta_L(\theta)+\alpha_L(\theta)^2\big)\,\|x-x'\|_2 .

Proposition 5

Under Assumption E, for $l=1,\dots,L$ ,

\|F_l(\theta;x)-F_l(\theta;x')\|_2\le\alpha_l(\theta)\|x-x'\|_2,\qquad \|J_xF_l(\theta;x)-J_xF_l(\theta;x')\|_{\mathrm{op}}\le\beta_l(\theta)\|x-x'\|_2 .

Milestones

In the order the paper's proof uses them: Lemma 6 (the chain rule for $J_xF_l$ , recursively and as a product); Proposition 5, first part; the telescoping representation (34) of $J_xF_l(\theta;x)-J_xF_l(\theta;x')$ ; Proposition 5, second part; the softmax constants of §B.9 (gradient $p(v)-e_y$ , Lipschitz constant $\sqrt2$ , smoothness constant $1$ ); and the recursion of §B.9 for $\alpha_l,\beta_l$ with its instance $\beta_{L+1}=\sqrt2\,\beta_L+\alpha_L^2$ for a softmax output layer.

Significance

Corollary 4 converts the abstract hypothesis $\gamma>L_{zz}$ of the paper's convergence and certification results (missions 1 and 2 of this series) into a checkable condition on a trained network: $L_{zz}\le\sqrt2\,\beta_L(\theta)+\alpha_L(\theta)^2$ , computable from spectral norms of the weights and from constants of standard activations (the paper lists average pooling, sigmoid and ELU). Proposition 5 is a reusable statement about any composition of smooth maps with linear layers, independent of the softmax and of robust optimization.

The results are proved in the paper (§B.8–§B.9). No machine-checked proof of them is known to exist. This mission produces a formal development of the input Jacobian of a layered network with varying widths, the telescoping estimate for its variation, and the smoothness constants of the softmax loss, all with the paper's explicit constants.

Difficulty

The function-level bound (first part of Proposition 5) is a direct induction. The derivative-level bound is not: the obvious induction on $J_xF_{l+1}=J\sigma_{l+1}\cdot\theta_{l+1}\cdot J_xF_l$ needs both a bound on $\|J_xF_l\|_{\mathrm{op}}$ , which comes from the Lipschitz half and the differentiability of every layer, and a bound on the variation of the Jacobian of the previous layers, and the two must be combined so that the constant comes out as exactly $\beta_l(\theta)$ of (21), whose definition uses quotients by $(L^0_j)^2$ . For the corollary, the softmax loss must be shown to have Lipschitz constant $\sqrt2$ (a supremum that is not attained) and a $1$ -Lipschitz derivative; the paper's eigenvalue argument for the latter is loose and its displayed initial condition for the recursion of the constants is misprinted, so the printed text cannot be transcribed line by line. In Lean, the widths change from layer to layer, so the network is a family of maps between different Euclidean spaces, and every product of Jacobians is a dependently typed composition.

Formalization scope

Inputs, pre-activations and outputs are EuclideanSpace ℝ (Fin n); weights are continuous linear maps, so ‖θ l‖ is the spectral norm; Jacobians are Fréchet derivatives with the operator norm. A Frobenius or entrywise norm would state a different theorem and is not used.
Layers are indexed from $0$ in Lean: Lean layer l is the paper's layer $l+1$ (θ l, σ l, L0 l, L1 l); F l, α L0 l, β L0 L1 l carry the paper's index $l$ . Widths vary with the layer; they are not collapsed to a single dimension.
Assumption E is stated for the first $L$ layers and includes two hypotheses implicit on the page: each $\sigma_l$ is differentiable (the assumption speaks of its Jacobian) and $L^1_l\ge0$ . The paper's $L^0_l>0$ is kept.
$\alpha_l$ and $\beta_l$ are the explicit product and sum of (21); they are definitions, not free parameters. Consequently $\alpha_0=1$ and $\beta_0=0$ ; the paper's " $\beta_0(\theta)=\alpha_0(\theta)=1$ " in §B.9 is a misprint and is not followed. The recursion $\beta_{l+1}=(\alpha_{l+1}/\alpha_l)\beta_l+\dots$ is stated in the division-free form $\beta_{l+1}=L^0_{l+1}\|\theta_{l+1}\|_{\mathrm{op}}\beta_l+\dots$ , and in the paper's form when $\alpha_l\ne0$ .
In (34) the first displayed line (a "product of differences") is a misprint; only the telescoped sum is formalized.
The softmax loss is real-valued on $\mathbb R^K$ with $K=d_{L,O}$ and a class $y$ in Fin K; the goal uses Mathlib's gradient, whose norm equals the operator norm of the derivative.
The goal is not trivialized by free constants: a version with $\alpha,\beta$ as arbitrary parameters, or with the loss not tied to $F_L$ , would not be Corollary 4 and is not what is posed.
Not formalized: the Hessian formula $\nabla^2\sigma_y=\operatorname{diag}p-pp^T$ and the eigenvalue argument (only their conclusion $L^1=1$ is stated); attainment of $\sup_x\|p(x)-e_y\|_2=\sqrt2$ (the value of the supremum, for $K\ge2$ , is stated; it is not attained); Examples 1–3 (constants of pooling, sigmoid and ELU).

A complete development needs the chain rule for the network map, the mean value inequality for the softmax loss, and the algebra of (21). The definitions of the layered network and of the softmax loss are independent of robust optimization and are reusable for other Lipschitz and smoothness bounds of deep networks. Proofs of any milestone, and alternative arguments with sharper constants stated as separate theorems, are welcome.

Selected references

A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
C. Szegedy et al., Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
P. Bartlett, D. Foster, M. Telgarsky, Spectrally-normalized margin bounds for neural networks, NeurIPS 2017. https://arxiv.org/abs/1706.08498

9 thms2 active usersReviewed

Optimization Probability·Captain: visuddhi

VC Theory for Inventory Policies: Xie–Ma–Xin BoundsResearch Paper

Learning inventory policies from historical demand

An inventory policy chooses how much stock to order before demand is observed. Its quality is assessed by the holding and backlogging costs it incurs on future demand. A policy chosen to perform well on historical demand can overfit those observations. A useful statistical guarantee therefore controls the difference between historical and future costs simultaneously over the policies that the procedure may select. Xie, Ma and Xin establish such guarantees for stationary base-stock, $(s,S)$ , and nonstationary base-stock policy classes.

This formalization covers the principal bound families in that paper. Its first goal is the expected generalization and estimation bound for nonstationary base-stock policies with no fixed ordering cost, Corollary 4.10. Its supporting targets include Theorem 4.9 and the constructive product-sample partition in Lemma 4.12. The other principal bounds remain in the explicit scope below and await their own full Lean declarations. The companion inventory-information project needs these results as proved dependencies; merely citing the paper does not close that project's formal proof obligations.

Demand, policy classes and statistical errors

There are $T+L$ periods, a deterministic lead time $L\ge0$ , and demand bounded by $U>0$ . The first order arrives in period $L+1$ . Average loss means the sum of holding and backlogging costs in periods $L+1,\ldots,T+L$ , divided by the positive horizon $T$ . The initial pipeline is empty, and initial inventory is nonpositive for the base-stock models. Holding and backlogging cost coefficients are $h,b\in[0,1]$ . Nonstationary base-stock policies in the first goal have no fixed ordering cost and use levels $S^t\in[0,(L+1)U]$ .

The Lean model indexes the first period by zero. It uses the source's explicit finite-maximum formula for post-replenishment inventory, with the demand interval summed up to, but excluding, the observation period. In mathematical notation the inventory in period $L+k+1$ is $\max_{0\le j\le k}(S_j-\sum_{j\le r<k+L}d_r)$ . Cost is evaluated after subtracting the current demand $d_{L+k}$ . This is a backlog model; applications to lost sales require a separate equivalence argument.

Data comprise $N>0$ IID demand trajectories from a probability measure $\mu$ on the bounded trajectory space. Different periods of the same trajectory can be dependent. Generalization error is the one-sided supremum $\mathrm{GE}=\sup_S(R(S)-\widehat R(S))$ , where $R$ is expected average loss and $\widehat R$ is empirical average loss. Estimation error is $R(\widehat S)-R(S_*)$ , for an empirical minimizer and a best-in-class population policy. It is not the error relative to every history-dependent inventory policy. These conventions follow Sections 3 and 4.

Formalization targets

The first goal, Corollary 4.10, asserts the existence of one absolute constant $C>0$ such that

\mathbb E\mathrm{EE}\le\mathbb E\mathrm{GE}\le C(L+1)U/\sqrt N.

The constant is quantified before the horizon, lead time, support, costs, demand distribution, sample size, and policy selections. The first inequality explicitly refers to actual minimizers, with an integrable selected risk. The GE conclusion holds independently of whether a particular selector has been supplied.

Its principal complexity target is Theorem 4.9: for each relevant period and $0<\gamma\le1$ , the normalized inventory class has fat-shattering dimension at most $2/\gamma+1$ . The Lean statement says directly that every $\gamma$ -shattered indexed sample has cardinality at most that number. It uses the source convention of a strict upper label and non-strict lower label.

Lemma 4.12 partitions all $N^D$ product indices into $N^{D-1}$ groups of $N$ indices. Every coordinate of every group traverses the original row indices exactly once. The formal statement uses a bijection between anchor-offset pairs and complete index tuples, together with a coordinate-permutation assertion. The dimension $D=d+1$ is positive, and $N=1$ and $D=1$ are included.

The full scope also retains Theorem 4.1 and Corollary 4.2 (stationary policies), Theorem 4.4 and Corollary 4.5 ( $(s,S)$ upper bounds), Theorem 4.7 and Corollary 4.8 ( $(s,S)$ fat-shattering and GE lower bounds), and the expected Product ERM comparison in equation (4.7). They are catalogued with their assumptions but are not yet all encoded. The GE lower bound is not asserted to be a minimax policy-regret lower bound.

What the formalization supplies

The nonstationary policy vector grows with the horizon, while the expected average-loss bound has no horizon factor. A verified version supplies a reusable statistical ingredient for finite-horizon inventory learning. Total-cost bounds require multiplication by the horizon. Absolute uniform deviation, period-dependent costs, high-probability statements, initial-state reductions, and censoring require further bridge theorems. They are not attributed to Corollary 4.10 without those proofs.

The cyclic partition has a complete locally checked Lean proof with axiom dependencies only propext and Quot.sound. The two statistical targets remain open. Neither a drafted declaration nor a local proof is described as a server-verified contribution.

Mathematical difficulty

Ordinary pseudodimension can grow with the horizon for the nonstationary class, so it does not by itself give the desired horizon-free rate. A full proof needs scale-sensitive complexity, probability, and integration infrastructure. For Product ERM, coordinate independence must be explicit: the groups in the partition need not be independent of each other. The expected comparison transfers upper bounds; it cannot reverse direction to transfer a GE lower bound.

Formalization scope and conventions

The shared environment is Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Demand and policy coordinates are bounded real subtypes with their usual measurable structures. Probability is over IID whole trajectories. Finite maximum indices are nonempty. Positive $T,N,U$ prevent zero denominators in the targets. General definitions remain total, and their behavior outside these hypotheses is exposed in the independent read-backs.

Complete proofs must establish the boundedness and measurability needed for the real suprema and integrals to have their usual meaning. They may not assume the convergence bound, replace arbitrary probability measures by finite-support distributions, or silently restrict the policy class. The $(s,S)$ branch additionally needs explicit unbounded-domain conventions when holding or backlogging costs vanish. Reusable contributions include shattering, symmetrization, entropy bounds, selection and integrability facts, and finite-product sampling.

Selected references

Yaqi Xie, Will Ma and Linwei Xin, VC Theory for Inventory Policies, arXiv:2404.11509v3, 2026. https://arxiv.org/abs/2404.11509v3
Hanzhang Qin, David Simchi-Levi and Ruihao Zhu, Information Limits of Multistage Inventory Control: Learning, Valuation, and Censoring, arXiv:2609.37380v1, 2026. https://arxiv.org/abs/2609.37380v1

6 thms2 active usersReviewed

Computational Geometry Linear algebra Machine Learning·Captain: mikedeng1

Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering I: The Rank-m SVD Truncation Plus Its Residual Preserves the Cost of Every j-Dimensional ShapeResearch Paper

Motivation

Large data sets make clustering and subspace fitting expensive because a candidate solution must be evaluated against every input point. A dimensionality reduction replaces the data by a lower-rank matrix whose costs approximate those of the original input for an entire class of candidate solutions. Feldman, Schmidt, and Sohler study reductions that retain enough information for $k$ -means, principal component analysis, and projective clustering. Their journal paper identifies a rank truncation and one residual scalar that preserve the fitting cost of every shape lying in a low-dimensional linear subspace Feldman, Schmidt, and Sohler (2020), Theorem 22.

The published article also records that some coreset sizes in its 2013 conference version were incorrect. This mission uses the 2020 journal statement and its page numbering throughout. The authors cite earlier SVD-based approximations to $k$ -means on p. 613, while their Theorem 22 gives a uniform cost guarantee for arbitrary nonempty shapes contained in a $j$ -dimensional subspace Feldman, Schmidt, and Sohler (2020), pp. 603, 613, 620.

Setting

The input is a real matrix $A\in\mathbb R^{n\times d}$ . Its $n$ rows are points in $\mathbb R^d$ . For a nonempty set of candidate locations or shapes $C\subseteq\mathbb R^d$ , let $\operatorname{dist}(a_i,C)$ be the infimum of Euclidean distances from row $a_i$ to points of $C$ . The shape cost is

\operatorname{dist}^2(A,C)=\sum_{i=1}^{n}\operatorname{dist}(a_i,C)^2.

The set $C$ need not be closed and need not be a subspace. For example, it can be a finite set of cluster centers. The restriction is that all of its points lie in some linear subspace of dimension $j$ . This matches the paper's shape class in §5; the affine case is treated separately Feldman, Schmidt, and Sohler (2020), pp. 619–620.

Fix a singular value decomposition $A=U\Sigma V^T$ , where $U$ and $V$ are orthogonal and the diagonal entries of the rectangular matrix $\Sigma$ are nonnegative and nonincreasing. The entry $\sigma_i$ is indexed from one. The rank- $m$ truncation $A^{(m)}=U\Sigma^{(m)}V^T$ keeps the first $m$ diagonal entries and sets the rest to zero. Its squared Frobenius residual is $\Delta=\|A-A^{(m)}\|_F^2$ . The corrected cost of $C$ is $\operatorname{dist}^2(A^{(m)},C)+\Delta$ Feldman, Schmidt, and Sohler (2020), Definition 1 and §2.

Formalization targets

Linear subspace estimates

The milestones first record the matrix Pythagorean identity, the $j\sigma_{m+1}^2$ projection and residual bounds, and the lower bound on the cost of a linear $j$ -subspace. They then state the residual-corrected approximation in Corollary 16:

\|AY\|_F^2\le\|A^{(m)}Y\|_F^2+\Delta\le(1+\varepsilon)\|AY\|_F^2, \qquad m\ge\lceil j/\varepsilon\rceil+j-1.

Here $Y$ has $d-j$ orthonormal columns spanning the complement of the candidate subspace. Corollary 20, Corollary 21, and display (9) connect these linear estimates to costs of general sets $C$ Feldman, Schmidt, and Sohler (2020), pp. 604, 613–615, 619–620.

Goal: uniform shape-cost preservation

The goal is Theorem 22. For $1\le j\le d-1$ , $0<\varepsilon\le1$ , and $\lceil8j/\varepsilon^2\rceil-1\le m\le\min\{n,d\}-1$ , every nonempty $C$ contained in a linear $j$ -dimensional subspace satisfies

\left|\bigl(\operatorname{dist}^2(A^{(m)},C)+\|A-A^{(m)}\|_F^2\bigr) -\operatorname{dist}^2(A,C)\right| \le\varepsilon\operatorname{dist}^2(A,C).

The quantifier over $C$ makes this a guarantee for every admissible candidate on the same reduced data, rather than a statement about one selected optimum Feldman, Schmidt, and Sohler (2020), Theorem 22, p. 620.

Significance

The theorem preserves objective values after replacing $A$ by a rank- $m$ matrix and one number. For a fixed $j$ and accuracy parameter, the rank threshold depends on $j$ and $\varepsilon$ , with no direct dependence on the number of points $n$ or ambient dimension $d$ except the upper bound on feasible $m$ . In the paper, the result leads to a guarantee for $k$ -means candidates, since $k$ centers span a linear subspace of dimension at most $k$ Feldman, Schmidt, and Sohler (2020), Corollary 23, p. 621.

The result is proved in the paper, but this mission's Lean theorems are posed with sorry; they do not yet have machine-checked proofs. A completed development would connect a reusable rectangular SVD model, matrix projection identities, infimum distances to arbitrary nonempty sets, and a uniform cost inequality. The SVD definition is already published in the platform library; the row-cost and singular-value conventions here supply the interface needed for this paper Feldman, Schmidt, and Sohler (2020), §§2, 3, 5.

Difficulty

The linear subspace bound compares a projection cost with a tail sum of squared singular values. The paper recalls that fact in §3 without proving it, so the formal development needs a suitable singular-value inequality or a derivation from existing matrix approximation results. For general shapes $C$ , a bound on the cost of one linear subspace does not by itself control the distance from each projected point to every point of $C$ . The remaining milestones state the projection error, the squared-distance perturbation bound, and the Pythagorean cost split that address that gap Feldman, Schmidt, and Sohler (2020), pp. 613, 619–621.

The proof printed after Theorem 22 invokes earlier corollaries under a stronger rank threshold than the theorem states. The mission keeps the printed theorem threshold, whose claim remains valid; a formal proof must bridge that discrepancy Feldman, Schmidt, and Sohler (2020), pp. 620–621.

Formalization scope

Matrices are Matrix (Fin n) (Fin d) ℝ, and rows are points of EuclideanSpace ℝ (Fin d). Squared Frobenius norm is an explicit finite sum of squared entries. Shape cost sums squared Metric.infDist values over rows. Since Mathlib assigns a real default value to distance from the empty set while the paper assigns infinity, every theorem about a general shape $C$ requires C.Nonempty. This is the page's own requirement for Theorem 22 and Corollary 21, and is also needed for display (9).

The SVD and its truncation use the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every SVD statement quantifies over an arbitrary valid triple $(U,\Sigma,V)$ ; tied singular values do not fix a unique truncation. The local $\sigma_i$ is one-based, while truncSVD m keeps zero-based diagonal positions below $m$ . Orthonormal columns of $X$ satisfy $X^TX=I$ , their orthogonal complement has $d-j$ columns, and projection in ambient coordinates is $AXX^T$ . Theorem 22 quantifies over arbitrary nonempty $C$ contained in a linear $j$ -subspace; it does not restrict $C$ to subspaces or replace linear containment by affine containment.

The integer inequalities in Lean use additive forms such as $\lceil8j/\varepsilon^2\rceil\le m+1$ to avoid truncated natural-number subtraction. The theorem retains the printed $m$ threshold, including the proof gap described above. Running-time clauses are outside the mission's mathematical statements. Contributions are welcome toward the singular-value lower bound, the projection and infimum-distance identities, and the final uniform inequality; the matrix and distance definitions are reusable in the companion affine-subspace mission.

Selected references

Dan Feldman, Melanie Schmidt, and Christian Sohler, Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering, SIAM Journal on Computing 49(3):601–657, 2020. DOI: 10.1137/18M1209854.

11 thms2 active usersReviewed

Convex Optimization Information Theory Optimization+1·Captain: mikedeng1

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization I: The Linearly Constrained de Finetti SDP Hierarchy Satisfies Q ≤ SDPₙ ≤ Q + ‖G‖∞·d_B²(d_B+1)·√((2 ln 2) log d_A / n)Research Paper

Motivation

Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.

For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of $n$ -extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).

Setting

A $d$ -dimensional quantum system has operator space $\mathcal S=\mathbb C^{d\times d}$ ; a state is a positive semidefinite $W\in\mathcal S$ with $\mathrm{Tr}\,W=1$ . Let $A$ and $B$ be systems of dimensions $d_A$ and $d_B$ . The data are an objective $G_{AB}\in\mathcal S_A\otimes\mathcal S_B$ , arbitrary linear maps $\Lambda_{A\to C_A}:\mathcal S_A\to\mathcal S_{C_A}$ and $\Gamma_{B\to C_B}:\mathcal S_B\to\mathcal S_{C_B}$ , and matrices $X_{C_A}$ , $Y_{C_B}$ . The constrained bilinear program is

Q=\max\ \mathrm{Tr}[G_{AB}(W_A\otimes W_B)]\quad\text{s.t. } W_A,W_B\ \text{states},\quad \Lambda_{A\to C_A}(W_A)=X_{C_A},\quad \Gamma_{B\to C_B}(W_B)=Y_{C_B}.

For $n\ge1$ let $B_1,\dots,B_n$ be copies of $B$ . A state $W_{AB_1^n}$ on $A\otimes B_1\cdots B_n$ is symmetric with respect to $A$ if it is invariant under every permutation $\mathcal U^\pi_{B_1^n}$ of the copies $B_1,\dots,B_n$ , $\pi\in\mathfrak S_n$ . Write $W_{B_1^n}=\mathrm{Tr}_A W_{AB_1^n}$ , $W_{B_1^{n-1}}=\mathrm{Tr}_{B_n}W_{B_1^n}$ and $W_{AB_1}=\mathrm{Tr}_{B_2^n}W_{AB_1^n}$ . The level- $n$ program is

\mathrm{SDP}_n=\max\ \mathrm{Tr}[G_{AB}W_{AB_1}]\quad\text{s.t. } W_{AB_1^n}\ \text{a state, symmetric with respect to } A,

(\Lambda_{A\to C_A}\otimes\mathcal I_{B_1^n})(W_{AB_1^n})=X_{C_A}\otimes W_{B_1^n},\qquad (\mathcal I_{B_1^{n-1}}\otimes\Gamma_{B_n\to C_B})(W_{B_1^n})=W_{B_1^{n-1}}\otimes Y_{C_B}.

It is a semidefinite program of size polynomial in $d_A$ and $d_B^n$ .

The rate involves the trace norm $\|X\|_1=\mathrm{Tr}|X|$ , the Schatten $\infty$ -norm $\|G\|_\infty$ (largest singular value), and the minimal distortion with side information of $B$ ,

f(B|\cdot)=\inf_{\mathcal M_B}\ \sup_{\substack{\xi_{AB}^\dagger=\xi_{AB}\\ \xi_A=0,\ \xi_B=0}}\frac{\|\xi_{AB}\|_1}{\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1},

the infimum over measurements $\mathcal M_B$ on $B$ and the supremum over all finite-dimensional $A$ ; $f(A,B)$ is the analogue with product measurements $\mathcal M_A\otimes\mathcal M_B$ . Throughout, $\log$ is base 2.

Formalization targets

Goal: Theorem 3.1 with its explicit rate

Q\ \le\ \mathrm{SDP}_n\ \le\ Q+\|G_{AB}\|_\infty\,d_B^2(d_B+1)\sqrt{\frac{(2\ln2)\log d_A}{n}}\quad(n\ge1),\qquad Q=\lim_{n\to\infty}\mathrm{SDP}_n.

The page states $0\le\mathrm{SDP}_n-Q\le\mathrm{poly}(d)/\sqrt n$ with $d=\max\{d_A,d_B\}$ . The goal makes explicit the rate the proof gives.

Milestones, in attack order

Lemma 2.1 (p. 6): for a permutation-invariant classical-quantum state $\rho_{AZ_1^n}$ there is $0\le m<n$ with $\mathbf E_{z_1^m}\|\rho_{AZ_{m+1}|z_1^m}-\rho_{A|z_1^m}\otimes\rho_{Z_{m+1}|z_1^m}\|_1^2\le(2\ln2)\log d_A/n$ .
Lemma D.1 (p. 29): for a state two-design $\{P_z\}$ and $\mathcal M_B$ with effects $\frac{d_B}{t}P_z$ , $\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1\ge\|\xi_{AB}\|_1/(d_B^2(d_B+1))$ for every Hermitian $\xi_{AB}$ .
Existence of state two-designs in every dimension (p. 29).
$f(B|\cdot)\le d_B^2(d_B+1)$ (p. 6).
Conditional constraints (p. 8): the states obtained by measuring $B_1,\dots,B_m$ and conditioning satisfy $\Lambda(\rho_{A|z_1^m})=X_{C_A}$ and $\Gamma(\rho_{B_{m+1}|z_1^m})=Y_{C_B}$ .
Theorem 2.3 (p. 7): under the constraints of $\mathrm{SDP}_n$ , $\|\rho_{AB}-\sum_ip_i\sigma^i_A\otimes\omega^i_B\|_1\le\min\{f(A,B),f(B|\cdot)\}\sqrt{(2\ln2)\log d_A/n}$ with states $\Lambda(\sigma^i_A)=X_{C_A}$ , $\Gamma(\omega^i_B)=Y_{C_B}$ .
Eq. (3) (p. 2): $Q$ equals the maximum over mixtures of feasible product states.
Hölder step (p. 11): $\mathrm{Tr}[GW]\le\mathrm{Tr}[GV]+\|G\|_\infty\|W-V\|_1$ .
$0\le\mathrm{SDP}_n-Q$ (p. 11).

Significance

Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate $O(1/\sqrt n)$ , with a constant that depends polynomially on $d_B$ and logarithmically on $d_A$ . Every level is a certified upper bound; together with any feasible point it brackets $Q$ . The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.

The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.

Difficulty

The obvious route measures every copy $B_i$ with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates $\rho_{AB}$ by a mixture of product states, but the states in the mixture need not satisfy $\Gamma(\omega^i)=Y$ , and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only $m$ copies and keeps $B_{m+1}$ quantum; the constraint on $B_n$ then transfers to the conditional state of $B_{m+1}$ by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system $A$ , which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.

Formalization scope

Systems are finite index types: $A\otimes B_1\cdots B_N$ is indexed by Fin dA × (Fin N → Fin dB), $\otimes$ is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps $\Lambda$ , $\Gamma$ are arbitrary $\mathbb C$ -linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of $\mathrm{Tr}[G\,W]$ , equal to $\mathrm{Tr}[G\,W]$ for Hermitian $G$ . Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has $n\ge1$ copies of $B$ , the Lean has n + 1: SDPval … n is the page's $\mathrm{SDP}_{n+1}$ , and the bounds have denominator $n+1$ . The distortions $f(A,B)$ and $f(B|\cdot)$ take values in $[0,\infty]$ ; the standalone bound on $f(B|\cdot)$ assumes $d_B\ge1$ .

No feasibility hypothesis is added to the goal. The feasible sets of $Q$ and of every level are empty or nonempty together, and the empty case reads $0\le0\le0+\dots$ . The goal mentions only $Q$ , $\mathrm{SDP}_n$ , $G$ , $d_A$ , $d_B$ and $n$ ; a formalization in which $Q$ or $\mathrm{SDP}_n$ were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.

Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.

Selected references

M. Berta, F. Borderi, O. Fawzi, V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3. https://arxiv.org/abs/1810.12197
F. G. S. L. Brandão, A. W. Harrow, Quantum de Finetti theorems under local measurements with applications, STOC 2013. https://arxiv.org/abs/1210.6367
M. Christandl, R. König, G. Mitchison, R. Renner, One-and-a-half quantum de Finetti theorems, Communications in Mathematical Physics 273, 2007. https://arxiv.org/abs/quant-ph/0602130
A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 2004. https://arxiv.org/abs/quant-ph/0308032

17 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity 2: Under Unknown Sparsity, Lasso-Based ILQX Pricing Has Regret at Most Cs√T(log d + log T)Research Paper

Motivation

Online sellers of loans, insurance, travel and retail goods observe data about each arriving customer before quoting a price. Using that data to price individually is attractive only if the seller can learn, from its own sales, how demand responds to price for customers with given characteristics. Two features make this hard in practice. The number of recorded characteristics $d$ is often large, possibly larger than the selling horizon $T$ , while only a few of them matter. And price sensitivity is itself heterogeneous: different customers respond to the same price change differently.

Ban and Keskin (Management Science 67(9), 2021) model both features and ask how fast the revenue lost to learning can grow. Their answer is that a seller who learns with lasso-regularized quasi-likelihood estimation and occasional price experiments loses revenue of order $s\sqrt T$ up to logarithmic factors, where $s$ is the number of relevant characteristics, and that no policy can do better than order $s\sqrt T$ . This mission formalizes the upper bound for the general (nonlinear-link) model with unknown sparsity, Theorem 3 of the paper.

Setting

In each period $t = 1, 2, \dots, T$ a customer arrives with a raw feature vector $Z_t \in \mathbb R^d$ . The $Z_t$ are i.i.d., take values in a compact set $\mathcal Z$ inside a ball of radius $z_{\max}$ , have mean zero and positive definite covariance $\Sigma_Z$ . The seller sees the augmented vector $X_t = [1; Z_t] \in \mathbb R^{d+1}$ , charges a price $p_t \in [\ell, u]$ with $0 < \ell < u$ , and observes the demand

D_t = g\big(\alpha \cdot X_t + (\beta \cdot X_t)\, p_t\big) + \varepsilon_t .

Here $\theta = (\alpha, \beta)$ is an unknown parameter in a compact rectangle $\Theta \subset \mathbb R^{2(d+1)}$ , the link $g$ is known, differentiable and increasing with $\tilde\ell \le g' \le \tilde u$ on the relevant domain, and the demand shocks $\varepsilon_t$ form a sub-Gaussian martingale difference sequence. The term $\beta \cdot X_t$ is the customer's own price sensitivity. With $u(p, x) = [1; p] \otimes x$ the argument of $g$ is $\theta \cdot u(p, x)$ .

The sparsity of $\theta$ is $s = |\mathcal S|$ , $\mathcal S = \{i : \alpha_i \neq 0\} \cup \{i : \beta_i \neq 0\}$ . The seller does not know $\mathcal S$ .

The expected revenue of price $p$ is $r(p, \theta, x) = p\, g(\theta \cdot u(p,x))$ , and the clairvoyant price $\varphi(\theta, x)$ maximizes it; it is assumed to lie in the interior of $[\ell, u]$ for $\theta \in \Theta$ , $x \in \mathcal X = \{1\} \times \mathcal Z$ . The regret of a policy over $T$ periods is

\Delta^\pi_\theta(T) = \mathbb E\Big[\sum_{t=1}^T r^*(\theta, X_t) - r(p_t, \theta, X_t)\Big], \qquad r^*(\theta,x) = r(\varphi(\theta,x),\theta,x).

The policy ILQX $(m_1, m_2, \lambda)$ charges the experimental price $m_1$ in periods $M_1 = \{1, 4, 9, \dots\}$ and $m_2$ in periods $M_2 = \{2, 5, 10, \dots\}$ , and otherwise charges $\varphi(\mathcal P_\Theta \hat\theta_t, X_t)$ , where $\hat\theta_t$ maximizes the lasso-penalized quasi-likelihood

Q_{t-1}(\tilde\theta, \lambda_t) = \sum_{k=1}^{t-1} \chi_k \int_{D_k}^{g(\tilde\theta \cdot u_k)} \frac{D_k - y}{g'(g^{-1}(y))}\, dy - \lambda_t \|\tilde\theta\|_1

over the experimental periods ( $\chi_k = \mathbb I\{k \in M_1 \cup M_2\}$ ), and $\mathcal P_\Theta$ is the projection onto $\Theta$ . The regularization level is $\lambda_{t+1} = \tilde c\, t^{1/4} \sqrt{\log d + \log t}$ for a constant $\tilde c > 0$ .

Formalization targets

Goal: Theorem 3

There is a finite constant $\tilde C > 0$ such that

\Delta^\pi_\theta(T) \le \tilde C\, s \sqrt T\, (\log d + \log T) \qquad \text{for all } \theta \in \Theta,\ T \ge 2 .

$\tilde C$ is fixed with the model and is uniform over $\Theta$ ; since $s = s(\theta)$ varies over $\Theta$ , the factor $s$ carries content.

Milestones

The counting property of the schedule (7): for $t \ge 5$ each experimental price is charged at least $\tfrac14 \sqrt t$ times in periods $1, \dots, t$ .
Lemma 3, the estimation error of the lasso quasi-likelihood estimate:

\mathbb P\Big\{\|\hat\theta^{(\mathrm{lasso})}_{t+1}(\lambda_{t+1}) - \theta\|^2 \le \rho_3 \frac{s(\log d + \log t)}{\sqrt t}\Big\} \ge 1 - \kappa_3 \frac{s(\log d + \log t)}{\sqrt t}, \qquad t \ge t_1 .

Significance

Theorem 3 says that a seller facing many potentially relevant customer characteristics, without knowing which matter and under a nonlinear demand link such as logit, loses revenue at a rate governed by the number $s$ of relevant characteristics and only logarithmically by the total number $d$ . Combined with the paper's $s\sqrt T$ lower bound (Theorem 1, for the linear model), it makes ILQX first-order optimal up to logarithmic factors. An unregularized policy would pay order $d\sqrt T$ , which is linear in $T$ when $d$ exceeds $\sqrt T$ .

The paper's proofs are in its electronic companion, which this mission does not reproduce; no machine-checked version of the result exists. A complete formalization would also produce a reusable high-probability error bound for lasso-regularized quasi-likelihood estimation under adaptively collected data (Lemma 3), and a machine-checked model of feature-based dynamic pricing on which related policies can be stated.

Difficulty

The estimation error must be controlled on data collected by the policy itself. The design vectors $u_k = [1; m_{i(k)}] \otimes X_k$ use only two prices, so the information about the price sensitivity accrues only from the $\Theta(\sqrt t)$ experimental periods. Standard lasso error bounds assume a fixed or i.i.d. design and a restricted-eigenvalue condition on it; here a restricted-eigenvalue-type property of the random Kronecker design must be derived from $\Sigma_Z \succ 0$ and $m_1 \ne m_2$ , and the noise enters through a martingale whose conditional law may depend on past prices. The quasi-likelihood is not a least-squares objective, so the curvature comes from the bounds $\tilde\ell \le g' \le \tilde u$ , which hold only on the bounded domain $\{\theta \cdot u(p,x) : \theta \in \Theta\}$ and not at an unconstrained estimate. Finally, the regret bound has to turn a squared-error bound holding with probability $1 - O(s \log(dt)/\sqrt t)$ into an expected revenue loss, which requires the revenue loss to be second order in the parameter error at an interior optimum.

Formalization scope

Coordinates. $x \in \mathbb R^{d+1}$ is Fin (d+1) → ℝ with the intercept at index 0; $\theta$ is Fin 2 × Fin (d+1) → ℝ with $\theta(0,i) = \alpha_i$ , $\theta(1,i) = \beta_i$ . Periods are 1-based. $d \ge 1$ .
Objective. The integrated form $\sum_k \chi_k \big(D_k\,(\tilde\theta \cdot u_k) - \int_0^{\tilde\theta \cdot u_k} g\big) - \lambda \|\tilde\theta\|_1$ , which differs from the paper's (17) by a term not depending on $\tilde\theta$ and therefore has the same maximizers.
Estimator. Any measurable selection that is a maximizer whenever one exists; the theorems hold for every such selection. The paper's claim that (17) is strictly concave with a unique maximizer fails when $2(d+1)$ exceeds the rank of the design.
Policy. The price is defined by strong recursion over the realized history; the estimator sees $\theta$ only through the realized demands.
Regret is a lower Lebesgue integral of nonnegative losses; conditional moments of the shocks use the conditional Lebesgue expectation; probabilities are compared in $[0, \infty]$ .
Standing assumptions formalized: i.i.d. measurable features in a compact $\mathcal Z$ inside a Euclidean ball, mean zero, positive definite $\Sigma_Z$ ; fresh customers ( $Z_{t+1}$ independent of the past); sub-Gaussian martingale-difference shocks; $m_1 \ne m_2$ in $[\ell, u]$ ; $g$ differentiable and increasing with derivative bounds on the relevant domain (endnote 2 states them as a consequence, which is false; here they are a hypothesis); $\varphi$ an unconstrained revenue maximizer in $(\ell, u)$ whose pricing map after projection and feature augmentation is measurable. The processes are constrained only at the used periods $t\ge1$ .
Added hypotheses, per $\theta$ : $s(\theta) \ge 1$ (the paper's $s \in \{1, \dots, d+1\}$ ), and almost surely every realized demand lies in the closure of the range of $g$ , which guarantees that a maximizer of (17) exists (true for the linear link and for binary demand under a logit link).
Not formalized: the paper's support condition on continuous features; Remark 7's independence of $\tilde C$ from $d$ ; dependence of the shock law on $\theta$ (the shocks are one fixed process).
Ruled-out trivializations. The regret cannot vanish by non-integrability; the estimator cannot be an arbitrary function, since it must maximize the objective; $\tilde C$ and $\kappa_3, \rho_3, t_1$ are chosen before $\theta$ , so they cannot absorb $s$ ; the hypotheses are jointly satisfiable (a linear-link instance with $d = 1$ is checked).

Contributions welcome: existence of a measurable maximizer of the objective, the counting lemma, and supporting lemmas for Lemma 3 and the regret bound.

Selected references

G.-Y. Ban and N. B. Keskin, Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity, Management Science 67(9):5549–5568, 2021. https://doi.org/10.1287/mnsc.2020.3680
A. V. den Boer and B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
N. B. Keskin and A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014. https://doi.org/10.1287/opre.2014.1294
A. Javanmard and H. Nazerzadeh, Dynamic Pricing in High-Dimensions, Journal of Machine Learning Research 20(9):1–49, 2019. https://jmlr.org/papers/v20/17-357.html

6 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness II: Fixed-Frequency Restarts Shrink the Distance to the Solution Set by β per Restart on Sharp ProblemsResearch Paper

Motivation

Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.

This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor $\beta$ per restart.

Setting

Let $X \subseteq \mathbb R^n$ and $Y \subseteq \mathbb R^m$ be closed convex sets and let $L(x, y)$ be differentiable, convex in $x$ and concave in $y$ . Problem (1) is

\min_{x \in X} \max_{y \in Y} L(x, y),

with feasible region $Z = X \times Y$ and primal-dual points $z = (x, y)$ . Its solution set $Z^\star$ is the set of saddle points $z^\star \in Z$ : $L(x^\star, y') \le L(x^\star, y^\star) \le L(x', y^\star)$ for all $x' \in X$ , $y' \in Y$ . Throughout, $Z^\star \neq \emptyset$ .

Distances are measured in a semi-norm $\|\cdot\|$ , which the paper allows in order to cover ADMM. Write $\operatorname{dist}(z, Z^\star) = \inf_{z^\star \in Z^\star}\|z - z^\star\|$ , $\operatorname{diam}(S) = \sup_{s, s' \in S}\|s - s'\|$ , and $W_r(z) = \{\hat z \in Z : \|z - \hat z\| \le r\}$ . The primal-dual gap (3) at $z$ is $\sup_{\hat z \in Z}\{L(x, \hat y) - L(\hat x, y)\}$ , and the normalized duality gap (4a)–(4b) is

\rho_r(z) = \frac{1}{r}\sup_{\hat z \in W_r(z)}\{L(x, \hat y) - L(\hat x, y)\} \quad (r > 0), \qquad \rho_0(z) = \limsup_{r \to 0^+}\rho_r(z).

By Definition 1, problem (1) is $\alpha$ -sharp on $S \subseteq Z$ if $\alpha\operatorname{dist}(z, Z^\star) \le \rho_r(z)$ for all $z \in S$ and all $r \in (0, \operatorname{diam}(S)]$ .

The base method is abstract. From a start $z^0$ it outputs averaged points $\bar z^t$ , $t \ge 1$ . It has Property 3 with constants $q, C > 0$ if, for every start $z^0 \in Z$ and every $t \ge 1$ , $\bar z^t \in Z$ and

i. $\rho_{\|\bar z^t - z^0\|}(\bar z^t) \le 2C\|\bar z^t - z^0\|/t$ ,

ii. $\|\bar z^t - z^0\| \le (q + 2)\operatorname{dist}(z^0, Z^\star)$ .

Algorithm 1 with fixed-frequency restarts (29) runs the base method from $z^{n,0}$ for

t^\star = \left\lceil \frac{2C(q+2)}{\alpha\beta}\right\rceil

steps, sets $z^{n+1,0} = \bar z^{n,t^\star}$ , and repeats, with $\beta \in (0, 1)$ .

Formalization targets

Goal: Theorem 1 (p. 17)

If the base method has Property 3 and (1) is $\alpha$ -sharp on $W_R(z^{0,0})$ with $R = \frac{q+2}{1-\beta}\operatorname{dist}(z^{0,0}, Z^\star)$ , then for every $n \ge 0$

\operatorname{dist}(z^{n,0}, Z^\star) \le \beta^n \operatorname{dist}(z^{0,0}, Z^\star). \tag{31}

Milestones

Proposition 5 (p. 11): for $z \in Z$ , $\rho_r(z)$ is non-increasing in $r \in [0, \infty)$ .
Proposition 6 (p. 11): for $z \in Z$ and $r \ge 0$ , the primal-dual gap at $z$ is zero if and only if $\rho_r(z) = 0$ .
Proposition 8 (p. 17): under Property 3, $\|\bar z^t - z^0\| = 0$ implies $\bar z^t \in Z^\star$ .
First display of the proof of Theorem 1 (p. 17): if (31) holds for all $n \le N$ , then $\|z^{N+1,0} - z^{0,0}\| \le R$ , so $z^{N+1,0} \in W_R(z^{0,0})$ .
Display (32) (p. 17): if $z^{N,0}, z^{N+1,0} \in W_R(z^{0,0})$ , then

\operatorname{dist}(z^{N+1,0}, Z^\star) \le \beta\operatorname{dist}(z^{N,0}, Z^\star).

Companion statements

Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates $z^t$ and targets $\hat z^t$ has Property 1 with $C$ if $L(\hat x^{t+1}, y) - L(x, \hat y^{t+1}) \le \frac C2\|z - z^t\|^2 - \frac C2\|z - z^{t+1}\|^2$ for every $z \in Z$ (12). It has Property 2 with $q$ if $\|\hat z^t - z^t\| \le q\operatorname{dist}(z^t, Z^\star)$ or $\|\hat z^t - z^{t-1}\| \le q\operatorname{dist}(z^t, Z^\star)$ .

Proposition 2: Property 1 gives non-expansiveness $\|z^{t+1} - z^\star\| \le \|z^t - z^\star\|$ and the ergodic rate $L(\bar x^t, y) - L(x, \bar y^t) \le C\|z - z^0\|^2/(2t)$ .
Proposition 4: Properties 1 and 2 give Property 3 for the averages $\bar z^t = \frac1t\sum_{i=1}^t \hat z^i$ , with the same $q$ and $C$ .

Fact 1 (p. 11), that $r\rho_r(z)$ is non-decreasing in $r$ , is included as well.

Significance

Theorem 1 converts any primal-dual method with an $O(1/t)$ ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is $O\big(\frac{C}{\alpha}\log\frac1\epsilon\big)$ iterations to reach $\operatorname{dist}(z, Z^\star) \le \epsilon$ (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with $\alpha$ the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.

The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.

Difficulty

Each proof is short, but the statements are delicate in ways the paper passes over.

The paper's argmax over $W_r(z)$ need not exist under a semi-norm, and $\rho_r(z)$ may be $+\infty$ . Proposition 5 therefore has to be proved with suprema, through the convex-combination scaling $z + \frac{r_1}{r_2}(\hat z - z)$ , not with a maximizer.
Sharpness is only available at radii in $(0, \operatorname{diam}(W_R(z^{0,0}))]$ and only at points of $W_R(z^{0,0})$ . So the induction in Theorem 1 must carry two facts together: the contraction (31), and the fact that every restart point stays in $W_R(z^{0,0})$ .
The step size $r = \|z^{N+1,0} - z^{N,0}\|$ may be zero, which is why Proposition 8, and through it Propositions 5 and 6 at $r = 0$ , is needed.

A direct contraction argument that applies sharpness at an arbitrary radius, or on all of $Z$ , does not prove the theorem as stated.

Formalization scope

$\mathbb R^n$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). $n = 0$ and $m = 0$ are allowed.
The semi-norm is an arbitrary Seminorm ℝ on their product, never the product's built-in norm.
The primal-dual gap, $\rho_r$ and $\operatorname{diam}$ are suprema in EReal, so unbounded sets give $+\infty$ and not a junk $0$ . $\operatorname{dist}(\cdot, Z^\star)$ is a real infimum over the nonempty set $Z^\star$ .
The base method is a map from starts to sets of admissible output sequences, because a primal-dual step can be an argmin and need not be single-valued. Property 3 quantifies over every start in $Z$ and every run, with $q$ and $C$ fixed first.
The restart length is the natural number $\lceil 2C(q+2)/(\alpha\beta)\rceil$ , and every inner loop has exactly this length.

Standing assumptions and added hypotheses:

$X$ and $Y$ are closed and convex, and $L$ is convex-concave and differentiable on the whole space.
$Z^\star \neq \emptyset$ replaces the page's "non-empty feasible region and bounded optimal value".
$\alpha > 0$ is assumed.
Property 1 is required for every $t \ge 0$ , although the paper's $\mathbb N$ starts at one: the proof of Proposition 2 telescopes from $z^0$ .
The iterates of a generic algorithm stay in $Z$ , which the page leaves implicit.

Departures from the page:

Proposition 8 asserts only $\bar z^t \in Z^\star$ . The page's " $\bar z^{n,t} = z^{n,0}$ " does not follow under a semi-norm.
Milestones that do not use a standing assumption drop it.

The goal is not trivialized by its hypotheses. A companion check file exhibits $L(x, y) = xy$ on $\mathbb R \times \mathbb R$ , with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and $\operatorname{dist}(z^{0,0}, Z^\star) = 1$ . Sharpness is assumed only where Definition 1 and the theorem assume it: replacing $W_R(z^{0,0})$ by $Z$ , or the radius range by all $r > 0$ , would weaken the theorem.

A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of $\rho_r$ , sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.

Selected references

D. Applegate, O. Hinder, H. Lu, M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Math. Program. (2022); arXiv:2105.12715v4. https://arxiv.org/abs/2105.12715 · https://doi.org/10.1007/s10107-022-01901-9
D. Applegate, M. Díaz, O. Hinder, H. Lu, M. Lubin, B. O'Donoghue, W. Schudy, Practical Large-Scale Linear Programming using Primal-Dual Hybrid Gradient, NeurIPS 2021. https://arxiv.org/abs/2106.04756
A. Chambolle, T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, J. Math. Imaging Vision 40 (2011). https://doi.org/10.1007/s10851-010-0251-1
A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15 (2004). https://doi.org/10.1137/S1052623403425629

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs III: Under a Consistent Allocation Rule, (α, β)-Balanced Prices Are Closed Under Maxima of ValuationsResearch Paper

Motivation

Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020

One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B

Setting

There are $n$ agents in a fixed order. Agent $i$ receives an outcome $x_i$ from a space $X_i$ containing a null outcome. A profile $x=(x_i)_i$ is feasible when it lies in $\mathcal F$ . The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents $S$ , write $x_S$ for the profile retaining $x_i$ on $S$ and assigning the null outcome elsewhere. The prefix $x_{[i-1]}$ retains only the agents before $i$ . Dütting et al., 2020, §2

A valuation profile $v$ assigns each agent a function $v_i:X_i\to\mathbb R$ . The welfare of $x$ is $v(x)=\sum_i v_i(x_i)$ . Every base valuation takes values in $[0,1]$ , the normalization stated in §2. For any set $S$ of profiles, $v(\operatorname{OPT}(v,S))$ denotes the best welfare achievable in $S$ . An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price $p_i(x_i\mid y)$ to outcome $x_i$ when the partial profile is $y$ ; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548

An exchange-compatible family $(\mathcal F_x)_{x\in X}$ specifies a set of comparison profiles for each profile $x$ . It is exchange compatible when replacing any one coordinate of $x$ by the corresponding coordinate of any $y\in\mathcal F_x$ gives a feasible profile. This property is required for every $x$ in the full outcome space. A rule $p^v$ is $(\alpha,\beta)$ -balanced for valuation $v$ , ALG, and that family, for constants $\alpha>0$ and $\beta\ge0$ (Definition 3.1), when both inequalities hold for every feasible $x$ and every $x'\in\mathcal F_x$ :

\frac{v(\operatorname{ALG}(v))-v(\operatorname{OPT}(v,\mathcal F_x))}{\alpha} \le \sum_i p_i^v(x_i\mid x_{[i-1]}), \qquad \sum_i p_i^v(x'_i\mid x_{[i-1]}) \le \beta v(\operatorname{OPT}(v,\mathcal F_x)).

The maximum extension $V_i^{\max}$ of a base valuation space $V_i$ consists of nonempty finite pointwise maxima of elements of $V_i$ . A base profile $\tilde v$ supports an extended profile $v$ at $x$ if $\tilde v_i\le v_i$ at every outcome and $\tilde v_i(x_i)=v_i(x_i)$ for every agent. ALG is consistent when $\tilde v(\operatorname{ALG}(\tilde v))\ge\tilde v(\operatorname{ALG}(v))$ whenever $\tilde v$ supports $v$ at $\operatorname{ALG}(v)$ . The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554

Formalization targets

Closure under maxima

The goal is Theorem 5.3. Given one exchange-compatible family and a collection $(p^w)_{w\in V}$ balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:

v\in V^{\max},\quad \tilde v\in V\text{ supports }v\text{ at }\operatorname{ALG}(v) \quad\Longrightarrow\quad p^{\tilde v}\text{ is }(\alpha,\beta)\text{-balanced for }v.

The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family $\mathcal F_x$ remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof

Closure under addition and weak balancedness

Theorem 5.4 treats $m$ separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same $\alpha$ and $\beta$ . Appendix B changes the second balancedness bound to $\beta_1v(\operatorname{OPT}(v,\mathcal F_x))+\beta_2v(\operatorname{ALG}(v))$ and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve $\alpha,\beta_1,\beta_2$ under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3

Significance

The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555

These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.

Difficulty

For maximum closure, the prices are indexed by a base profile $\tilde v$ but must be balanced for a different profile $v$ that is pointwise larger. A supporting profile agrees with $v$ only at ALG's outcome $\operatorname{ALG}(v)$ , while condition (a) refers to $\operatorname{ALG}(\tilde v)$ , an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over $\mathcal F_x$ , where $\tilde v$ and $v$ can differ. Balancedness of $p^{\tilde v}$ for $\tilde v$ therefore says nothing about $v$ on its own; without a hypothesis tying ALG's choices for $v$ and $\tilde v$ together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the $[0,1]$ normalization of §2 is carried through to $V^{\max}$ . Dütting et al., 2020, Definition 5.1 and Theorem 5.3

For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4

Formalization scope

Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to $\mathbb R$ with base values in $[0,1]$ . The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so $+\infty$ is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.

The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on $V^{\max}$ , which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over $\mathcal F$ on every profile in $V^{\max}$ , the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off $\mathcal F$ ). Their ALG feasibility premise concerns the component profiles supplied in the theorem.

The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to $\tilde v=v$ would lose the intended maximum extension and does not satisfy the goal's universal quantification.

Selected references

P. Dütting, M. Feldman, T. Kesselheim, and B. Lucier, Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs, SIAM Journal on Computing 49(3):540–582, 2020. DOI: 10.1137/20M1323850.

7 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Partially Observable Total-Cost Markov Decision Processes with Weakly Continuous Transition Probabilities 2: Setwise-Continuous Observations Do Not Make the Belief Transition Weakly ContinuousResearch Paper

Motivation

A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.

Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.

Setting

The hidden state space is $X=\{1,2\}$ and the observation space is $Y=[0,1]$ with Lebesgue probability measure $m$ . The action space is $A=\{0\}\cup\{1/n:n=1,2,\ldots\}$ , equipped with the topology inherited from $\mathbb R$ . The state does not move: its transition law $P(\cdot\mid x,a)$ is the point mass at $x$ for every action. Its continuity in total variation is immediate from this fixed-state behavior.

At hidden state 1 the observation law is always $m$ . At hidden state 2, action zero also produces $m$ . Under action $1/n$ , state 2 produces a law $m^{(n)}=f^{(n)}m$ . The density $f^{(n)}$ equals zero on the open left half of each cell in the $2^n$ -part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as $n$ grows, and the paper establishes $m^{(n)}(C)\to m(C)$ for every fixed Borel set $C$ . Thus the observation kernel $Q(\cdot\mid a,x)$ is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.

A belief $z\in\mathcal P(X)$ assigns a probability to each hidden state. For a current belief $z$ and an action $a$ , the joint law $R(\cdot\mid z,a)$ covers the next state and its observation, and $R'(\cdot\mid z,a)$ is the observation marginal. A filter $H(z,a,y)$ is a conditional law of the next state given observation $y$ : it satisfies the disintegration identity (3.3). The belief transition $q_H(\cdot\mid z,a)$ is the law of the random posterior $H(z,a,y)$ when $y$ has law $R'(\cdot\mid z,a)$ . These objects are defined in (3.1)–(3.5) of the paper. Different versions of $H$ agree only almost everywhere for each current belief and action, yet they yield the same belief transition.

Formalization targets

Example 4.1: failure of weak belief continuity

At the uniform belief $z=(1/2,1/2)$ , action zero reveals nothing, while every positive-index action produces the same two-point posterior law:

q_H(\cdot\mid z,0)=\delta_z,\qquad q_H(\cdot\mid z,1/n)=\tfrac34\delta_{(1/3,2/3)}+\tfrac14\delta_{(1,0)} \quad(n\ge1).

The mission's goal asserts that $P$ is total-variation continuous, $Q$ is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as $1/n\to0$ . It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of $Q$ , the two posterior values almost everywhere, and the explicit laws of $q_H$ .

Significance

The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.

A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.

Difficulty

Setwise continuity controls $Q(C\mid a,x)$ for each fixed Borel set $C$ . A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with $n$ , so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of $Q$ to weak convergence of $q_H$ .

The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every $y$ would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of $H$ .

Formalization scope

Lean represents $X$ by Fin 2, with 0 for the paper's state 1 and 1 for state 2; $Y$ by unitInterval; and $A$ by the specified subtype of $\mathbb R$ . Positive integers are a subtype of $\mathbb N$ , so the density and the action $1/n$ are never evaluated at $n=0$ . The measure $m$ is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition $P$ and observation law $Q$ use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete $Q$ and existence of a valid $H$ , guarding the universal filter clause against vacuity.

Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of $q_H$ carries the Borel σ-algebra of the weak topology on $\mathcal P(X)$ , stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in $y$ for fixed $(z,a)$ in both structures. Joint measurability in $(z,a,y)$ is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.

No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on $A$ , or a claim for only one version of $H$ would change the counterexample and is excluded by the definitions and goal.

Selected references

E. A. Feinberg, P. O. Kasyanov, and M. Z. Zgurovsky, Partially Observable Total-Cost Markov Decision Processes with Weakly Continuous Transition Probabilities, Mathematics of Operations Research 41(2), 2016; arXiv:1401.2168v2. This mission follows the pinned preprint's numbering and pages.

6 thms2 active usersReviewed

Machine Learning Optimal Transport Probability+1·Captain: mikedeng1

Wasserstein Distributionally Robust Optimization and Variation Regularization III: With Probability 1 − e^(−t), E_Pn[(ρ − d(z, D_f))₊] ≤ Cρ² + 2ρ·E[Rademacher] + ρ√(t/2n) for Every fResearch Paper

Motivation

Wasserstein distributionally robust optimization (DRO) replaces the empirical risk $\mathbb E_{P_n}[f]$ of a loss $f$ by its worst case over all distributions within Wasserstein distance $\rho$ of the empirical law $P_n$ . Gao, Chen and Kleywegt (arXiv:1712.06050; Operations Research, 2024, doi:10.1287/opre.2022.2383) show that, for small radii, this worst-case risk is the empirical risk plus $\rho$ times a variation of the loss (a norm of its gradient or local slope), up to a remainder. This links DRO to gradient-norm regularization, as used in adversarial training and in data-driven newsvendor and pricing models.

For smooth losses the remainder is of order $\rho^2$ . Many losses used in practice are only piecewise smooth: hinge, ReLU networks, newsvendor costs, $\theta z \wedge 1$ . Near the set $\mathcal D_f$ where the pieces meet, the first-order expansion fails, and the paper's Theorem 1(I)–(II) carries an extra boundary term $M\,\mathbb E_{P_n}[(\rho - d(z,\mathcal D_f))_+]$ . Theorem 1(III) shows that this term is small with high probability, uniformly over the loss class, provided the data distribution does not concentrate near the non-smooth points. This mission formalizes that probabilistic bound.

Setting

Let $(\mathcal Z, d)$ be a metric space with its Borel $\sigma$ -algebra, $P_{\rm true}$ a probability measure on $\mathcal Z$ , and $z_1, \dots, z_n$ an i.i.d. sample from $P_{\rm true}$ , with empirical law $P_n = \frac1n\sum_i \delta_{z_i}$ . The sampling law is the product $P_\otimes = P_{\rm true}^{\otimes n}$ on $\mathcal Z^n$ , and $\mathbb E_\otimes$ is its expectation. The formal statements also assume the metric space is second countable.

Let $\mathcal F$ be a set of losses $f : \mathcal Z \to \mathbb R$ , and for each $f$ let $\mathcal D_f \subseteq \mathcal Z$ be its non-smooth set: for a piecewise smooth $f$ with pieces $\mathcal Z_{f,1}, \dots, \mathcal Z_{f,K_f}$ , the union of the pairwise intersections of their closures (Assumption 1). The paper assumes $\mathcal D_f$ is $P_{\rm true}$ -null. The distance to a set is $d(z, D) = \inf_{\tilde z\in D} d(z,\tilde z)$ , with $d(z,\varnothing) = +\infty$ .

The objects of the mission are:

the boundary gap $(\rho - d(z, \mathcal D_f))_+$ and the near indicator $\mathbf 1\{d(z,\mathcal D_f) < \rho\}$ ;
the indicator class $\mathcal I_\rho = \{z\mapsto \mathbf 1\{d(z,\mathcal D_f)<\rho\} : f\in\mathcal F,\ \mathcal D_f\neq\varnothing\}$ ;
the empirical Rademacher complexity $\mathfrak R_n(\mathcal H) = \mathbb E_\sigma\bigl[\sup_{h\in\mathcal H}\frac1n\sum_i\sigma_i h(z_i)\bigr]$ of a class $\mathcal H$ , with i.i.d. uniform signs $\sigma_i$ , and the Rademacher complexity $\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$ ;
Assumption 3 (bounded density):

\limsup_{\delta\downarrow 0}\ \sup_{f\in\mathcal F:\,\mathcal D_f\ne\varnothing}\frac{P_{\rm true}\{z : 0 < d(z,\mathcal D_f) < \delta\}}{\delta} < \infty.

In Lean the boundary gap is the shared WassVarReg.PInf.boundaryGap; nearIndicator, indicatorClass, empRademacher, rademacher and Assumption3 are in WassVarReg.Boundary. The sample law is the published MinimaxWass.DataDep.sampleLaw.

Formalization targets

Goal: Theorem 1(III), first display (p. 8)

Under Assumption 3 there exist $\bar\rho, C > 0$ such that for all $n\ge1$ , $t>0$ and $0\le\rho<\bar\rho$ , with probability at least $1-e^{-t}$ , for every $f\in\mathcal F$ ,

\mathbb E_{P_n}\bigl[(\rho - d(z,\mathcal D_f))_+\bigr] \le C\rho^2 + 2\rho\,\mathbb E_\otimes[\mathfrak R_n(\mathcal I_\rho)] + \rho\sqrt{\frac{t}{2n}}.

The constants $C$ and $\bar\rho$ are left unspecified; they depend only on Assumption 3.

Milestones

Lemma EC.5 (p. ec4): for a class $\mathcal H$ of measurable functions with values in $[0,M]$ , with probability at least $1-e^{-t}$ , $\mathbb E_{P_n}[h] \le \mathbb E_{P_{\rm true}}[h] + 2\,\mathbb E_\otimes[\mathfrak R_n(\mathcal H)] + M\sqrt{t/(2n)}$ for all $h\in\mathcal H$ .
Assumption 3 bounds the true mass (proof of Lemma EC.11, p. ec11): $\mathbb E_{P_{\rm true}}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}] \le C\rho$ for $0\le\rho<\bar\rho$ , uniformly in $f$ .
Lemma EC.11 (p. ec11): with probability at least $1-e^{-t}$ , for every $f$ , $\mathbb E_{P_n}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}] \le C\rho + 2\,\mathbb E_\otimes[\mathfrak R_n(\mathcal I_\rho)] + \sqrt{t/(2n)}$ .
Gap versus mass (p. ec11): $\mathbb E_{P_n}[(\rho-d(z,\mathcal D_f))_+] \le \rho\,\mathbb E_{P_n}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}]$ .

Significance

The result. With $\rho_n = \rho_0/\sqrt n$ and a class $\mathcal I_\rho$ of bounded complexity, the right side of the goal is $O_p(1/n)$ . Combined with Theorem 1(I)–(II), it gives the paper's conclusion that $p$ -Wasserstein DRO with $p\in(1,\infty]$ is asymptotically equivalent to empirical variation regularization, $\min_f\{\mathbb E_{P_n}[f] + \rho_n\mathcal V_{P_n,q}(f)\} + O_p(1/n)$ , for non-smooth losses, uniformly over the class. Without it, the boundary term is only bounded by $M\rho$ , and the expansion has no better accuracy than first order. Assumption 3 is the condition under which the non-smooth set does not matter statistically.

Formalizing it. The result is proved in the paper; it has no machine-checked proof. Its proof composes a uniform deviation bound (McDiarmid's inequality plus symmetrization) with a bounded-density estimate. The mission produces a general Rademacher deviation bound for bounded classes on an arbitrary metric space with a measurability guard, reusable by any statistical-learning mission, and fixes the printed constant of Lemma EC.5 ( $M\sqrt{2t/n}$ on the page, $M\sqrt{t/(2n)}$ from its proof).

Difficulty

The deterministic parts are short. The difficulty is in Lemma EC.5. McDiarmid's inequality must be applied to the uniform deviation over an arbitrary, possibly uncountable, class. Symmetrization must then be carried out with Bochner integrals over $\mathcal Z^n\times\mathcal Z^n$ and a finite sign space. Neither tool is in Mathlib in this form. A tempting shortcut, bounding each fixed $h$ by Hoeffding's inequality and taking a union bound, fails: the class is infinite, and the bound must hold simultaneously for all $f$ inside a single event. A second point is Assumption 3: it controls only the shell $0 < d(z,\mathcal D_f) < \delta$ , so the mass of $\{d = 0\}$ has to come from the null closure of $\mathcal D_f$ .

Formalization scope

Space and sample. $\mathcal Z$ is a metric space with [MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z] in the goal-level statements. Second countability is an added technical hypothesis used throughout this paper's mission series. A sample is ω : Fin n → Z with $n\ge1$ , and its law is Measure.pi. Empirical means are $\frac1n\sum_{i : \mathrm{Fin}\,n}$ .
Distance to a set. Metric.infEDist, which is $+\infty$ on $\varnothing$ . A loss with $\mathcal D_f=\varnothing$ thus has boundary gap $0$ and is excluded from $\mathcal I_\rho$ , as on the page. The real-valued Metric.infDist (which is $0$ on $\varnothing$ ) would give such a loss gap $\rho$ and is not used.
The non-smooth sets are an arbitrary family D : (Z → ℝ) → Set Z. The goal-level statements assume each $\mathcal D_f$ is closed and $P_{\rm true}$ -null, the standing consequence of its construction in Assumption 1. The details of the piecewise smooth loss model are not needed for this probability estimate.
Probabilities are written as $P_\otimes\{\omega : \neg\,\forall f\in\mathcal F, \dots\}\le e^{-t}$ , with the quantifier over $\mathcal F$ inside the event (an outer measure for uncountable $\mathcal F$ ).
Rademacher complexity. The sign expectation is an average over $\{\pm1\}^n$ . Suprema are real suprema of classes with values in $[0,M]$ ; an empty class gives $0$ . $\mathbb E_\otimes$ is a Bochner integral.
Measurability guard (added): the uniform deviation, the empirical Rademacher complexity and the double-sample deviation of the class are measurable. This holds, for instance, for countable $\mathcal F$ , and the paper leaves it implicit.
Quantifier order. $\bar\rho$ and $C$ are chosen before $n$ and $t$ , which is stronger than the page's order. The radius satisfies $\rho\ge0$ .
Not stated. The second display of Theorem 1(III) and the "Moreover" part of Lemma EC.11, which use Dudley's entropy integral: their proof bounds the empirical Rademacher complexity, while Lemma EC.5 needs its expectation.
Trivialization ruled out. The Rademacher term is that of the specific class $\mathcal I_\rho$ built from the sets $\mathcal D_f$ . It is not a free constant, and no hypothesis assumes the conclusion of Lemma EC.5.

Contributions welcome: a general McDiarmid inequality for product measures, a symmetrization lemma for measurable classes, and proofs of the milestones in any order.

Selected references

R. Gao, X. Chen, A. J. Kleywegt, Wasserstein Distributionally Robust Optimization and Variation Regularization, Operations Research, 2024. arXiv:1712.06050, doi:10.1287/opre.2022.2383
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Theorem 26.5. doi:10.1017/CBO9781107298019
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141, 1989. doi:10.1017/CBO9781107359949.008
M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Ch. 5. doi:10.1017/9781108627771

8 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes 1: In the Well-Separated Case, Algorithm-I with m Price Changes Has Regret at Most KT^(1/(m+1))Research Paper

Motivation

Retailers set prices and stock levels without knowing how demand responds to price. They must learn the demand curve from their own sales while still earning money, which is the exploration–exploitation trade-off of dynamic pricing with learning (den Boer 2015). Two features of practice make the problem harder than the textbook bandit. First, demand is censored: when the shelf runs empty, the firm sees only its sales $\min\{d_t,y_t\}$ , not the demand $d_t$ . Second, firms change prices rarely, because of menu costs and customer reaction, so a policy may change its price at most $m$ times over the whole horizon (Cheung, Simchi-Levi and Wang 2017).

Chen, Chao and Wang study a firm facing both features at once, in a parametric model where the demand distribution is known up to a parameter. For the well-separated case they give an algorithm, Algorithm-I, whose regret grows as $T^{1/(m+1)}$ , and they show that no admissible policy does better in general. This mission formalizes the upper bound. A companion mission formalizes the lower bound.

Setting

A firm sells one product over periods $t=1,\dots,T$ . At the start of period $t$ it holds inventory $x_t$ (with $x_1=0$ ). It chooses a price $p_t\in\mathcal P=[p^l,p^h]$ and an order-up-to level $y_t\in\mathcal Y=\{y^l,\dots,y^h\}$ with $y_t\ge x_t$ , and the order arrives at once. Demand $d_t$ then has probability mass function $f(\cdot;p_t,z)$ on $\{d^l,d^l+1,\dots,d^h\}$ , where $d^h\le+\infty$ and the parameter $z$ lies in $\mathcal Z=[z^l,z^h]$ , $0\le z^l\le z^h$ . Unmet demand is lost, and the firm observes only the sales $\min\{d_t,y_t\}$ . Leftover stock carries over, $x_{t+1}=(y_t-d_t)^+$ . Each unit left over costs $h\ge0$ and each lost sale costs $b\ge0$ . The single-period expected profit is

G(p,y,z)=p\,\mathbb E[D(p,z)]-h\,\mathbb E[y-D(p,z)]^+-(b+p)\,\mathbb E[D(p,z)-y]^+ .

For each $y$ , $p^*_y(z)$ is an optimal price, $\max_{p\in\mathcal P}G(p,y,z)=G(p^*_y(z),y,z)$ , and the clairvoyant value is $G^*(z)=\max_{(p,y)\in\mathcal P\times\mathcal Y}G(p,y,z)$ .

A policy's decision in period $t$ may depend only on past decisions and past sales. The regret of a policy is

R(T)=T\,G^*(z)-\mathbb E[V^\phi(T,z)]=\sum_{t=1}^T\mathbb E\big[G^*(z)-G(p_t,y_t,z)\big].

The family is well-separated (Definition 1) if for every price the pmfs $f(\cdot;p,z)$ , $z\in\mathcal Z$ , are pairwise distinct.

Algorithm-I splits the horizon into $m+1$ stages of lengths $I_i=\lceil T^{i/(m+1)}\rceil$ for $i\le m$ , with $I_{m+1}=T-\sum_{i\le m}I_i$ . Stage $i$ uses one price $\hat p_i$ and the order-up-to target $\tilde y_i$ . The target equals the planned level $\hat y_i$ , raised by $\Delta\ge1$ when $\hat y_i=d^l$ so that the sales carry information. At the end of the stage the algorithm computes the censored-data maximum-likelihood estimate $\hat z_i$ (5). It then sets the next stage's decisions to a maximizer of $G(\cdot,\cdot,\hat z_i)$ (6). It changes its price at most $m$ times.

Formalization targets

Goal: Theorem 1

Under Assumption A (regularity of $G$ and of $p^*_y$ near the true $z$ ), Assumption 1 (Fisher-information bounds, a positive lower bound on the pmf, strict monotonicity of $f(d^l;p,\cdot)$ ), Definition 1, and the condition that every optimal order-up-to level exceeds $d^l$ , there is $K_6>0$ such that for all large $T$

R(T)\le K_6\,T^{\frac1{m+1}} .

The constant may depend on the model, the true parameter and the algorithm's inputs. The rate $T^{1/(m+1)}$ is the content.

Milestones

Theorem B1: if an estimator satisfies $\mathbb P\{\|\hat z-z\|\ge\epsilon\}\le K_{14}e^{-nK_{15}\epsilon^2}+K_{16}/n$ , then the plug-in decision has optimality gap $G^*(z)-\mathbb E[G(\hat p^*,\hat y^*,z)]\le K_{17}/n$ .
Proposition 1: the censored MLE satisfies $\mathbb P\{|z-\hat z_i|\ge\epsilon\}\le K_3e^{-K_4I_i\epsilon^2}+K_5/I_i$ .
Per-stage estimation regret (p. 25): $\mathbb E[G^*(z)-G(\hat p_i,\hat y_i,z)]\le K_{17}/I_{i-1}$ .
(25): the summed estimation regret is at most a constant times $mT^{1/(m+1)}$ .
(26): $\mathbb P(\hat y_i\ne\tilde y_i)\le K/I_{i-1}$ , so exploration after stage 1 is rare.

Significance

The upper bound shows that a budget of $m$ price changes costs only a $T^{1/(m+1)}$ regret even under censoring. With $m$ of order $\log T$ the rate drops to logarithmic (Theorem 3 of the paper). Together with the matching lower bound (Theorem 2), it identifies the exact price of limiting price changes in this model. Theorem B1 is a general transfer principle, from a large-deviation bound on an estimate to a $1/n$ optimality gap of the plug-in decision. It allows continuous and discrete decisions together and needs no unique optimizer. It is reusable for any parametric learning problem with that structure. Proposition 1 is a large-deviation bound for maximum likelihood from censored, dependent, non-identically distributed data. The paper notes that such results were not previously available in the statistics literature.

The results are proved in the paper's appendices. None of them has a machine-checked proof. A formalization would check the regret decomposition (23), the stagewise bookkeeping with ceilings, and the large-deviation argument for the censored MLE. It would also make the reading of several loosely stated steps exact (see Formalization scope).

Difficulty

The obvious argument plugs a consistent estimator into the optimizer and bounds the regret by the estimation error. It fails twice. The error of $\hat z_i$ is of order $I_{i-1}^{-1/2}$ , so a Lipschitz bound on the profit would give regret of order $I_i/\sqrt{I_{i-1}}$ per stage, which is too large. The $1/n$ rate of Theorem B1 needs the first-order condition at an interior optimum and the exact gap $\delta$ between optimal and suboptimal discrete levels. Second, the data are censored and dependent. The censoring level $y_t$ depends on carried inventory, which depends on past demand and on past prices. The classical large-deviation results for maximum likelihood assume i.i.d. uncensored samples (Borovkov 1998) and do not apply. Proposition 1 needs a separate argument that the inventory target is reached in most periods with high probability.

Formalization scope

The model is encoded with a scalar parameter. $\mathcal P$ , $\mathcal Y$ and $\mathcal Z$ are as above. The pmf is positive exactly on $\{d^l,\dots,d^h\}$ and sums to one, and $d^h=+\infty$ is allowed. The expected profit $G$ is built from these sums. $G^*(z)$ is the finite maximum $\max_{y}G(p^*_y(z),y,z)$ for a price selection $p^*$ , not a real supremum. Periods are 0-based in Lean, while stages keep the paper's indices. Expectations and probabilities are sums over demand paths $d\in\mathbb N^T$ weighted by $\prod_tf(d_t;p_t,z)$ , the law of the path under the algorithm, taken in $[0,\infty]$ . Every regret summand is nonnegative.

Algorithm-I reads demand only through sales. Step 2's arg max is any maximizer of the censored product likelihood, which exists by compactness. Step 3's arg max is $\hat y$ , any maximizer of $y\mapsto G(p^*_y(\hat z),y,\hat z)$ , together with the price $p^*_{\hat y}(\hat z)$ of Assumption A(iii). This is the decision the proof of Theorem B1 analyses. Proposition 1's "large enough $i$ " is read as "large enough $T$ , uniformly in the stage and in $\epsilon$ ". Theorem B1 is stated for a scalar price and level and a parameter in $\mathbb R^k$ .

Three hypotheses are added and disclosed. Differentiability of $f$ in $z$ is presupposed by Assumption 1. Finiteness of the mean demand is needed for (4) when $d^h=\infty$ . The condition $d^l\le y^l$ is needed because Step 1 defines the target only for $\hat y\ge d^l$ . "The optimal order-up-to level exceeds $d^l$ " is read for every optimal level.

A trivializing formalization is ruled out. Regret and probabilities are path sums of nonnegative terms, not Bochner integrals that vanish on non-integrable inputs. $T^{1/(m+1)}$ is a real power. The hypotheses are jointly satisfiable: a Bernoulli instance with $\mathcal Y=\{1\}$ , $\mathcal P=[1,2]$ , $\mathcal Z=[2/3,4/5]$ , $f(0;p,z)=zp/2$ satisfies all of them, together with explicit selections, and this has been verified in Lean.

A complete development needs the following:

Hoeffding-type concentration for dependent bounded sums;
a large-deviation bound for the censored log-likelihood;
Taylor's theorem with integral remainder on an interval;
bookkeeping lemmas for the stage lengths $\lceil T^{i/(m+1)}\rceil$ .

Theorem B1 and the model definitions are reusable for the paper's later results (Theorems 3, 5, 6), which repeat these arguments. Contributions to any milestone are welcome, including alternative proofs of Proposition 1.

Selected references

B. Chen, X. Chao, Y. Wang, Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, Operations Research (technical note), 2020; read in the SSRN revision of 2020-02-10. https://doi.org/10.1287/opre.2020.1993, https://ssrn.com/abstract=2700747
W. C. Cheung, D. Simchi-Levi, H. Wang, Dynamic Pricing and Demand Learning with Limited Price Experimentation, Operations Research 65(6), 2017. https://doi.org/10.1287/opre.2017.1629
J. Broder, P. Rusmevichientong, Dynamic Pricing under a General Parametric Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1057
A. A. Borovkov, Mathematical Statistics, Gordon and Breach, 1998.
A. V. den Boer, Dynamic pricing and learning: Historical origins, current research, and new directions, Surveys in Operations Research and Management Science 20(1), 2015. https://doi.org/10.1016/j.sorms.2015.03.001

10 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness I: The LP Saddle-Point Problem Is 1/(H(K)√(1+4R²))-Sharp on Every Ball W_R(0)Research Paper

Motivation

First-order primal-dual methods (PDHG, extragradient, ADMM) are the engine of a new generation of large-scale linear programming solvers, such as PDLP, because they need only matrix–vector products with the constraint matrix. Their textbook guarantees for convex–concave saddle-point problems are sublinear, $O(1/t)$ for the averaged iterate, while in practice restarted variants converge linearly on linear programs. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715v4, Math. Program. 2022) explain this gap through a sharpness condition on the normalized duality gap, and show that restarts turn sharpness into linear convergence.

This mission formalizes the part of that paper which shows that linear programming is sharp: Lemma 5 (p. 15), together with the bound of the KKT residual by the normalized duality gap (Lemma 4, p. 14) and the bilinear results of §3.2. The restart theorems that consume this property are the subject of the companion missions II and III of this series.

Setting

Let $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ . The standard-form LP and its dual are

\min_{x\in\mathbb R^n} c^\top x\ \text{ s.t. } Ax=b,\ x\ge0 \qquad (17), \qquad\quad \max_{y\in\mathbb R^m} b^\top y\ \text{ s.t. } A^\top y\le c \qquad (18),

and their Lagrangian form is the saddle-point problem

\min_{x\ge0}\ \max_{y\in\mathbb R^m}\ L(x,y)=c^\top x+y^\top b-y^\top Ax. \qquad (19)

A primal-dual point is $z=(x,y)$ , the feasible region is $Z=\{x\ge0\}\times\mathbb R^m$ , and $Z^\star$ is the set of saddle points of $L$ on $Z$ . On $\mathbb R^{n+m}$ the norm is the Euclidean norm $\|(x,y)\|=\sqrt{\|x\|_2^2+\|y\|_2^2}$ , and $\operatorname{dist}(z,Z^\star)=\inf_{\hat z\in Z^\star}\|z-\hat z\|$ .

For $r>0$ let $W_r(z)=\{\hat z\in Z:\|z-\hat z\|\le r\}$ . The normalized duality gap (4a) is

\rho_r(z)=\sup_{\hat z\in W_r(z)}\frac{L(x,\hat y)-L(\hat x,y)}{r}.

The problem is $\alpha$ -sharp on a set $S\subseteq Z$ (Definition 1) if $\alpha\,\operatorname{dist}(z,Z^\star)\le\rho_r(z)$ for all $z\in S$ and all $r\in(0,\operatorname{diam}(S)]$ .

The KKT system (20) collects primal feasibility, dual feasibility and a nonpositive duality gap as $Kz\ge h$ , with

K=\begin{pmatrix} I & 0\\ -A & 0\\ A & 0\\ 0 & -A^\top\\ -c^\top & b^\top\end{pmatrix},\qquad h=\begin{pmatrix}0\\-b\\b\\-c\\0\end{pmatrix}.

The KKT residual $\|(h-Kz)^+\|$ is the Euclidean norm of the componentwise positive part, a standard stopping criterion of LP solvers. A Hoffman constant $H(K)$ (Hoffman 1952) is a constant with

\operatorname{dist}(z,Z^\star)\le H(K)\,\|(h-Kz)^+\|\quad\text{for all } z\in\mathbb R^{n+m}. \qquad (26)

Formalization targets

Goal: Lemma 5 (Sharpness of linear programming), p. 15

If (19) has a solution and $H(K)>0$ satisfies (26), then for every $R\in(0,\infty)$ the problem (19) is $\alpha$ -sharp on $W_R(0)=\{z\in Z:\|z\|\le R\}$ with

\alpha=\frac{1}{H(K)\sqrt{1+4R^2}}.

Milestones (proof of Lemma 4, p. 14)

With $v=\big((-c+A^\top y)^+,\ b-Ax\big)$ :

\text{(22)}\quad \rho_r(z)\ge\|v\|\quad (z\in Z,\ r>0),\qquad\qquad \text{(25)}\quad \rho_r(z)\ge\tfrac1R\,(c^\top x-b^\top y)^+\quad (z\in W_R(0),\ 0<r\le R),

and their combination, Lemma 4:

\|(h-Kz)^+\|\le\rho_r(z)\sqrt{1+R^2}\qquad (R>0,\ r\in(0,R],\ z\in W_R(0)).

Companion statements

§3.3, p. 13: if (17) and (18) are feasible, $Z^\star=\{z: Kz\ge h\}$ , so that (26) is Hoffman's bound for a polyhedron.
Lemma 2, p. 12: for $S=\{z:Hz=h\}\neq\emptyset$ , $\operatorname{dist}(S,z)\le\|Hz-h\|/\sigma^+_{\min}(H)$ .
Lemma 3, p. 12: the unconstrained bilinear problem $L(x,y)=c^\top x-y^\top Ax+b^\top y$ on $\mathbb R^{n+m}$ is $\sigma^+_{\min}(A)$ -sharp on all of $\mathbb R^{n+m}$ ; with the identities (14) and (15) from its proof.

Significance

Lemma 5 is the input that makes the paper's restart theorems apply to linear programming: combined with Theorems 1 and 2 (missions II and III), it yields linear convergence of restarted PDHG, extragradient and ADMM on any feasible LP, with a rate governed by the Hoffman constant of the KKT system. Lemma 4 is of independent use: it shows that the normalized duality gap, which restart schemes can monitor, controls the KKT residual that solvers report.

The results are proved in the paper. As far as the platform and Mathlib show, none of them is formalized: there is no normalized duality gap, no primal-dual sharpness and no Hoffman bound for KKT systems in Mathlib. The remaining work is to formalize the paper's proofs. Strong duality for standard-form LP, needed for the §3.3 companion, exists on the platform (Polyhedral.lp_strong_duality, LinearOptimization.lp_strong_duality) in a different form.

Difficulty

The sharpness inequality relates two quantities of different nature: $\operatorname{dist}(z,Z^\star)$ is a geometric distance to an implicitly defined polyhedron, while $\rho_r(z)$ is a supremum of a bilinear gap over a truncated ball $W_r(z)$ that is cut by the constraint $x\ge0$ . The unconstrained argument of Lemma 3, which identifies $\rho_r(z)$ with $\|F(z)\|$ , fails once $x\ge0$ is imposed, because the ball is no longer symmetric around $z$ and the maximizing direction may leave $Z$ . Control of the duality-gap row of the KKT system also depends on the size of $z$ , which is why the constant degrades with $R$ and sharpness is claimed only on bounded sets $W_R(0)$ . In Lean the normalized duality gap is an extended-real supremum over a set defined by a non-default norm, so each lower bound requires exhibiting a feasible point of $W_r(z)$ and computing its gap.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and a primal-dual point is a pair. The norm on pairs is the $L^2$ norm of WithLp 2, eucl. The norm instance of the bare product type is the sup norm and is not used: with the sup norm the constants $\sqrt{1+R^2}$ and $\sqrt{1+4R^2}$ would describe different statements. $\rho_r$ and $\operatorname{diam}$ are suprema in EReal. $\operatorname{dist}(z,Z^\star)$ is a real infimum, and every statement that uses it assumes $Z^\star\neq\emptyset$ ("(19) has a solution"). $Z^\star$ is defined as the set of saddle points of $L$ on $Z$ . $K$ and $h$ are encoded row block by row block exactly as (20) prints them; the page's " $A^\top y\ge c$ " in (18) is a misprint for $A^\top y\le c$ , which is what (20) encodes.

The Hoffman constant enters only through its defining property (26), quantified over all $z\in\mathbb R^{n+m}$ , together with $H(K)>0$ . Lemma 5 is stated for every such constant. Sharpness follows Definition 1 literally, with $r\in(0,\operatorname{diam}(W_R(0))]$ ; replacing that range by $(0,2R]$ would be a different statement. A formalization that restricts (26) to $z\in Z$ , uses the sup norm, or takes a real-valued supremum for $\rho_r$ would trivialize or change the goal and is ruled out. $\sigma^+_{\min}(H)$ is the least $\sigma>0$ with $\sigma^2$ an eigenvalue of $H^\top H$ ; its Lean value for $H=0$ is $0$ .

Contributions welcome: proofs of (22) and (25), whose combination gives Lemma 4 and then Lemma 5; general lemmas on suprema over Euclidean balls in WithLp 2 products; and a Hoffman-type existence theorem for $\{Kz\ge h\}$ , which this mission does not pose. The bilinear statements (Lemmas 2–3) need a minimum-nonzero-singular-value API and are reusable beyond this mission.

Selected references

D. Applegate, O. Hinder, H. Lu, M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Math. Program. (2022); cited from arXiv:2105.12715v4. https://arxiv.org/abs/2105.12715 · https://doi.org/10.1007/s10107-022-01901-9
A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Natl. Bur. Stand. 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
D. Applegate, M. Díaz, O. Hinder, H. Lu, M. Lubin, B. O'Donoghue, W. Schudy, Practical Large-Scale Linear Programming using Primal-Dual Hybrid Gradient, NeurIPS 2021. https://arxiv.org/abs/2106.04756
A. Chambolle, T. Pock, A first-order primal-dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40 (2011) 120–145. https://doi.org/10.1007/s10851-010-0251-1

7 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity 1: Under Known Sparsity, ILSX Pricing Has Regret at Most Cs√T log TResearch Paper

Motivation

A seller who changes prices while learning demand faces two costs: a price experiment may earn less revenue now, while insufficient experimentation leaves later prices poorly calibrated. Customer features make the balance harder because both willingness to buy and sensitivity to price may vary between customers. Ban and Keskin study this problem when the number of recorded features can be large relative to the selling horizon. Their known-support policy, ILSX, provides the upper bound formalized here Ban and Keskin, 2021, §§2 and 4.1.

The paper's result is a statement about learning a demand model while serving sequential customers, rather than about fitting that model after all observations are available. A price at period $t$ must use information then available, including the arriving customer's features but excluding that customer's demand shock. The seller therefore needs a policy whose expected revenue loss can be bounded uniformly over the unknown parameters in a specified model Ban and Keskin, 2021, pp. 5552–5556.

Setting

In each period $t=1,2,\ldots$ , a customer arrives with a feature vector $Z_t\in\mathbb R^d$ . The seller observes the augmented vector $X_t=[1;Z_t]$ , posts a price $p_t\in[\ell,u]$ with $0<\ell<u$ , and then observes demand. In the linear demand model, demand equals

D_t=\alpha\cdot X_t+(\beta\cdot X_t)p_t+\varepsilon_t.

The intercept and slope vectors $\alpha,\beta$ are unknown. The seller knows the sparsity structure $\mathcal S$ : outside this set of coordinate indices, both parameter vectors vanish. The compressed parameter $\theta_{\mathcal S}=(\alpha_{\mathcal S},\beta_{\mathcal S})$ lies in a compact coordinate rectangle $\Theta_{\mathcal S}$ , and $s=|\mathcal S|\ge1$ . The compressed customer vector is $X_{\mathcal S,t}=(X_{t,i})_{i\in\mathcal S}$ Ban and Keskin, 2021, pp. 5552–5555.

At price $p$ , expected single-period revenue is $r(p,\theta_{\mathcal S},x)=p[\alpha_{\mathcal S}\cdot x+(\beta_{\mathcal S}\cdot x)p]$ . The clairvoyant price is $\varphi(\theta_{\mathcal S},x)=-(\alpha_{\mathcal S}\cdot x)/(2\beta_{\mathcal S}\cdot x)$ when the slope is negative. The paper assumes this price is in $(\ell,u)$ throughout its model domain. Expected regret $\Delta^{\pi}_{\theta_{\mathcal S}}(T)$ is the expected sum, through period $T$ , of the clairvoyant revenue minus the revenue at the policy's price Ban and Keskin, 2021, (2)–(4), p. 5553–5554.

The ILSX policy charges one fixed experimental price $m_1$ at periods $1,4,9,\ldots$ and a distinct price $m_2$ at periods $2,5,10,\ldots$ . At every other period it estimates the compressed demand parameter by least squares using experimental observations, projects the estimate onto $\Theta_{\mathcal S}$ , and applies $\varphi$ to the projected estimate and the current customer vector. Both prices lie in $[\ell,u]$ Ban and Keskin, 2021, (7), (8), (12), pp. 5555–5556.

Formalization targets

The goal is Theorem 2: for the stated model and ILSX policy, a finite positive constant $C$ exists such that

\Delta^{\mathrm{ILSX}(m_1,m_2)}_{\theta_{\mathcal S}}(T)\le Cs\sqrt T\log T\qquad(\theta_{\mathcal S}\in\Theta_{\mathcal S},\ T\ge2).

The constant is chosen after the model, shock process, experimental prices, and estimator selection are fixed, but before the parameter and horizon. The theorem and Remark 5 are on pp. 5556–5557 of Ban and Keskin, 2021.

The milestones reproduce the paper's route into this claim: the experimental-period count following (7); the growth bound (15) for the price-variation statistic $J_t$ ; Lemma 1's minimum-eigenvalue probability bound for the experimental information matrix $\widetilde{\mathcal J}_{\mathcal S,t}$ ; and Lemma 2's high-probability bound for its noise-driven estimation error. The least-squares error identity (11) is included as a supporting item on invertible samples, not as a milestone. The constants and thresholds in these targets remain existential where the article leaves them existential Ban and Keskin, 2021, pp. 5555–5556.

Significance

The theorem gives a guarantee for a concrete pricing policy under feature-dependent price sensitivity. The bound grows with the horizon at order $\sqrt T\log T$ for a fixed known support, with an explicit factor $s$ in the published statement. It lets a seller compare the cost of this policy with the revenue of a seller who knew the demand coefficients before pricing. The paper presents its result as matching its lower-bound benchmark up to logarithmic factors, under the paper's respective hypotheses Ban and Keskin, 2021, Theorems 1–2, pp. 5554–5556.

The mathematical result was published in 2021. This mission seeks a machine-checked statement and proof of the known-support guarantee and its stated intermediate results. The checked Prove2Me prior-art catalog contains featureless dynamic-pricing results and separate least-squares results, but no matching formalization of ILSX. A completed development would add reusable definitions for a feature-dependent price regressor, experimental information matrix, nonanticipating estimator selection, and expected regret. The article places its proofs in an electronic companion, which is not included in the held source PDF; this mission does not reproduce those proofs as source material.

Difficulty

The policy learns from a sparse set of deliberately chosen periods, while its regret accumulates at every period. A pointwise least-squares identity alone does not control the regret: the information matrix can be singular at early periods, and the customer features and shocks are random. In particular, the printed inverse identity (11) says “for all $t\ge2$ ”, although at $t=2$ the matrix has rank at most two and cannot be invertible when $s\ge2$ . The formal statement therefore confines the inverse identity to invertible samples. Lemma 2's event also includes invertibility so a default inverse of a singular matrix cannot make its error bound automatic Ban and Keskin, 2021, (9)–(11), Lemma 2, p. 5556.

Formalization scope

Lean uses one-based periods and a support subtype of the augmented feature coordinates. Coordinate zero is the paper's intercept coordinate one. The parameter has coordinates $(j,i)$ for demand intercept or price slope $j\in\{0,1\}$ and support index $i\in\mathcal S$ . The regressor $[1;p]\otimes X_{\mathcal S,t}$ gives the information matrix in (10). Euclidean squared norms are explicit sums of squares, and the minimum-eigenvalue claim is the equivalent Rayleigh inequality. The parameter rectangle is nonempty, and its Euclidean projection is coordinatewise clamping.

The standing assumptions are $d\ge1$ , $s\ge1$ , $0<\ell<u$ , distinct experimental prices in $[\ell,u]$ , bounded i.i.d. features with mean zero and positive-definite covariance, and a fixed shock process with conditional mean zero, bounded conditional second moment, and finite conditional exponential moments near zero. The feature process is measurable and integrable. The model additionally states independence of the next customer's features from the past primitives, the reading of the paper's joint probability construction used here. The slope is negative and the clairvoyant price lies in $(\ell,u)$ for every allowed parameter and realized feature. These conditions ensure that the price formula represents a genuine revenue maximum. The phrase about continuous features having positive measure in the interior of their domains is omitted because the page does not specify the domains or a reference measure Ban and Keskin, 2021, §2, pp. 5552–5554.

The estimator is any measurable minimizer of the experimental least-squares objective for histories with at least two observations. Its type depends only on earlier observations; at nonexperimental periods the recorded pseudo-observations are ignored by the objective. The shock law is fixed while the parameter varies. Expected regret uses a nonnegative integral, and conditional second and exponential moments use nonnegative conditional expectations. The theorem binds $C$ before the parameter and horizon, while leaving support size fixed with the model. Consequently, the stronger uniformity in $s$ suggested by Remark 5 is outside this statement. These choices exclude vacuous integrals, unconstrained estimators, and accidental bounds from a singular matrix inverse. Work on the probability estimates, least-squares identity, and regret bound is welcome under these exact definitions.

Selected references

G.-Y. Ban and N. B. Keskin, Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity, Management Science 67(9):5549–5568, 2021. DOI: 10.1287/mnsc.2020.3680.

6 thms2 active usersReviewed

Bandit Algorithms Machine Learning Probability+1·Captain: mikedeng1

The Multi-Armed Bandit Problem with Covariates I: Successive Elimination Has Expected Regret at Most 392γ²(1 + n/T)(K/Δ)log(TΔ²/18γ²) + nΔ⁻ Under a Random HorizonResearch Paper

Motivation

In a multi-armed bandit, a decision maker repeatedly chooses an arm, observes a reward, and tries to learn which arm has the highest average reward while losing little reward during learning. A policy that requires the number of future pulls in advance cannot be used unchanged when stopping time is uncertain. Perchet and Rigollet study successive elimination (SE), which removes poorly performing arms from a shrinking active set and can run without knowing the realized horizon. Their Theorem 2.1 bounds its expected regret when the horizon is random and independent of rewards Perchet and Rigollet, 2013, Theorem 2.1.

The static-bandit theorem also supplies a concentration and elimination analysis used in the paper's broader study of bandits with covariates. This mission isolates that theorem and the intermediate estimates that make its quantitative constant explicit. The paper proves the result in §2, with a concentration lemma in the Appendix; the goal here is a machine-checked statement and, eventually, a machine-checked proof of that known result.

Setting

There are $K+1\ge2$ arms. For each arm $i$ , the reward stack $Y_{i,1},Y_{i,2},\ldots$ lists the rewards that successive pulls of that arm will reveal. Rewards lie in $[0,1]$ , are identically distributed along each arm, and have mean $f_i$ . The stacks are mutually independent. Arms are indexed so that $f_1\le\cdots\le f_{K+1}$ , and the last arm, denoted $*$ , is uniquely best. Its gap from arm $i$ is $\Delta_i=f_*-f_i$ . A gap is zero only for the best arm.

The policy works in rounds. At the start of round $\tau$ , a nonempty set $I_\tau$ is active. It pulls each arm in $I_\tau$ once, in increasing index order, and computes the mean $\bar Y_i(\tau)$ from that arm's first $\tau$ rewards. It retains an arm when its mean is within $\gamma U(\tau,T)$ of the largest active mean, where $T\ge1$ is an integer, $\gamma\ge1$ , and

\overline{\log}(x)=\max\{\log x,1\},\qquad U(\tau,T)=2\sqrt{\frac{2\overline{\log}(T/\tau)}{\tau}}.

Concatenating the rounds gives the pull sequence $\widehat\pi_1,\widehat\pi_2,\ldots$ . For a horizon $N$ , its regret is $R_N(\widehat\pi)=\sum_{t=1}^{N}\Delta_{\widehat\pi_t}$ . If $N$ is random, independent of the reward stacks, and has mean $n$ , the paper studies $\mathbb E R_N(\widehat\pi)$ . For a threshold $\Delta>0$ , let $\Delta^-$ be the largest arm gap strictly smaller than $\Delta$ , or zero if none exists.

Formalization targets

The goal is Theorem 2.1, for every positive threshold $\Delta$ :

\mathbb E R_N(\widehat\pi) \le 392\gamma^2\left(1+\frac nT\right) \frac K\Delta\, \overline{\log}\!\left(\frac{T\Delta^2}{18\gamma^2}\right) +n\Delta^-.

The $K$ in this formula counts suboptimal arms; there are $K+1$ arms in total. The paper writes $\Delta\ge0$ under a convention that division by zero is infinite. The real-valued Lean goal states the informative positive-threshold case.

The milestones include the Appendix's maximal Hoeffding–Azuma inequality and Lemma A.1, which controls all empirical averages up to a fixed time. In §2 they continue with the stopping-round estimate (2.2), the empirical-gap tail (2.5), the bound $\Phi_j(\tau)\le4\tau/T$ for a false elimination of the best arm, and the final comparison for $\phi(x)=\overline{\log}(a x^2)/x$ . Each has its own statement so that a proof of the goal can import the exact estimate it needs.

Significance

The bound separates the cost of learning arms with gaps above $\Delta$ from the remaining regret represented by $n\Delta^-$ . It applies when the policy uses a tuning value $T$ but the number of pulls actually made is the random variable $N$ . Thus it gives a quantitative guarantee without asking the algorithm to know its stopping time in advance. Its constants and dependence on $T$ , $n$ , $K$ , and $\gamma$ are explicit Perchet and Rigollet, 2013, §2.

The result is proved in the paper, while the Lean declarations in this proposal are open statements. Completing them would add a reusable formal account of elimination on a reward stack and of the Appendix's time-uniform concentration estimate. Mathlib and existing platform theorems contain related Hoeffding–Azuma tools, but this paper's peeling inequality, its particular stopping rule, and the random-horizon regret conclusion still require proofs in the stated model.

Difficulty

An ordinary concentration bound at one sample size does not control every round in which an arm could eliminate the best arm. Taking a naive union bound over all rounds loses the dependence on $T$ needed for the displayed regret constant. The Appendix instead states a maximal inequality and a bound that holds across a range of sample sizes. The regret calculation must then account for both kinds of error: removing the best arm and retaining a suboptimal arm for too long.

The stopping round depends on the gap through $U(\tau,T)$ , which itself contains $\overline{\log}(T/\tau)$ . Its upper bound, the event decomposition across ordered arms, and the final comparison of gap-dependent terms all retain the paper's exact constants. A proof that only establishes the asymptotic rate would not close this goal.

Formalization scope

Lean uses Fin (K+1) with zero-based indices, so its last element is the paper's arm $K+1$ . The published stochastic-bandit definition supplies the mutually independent reward stack and arm means. The [0,1] bound, sorted means, and unique best arm are explicit assumptions. A separate martingale-difference definition supplies the Appendix's adapted, integrable sequence, including centering of its first term; the page's one-line definition leaves that first-step condition unstated. The concentration milestones require a nondegenerate interval $a<b$ : the displayed maximal exponent divides by $(b-a)^2$ , and Lemma A.1 is false at $a=b=0$ for a zero sequence and $\delta<1$ .

The SE policy is a function of observed rewards in the stack. It uses the end-of-round test described in the text and proof of §2, with equality retained, since Policy 1's pseudocode tests at a different point in the round. The active set starts with all arms and remains nonempty; the total Lean pull function has a fallback value that is unreachable under the theorem's parameters. The policy never reads the unknown means. Empirical means and $U$ are used only at positive rounds.

The horizon is measurable and integrable, has mean $n$ , and is independent of the entire reward stack. Since regret is bounded by the horizon, its expectation is a genuine integral rather than the default value of a non-integrable Lean integral. The positive-threshold condition avoids Lean's zero-valued division at $\Delta=0$ . Finite maxima are taken over finite arm sets, and $\overline{\log}$ is kept distinct from the ordinary logarithm in the Appendix's bounds. The paper's printed $n$ in the logarithm of (2.7) and the final $\phi$ comparison is read as $T$ , consistently with (2.2) and Theorem 2.1. Contributions to the concentration lemmas, stopping-round analysis, elimination events, and final regret proof all fit this scope.

Selected references

V. Perchet and P. Rigollet, The multi-armed bandit problem with covariates, Annals of Statistics 41(2), 2013, 693–721. arXiv:1110.6084v3; DOI:10.1214/13-AOS1101.
S. Bubeck and N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721.

10 thms2 active usersReviewed

All missions

The Statistical Complexity of Interactive Decision Making III: E2D with Hellinger Confidence Sets Has Regret at Most Σ_t sup dec_γ(M_εt(M̄), M̄) + γ·Est_H(T,δ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1, (35) (in the form (137) of Theorem 4.1a)

Milestones (the steps of the proof in App. D.1)

Companion results

Significance

Difficulty

Formalization scope

Selected references

Potential Games Are Necessary to Ensure Pure Nash Equilibria in Cost Sharing Games 1: Every Game Has a Pure Nash Equilibrium Iff the Distribution Rules Are Generalized Weighted Shapley ValuesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

Information Sharing in Competing Supply Chains with Production Cost Reduction: Under Cournot Competition Both Chains Share Below k_N, Both or Neither Between k_N and k_S, and Neither Above k_SResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 7(a)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Approximation Bounds for Random Neural Networks and Reservoir Systems I: Random ReLU Networks with Sampled Inner Weights Approximate Fourier-Represented Functions on a Hilbert Space (Theorem 1)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (pp. 37–38)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Approximation Bounds for Random Neural Networks and Reservoir Systems III: Echo State Networks with Output Feedback and Random Weights Approximate Contracting Reservoirs (Theorem 4)Research Paper

Motivation

Setting

Formalization targets

Steps of the proof

Goal: Theorem 4

Significance

Difficulty

Formalization scope

Selected references

Cycle Lengths in Expanding Graphs 1: Every α-Expander on n Vertices Has a Cycle of Length in [ℓ, ℓ+O(1/α)] for Every Integer ℓ from O(1/α)·log n up to 2^(−O(log(1/α)/α))·nResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 3)

Milestones (§2, in the order the proof uses them)

Significance

Difficulty

Formalization scope

Selected references

Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space 1: SA[p ± 1] Is Recovered From the Sample at the Phrase Start Preceding SA[p] − 1Research Paper

Motivation

Setting

Formalization targets

Goal: the identity in the proof of Lemma 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Statistical Complexity of Interactive Decision Making II: Every Algorithm Has Expected Regret at Least (1/6)·dec_γ(M^∞_ε̄γ(M̄), M̄)·T, the Localized DEC Lower BoundResearch Paper

Why expected regret needs a lower bound

Models, algorithms and the coefficient

Formalization targets

Localized DEC lower bound

Supporting targets

What the result supplies