Machine Learning

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

The Power of Subsampling in Submodular Maximization: SampleGreedy is a (p+1)²/p-approximation for non-negative submodular maximization over p-extendible systemsResearch Paper

Motivation

Many selection problems in machine learning and operations research ask for a set of items that maximizes a utility with diminishing returns, subject to a combinatorial feasibility constraint: summarizing a collection of images or documents, placing sensors, recommending a diverse set of products, or choosing a set of edges that forms a matching. Diminishing returns is submodularity; the feasibility constraints in these examples (matroids, intersections of matroids, matchings, knapsack-type systems) are instances of $p$ -extendible systems, a class introduced by Mestre (ESA 2006). Many useful objectives, such as graph cuts and diversity-regularized utilities, are non-monotone: adding an item can lower the value.

The greedy algorithm has a long history for this problem class. Fisher, Nemhauser and Wolsey (1978, doi:10.1007/BFb0121195) showed that greedy gives a $(p+1)$ -approximation for monotone submodular objectives over $p$ -systems, a class that contains $p$ -extendible systems. For non-monotone objectives, the known greedy-based algorithms ran the greedy algorithm repeatedly. Gupta, Roth, Schoenebeck and Talwar (WINE 2010) obtained roughly $3p$ , Mirzasoleiman et al. (2016) roughly $2p$ , and Feldman, Harshaw and Karbasi (COLT 2017) $p + O(\sqrt p)$ , each with $\Omega(nkp)$ or $\Omega(nk\sqrt p)$ oracle queries. Harshaw, Kazemi, Feldman and Karbasi (arXiv:2104.02772; Mathematics of Operations Research, 2022) showed that a single random subsampling of the ground set, followed by one run of the plain greedy algorithm, gives a $(p+1)^2/p$ -approximation for non-negative submodular objectives with expected $O(n + nk/p)$ oracle calls. This mission formalizes that guarantee.

Setting

Let $\mathcal N$ be a finite ground set of size $n$ , with a fixed linear order $u_1 < \dots < u_n$ that is used only to break ties. A set function is a map $f : 2^{\mathcal N} \to \mathbb R$ . The marginal gain of $u$ at $S$ is $f(u \mid S) = f(S \cup \{u\}) - f(S)$ .

$f$ is submodular if $f(A \cup \{e\}) - f(A) \ge f(B \cup \{e\}) - f(B)$ whenever $A \subseteq B$ and $e \notin B$ ; monotone if $A \subseteq B$ implies $f(A) \le f(B)$ ; linear if the submodular inequality always holds with equality.
A predicate $\mathcal I$ on subsets is an independence system if $\emptyset \in \mathcal I$ and $\mathcal I$ is closed under taking subsets. It is $p$ -extendible if for all $A \subseteq B$ in $\mathcal I$ and every $e \notin A$ with $A \cup \{e\} \in \mathcal I$ there is $Y \subseteq B \setminus A$ with $|Y| \le p$ and $(B \setminus Y) \cup \{e\} \in \mathcal I$ .

The problem is $\max_{S \in \mathcal I} f(S)$ for non-negative submodular $f$ ; OPT denotes a maximizer.

SampleGreedy with sampling probability $q$ keeps each element independently with probability $q$ , giving a sample $\mathcal N'$ . It then starts from $S = \emptyset$ and repeatedly adds the element $u \in \mathcal N'$ of largest marginal gain among those with $S \cup \{u\} \in \mathcal I$ and $f(u \mid S) > 0$ , ties broken by the fixed order, until no such element is left. Its expected value is

\mathbb E_q[f(S)] = \sum_{\mathcal N' \subseteq \mathcal N} q^{|\mathcal N'|}(1-q)^{n-|\mathcal N'|}\, f\big(\mathrm{SampleGreedy}(\mathcal N')\big).

For the analysis the paper introduces Algorithm 2, which runs greedy over the whole ground set, flips a $q$ -coin for each chosen element, and maintains a set $O$ (initially OPT), removal sets $O_u$ , snapshots $S_u$ and indicators $X_u$ (" $u$ was considered") and $Y_u$ .

Formalization targets

Goal: Theorem 1 (p. 7)

For non-negative submodular $f$ , a $p$ -extendible system with $p \ge 1$ , and every $T \in \mathcal I$ : SampleGreedy's output is always independent, and $$f(T) \le \frac{(p+1)^2}{p},\mathbb E_{1/(p+1)}[f(S)], \qquad f(T) \le (p+1),\mathbb E_{1/(p+1)}[f(S)] \ \text{if $f$ is monotone},

f(T) \le p,\mathbb E_{1/p}[f(S)] \ \text{if $f$ is linear}.$$

Milestones

In attack order: Lemma 3 (p. 8, already Proved on the platform: a random set whose elements each appear with probability at most $q$ keeps a $(1-q)$ fraction of $g(\emptyset)$ in expectation); Lemma 4 (p. 10, SampleGreedy and Algorithm 2 have the same output law); Lemma 5 (p. 11, invariants of Algorithm 2); Lemma 6 (p. 12, $f(S) \ge f(S\cup \mathrm{OPT}) - \sum_u |O_u \setminus S|\, f(u\mid S_u)$ ); Lemma 7 (p. 13, inequality (5)); Lemma 8 (p. 14); the display of §4.1.1 (p. 14); Lemma 9 (p. 15, linear objectives); Lemma 10 (p. 16, inequality (7)).

Significance

The result shows that one random subsample plus one greedy pass beats the repeated-greedy algorithms for non-monotone objectives over $p$ -extendible systems, both in ratio and in query count, and matches the classical $p+1$ for monotone objectives. Since no polynomial-query algorithm achieves a ratio better than $p + 1/2$ for this problem (Feldman, Harshaw and Karbasi 2017, Theorem 4), the ratio $(p+1)^2/p = p + 2 + 1/p$ is nearly tight. The proof technique, which couples the subsampled algorithm with an auxiliary algorithm that flips coins only for the elements it considers, is reused in the paper's streaming algorithm and in later subsampling-based algorithms.

The result is proved on paper; no machine-checked version is known. A formalization would give a checked analysis of a randomized greedy algorithm over an abstract independence system, including the coupling of two random processes, which is the step that informal proofs usually treat most briefly. It would also give reusable definitions of $p$ -extendible systems and of greedy runs with explicit tie-breaking. The mission also records a defect of the printed text: Lemma 9 as printed is false for linear functions with $f(\emptyset) > 0$ , so it is stated here with $f(\emptyset) = 0$ .

Difficulty

The obvious argument would analyze SampleGreedy directly, but there the sample and the greedy path are entangled: which element is chosen next depends on the whole sample. The analysis instead goes through Algorithm 2, and the hard step is Lemma 4, an exact equality of output laws. Its proof needs both algorithms to break ties identically and the coins to be fixed in advance. After that, the expectation bounds of Lemmas 7, 8 and 10 condition on the history up to the iteration in which a given element is considered, and the coin of that element is independent of that history. In the finite-sum encoding this conditioning becomes a combinatorial regrouping of the $2^n$ coin outcomes, which has to be carried out explicitly. Lemma 6 requires a disjointness argument for the sets $O_u \setminus S$ across the whole run.

Formalization scope

The ground set is a Fintype α with a LinearOrder α, which is the paper's tie-breaking order (p. 10). Set functions are Finset α → ℝ, and $\mathcal I$ is a predicate Finset α → Prop. The parameter $p$ is a natural number with $p \ge 1$ . Submodularity is the published lattice form NonmonotoneSubmod.Shared.Submodular ( $f(S\cup T)+f(S\cap T)\le f(S)+f(T)$ ), equivalent on finite ground sets to the paper's (1). The while loops run for exactly $n$ iterations, which is enough because each effective iteration adds or considers a new element. Expectations are exact finite sums over the $2^n$ samples or coin outcomes. Algorithm 2's coins are a fixed bit set, and its line 6 is one fixed minimum-cardinality choice. " $\alpha$ -approximation" for a randomized algorithm is read, as in the paper's proof, as $\mathbb E[f(S)] \ge f(\mathrm{OPT})/\alpha$ , stated against every independent $T$ . Linear means (1) with equality and allows $f(\emptyset) \neq 0$ , except in Lemma 9, which adds $f(\emptyset)=0$ . The oracle-count clause $O(nk/p)$ of Theorem 1 is not formalized.

Trivializing encodings are excluded. The expected value is a sum over the greedy runs on each sample, with the sample as the greedy pool (not the whole ground set followed by a filter). The weights sum to 1. The comparison set is always assumed independent. The ratio $(p+1)^2/p$ is real division. A sanity file checks that the output on a sample differs from the output on the whole ground set.

A complete development needs the greedy run's invariants, the coupling of Lemma 4, and the regrouping of finite sums over coin outcomes by the history before a given element is considered. The last of these is reusable for any analysis of an algorithm that flips independent coins. Proofs of any milestone, and alternative proofs of Lemma 4, are welcome.

Selected references

C. Harshaw, E. Kazemi, M. Feldman, A. Karbasi, The Power of Subsampling in Submodular Maximization, Mathematics of Operations Research, 2022; preprint arXiv:2104.02772v1, 2021. https://arxiv.org/abs/2104.02772
M. Feldman, C. Harshaw, A. Karbasi, Greed is Good: Near-Optimal Submodular Maximization via Greedy Optimization, COLT, 2017. https://arxiv.org/abs/1704.01652
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, Submodular Maximization with Cardinality Constraints, SODA, 2014. https://doi.org/10.1137/1.9781611973402.106
M. L. Fisher, G. L. Nemhauser, L. A. Wolsey, An analysis of approximations for maximizing submodular set functions – II, Mathematical Programming Study 8, 1978. https://doi.org/10.1007/BFb0121195
J. Mestre, Greedy in Approximation Algorithms, ESA, 2006. https://doi.org/10.1007/11841036_49

13 thms3 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Dynamic Pricing with Unknown Non-Parametric Demand and Limited Price Changes: The SLPE Policy Has Regret O(√T log T log log T) on Its Concentration Event and Makes O(log log T) Price ChangesResearch Paper

Motivation

A retailer selling one product over $T$ periods must choose a price each period without knowing how demand responds to price. Charging different prices reveals the demand curve but costs revenue, and in practice every price change has its own cost: relabelling, customer goodwill, contractual limits on repricing. Dynamic pricing with learning asks for policies whose cumulative revenue loss against the best fixed price, the regret, grows slowly in $T$ , and recent work also asks that the policy change its price rarely.

The paper's literature review (pp. 3–5) frames the gap. For parametric demand, Broder (2011) gives an MLE-based policy with $\tilde O(\sqrt T)$ regret and $O(\log T)$ price changes, and Cheung, Simchi-Levi and Wang (2017) study limited price changes when demand is one of finitely many known curves. Non-parametric policies such as Besbes and Zeevi (2015) and the continuum-armed bandit algorithm of Agarwal et al. (2011) do not control price changes and incur at least $O(\log T)$ of them. Perakis and Singhvi (SSRN 3336949; published in Operations Research, doi:10.1287/opre.2020.0445) show that, under a two-point bandit feedback assumption borrowed from online convex optimisation (Agarwal and Dekel 2010, Nesterov 2011), a non-parametric policy can keep $\tilde O(\sqrt T)$ regret while changing its price only $O(\log\log T)$ times.

Setting

Prices lie in $[0,1]$ . In period $t$ the retailer charges $p_t$ and observes demand

Y_t=d(p_t)+\epsilon_t,

where $d$ is an unknown smooth non-increasing demand curve and $\epsilon_t$ is noise. The revenue is $r(p)=p\,d(p)$ , maximised on $[0,1]$ at a unique interior price $p^*$ . The two performance measures are

\mathcal R(T)=\sum_{t=1}^T\big(r(p^*)-r(p_t)\big),\qquad LPC(T)=1+\big|\{2\le t\le T:\ p_t\ne p_{t-1}\}\big|.

Assumption 1 asks for $\kappa>0$ with $d(p^*)-\kappa(p-p^*)^2\le-d'(p)\,p^*$ ; Assumption 2 asks that among the observations at two charged prices there is one pair with identical noise, and that the policy can identify it. $K_1$ bounds $|d^{(k)}|$ for $k\le3$ .

The SLPE policy (Algorithm 1) runs in rounds $i=1,2,\dots$ with half-widths $\Delta_1=\tfrac12$ , $\Delta_{i+1}=\mu\Delta_i^2$ . Round $i$ charges $p^L_i=p^M_i-\Delta_i$ , $p^M_i$ and $p^H_i=p^M_i+\Delta_i$ for $n_i=2\rho^4\log T/\Delta_i^4$ periods each, starting from $p^M_1=\tfrac12$ . It fits a two-piece linear demand estimate whose level is the average demand $\bar D_{n_i}(p^M_i)$ and whose slopes are finite differences of the two identical-noise pairs, maximises the estimated revenue on $[p^L_i,p^H_i]$ to obtain $\tilde p^*_i$ , and recentres: $p^M_{i+1}=\tilde p^*_i$ .

Formalization targets

Goal: Theorem 1 and Corollary 1

Under Assumption 1, the gradient condition $|d'(p^*)|\ge(K_1/24+\kappa/4)\tfrac14+c/2$ with $c>0$ , and

2>\mu\ge M=\tfrac1c\big(\tfrac1{\rho^2}+\tfrac{K_1}6+\tfrac\kappa4\big)+\tfrac{K_1}{12}+4\kappa,

there are constants $C_1,C_2,C_3$ independent of $T$ such that for every $T\ge3$ , every noise realisation and every choice of the policy's tie-breaking and pair selection,

LPC^{SLPE}(T)\le C_3+3\log_2(\log T),

and, on every realisation where Assumption 2 and the concentration event $|\bar D_{n_i}(p^M_i)-d(p^M_i)|\le\Delta_i^2/\rho^2$ hold in each used round,

\mathcal R^{SLPE}(T)\le\big(C_1+C_2\log(\log T)\big)\sqrt T\log T .

Milestones

Lemma 1 (p. 10): Assumption 1 gives $p^*(d'(p)-d'(p^*))\le\kappa(p-p^*)^2$ .
Lemma 2 (p. 11): $d''(p^*)=0$ with Lipschitz $r''$ and $d'$ gives the same inequality with $\kappa=\Psi+\bar\Psi+2K_1$ .
Lemma 3 (p. 17): the identical-noise finite differences of round $i$ are within $\tfrac12K_1\Delta_i^2/12$ of $d'$ at the midpoints.
Hoeffding step (pp. 19–20): $\mathbb P(|\bar X_n|>\Delta^2/\rho^2)\le1/T^2$ for $n\ge2\rho^4\log T/\Delta^4$ and sub-Gaussian noise with variance proxy at most $1/3$ .
Lemma 4 (p. 17): $|p^*-\tilde p^*_i|\le M\Delta_i^2$ on the good event of rounds $1,\dots,i$ .
Containment (p. 17): $p^L_i\le p^*\le p^H_i$ on the good event of earlier rounds.
Round count (p. 24): at most $C+\log_2(\log T)$ rounds start before $T$ .

Significance

The result gives a non-parametric pricing policy whose number of price changes is doubly logarithmic, the same order as the number of batches needed in batched multi-armed bandits, while its regret is within $\log T\log\log T$ of the $\Omega(\sqrt T)$ lower bound of Keskin and Zeevi (2014). Its key estimate, Lemma 4, is a perturbation bound for the maximiser of a piecewise linear surrogate of a smooth revenue function; it applies wherever an optimum is located from noisy function values with matched-noise finite differences.

The theorem is proved on paper and, to the extent that can be determined, has no machine-checked proof. Formalizing it adds a continuum-armed pricing policy with an explicit price-change bound, and a checked version of an argument whose printed proof has gaps: a high-probability step that is false as printed, an inequality used two-sidedly that is assumed one-sidedly, and a logarithm base that does not match. Lemma 4 is posed as printed. It is supported numerically but its printed proof is incomplete, so a formal proof, or a counterexample, is itself new information.

Difficulty

The obvious argument for Lemma 4 compares the first-order condition of the surrogate with that of the true revenue. It fails as written: the surrogate's maximiser may sit at an endpoint of $[p^L_i,p^H_i]$ or at the kink $p^M_i$ , where no first-order condition holds, and the comparison needs a two-sided bound on $d'(p)-d'(p^*)$ while Assumption 1 is one-sided and weighted by $p^*$ . The regret bound then needs the induction that keeps $p^*$ inside every round's range, a careful treatment of the last round, which the horizon truncates, and the conversion of the doubly exponential decay of $\Delta_i$ into a $\log_2\log T$ round count.

Formalization scope

Periods are 0-based and rounds 1-based. The demand is d : ℝ → ℝ, and $p^*$ is a parameter satisfying hypotheses, not a defined argmax. The noise is a single realisation ε : ℕ → ℝ, and the regret and the price-change count are numbers on it, with no expectation. The policy receives only $T,\mu,\rho$ , an argmax selector (any rule returning a maximiser of a continuous function on an interval), a pair selector (four periods per round), and the observations $d(p)+\epsilon_t$ at the prices it charges. $n_i$ is rounded up. The concentration event's probability is the separate Hoeffding milestone.

The following hypotheses and repairs are added and disclosed in each item:

Assumption 1 and the bound $K_1$ are imposed on $[-1,2]$ , because SLPE can charge prices outside $[0,1]$ .
$p^*<1$ , so that the optimum is interior.
Assumption 2 is a property of the realisation, not an almost-sure statement, because under i.i.d. continuous noise it has probability zero.
The Hoeffding step carries $\sigma^2\le1/3$ and $T\ge2$ , since the printed $1-1/T^2$ is false for $\sigma\ge1$ .
The round count and Corollary 1 use $\log_2\log T$ ; the printed natural-log bounds fail numerically (19 price changes against a printed bound of 15.8 at $T=10^6$ ).
The inner $\log(T/(2\mu\rho^4\log T))$ is replaced by $\log T$ , which only changes the constants.
Lemma 1 is posed with Assumption 1's own $\kappa$ , since the printed " $\forall p\,\exists\kappa$ " is trivial.

Four formalizations would make the goal trivial, and the statements rule each out: a policy that reads $d$ or $p^*$ , constants allowed to depend on $T$ or on the realisation, an argmax or pair oracle not tied to the observations, and an Assumption 2 that no realisation can satisfy (zero noise with in-block pairs satisfies it, and a sanity check exhibits a full instance).

Theorem 2 (the relaxed Assumption 2A and Algorithm 2) is not part of the mission. A complete development needs Taylor's theorem with remainder, sub-Gaussian tail bounds (available as Mathlib's HasSubgaussianMGF and the platform theorem BanditAlgorithm.subgaussian_sample_mean_tail_bound), and bookkeeping for the round schedule. The schedule lemmas and the finite-difference bound are reusable beyond this paper. Proofs of any milestone are welcome, as is a counterexample to Lemma 4's constant.

Selected references

G. Perakis and D. Singhvi, Dynamic Pricing with Unknown Non-Parametric Demand and Limited Price Changes, SSRN 3336949 (PDF of 2020-07-03); published in Operations Research. https://ssrn.com/abstract=3336949, https://doi.org/10.1287/opre.2020.0445
O. Besbes and A. Zeevi, On the (Surprising) Sufficiency of Linear Models for Dynamic Pricing with Demand Learning, Management Science 61(4), 2015. https://doi.org/10.1287/mnsc.2014.2031
W. C. Cheung, D. Simchi-Levi and H. Wang, Dynamic Pricing and Demand Learning with Limited Price Experimentation, Operations Research 65(6), 2017. https://doi.org/10.1287/opre.2017.1629
N. B. Keskin and A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1294
A. Agarwal, D. P. Foster, D. Hsu, S. M. Kakade and A. Rakhlin, Stochastic Convex Optimization with Bandit Feedback, NeurIPS 2011. https://arxiv.org/abs/1107.1744
V. Perchet, P. Rigollet, S. Chassang and E. Snowberg, Batched Bandit Problems, Annals of Statistics 44(2), 2016. https://arxiv.org/abs/1505.00369

10 thms3 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models: The Adaptive-Confidence Trisection Policy Has N-Independent Regret at Most C√TResearch Paper

Learning which products to offer

A retailer that sells $N$ substitutable products must decide, for each arriving customer, which subset of products to display. Customer preferences are unknown at the start and have to be learned from purchases, while every suboptimal display costs revenue. This is dynamic assortment planning, a standard problem of revenue management in e-commerce and online advertising, and its learning version is a bandit problem whose arms are the $2^N$ subsets of products.

Under the multinomial logit (MNL) choice model the problem has been studied through the regret of a policy over $T$ customers (Chen, Wang and Zhou, §2 and Table 1):

Rusmevichientong, Shen and Shmoys (2010) analysed the same revenue potential as this paper with a golden-ratio search; their bound involves $\log N$ and needs a separability (gap) assumption between candidate assortments.
Sauré and Zeevi (2013) also cast MNL assortment learning as regret minimization.
Agrawal, Avadhanula, Goyal and Zeevi gave UCB and Thompson-sampling policies with regret $\tilde O(\sqrt{NT} + N)$ for assortments of capacity $K$ .
Chen and Wang (2018) proved an $\Omega(\sqrt{NT})$ lower bound in the capacitated model when $K \le N/4$ .

In the capacitated model the regret must grow with $N$ . Chen, Wang and Zhou (arXiv:1805.04785v2, Mathematics of Operations Research 2021) show that without a capacity constraint it need not: a trisection policy achieves regret $C_1\sqrt T$ with a universal constant, and $\sqrt T/384$ is a lower bound. This mission formalizes the upper bound.

Setting

There are $N$ items with known revenues $r_1,\dots,r_N \in [0,1]$ and unknown utilities $v_1,\dots,v_N \ge 0$ ; the no-purchase option has utility $v_0 = 1$ . In each period $t = 1,\dots,T$ the retailer offers an assortment $S_t \subseteq [N]$ , and the customer buys $j \in S_t$ with probability $v_j/(1+\sum_{i\in S_t} v_i)$ or buys nothing with probability $1/(1+\sum_{i\in S_t} v_i)$ , independently of the past. The expected revenue of $S$ is

R(S) = \frac{\sum_{j\in S} r_j v_j}{1 + \sum_{j\in S} v_j},

and the regret of a policy is $\mathrm{Regret} = \mathbb E\sum_{t=1}^T R(S^*) - R(S_t)$ , where $S^*$ maximizes $R$ over all $2^N$ subsets.

The policy rests on two objects. The level set $\mathcal L_\theta = \{i : r_i \ge \theta\}$ collects the items whose revenue is at least $\theta$ . The revenue potential $F(\theta) = R(\mathcal L_\theta)$ is a piecewise-constant function of one real variable. Its maximum is $F^* = \sup_{\theta \ge 0} F(\theta)$ , its right limit is $F(\theta^+)$ , and $\theta^*$ denotes the fixed point $\theta^* = F(\theta^*) = F^*$ .

The adaptive-confidence trisection policy keeps an interval $[a_\tau, b_\tau]$ , starting from $[0,1]$ . In epoch $\tau$ it forms the points $x_\tau = \tfrac23 a_\tau + \tfrac13 b_\tau$ and $y_\tau = \tfrac13 a_\tau + \tfrac23 b_\tau$ , at distance $\varepsilon_\tau = y_\tau - x_\tau = \tfrac13(\tfrac23)^\tau$ , and runs $n_\tau = 8\lceil\varepsilon_\tau^{-2}\ln(8T\varepsilon_\tau^2)\rceil$ inner iterations. Each inner iteration does two things:

while $y_\tau$ lies inside the current confidence interval $[\ell, u]$ for $F(y_\tau)$ , it explores: it offers $\mathcal L_{y_\tau}$ , adds the revenue to the running sum $\rho_t$ , and sets $[\ell_t, u_t] = \rho_t/t \pm \sqrt{2\ln(8T/t)/t}$ ;
it then exploits by offering $\mathcal L_{a_\tau}$ .

At the end of the epoch the policy sets $b_{\tau+1} = y_\tau$ if $u < y_\tau$ , and $a_{\tau+1} = x_\tau$ otherwise. The policy knows $r$ and $T$ but never $v$ .

Formalization targets

Goal: Theorem 3

There is a universal constant $C_1 > 0$ such that for every $N$ , every horizon $T$ , all $v_i \ge 0$ and all $r_i \in [0,1]$ , the adaptive-confidence trisection policy satisfies

\mathbb E\sum_{t=1}^T R(S^*) - R(S_t) \le C_1\sqrt T.

No gap condition and no bound on $v$ is assumed. The constant is left unspecified, as in the paper.

Milestones

Structure of $F$ . Lemma 1 (revenue-ordered optimality), Corollary 1 ( $F^* = R(S^*)$ ), Lemma 2 (the fixed point, under $F^* > 0$ ), the jump identity (S4)/(S8), and Lemmas 3–4 ( $F$ is below the diagonal to the right of $\theta^*$ and above it to the left).
Concentration. Hoeffding's inequality (Lemma 15, already proved on the platform), the uniform inequality with growing confidence levels (Lemma 8, (11)), and the two tail bounds (S32) and (S33) used in the proof of Lemma 10.
Recursion. With $\psi^\omega_\tau(\alpha,\beta)$ the expected regret of epochs $\tau,\dots,\tau_0$ conditioned on the relative position of $a_\tau$ , $b_\tau$ and $\theta^*$ ((14)): Lemma 11 (Case 3, $\psi^3_\tau \le \alpha T$ ), Lemma 9 (Case 1) and Lemma 10 (Case 2).

Significance

Theorem 3, together with the lower bound of Theorem 4, settles the minimax regret of uncapacitated MNL assortment learning at $\Theta(\sqrt T)$ , independent of the number of products. The policy uses no estimate of the individual utilities, and its cost per period is one level-set offer, so it applies to catalogues where $N$ is large compared with $T$ . The structural lemmas on the revenue potential (Lemmas 1–4) are standard tools for MNL assortment problems and are reusable by other missions on static and dynamic assortment optimization. Lemma 8 is a MOSS-style concentration inequality whose confidence level grows with the sample size; it is the device that removes the $\sqrt{\log T}$ factor of the paper's baseline bound (Theorem 2).

The result is proved in the paper and is not presented as open; no machine-checked proof of any part of it is known. The platform has the MNL model, the UCB policy of Agrawal et al. (whose bound depends on $N$ ) and Hoeffding's inequality, but no level-set or trisection analysis. A formal proof would also check the paper's argument, whose printed slips are recorded in the scope section.

Difficulty

The regret concerns a stateful algorithm whose epochs end at random times: an inner iteration takes two periods while exploration is active and one afterwards, and the policy's internal state must be recomputed from the purchase history alone. The obvious argument fixes a confidence level $1/T^2$ , bounds each epoch's regret on the event that all confidence intervals hold, and sums a geometric series. That argument loses a $\sqrt{\log T}$ factor, and it is the paper's own Theorem 2. Removing the factor needs confidence levels that weaken as data accumulate. A failure is then no longer rare enough to be ignored, so the analysis has to track its cost. This is done by a recursion on conditional expected regrets across three cases (interval to the right of, containing, or to the left of $\theta^*$ ), in which a wrong decision in one epoch passes to another case with controlled probability. Within an epoch, the purchases made while exploring a level set must be shown to behave like i.i.d. samples with mean $F(y_\tau)$ , although the number of explorations is itself random.

Formalization scope

Model. The model is the published MNLBandit.UCB.Setting with every subset admissible: histories are sequences of choices in Option (Fin N) (none = no purchase), policies are deterministic functions of the past choices, and expectations are finite sums over histories. Items and periods are 0-based in Lean; epochs and inner iterations are as on the page.
Policy. The policy is defined exactly. Confidence radius $\sqrt{2\ln(8T/t)/t}$ (δ = 1/T in (12)); $n_\tau = \max(1, 8\lceil(y_\tau-x_\tau)^{-2}\ln(8T(y_\tau-x_\tau)^2)\rceil)$ ; trisection weights $2/3, 1/3$ ; the update $b \leftarrow y_\tau$ if and only if $u < y_\tau$ ; exploitation of $\mathcal L_{a_\tau}$ in every inner iteration; exploration only while $\ell \le y_\tau \le u$ .
Conventions.
- The $\max(1,\cdot)$ matters only for tiny $T$ , where the printed $n_\tau$ is $0$ .
- The empty assortment is allowed (§3 asks $S_t \neq \varnothing$ ; $R(\varnothing) = 0$ ).
- §3's $r_i > 0$ is relaxed to Theorem 3's $r_i \in [0,1]$ .
- $F$ is defined on all of $\mathbb R$ , and $F(\theta^+)$ is Mathlib's Function.rightLim.
- $\theta^*$ is defined as $F^*$ .
- $\psi$ is a ratio of finite sums and is $0$ on a conditioning event of probability $0$ .
- Every $O(\cdot)$ and $\lesssim$ is an existential constant chosen before all other quantities.
Added hypotheses. Lemma 2 assumes $F^* > 0$ , which its proof uses. Lemmas 9 and 10 and (S33) assume $T \ge 25$ and that epoch $\tau$ can start ( $\sum_{\tau'<\tau} n_{\tau'} < T$ ); without these, $\log(T\varepsilon^2)$ can be negative.
Repairs. Two printed statements are repaired.
- (S32) is stated with $\exp\{-n_\tau\Delta^2/2\}$ , which its printed justification gives; the printed $\exp\{-n_\tau\Delta^2\}$ fails on an explicit instance.
- Lemma 9 sums from $\tau' = \tau$ , as its proof does, with exponent $n_{\tau'}$ and the deterministic last epoch $\bar\tau(T)$ as upper limit.
Ruled out. Three formalizations would make the goal trivial, and none is admissible: a policy that receives $v$ (it could offer $S^*$ in every period); a constant $C_1$ that depends on $T$ , $N$ or the instance (the regret is at most $T$ ); and an abstract "trisection oracle" with assumed guarantees in place of the algorithm above.
Not included. Theorem 4 (the $\sqrt T/384$ lower bound) and its Lemmas 12–14 are not part of the mission, and neither are Theorem 2 and its Lemmas 5–7 (the baseline policy) or Proposition 1.
Contributions welcome. Lemmas 1–4 need only finite sums; Lemma 8 and (S32)/(S33) need Hoeffding's inequality and a union bound over sample sizes; the reduction of exploration purchases to i.i.d. samples is reusable for other level-set policies.

Selected references

X. Chen, Y. Wang, Y. Zhou, An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models, arXiv:1805.04785v2, 2019; Mathematics of Operations Research 46(4), 2021. https://arxiv.org/abs/1805.04785
S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://arxiv.org/abs/1706.03880
X. Chen, Y. Wang, A note on tight lower bound for MNL-bandit assortment selection models, Operations Research Letters 46(5), 534–537, 2018.
P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
J.-Y. Audibert, S. Bubeck, Minimax Policies for Adversarial and Stochastic Bandits, COLT 2009.

17 thms3 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

Geometric Deep Learning IX: Message-Passing GNNs Are No More Powerful Than the Weisfeiler–Lehman Test — Equal Colour Histograms Force Equal OutputsTextbook

Motivation

Graph neural networks (GNNs) compute representations of nodes and whole graphs by repeatedly combining each node's state with information from its neighbours. Soon after they became a standard tool, the question arose of what they cannot do. A natural test case is graph isomorphism: given two graphs that are not isomorphic, can the network attach different representations to them? If it cannot, it is hopeless on any task that needs to tell the two graphs apart.

The yardstick for this question is the Weisfeiler–Lehman (WL) test (Weisfeiler and Leman, 1968), a colour-refinement procedure that is a necessary condition for isomorphism. Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2) reports, in its historical chapter (Ch. 7, p. 120), the conclusion of Morris et al. (2019) and Xu et al. (2019): any GNN of the three flavours of §5.3 "cannot be more powerful than the WL test". This mission formalizes that claim, together with the surrounding remarks of the book that make it precise.

Timeline. 1968: Weisfeiler and Leman introduce the refinement. 2011: Shervashidze et al. use the WL iteration to build graph kernels. 2017: Gilmer et al. unify many architectures as message-passing neural networks. 2019: Morris et al. and Xu et al. independently prove that message-passing GNNs are bounded by 1-WL, and that injective aggregation attains the bound (the Graph Isomorphism Network). 2020: Corso et al. show that with continuous features injective aggregation needs several aggregators.

Setting

A graph $G$ has node set $V = \{0, \dots, n-1\}$ and a symmetric, loopless adjacency relation. The neighbourhood of a node is $\mathcal N_u = \{v : (u, v) \in E\}$ (eq. (11), p. 34); it does not contain $u$ .

The WL colour refinement on a featureless graph starts with the same colour $c^0(u)$ for every node and sets

c^{s+1}(u) = \big(c^s(u), \{\!\{c^s(v) : v \in \mathcal N_u\}\!\}\big),

where $\{\!\{\cdot\}\!\}$ is a multiset. Colours carry their full history, so colours of nodes of two different graphs can be compared directly. The colour histogram at round $s$ is the multiset $\{\!\{c^s(u) : u \in V\}\!\}$ . The WL test declares two graphs indistinguishable when their histograms agree at every round.

A message-passing layer (eq. (35), p. 79) has a message function $\psi$ , a permutation-invariant aggregator $\bigoplus$ and an update $\phi$ , and updates node features $h$ by

h_u \leftarrow \phi\Big(h_u, \bigoplus_{v \in \mathcal N_u} \psi(h_u, h_v)\Big).

A GNN starts from a constant feature $h^0_u = c$ and applies layers $t = 0, 1, \dots$ , with parameters $(\psi_t, \bigoplus_t, \phi_t)$ shared by all graphs. Its graph-level output after $T$ rounds is a read-out of the multiset $\{\!\{h^T_u : u \in V\}\!\}$ .

Formalization targets

Goal: GNNs are bounded by WL

For every GNN, read-out, depth $T$ and pair of graphs $G$ , $G'$ (of possibly different sizes):

c^t_G(u) = c^t_{G'}(v) \implies h^t_G(u) = h^t_{G'}(v) \quad (t \le T),

\{\!\{c^T_G(u)\}\!\}_u = \{\!\{c^T_{G'}(v)\}\!\}_v \implies \mathrm{readout}\big(\{\!\{h^T_G(u)\}\!\}_u\big) = \mathrm{readout}\big(\{\!\{h^T_{G'}(v)\}\!\}_v\big).

The statement fixes no architecture and no feature space: it quantifies over all message, aggregation, update and read-out functions.

Milestones

Injective $\phi$ is one WL step (§4.1, p. 34): for the local layer $h_u \mapsto \phi(h_u, \{\!\{h_v : v \in \mathcal N_u\}\!\})$ with $\phi$ injective, if equal features are exactly equal round- $s$ colours, then equal new features are exactly equal round- $(s+1)$ colours.
Isomorphic graphs (side-note p. 119): a GNN attaches identical representations to isomorphic graphs.
$C_6$ versus $2K_3$ (side-note p. 120): the 6-cycle and two disjoint triangles have equal WL histograms at every round but are not isomorphic.
Max and mean (side-note p. 120): the multisets $\{\!\{a, b\}\!\}$ and $\{\!\{a, a, b, b\}\!\}$ differ but have the same maximum and the same mean.

Companion: reaching the bound

If every layer's update $(x, S) \mapsto \phi_t(x, \bigoplus_{y \in S} \psi_t(x, y))$ is injective, then equal features are exactly equal WL colours (Xu et al.).

Significance

The result. The bound says that a GNN's ability to separate graphs is capped by a cheap combinatorial procedure. Every pair of non-isomorphic graphs that WL fails to separate — all regular graphs of the same degree and size, such as $C_6$ and $2K_3$ — is also inseparable by every message-passing GNN, whatever its width, depth or training. This limitation motivated the higher-order and subgraph-based architectures discussed later in Ch. 7. The companion result explains why architectures with injective (sum-type) aggregation, such as GIN, are the maximally expressive members of the class, and the max/mean example explains why common aggregators fall short of it.

Formalizing it. The results are proved on paper; to the knowledge of this mission none has a machine-checked proof. The formalization makes explicit what the informal statements leave open: that the comparison needs parameters shared across graphs, that it concerns featureless graphs, which flavour of layer is covered, and in what sense "equivalent to one step" holds. It reuses a published 1-WL colour refinement (WLIdentification), so the GNN results connect to the platform's existing WL statements.

Difficulty

The statements are close to their definitions, and the difficulty is in the bookkeeping rather than in an idea. The comparison is between two different graphs, whose node sets are different types, so the relation between features and colours has to be carried across graphs rather than within one; equalities of colour multisets over neighbourhoods have to become equalities of multisets of messages, and histograms of colours have to become multisets of features. The $C_6$ / $2K_3$ example needs the colours of a regular graph at every round and a separate non-isomorphism argument. A tempting shortcut, defining the GNN's features to be the WL colours, proves nothing: the goal quantifies over all GNNs.

Formalization scope

Graphs are the published OAI.WLIdentification.Graph (order $n$ , Boolean symmetric loopless adjacency on Fin n); the WL test is its neighborColor and neighborHistogram, featureless and with history-carrying colours. The book numbers no theorems, so every item is cited by section, equation and printed page.

Conventions committed to:

Featureless graphs. The GNN's initial features are a constant, matching the featureless WL refinement (the WL analyses "almost always consider featureless or categorically-featured graphs", side-note p. 120). The featured version is not stated.
The message-passing flavour. The goal is posed for layers (35). It covers the attentional flavour (34) and the convolutional flavour (33) when the coefficient $c_{uv}$ is a function of the features of $u$ and $v$ . A coefficient that is an arbitrary function of the graph is outside the claim; with $c_{uv}$ the number of triangles through $u$ , a convolutional layer separates $C_6$ from $2K_3$ .
Shared parameters. One GNN is evaluated on both graphs. A formalization in which each graph receives its own parameters would be trivially satisfiable and is ruled out.
Aggregation on multisets. The aggregator is a function of the multiset of messages, so permutation invariance holds by construction; message, aggregate and feature types are arbitrary types.
Neighbourhoods exclude the node itself; the node's own state enters through the first argument of $\phi$ .
The page's slips. The WL test is described (p. 120) as "randomly hashing their sums"; the refinement used hashes the multiset injectively. "With summation being a key representative" is not formalized: on real features summation is not injective on multisets, and Xu et al.'s result uses a chosen feature embedding.

Infrastructure needed is light: multiset bijections along equal maps (Multiset.map), induction over rounds, and finite computations on six-node graphs. The induction lemmas relating features to colours across two graphs are reusable for any further GNN-expressivity statement (higher-order WL, subgraph GNNs). Proofs of the milestones, of the companion, and alternative proofs of the goal through the companion are welcome.

Selected references

M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021. https://arxiv.org/abs/2104.13478v2
B. Weisfeiler, A. Leman, The reduction of a graph to canonical form and the algebra which appears therein, Nauchno-Technicheskaya Informatsia, 1968 (English translation). https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
K. Xu, W. Hu, J. Leskovec, S. Jegelka, How Powerful are Graph Neural Networks?, ICLR, 2019. https://arxiv.org/abs/1810.00826
C. Morris, M. Ritzert, M. Fey, W. L. Hamilton, J. E. Lenssen, G. Rattan, M. Grohe, Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networks, AAAI, 2019. https://arxiv.org/abs/1810.02244
J. Gilmer, S. S. Schoenholz, P. F. Riley, O. Vinyals, G. E. Dahl, Neural Message Passing for Quantum Chemistry, ICML, 2017. https://arxiv.org/abs/1704.01212
N. Shervashidze, P. Schweitzer, E. J. van Leeuwen, K. Mehlhorn, K. M. Borgwardt, Weisfeiler-Lehman Graph Kernels, JMLR 12, 2011. https://www.jmlr.org/papers/v12/shervashidze11a.html
G. Corso, L. Cavalleri, D. Beaini, P. Liò, P. Veličković, Principal Neighbourhood Aggregation for Graph Nets, NeurIPS, 2020. https://arxiv.org/abs/2004.05718

7 thms3 active usersReviewed

Completed

Dynamical Systems·Captain: mikedeng1

Geometric Deep Learning VIII: An RNN Seeded at a Fixed Point h⁽⁰⁾ = R(0, h⁽⁰⁾) Is Equivariant to Left Shifts of a Zero-Padded Input SequenceTextbook

Why sequence boundaries matter

A recurrent neural network (RNN) processes an ordered stream while retaining a summary of earlier inputs. The same update rule is applied at every time step, so it is natural to ask whether shifting the input stream simply shifts the resulting sequence of summaries. The answer depends on how the run begins. The first summary is supplied as an initial state, while the first input encountered after a shift can be different. Bronstein, Bruna, Cohen and Veličković use this boundary effect to explain a precise form of temporal translation equivariance for RNNs in §5.7 of Geometric Deep Learning (arXiv:2104.13478v2, pp. 90–93).

The claim matters when the same sequential model is applied to streams presented with different starting times. Without a specified boundary convention, the shared update rule alone does not guarantee that corresponding hidden states agree. The chapter's zero-padding construction makes that convention explicit. Its condition on the initial state can then be stated independently of a particular architecture or training procedure. The book numbers equations but no theorems or lemmas here; the mission's items are cited by section, equation, page, and, for a marginal statement, “side-note.”

RNN runs and padded sequences

Let $z(t)\in\mathbb R^k$ be the input at time $t$ , let $h(t)\in\mathbb R^m$ be its hidden summary, and let $R:\mathbb R^k\times\mathbb R^m\to\mathbb R^m$ be a shared update map. Given a seed $h_0$ , equation (38) defines a run by

h(0)=h_0,\qquad h(t+1)=R\bigl(z(t+1),h(t)\bigr).

The first processed input is $z(1)$ ; $z(0)$ is unused. This is the book's time convention, including the named state $h(0)$ (Bronstein et al., §5.7, p. 90, equation (38)). The update map is arbitrary: the results concern the recurrence itself, so they do not require the affine layer and activation used as one example in equation (39).

A left shift by $s$ steps replaces the input at time $t$ with the old input at time $t+s$ . A left-padded input of length $d$ is

\bar z(t)= \begin{cases} 0,&t\le d,\\ z(t-d),&t>d. \end{cases}

Here $0$ is the zero vector in $\mathbb R^k$ . The original input begins at time $d+1$ . The two runs being compared use the same update map and the same seed. This is the exact padding convention displayed on p. 93 of the book (Bronstein et al., §5.7, p. 93).

Formalization targets

The capstone is the chapter's one-step equivariance claim. For every update map, input sequence, and seed fixed by the zero-input update, one or more zero-padding steps suffice:

d\ge1,\qquad R(0,h_0)=h_0 \quad\Longrightarrow\quad h_{\bar z(\cdot+1)}(t)=h_{\bar z}(t+1) \quad\text{for every }t\ge0.

The multi-step side note extends the conclusion to every $s$ with $0\le s\le d$ :

h_{\bar z(\cdot+s)}(t)=h_{\bar z}(t+s) \quad\text{for every }t\ge0.

The milestone list also records the book's unpadded boundary counterexample and its observation that a contraction $\gamma(h)=R(0,h)$ has a unique attracting fixed point. The latter is represented by an already proved, reusable Banach fixed-point theorem rather than a second draft of the same result (Bronstein et al., §5.7, pp. 92–93, equations (40)–(42) and side-note).

What the result supplies

The equivariance theorem identifies a checkable condition under which the hidden-state sequence tracks a left-shifted input exactly, including at the first state. It also marks the limit of the informal idea that sharing the same update map across time automatically creates shift equivariance: the unpadded run can fail already at time $1$ . The fixed-point condition is therefore part of the mathematical claim, rather than an implementation preference (Bronstein et al., §5.7, pp. 92–93).

The RNN shift statements are targets for machine-checked proofs. The contraction milestone already has a machine-checked proof in the referenced CursoEDO.contraction_fixed_point theorem. A completed development would make the boundary convention and the arbitrary-update-map quantifiers available for later statements about sequential models. The recurrence and padding definitions are reusable whenever a discrete-time state update is compared before and after a shift.

The boundary difficulty

The tempting comparison takes two runs that begin with the same seed, then tries to pair the shifted run's state at $t$ with the original run's state at $t+1$ . At the first step, those states have encountered different input histories. Equations (40)–(41) display the mismatch: the original run has applied $R$ to its first input, while the shifted run still uses the supplied seed at the corresponding update. For an arbitrary $R$ and arbitrary first input, the states need not agree (Bronstein et al., §5.7, p. 92). A shift statement that omits its padding length or seed condition would therefore assert something the chapter explicitly rejects.

Formalization scope

Lean represents $\mathbb R^k$ and $\mathbb R^m$ as functions on Fin k and Fin m; time and padding lengths are natural numbers. The run uses $h(0)=h_0$ and consumes $z(t+1)$ at its next update. The padding function returns the zero vector through index $d$ and then the correspondingly indexed original input. These definitions cover every finite dimension, including zero-dimensional edge cases, while the unpadded counterexample uses one input and one hidden coordinate.

The target ranges over all update maps $R$ and all input sequences; it does not impose a special neural-network parameterization. The seed is any fixed point of $h\mapsto R(0,h)$ , not necessarily the zero state, and the zero-input update need not be the identity map. The formal statements include time $t=0$ and the endpoint $s=d$ . No contraction assumption is needed for shift equivariance itself; contraction enters only the separate existence-and-convergence milestone. The contraction theorem is stated for a nonempty complete metric space, which includes the finite-dimensional real hidden-state spaces used here.

The work requires a small discrete recurrence interface, an exact padding definition, and proofs for the boundary counterexample and shift identities. Those two definitions and the shift results can also support variants with a nonzero padding vector. The LSTM equations of §5.8 have a separate gated state model and are outside this mission's formalization scope. Contributions that keep the full fixed-point hypothesis and the stated boundary cases are welcome.

Selected references

M. M. Bronstein, J. Bruna, T. Cohen and P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021, arXiv:2104.13478v2, §5.7, pp. 90–93.

5 thms3 active usersReviewed

Completed

Harmonic Analysis Linear algebra·Captain: mikedeng1

Geometric Deep Learning III: An n × n Matrix Commutes with the Cyclic Shift S if and only if It Is Circulant, So Convolution Is Shift EquivarianceTextbook

Why convolution, and why the shift

Convolutional neural networks process images, audio and time series with layers whose weights are shared across positions. The Geometric Deep Learning programme of Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2) explains this architecture by symmetry: on a grid the relevant symmetry is translation, and a linear layer that respects translations is forced to be a convolution. Section 4.2 of the book makes this precise in the simplest setting, a one-dimensional periodic grid, and then derives the discrete Fourier transform from the same symmetry, as the common eigenbasis of all convolution operators. The material is classical in signal processing (see the tutorial of Bamieh, arXiv:1805.05533), and the book uses it as the template that the later chapters generalise to groups, graphs and manifolds; for example, graph signal processing (Sandryhaila and Moura, arXiv:1210.4752) replaces the shift by an adjacency matrix.

This mission formalises the characterisation the book calls the basis of "the overall philosophy of Geometric ML": a matrix is circulant if and only if it commutes with the shift (§4.2, p. 37). It is the third mission of a series on the book. The book numbers no theorems, lemmas or definitions; every item is cited by section, equation or position, and printed page.

Setting

Fix $n \ge 1$ and the ring graph with nodes $\mathbb Z_n = \{0, 1, \dots, n-1\}$ , arithmetic taken modulo $n$ . A signal is a vector $x = (x_0, \dots, x_{n-1})$ with entries in a commutative ring $R$ , for instance $\mathbb R$ .

The circulant matrix of a vector $\theta = (\theta_0, \dots, \theta_{n-1})$ is $C(\theta) = (\theta_{u - v \bmod n})_{u, v}$ : each row is the previous one shifted circularly by one position.
The circular convolution of a signal $x$ with a filter $\theta$ is $(x \star \theta)_u = \sum_{v=0}^{n-1} x_v\, \theta_{u - v \bmod n}$ .
The right shift $S$ is the circulant matrix of $\theta = (0, 1, 0, \dots, 0)^\top$ . It moves a vector one position to the right, $(Sx)_u = x_{u-1}$ .
Over $\mathbb C$ , the discrete Fourier basis is $\varphi_k(u) = n^{-1/2} e^{2\pi i k u / n}$ for $k = 0, \dots, n-1$ . The Fourier matrix $\Phi = (\varphi_0, \dots, \varphi_{n-1})$ has the $\varphi_k$ as columns, and $\Phi^*$ is its conjugate transpose.

In Lean the index set is ZMod n with [NeZero n], $C(\theta)$ is Mathlib's Matrix.circulant θ, and the mission's definitions GeomDL.Grids.conv, GeomDL.Grids.shift, GeomDL.Grids.fourierVec and GeomDL.Grids.fourierMatrix are the four objects above.

Formalization targets

Goal: commuting with the shift characterises circulant matrices

For every $n \times n$ matrix $M$ over a commutative ring $R$ ,

M S = S M \iff M = C(\theta) \text{ for some } \theta \in R^n .

The book states the converse direction tentatively ("the opposite direction appears to be true as well"); it is a theorem, and it is stated here without the hedge.

Milestones, in attack order

Circulant matrices are convolutions, $C(\theta)x = x \star \theta$ , and $S = C(0, 1, 0, \dots, 0)$ shifts right, $(Sx)_u = x_{u-1}$ (p. 37).
The left shift is $S^\top$ , and $S^\top S = S S^\top = I$ (side-note, p. 37).
Shift equivariance of convolution, $S\,C(\theta)\,x = C(\theta)\,S\,x$ (p. 37).
The Fourier basis vectors are eigenvectors of $S$ : $S\varphi_k = e^{-2\pi i k/n}\varphi_k$ , with eigenvalues that are $n$ -th roots of unity (p. 38 and side-note).
These eigenvalues are pairwise distinct (side-note, p. 37).
$\Phi^*\Phi = I$ (side-note, p. 38).

Companion: the Convolution Theorem

With $(\mathcal F\theta)_k = \sum_w \theta_w e^{-2\pi i k w/n}$ ,

C(\theta)\varphi_k = (\mathcal F\theta)_k\,\varphi_k, \qquad C(\theta) = \Phi\,\operatorname{diag}(\mathcal F\theta)\,\Phi^* .

The book prints this with $\hat\theta = \Phi^*\theta = n^{-1/2}\mathcal F\theta$ in place of $\mathcal F\theta$ , which is off by a factor $\sqrt n$ for $n \ge 2$ ; the corrected identity is stated. The transform form of the Convolution Theorem, $\mathcal F(u \star v) = \mathcal F u \cdot \mathcal F v$ with Mathlib's ZMod.dft, is already Proved on the platform as IntMul.HvdH.dft_cyclic_conv and is included as a reference item.

Significance

The goal identifies the space of linear translation-equivariant maps on $R^{\mathbb Z_n}$ with the convolutions, an $n$ -dimensional space parametrised by the filter $\theta$ . This is the statement that lets the book define convolution as a translation-equivariant linear operation, and it is the grid case of the general principle the book develops in §4.3 and §5: a linear map that commutes with a group action is a group convolution. Milestones 4–6 and the companion are the other half of §4.2: the shift has distinct eigenvalues, so every matrix commuting with it is diagonal in the shift's eigenbasis, and that eigenbasis is the Fourier basis; hence the Fourier transform diagonalises every convolution.

Mathlib contains circulant matrices, their commutativity (Matrix.circulant_mul_comm) and the discrete Fourier transform on ZMod n, but neither the converse characterisation nor the diagonalisation of circulant matrices by the normalised Fourier matrix. The mission adds these, in a form that later missions of the series (group convolutions, graph Fourier transforms) can be compared against.

Difficulty

The direction " $\Leftarrow$ " is a one-line consequence of the commutativity of circulant matrices. The content is " $\Rightarrow$ ": the equation $MS = SM$ is an equation between matrices, and it has to be turned into the statement that the entries of $M$ are constant along every cyclic diagonal, with the indices handled modulo $n$ . The spectral argument of the book (commuting matrices with a common eigenbasis) only applies over a field containing the $n$ -th roots of unity in which $n$ is invertible; over a general commutative ring, such as $\mathbb Z$ or $\mathbb Z/2$ , the goal has to be proved without it. For the Fourier statements the work is in the geometric sums of roots of unity and in the bookkeeping between the representatives $\{0, \dots, n-1\}$ used in the exponents and the arithmetic of $\mathbb Z_n$ .

Formalization scope

Indices live in ZMod n with [NeZero n], so $n \ge 1$ and matrices are finite; no lower bound $n \ge 2$ is needed (for $n = 1$ , $S = I$ and every matrix is circulant, so the goal holds). Exponents use the representatives ZMod.val $\in \{0, \dots, n-1\}$ , as on the page.
The goal and milestones 1–3 are stated over an arbitrary commutative ring $R$ ; milestones 4–6 and the companion are over $\mathbb C$ .
"Circulant" means equal to Matrix.circulant θ for some θ. Defining a matrix to be circulant when it commutes with $S$ would make the goal true by definition; the mission does not do that. A sanity file checks that the shift moves vectors to the right on $\mathbb Z_3$ and that $\operatorname{diag}(1, 0)$ on $\mathbb Z_2$ does not commute with $S$ .
The side-note on p. 38 calls $\Phi$ "orthogonal"; the property it writes, $\Phi^*\Phi = I$ with the conjugate transpose, is unitarity, and that is what is stated.
The Fourier normalisation is the book's $n^{-1/2}$ in $\varphi_k$ ; the eigenvalues in the companion use Mathlib's unnormalised ZMod.dft, and the factor $\sqrt n$ is written out in its statement.

No new infrastructure beyond Mathlib is required. Proofs of any item, and proofs of the goal that avoid the spectral argument, are welcome; the shift and Fourier lemmas are reusable for the graph Fourier transform later in the book.

Selected references

M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021 (v2). §4.2, pp. 35–38. https://arxiv.org/abs/2104.13478
B. Bamieh, Discovering Transforms: A Tutorial on Circulant Matrices, Circular Convolution, and the Discrete Fourier Transform, arXiv preprint, 2018. https://arxiv.org/abs/1805.05533
A. Sandryhaila, J. M. F. Moura, Discrete Signal Processing on Graphs, IEEE Transactions on Signal Processing, 2013. https://arxiv.org/abs/1210.4752
D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics, 2021 (source of the platform's proved IntMul.HvdH.dft_cyclic_conv). https://hal.science/hal-02070778

9 thms3 active usersReviewed

Probability·Captain: mikedeng1

Speculative Actions: A Lossless Framework for Faster Agentic Systems: Exact Expected Runtime Ratio of k-Branch Speculation Under Exponential LatenciesResearch Paper

Motivation

An agentic system may make several slow API calls in sequence: the answer to one call determines what to request next. A speculator can guess the current answer while the real call is running and start likely next calls early. When a guess is correct, the system can reuse a pending result; when it is wrong, it discards that result. This can shorten a run if concurrent calls do not interfere and incorrect calls have no lasting side effects. Ye and coauthors introduce this execution scheme for language-model and tool-using agents in Speculative Actions, §2.

The paper's Proposition 1 quantifies the expected latency of one-step speculation with exponential call times. Its proof in Appendix A states a stochastic timing model and computes a finite-horizon runtime ratio and its limit. The first author's existing Prove2Me mission, Speculative Actions: Cost-Latency Analysis for Agentic Speculation, contains proved algebraic identities for expressions named specTime and seqTime. Those expressions encode the values claimed for the expectations. This mission supplies the missing connection between random executions and those expressions, while reusing the published algebra.

Setting

There are $T$ real API calls, numbered $0$ through $T-1$ . The real-call latency of step $t$ is $B_t$ with exponential rate $\beta$ . At a speculation window during step $t$ , a speculator has latency $A_t$ with exponential rate $\alpha$ . It produces $k$ candidate next calls. Each candidate independently matches the actual next call with probability $p$ , so a hit means that at least one of the $k$ candidates matches. The hit probability is

p(k)=1-(1-p)^k.

All latencies and branch-correctness indicators are mutually independent. Proposition 1 assumes $0<\beta<\alpha$ and Assumption 1 gives $p>0$ ; as a probability, $p\le1$ . Assumption 2 permits concurrent API calls and reversible or side-effect-free pre-launching. The theorem also treats state transitions and construction of API parameters as having negligible duration. These conditions and the exponential laws are stated in §2 and Proposition 1.

The sequential runtime $T_{\mathrm{seq}}$ is $\sum_{t<T}B_t$ . The speculative runtime $T_s$ follows Appendix A's timing rule. At a window without a hit, the current step costs $B_t$ . At a hit, the block comprising steps $t$ and $t+1$ costs $\min(A_t,B_t)+B_{t+1}$ , and step $t+1$ opens no window. The last step cannot open a window. This is the model used in the paper's proof of Proposition 1, Appendix A, pp. 14–15. Its precise timing rule matters: reading Algorithm 1's awaits literally gives a different timeline, as does waiting for validation before accepting an early next-step result.

Let $S_n$ be the expected number of hits in $n$ potential windows, with a hit consuming the following window. The paper gives $S_0=0$ , $S_1=p(k)$ , and

S_n=p(k)(1+S_{n-2})+(1-p(k))S_{n-1}\qquad(n\ge2).

Formalization targets

Random-runtime identities

The new milestones identify the expectation of the sequential runtime, the saving from one correct speculation, and the expected hit count. The total-saving identity is

\mathbb E[T_s]=\frac{T}{\beta}-S_{T-1}\frac{\alpha}{\beta(\alpha+\beta)},\qquad T\ge1.

Here $S_{T-1}$ is the expectation of the random count defined by the execution model. The previously published expression SpecActions.specTime has this same algebraic form; proving equality with the integral of the random runtime is the new step. The closed form for $S_n$ and the algebraic ratio are linked as published milestones.

Proposition 1

For every integer $T\ge1$ , the goal is the Proposition 1 ratio for the actual expectations:

\frac{\mathbb E[T_s]}{\mathbb E[T_{\mathrm{seq}}]}=1-\frac1T\frac{\alpha}{\alpha+\beta}\left[\frac{(T-1)p(k)}{1+p(k)}+\frac{p(k)^2}{(1+p(k))^2}-\frac{p(k)^2}{(1+p(k))^2}(-p(k))^{T-1}\right].

The same goal states convergence of this random-runtime ratio as $T\to\infty$ to

1-\frac{p(k)}{1+p(k)}\frac{\alpha}{\alpha+\beta}.

The horizon condition protects the denominator: at $T=0$ , the sequential runtime is zero. The number of branches may be zero; then $p(0)=0$ and the ratio is one for positive horizons.

Significance

The formula describes how breadth $k$ , branch accuracy $p$ , and the two latency rates affect expected completion time, both for a finite sequence of calls and in a long run. It makes the expected benefit of extra branches a quantity that can be compared with their resource cost. The paper uses the time expression again in its cost–latency discussion, including Theorem 5, p. 20.

The author's existing mission has machine-checked proofs for the recurrence's closed form and for algebraic identities involving specTime and seqTime. It does not prove that those expressions are expectations of a random execution. Completing this mission adds that probabilistic interpretation and a reusable model of independent calls, branch indicators, skipped windows, and runtime. The proposed stochastic theorems remain open; their statements compile, while the published reference results are already proved.

Difficulty

The main issue is the dependence created by skipping a window after a hit. Hit indicators at different windows are independent, but the number of opportunities actually used is determined by earlier outcomes. Treating the hit count as an ordinary binomial count gives the wrong recurrence. Likewise, multiplying a mean saving by the number of potential windows ignores that skipped windows cannot hit. A formal proof must relate the random execution and hit count while preserving the independence between correctness indicators and latencies.

Formalization scope

Lean represents all primitive random variables on one probability space. An index type separates speculator latency, real-call latency, and each of the $k$ branch indicators at every window. IsSpecModel requires measurable variables, their exponential or real-valued Bernoulli laws, and mutual independence. A hit is an existential statement over the $k$ branch indicators. The runtimes and hit count are recursions on a finite horizon, and expectation is the real Bochner integral. The model has an explicit construction on a product probability space, so its hypotheses are satisfiable.

Windows start at index zero: a $T$ -step run has $T-1$ potential windows. The theorem keeps the paper's $\beta<\alpha$ and $p>0$ conditions, and specifies $p\le1$ . It adds $T\ge1$ wherever a runtime ratio is divided by its sequential denominator. Concurrency without interference and negligible non-call work are represented by the timing recurrence. The claim concerns integrals of those random runtimes; defining an “expected runtime” directly by the paper's closed form would omit the target of this mission.

The definition layer and hit-probability, baseline, saving, hit-count, and total-saving milestones are available as separate contributions. Mathlib supplies exponential probability measures, product measures, independence, and integration; the published SpecActions definition and algebraic theorems are referenced. Work on the probabilistic bridges, integrability, and the final composition is within scope.

Selected references

N. Ye, A. Ahuja, G. Liargkovas, Y. Lu, K. Kaffes, and T. Peng, Speculative Actions: A Lossless Framework for Faster Agentic Systems, arXiv preprint arXiv:2510.04371v2, 2026. arXiv

13 thms3 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination: The Partial Identification Set of Demographic Disparity Is the Closed Interval with Fréchet–Hoeffding EndpointsResearch Paper

Why the disparity is uncertain

An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).

The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.

Observed information and compatible joints

Let decision $\hat Y\in\{0,1\}$ and true outcome $Y\in\{0,1\}$ . The protected class $A\in\{a,b\}$ has two groups, with $a$ conventionally advantaged and $b$ disadvantaged. The proxy $Z$ takes values in a measurable space $\mathcal Z$ ; it may be categorical, continuous, or mixed. The primary marginal is $P(\hat Y,Y,Z)$ , and the auxiliary marginal is $P(A,Z)$ . Both share one proxy distribution $P(Z)$ , as required when they arise from a common population joint law.

For each proxy value $z$ , write $\eta_{\mathrm{aux}}(\alpha,z)=P(A=\alpha\mid Z=z)$ and $\eta_{\mathrm{priT}}(\hat y,y,z)=P(\hat Y=\hat y,Y=y\mid Z=z)$ . Their decision marginal is $\eta_{\mathrm{pri}}(\hat y,z)=\sum_y\eta_{\mathrm{priT}}(\hat y,y,z)$ . A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set $\mathcal P_D$ contains all measurable conditional joint arrays $\pi(\alpha,\hat y,y\mid z)$ that couple $\eta_{\mathrm{priT}}(\cdot,\cdot,z)$ and $\eta_{\mathrm{aux}}(\cdot,z)$ at each $z$ , together with the fixed $P(Z)$ . It imposes no additional assumptions on the unknown association of class and outcomes.

The demographic disparity of a compatible joint $P'$ is $\delta_{DD}(a,b;P')=P'(\hat Y=1\mid A=a)-P'(\hat Y=1\mid A=b)$ . Its partial identification set is

\Delta_{DD}(\mathcal P_D)=\{\delta_{DD}(a,b;P'):P'\in\mathcal P_D\}.

This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.

Formalization targets

For a group $\alpha$ , decision $\hat y$ , and proxy value $z$ , define the Fréchet–Hoeffding weight endpoints

w^L_\alpha(\hat y,z)=\max\left\{0,1+\frac{P(A=\alpha\mid Z=z)-1}{P(\hat Y=\hat y\mid Z=z)}\right\},\qquad w^U_\alpha(\hat y,z)=\min\left\{1,\frac{P(A=\alpha\mid Z=z)}{P(\hat Y=\hat y\mid Z=z)}\right\}.

For a class weight function $w$ , let $\mu(\alpha;w)=E[w_\alpha(\hat Y,Z)\hat Y]/P(A=\alpha)$ . The goal, Proposition 7, is the equality

\Delta_{DD}(\mathcal P_D)= \left[\mu(a;w^L)-\mu(b;w^U),\;\mu(a;w^U)-\mu(b;w^L)\right].

Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).

What the result gives

The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.

Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.

Central difficulty

The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome $Y$ remains in the compatible-joint model even though demographic disparity uses only $\hat Y$ . When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.

Formalization scope

The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on $Z$ and measurable, normalized, nonnegative conditional vectors $\eta_{\mathrm{aux}}$ and $\eta_{\mathrm{priT}}$ . The set $\mathcal P_D$ consists of measurable conditional couplings for every $z$ . Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of $\delta_{DD}(a,b;P')$ is computed from $P'$ , not inserted from the auxiliary marginal.

The theorem explicitly assumes $P(A=a)>0$ and $P(A=b)>0$ , since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every $z$ selects a version and does not change the attainable disparities. On a cell with $P(\hat Y=\hat y\mid Z=z)=0$ , weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.

The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.

Selected references

Nathan Kallus, Xiaojie Mao, and Angela Zhou, Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination, Management Science 68(3), 2022; preprint arXiv:1906.00285v2, 2020. Pinned preprint.

8 thms3 active usersReviewed

Completed

Markov Chain Operations Research Reinforcement Learning·Captain: mikedeng1

A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximation: Projected TD(0) Under Markov Chain Sampling Converges at Mixing-Time-Scaled RatesResearch Paper

Motivation

Temporal-difference (TD) learning is the basic algorithm of reinforcement learning for estimating the value function of a fixed policy from a single stream of experience. With a linear function approximation $V_\theta(s)=\phi(s)^\top\theta$ , TD(0) is the evaluation step inside many policy-iteration and actor–critic methods, and its behaviour governs how much data such methods need.

The asymptotic theory is classical. Tsitsiklis and Van Roy (1997) proved that TD(λ) with linear features converges almost surely along a single trajectory of an ergodic Markov chain, to the unique solution $\theta^*$ of the projected Bellman equation, under Robbins–Monro step sizes. Their proof uses the ODE method, which says nothing about how fast the iterates approach $\theta^*$ , nor how the rate depends on the step size, on the conditioning of the features, or on how quickly the chain mixes.

Finite-time results came later and mostly for independent samples. Dalal, Szörényi, Thoppe and Mannor (2018) and Lakshminarayanan and Szepesvári (2018) analysed TD(0) when the observed transitions are drawn i.i.d. from the stationary distribution. Bhandari, Russo and Singal (2018) gave a short analysis in the i.i.d. model and, for a projected variant of TD, the first finite-time bounds when the transitions come from one trajectory of the Markov chain, so that consecutive observations are strongly correlated. This mission formalizes that Markovian result, Theorem 3 of the paper.

Setting

A finite Markov reward process consists of a finite state space $S$ , a stochastic matrix $P$ with $P(s,s')$ the probability of moving from $s$ to $s'$ , transition rewards $R(s,s')$ with $|R(s,s')|\le r_{\max}$ , and a discount factor $0\le\gamma<1$ . The chain has a stationary distribution $\pi$ ( $\pi P=\pi$ ), and the observed trajectory $s_0,s_1,\dots$ starts from $\pi$ , so it is a stationary sequence.

Each state carries a feature vector $\phi(s)\in\mathbb{R}^d$ with $\|\phi(s)\|_2\le1$ . The steady-state feature covariance $\Sigma=\sum_s\pi(s)\phi(s)\phi(s)^\top$ has full rank, and $\omega>0$ is its minimum eigenvalue. Value functions are compared in the steady-state seminorm $\|V_\theta\|_D^2=\sum_s\pi(s)(\phi(s)^\top\theta)^2$ .

At a transition $(s,s')$ the TD direction is $g(\theta;s,s')=\big(R(s,s')+\gamma\phi(s')^\top\theta-\phi(s)^\top\theta\big)\phi(s)$ . Its steady-state mean is $\bar g(\theta)=\sum_{s,s'}\pi(s)P(s,s')\,g(\theta;s,s')$ , and the TD fixed point $\theta^*$ is the vector with $\bar g(\theta^*)=0$ . Projected TD(0) with radius $R\ge\|\theta^*\|_2$ starts from $\|\theta_0\|_2\le R$ and iterates

\theta_{t+1}=\Pi_{2,R}\big(\theta_t+\alpha_t\,g(\theta_t;s_t,s_{t+1})\big),

where $\Pi_{2,R}$ is the Euclidean projection onto the ball of radius $R$ . The averaged iterate is $\bar\theta_T=T^{-1}\sum_{t=0}^{T-1}\theta_t$ .

The chain mixes uniformly (Assumption 1): there are $m>0$ and $\rho\in(0,1)$ with $\sup_s d_{TV}(P^t(s,\cdot),\pi)\le m\rho^t$ for all $t\ge0$ . The mixing time is $\tau_{\mathrm{mix}}(\epsilon)=\min\{t\ge0: m\rho^t\le\epsilon\}$ . Write $G=r_{\max}+2R$ .

Formalization targets

Goal: Theorem 3 (pp. 17–18)

All three bounds are stated together, with $\mathbb{E}$ the expectation over the stationary trajectory:

(a) for $T\ge1$ and $\alpha_t\equiv1/\sqrt T$ ,

\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{\|\theta^*-\theta_0\|_2^2+G^2\big(9+12\tau_{\mathrm{mix}}(1/\sqrt T)\big)}{2\sqrt T(1-\gamma)};

(b) for a constant $\alpha_t\equiv\alpha_0\in\big(0,\,1/(2\omega(1-\gamma))\big)$ ,

\mathbb{E}\|\theta^*-\theta_T\|_2^2\le e^{-2\alpha_0(1-\gamma)\omega T}\|\theta^*-\theta_0\|_2^2+\alpha_0\frac{G^2\big(9+12\tau_{\mathrm{mix}}(\alpha_0)\big)}{2(1-\gamma)\omega};

(c) for $\alpha_t=1/(\omega(t+1)(1-\gamma))$ and $T\ge1$ ,

\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{G^2\big(9+24\tau_{\mathrm{mix}}(\alpha_T)\big)}{T(1-\gamma)^2\omega}(1+\log T).

Milestones

The milestones are the paper's own lemmas, in the order the proof in Appendix A uses them: norm equivalence $\sqrt\omega\|\theta\|_2\le\|V_\theta\|_D\le\|\theta\|_2$ (Lemma 1); the descent inequality $(\theta^*-\theta)^\top\bar g(\theta)\ge(1-\gamma)\|V_{\theta^*}-V_\theta\|_D^2$ (Lemma 3); the gradient bound $\|g_t(\theta)\|_2\le r_{\max}+2\|\theta\|_2$ (Lemma 6); the pathwise error recursion (Lemma 8); the coupling bound $|\mathbb{E}v(X,Y)-\mathbb{E}v(X',Y')|\le2\|v\|_\infty m\rho^\tau$ (Lemma 9); boundedness and Lipschitz continuity of the gradient error $\zeta_t$ (Lemma 10); and the bias bound $\mathbb{E}[\zeta_t(\theta_t)]\le G^2(4+6\tau_{\mathrm{mix}}(\alpha_T))\alpha_{t^*}$ (Lemma 11).

Significance

Theorem 3 gives explicit, non-asymptotic mean-squared-error bounds for TD(0) with linear features under Markovian sampling. Part (a) does not depend on the conditioning $\omega$ , part (b) shows exponential convergence to a neighbourhood whose radius scales with $\alpha_0G^2\tau_{\mathrm{mix}}(\alpha_0)$ , and part (c) gives an $\tilde O(1/T)$ rate. Compared with the i.i.d. bounds, the only change is a factor of order $\tau_{\mathrm{mix}}$ : roughly, one mixing time of correlated observations is worth one independent sample. The same argument carries over, in the paper itself, to projected TD(λ) (Theorem 4) and to Q-learning for optimal stopping (§10), so the lemmas formalized here are the core of all of its Markovian results.

The result is proved on paper but has not been machine-checked. The mission provides a Lean statement of the theorem and of each lemma of its proof, all built on one model. The trajectory-level definitions (path law, total-variation mixing, mixing time, projected iterates) can be reused by later formalizations of Markovian stochastic approximation.

Difficulty

The obvious approach, from the i.i.d. analysis, takes expectations in the error recursion of Lemma 8 and uses $\mathbb{E}[\zeta_t(\theta_t)]=0$ . Under Markov sampling this fails: $\theta_t$ is a function of $s_0,\dots,s_t$ and is correlated with the observation $(s_t,s_{t+1})$ at which it is evaluated, so the gradient is biased and the noise is not a martingale difference. Bounding that bias needs a quantitative decorrelation between the iterate $\tau$ steps back and the current observation, which is a total-variation estimate on the joint law of a path (Lemma 9). It also needs control of how far the iterates drift in $\tau$ steps, which is where the projection and the uniform gradient bound $G$ enter. The rest of the proof then combines telescoping, a geometric recursion and harmonic sums, with every constant ( $9+12\tau$ , $9+24\tau$ ) tracked exactly.

Formalization scope

State space and expectation. $S$ is a Fintype. The expectation over the stationary trajectory is the finite sum $\sum_{w\in S^{T+1}}\pi(w_0)\prod_iP(w_i,w_{i+1})\,F(w)$ , the exact law of $(s_0,\dots,s_T)$ for a finite chain started from $\pi$ , so no measure theory is used. The paper itself works with a finite $S$ (p. 5).
Coupling lemma. Lemma 9 uses probability measures for the conditional laws of $X,Y$ given $s_t,s_{t+\tau}$ ; their factorization expresses $X\to s_t\to s_{t+\tau}\to Y$ . The variables may take values in arbitrary measurable spaces, including the iterates and observations used in the proof.
Norms. Parameters and features live in EuclideanSpace ℝ (Fin d) with $d\ge1$ , so every $\|\cdot\|$ is Euclidean.
Standing hypotheses, added or made explicit: $0\le\gamma$ (the paper writes $\gamma<1$ ; the proof of Lemma 3 needs $\gamma\ge0$ ). $\omega$ is the least value of $\theta^\top\Sigma\theta$ on the unit sphere, that is $\lambda_{\min}(\Sigma)$ , together with $\omega>0$ (full rank). $\pi$ is a stationary probability vector, and no separate irreducibility hypothesis is added, since Assumption 1 implies ergodicity. $\theta^*$ is given as a vector with $\bar g(\theta^*)=0$ . The implicit conditions are explicit: $T\ge1$ in (a) and (c), $\alpha_0>0$ in (b), $\alpha_T>0$ in Lemma 11, and $\alpha_t\ge0$ in Lemma 8.
Conventions. $\Pi_{2,R}$ is defined by the rescaling formula of p. 16. $\bar\theta_T$ averages $\theta_0,\dots,\theta_{T-1}$ , as in the text and the proof (Algorithm 1's averaging recursion is a slip). $\tau_{\mathrm{mix}}$ is sInf over $\mathbb{N}$ and is only evaluated at positive thresholds, where it is a true minimum. "With probability 1" is stated for every path or transition.
No trivialization. The expectation must start from $\pi$ , never from an arbitrary state. $\theta_t$ and the observation must come from the same trajectory. $\omega$ must be $\lambda_{\min}(\Sigma)$ , not an arbitrary positive constant, since it fixes the step size in (c). A formalization with independent samples, with the sup norm on $\mathbb{R}^d$ , or with a junk-valued $\tau_{\mathrm{mix}}(0)=0$ would prove a different statement.
Not in scope. Theorem 1 (mean-path TD), Theorem 2 (i.i.d. model), Theorem 4 (projected TD(λ)) and §10 (Q-learning for optimal stopping) are separate results. Theorem 3's proof does not use them.
Welcome contributions. Proofs of the milestones, and general lemmas on finite path sums (marginalisation of the trajectory law, the variational form of total variation, nonexpansiveness of the ball projection).

Selected references

J. Bhandari, D. Russo, R. Singal, A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximation, arXiv:1806.02450v2, 2018; Operations Research 69(3), 2021. https://arxiv.org/abs/1806.02450
J. N. Tsitsiklis, B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
G. Dalal, B. Szörényi, G. Thoppe, S. Mannor, Finite Sample Analyses for TD(0) with Function Approximation, AAAI 2018. https://arxiv.org/abs/1704.01161
C. Lakshminarayanan, C. Szepesvári, Linear Stochastic Approximation: How Far Does Constant Step-Size and Iterate Averaging Go?, AISTATS 2018. http://proceedings.mlr.press/v84/lakshminarayanan18a.html
R. S. Sutton, Learning to Predict by the Methods of Temporal Differences, Machine Learning 3, 1988. https://doi.org/10.1007/BF00115009
D. A. Levin, Y. Peres, Markov Chains and Mixing Times, 2nd ed., AMS, 2017. https://doi.org/10.1090/mbk/107

10 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Private Sequential Learning: The Query Complexity of an (ϵ, δ, L)-Private Learner Lies Between max{log(1/ϵ), log(δ/ϵ) + 2L − 4} and log(1/(Lϵ)) + 2LResearch Paper

Motivation

A learner wants to locate an unknown number, the true value $v^* \in [0,1)$ , by asking threshold questions of a database: each query $q$ is answered by the single bit $\mathbb I(v^* \ge q)$ . Bisection finds $v^*$ to within $\epsilon/2$ with $\lceil \log_2(1/\epsilon) \rceil$ queries, and no strategy does better (Waeber, Frazier and Henderson, 2013). Bisection, however, reveals everything: each query is a function of the previous answers, so anyone who sees the queries can reconstruct the answers and hence $v^*$ .

Tsitsiklis, Xu and Xu study a learner whose queries, but not the answers, are watched by an adversary. Their motivating examples (pp. 2–3) are a firm testing prices whose surveys a competitor can observe, a consumer browsing products on a platform that sees what is browsed, and an optimizer whose test points are visible to the database it queries. The question is how many queries the learner needs if she must find $v^*$ accurately while keeping the adversary uncertain about it.

The model is from the authors' COLT 2018 extended abstract and Z. Xu's master's thesis (MIT, 2017); the journal version appeared in Operations Research (2021). This mission formalizes arXiv version 3 (26 Feb 2020), and all page and theorem numbers refer to it.

Setting

The learner submits $N$ queries one at a time. A random seed $Y$ , uniform on $\{1, \dots, \bar Y\}$ , lets her randomize. A learner strategy $\phi$ of length $N$ consists of query maps $\phi_k$ and an estimation map $\phi^E$ (§2.1, p. 8): the $k$ -th query is $q_k = \phi_k(r_1, \dots, r_{k-1}, Y) \in [0,1)$ , where $r_i = \mathbb I(v^* \ge q_i)$ are the responses so far, and the estimate is $\hat x = \phi^E(r_1, \dots, r_N, Y) \in [0,1)$ . The class $\Phi_N$ consists of the strategies of length $N$ that submit pairwise distinct queries. Write $\bar q(x,y)$ for the queries and $\hat x(x,y)$ for the estimate when $v^* = x$ and $Y = y$ .

The adversary knows $\phi$ and sees $\bar q$ . The set of query sequences that can occur when $v^* = x$ is $\mathcal Q(x) = \{\bar q(x,y) : y\}$ (eq. (1)), and the adversary's information set is

\mathcal I(\bar q) = \{x \in [0,1) : \bar q \in \mathcal Q(x)\} \qquad \text{(Definition 3.1, p. 9).}

Its size is measured by the $\delta$ -cover number $C_\delta(E)$ , the least number of closed intervals of length at most $\delta$ whose union contains $E$ (Definition 3.2, p. 10). A strategy is $(\epsilon, \delta, L)$ -private (Definition 3.3, p. 10) if

it is accurate: $|\hat x(x,y) - x| \le \epsilon/2$ for every $x \in [0,1)$ and every seed $y$ ; and
it is private: $C_\delta(\mathcal I(\bar q)) \ge L$ for every $x \in [0,1)$ and every $\bar q \in \mathcal Q(x)$ .

The query complexity is $N^*(\epsilon, \delta, L) = \min\{N : \Phi_N \text{ contains an } (\epsilon,\delta,L)\text{-private strategy}\}$ (eq. (5), p. 11). All logarithms are base 2 and are rounded up (footnote 1, p. 4).

Formalization targets

Goal: Theorem 4.1 (p. 12)

For $\epsilon > 0$ , $\delta > 0$ and an integer $L \ge 2$ with $2\epsilon < \delta \le 1/L$ ,

\max\left\{ \left\lceil \log_2 \tfrac1\epsilon \right\rceil,\ \left\lceil \log_2 \tfrac\delta\epsilon \right\rceil + 2L - 4 \right\} \le N^*(\epsilon,\delta,L) \le \left\lceil \log_2 \tfrac{1}{L\epsilon} \right\rceil + 2L.

Upper bound (§6)

The Opportunistic Bisection (OB) strategy first places $L$ "guesses" $[i/L, i/L+\epsilon)$ with $2L$ fixed queries, and then runs a bisection of $\lceil \log_2(1/(\epsilon L)) \rceil$ steps in one of the gaps. The bisection is truthful if no guess caught $v^*$ , and driven by the seed otherwise. The milestones are: OB is accurate; the union of guesses $\mathcal G$ has $C_\delta(\mathcal G) \ge L$ (Claim 6.3); $\mathcal G \subseteq \mathcal I(\bar q)$ for every observable $\bar q$ (Claim 6.4); the cover number is monotone; and OB is $(\epsilon,\delta,L)$ -private (Proposition 6.2).

Lower bound (§7)

For an accurate strategy, the final interval between consecutive sorted queries (with $q_0 = 0$ , $q_{N+1} = 1$ ) has length at most $\epsilon$ (§7.1), so $\mathcal I(\bar q) \subseteq \bar{\mathcal I}(\bar q)$ , the union of special intervals (display (20)). Lemma 7.1 puts $\lceil \log_2(\delta/\epsilon) \rceil$ queries in $(0,\delta)$ for some true value, and accuracy alone gives $N \ge \lceil \log_2(1/\epsilon) \rceil$ . A covering bound gives $C_\delta(\bar{\mathcal I}(\bar q)) \le (K+3)/2$ , with $K$ the number of special queries in $[\delta, 1]$ (p. 21). Together these give $N \ge \lceil \log_2(\delta/\epsilon) \rceil + 2L - 4$ for every private strategy.

Corollary 4.2 (the case $\delta = 1/L$ ) is Theorem 4.1 specialized and is not posed separately.

Significance

The result. The theorem gives the cost of privacy in this model up to an additive constant. At $\delta = 1/L$ the two bounds differ by at most 4 (Corollary 4.2), and the extra cost over plain bisection is at most an additive $2L$ . That is much less than the non-adaptive $\epsilon$ -dense strategy, which is always private but needs about $1/\epsilon$ queries (§5). The lower bound also shows that the $2L$ obfuscating queries cannot be shared with the queries that locate $v^*$ (§7, p. 19).

Formalizing it. The result is proved on paper, but Lemma 7.1 is given only an intuitive argument: the paper calls its proof "fairly standard" and omits it (p. 20). The covering step on p. 21 is argued component by component, with an exceptional component straddling $\delta$ . A formal development supplies both and checks the bookkeeping behind the constants $-4$ , $+3$ and $2L - 3$ . To our knowledge, no machine-checked proof of this theorem or of the bisection lower bound in this form exists.

Difficulty

The upper bound is a construction. Its delicate point is Claim 6.4. For every point $g$ of every guess one must exhibit a seed under which $g$ produces exactly the observed queries, and that seed differs according to whether the observed run was truthful or fictitious.

The lower bound is harder. Counting queries is not enough by itself, because the obvious argument conflates query values with query indices. Lemma 7.1 counts indices along a single run (a fixed true value and seed). The covering bound counts distinct values in $[\delta,1]$ , one of which may be the artificial point $1$ . The natural first idea, a direct counting bound on $N^*$ , is unavailable: $N^*$ is a minimum, so a lower bound must be proved for every private strategy of every length. Only the goal speaks about $N^*$ , where the upper bound shows the set being minimized is nonempty.

Formalization scope

Everything lives in the namespace PrivSeqLearn.QueryComplexity, built on Mathlib with no measure theory in any statement. Conventions:

The seed space is Fin Ybar with 0 < Ybar. "Positive probability" is read as "for some seed" and "probability one" as "for every seed", which is exact for a uniform seed on a finite set.
Response histories are List Bool, and the response to $q$ at true value $x$ is decide (q ≤ x). Queries are 0-indexed (Fin N).
$\Phi_N$ (InPhi) requires query values on every history of length $< N$ and estimate values on every history of length $N$ to lie in $[0,1)$ , and the queries to be pairwise distinct for every $x \in [0,1)$ and seed.
Covers are Fin L-indexed families of closed intervals Set.Icc. $C_\delta$ and $N^*$ are sInf over $\mathbb N$ , which equals the minimum when the set is nonempty.
Every logarithm term is ⌈Real.logb 2 ·⌉ computed in $\mathbb Z$ , so $2L - 4$ never truncates. In the regime, all log arguments exceed 1.
The OB seed is $\{0, \dots, L \cdot 2^M - 1\}$ , decoded as the gap $\tilde{\mathcal J}$ and the bits $Z_1, \dots, Z_M$ . The OB estimate, specified in the paper only inside the proof of Proposition 6.2, is the guess mid-point or the mid-point of the final bisection interval.
Disclosed deviations from the page:
- Lemma 7.1 assumes $\delta \le 1$ .
- The lower-bound milestones do not assume distinct queries, which is a strengthening.
- The OB-only milestones use $2\epsilon < 1/L$ in place of $2\epsilon < \delta \le 1/L$ .
- Cover-number monotonicity assumes a bounded superset.

Trivializing encodings are ruled out:

an empty seed space is excluded by 0 < Ybar;
information sets range over $[0,1)$ only;
privacy is required for every true value and every observable query sequence;
OB is the constructed strategy, not "some strategy".

Contributions are welcome on any milestone. The bisection lower bounds (Lemma 7.1 and the $\log_2(1/\epsilon)$ bound) and the interval-covering facts are reusable beyond this mission.

Selected references

J. N. Tsitsiklis, K. Xu, Z. Xu, Private Sequential Learning, arXiv:1805.02136v3, 2020; Operations Research, 2021. https://arxiv.org/abs/1805.02136
R. Waeber, P. I. Frazier, S. G. Henderson, Bisection search with noisy responses, SIAM Journal on Control and Optimization 51(3):2261–2279, 2013. https://doi.org/10.1137/120861898
M. Horstein, Sequential transmission using noiseless feedback, IEEE Transactions on Information Theory 9(3):136–143, 1963. https://doi.org/10.1109/TIT.1963.1057832
Z. Xu, Private sequential search and optimization, Master's thesis, MIT, 2017. http://hdl.handle.net/1721.1/112054

15 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Dynamic Incentive-Aware Learning: Robust Pricing in Contextual Auctions: Against Utility-Maximizing Buyers the CORP Policy Has Regret O(Nd(log(Td) log T + log²T / log²(1/γ)))Research Paper

Motivation

Display advertising is sold one impression at a time, mostly through second-price auctions with reserve prices. A reserve tailored to each buyer and to the features of the impression can raise the seller's revenue considerably, but the right reserve depends on the buyers' valuations, which the seller does not know and must learn from past auctions. The buyers participate in the same exchange day after day and know that their bids feed the seller's learning, so a patient buyer may bid untruthfully today to obtain lower reserves tomorrow. Learning reserve prices from strategic buyers is therefore a joint problem of statistics and incentives.

Golrezaei, Javanmard and Mirrokni (arXiv:2002.11137, Operations Research 69(1), 2021) study this problem in a contextual model and propose the policy CORP (Contextual Robust Pricing). Earlier work on learning against strategic buyers considered a single buyer facing posted prices, without contexts: Amin, Rostamizadeh and Syed (NeurIPS 2013) introduced the discounted strategic buyer, and contextual and revenue-optimization variants followed (Amin, Rostamizadeh and Syed, NeurIPS 2014; Mohri and Muñoz Medina, NeurIPS 2015). Personalized reserves in second-price auctions were studied by Paes Leme, Pál and Vassilvitskii (2016). The present paper treats many buyers, personalized reserves, contexts in $\mathbb R^d$ and censored observations (the seller sees who won, not the valuations).

Setting

In every period $t=1,2,\dots$ the seller observes a feature vector $x_t\in\mathbb R^d$ , drawn i.i.d. from a law $\mathcal D$ supported in the unit ball. Each of $N$ buyers has the valuation

v_{it}=\langle x_t,\beta_i\rangle+z_{it},

where $\beta_i\in\mathbb R^d$ is an unknown preference vector with $\|\beta_i\|\le B_p$ and the noises $z_{it}$ are i.i.d. with a known density $f$ on $[-B_n,B_n]$ , mean zero, and distribution function $F$ . Assumption 1 asks $F$ and $1-F$ to be log-concave on $[-B_n,B_n]$ .

Each period runs a lazy second-price auction with personalized reserves $r_{it}$ : the highest bidder $i^\star$ gets the item if $b_{i^\star t}\ge r_{i^\star t}$ and pays $\max\{r_{i^\star t},\max_{j\neq i^\star}b_{jt}\}$ ; nobody else pays. The benchmark knows the $\beta_i$ and sets $r^\star_i(x)=\arg\max_y y\,(1-F(y-\langle x,\beta_i\rangle))$ (4); its expected revenue against truthful buyers is $\mathrm{rev}^\star_t$ (5).

CORP works in episodes $E_k=\{\ell_k,\dots,\ell_{k+1}-1\}$ with $\ell_k=2^{k-1}$ . At the start of episode $k$ it computes, for each buyer, a maximum-likelihood estimate $\hat\beta_{ik}$ over $\|\beta\|\le B_p$ from the censored outcomes of episode $k-1$ (8)–(9). In each period of episode $k$ , with probability $1/\ell_k$ it explores: one uniformly chosen buyer is offered the item at a price uniform on $[0,B_p+B_n]$ . Otherwise it exploits with reserves $r_{it}=\arg\max_y y\,(1-F(y-\langle x_t,\hat\beta_{ik}\rangle))$ (10).

Buyer $i$ 's bid may depend on his own history of valuations, bids, allocations and payments, on $x_t$ , on $v_{it}$ and on private randomness. His utility is $\sum_t\gamma^t\,\mathbb E[v_{it}q_{it}-p_{it}]$ with a discount factor $\gamma\in(0,1)$ , and buyers are utility-maximizing. The regret after $T$ periods is $\sum_{t=1}^T(\mathrm{rev}^\star_t-\mathrm{rev}_t)$ , worst case over $\beta$ and $\mathcal D$ (7).

Formalization targets

Goal: Theorem 4.1 (p. 23)

There is $C$ , depending only on $B_p,B_n,M,f,c_{\min},c_{\max}$ , such that for all $N,d\ge1$ , $T\ge2$ , $\gamma\in(0,1)$ , all admissible $\mathcal D,\beta$ and all utility-maximizing buyers,

\mathrm{Regret}(T)\le C\,N d\Big(\log(Td)\log T+\frac{\log^2T}{\log^2(1/\gamma)}\Big).

Milestones, in the order the proof uses them

Proposition 3.1 (p. 15): the reserves (4) are revenue-optimal against truthful buyers.
Lemma 1 (p. 56): the conditional revenue $W_{it}$ is flat at $r^\star_{it}$ and has a bounded second derivative.
Lemma 2 (p. 56): $|r^\star_{it}-r_{it}|\le|\langle x_t,\beta_i-\hat\beta_{ik}\rangle|$ .
Lemma 3 (p. 57): the second-highest bid and the competing bid move by at most the shading and overbidding.
Proposition 9.2 (p. 53): per episode, a utility-maximizing buyer lies $O(\log(\ell/\delta)+\log(\ell N)/\log(1/\gamma))$ times, and his total shading and overbidding are $O(\log(\ell N)/\log(1/\gamma))$ , with high probability.
Corollary 18.2 (p. 88): the vector Freedman inequality.

Significance

If true, Theorem 4.1 says that a seller can learn personalized, contextual reserves from censored data at a cost logarithmic in $T$ and linear in $Nd$ , even when buyers manipulate their bids. The strategic term vanishes as buyers become impatient. The episodic delay between a bid and its effect on reserves, together with the random exploration prices, is what makes untruthful bidding unprofitable. The lemmas are of independent use. Proposition 3.1 and Lemma 2 concern the monopoly price under log-concave noise. Lemma 3 is a deterministic fact about second-price auctions. Corollary 18.2 is a vector concentration inequality.

Status. None of these results is machine-checked anywhere known to us. The paper's printed proof has gaps. Proposition 9.1 (p. 52), which bounds the estimation error of the MLE by the number of lies, fails as printed. With uniform noise a single lie per episode keeps the estimate a constant distance from $\beta_i$ . Its supporting Lemma 5 uses a constant $u_F$ that is infinite for every compactly supported $F$ (p. 71). Its curvature bound (89) also fails when a likelihood term leaves the support of $f$ . Lemma 6 (p. 76) conditions on an event the exploration lottery itself moves. A proof of Theorem 4.1, or a counterexample to it, would settle the question. The goal is stated as the paper states it, and is neither asserted nor denied here.

Difficulty

The natural route is the paper's. First bound the estimation error of the censored MLE in terms of the number of lies. Then bound the number of lies by comparing a lie's discounted future gain with its immediate loss under the exploration lottery. Finally sum over episodes.

The first step is where it breaks. With noise supported on $[-B_n,B_n]$ , an observation whose threshold falls outside the support carries no curvature. Its likelihood term is constant or $+\infty$ , so the minimizer of (9) is in general a set, not a point. A minimizer at the wrong end of that set can keep the reserve below the benchmark for many episodes, even with truthful buyers. Any proof must say which minimizer CORP takes, or show that all of them work. The second step must handle buyers who react to one another through their histories; the paper's proof holds the other buyers' bids fixed. The concentration steps need a vector martingale inequality and a covariance concentration bound, neither of which is in Mathlib.

Formalization scope

Lean represents features as EuclideanSpace ℝ (Fin d) and buyers as Fin N. Periods are indexed from $0$ internally (Lean's $n$ is the paper's $t=n+1$ ), and episodes likewise (Lean's $e$ is the paper's $k=e+1$ , so $\ell_k=2^e$ ). Period $1$ always explores. The per-period randomness consists of the features, the noises, the exploration coin, the chosen buyer, the exploration price and the buyers' seeds. It is independent across periods, under Measure.infinitePi, and the play is defined by recursion over periods. The likelihood (9) takes values in $[0,+\infty]$ with $-\log 0=+\infty$ ; a real-valued Real.log would make impossible observations free and change the estimator. The estimator (8) and the reserve rule (10) are arbitrary measurable selections of the argmin and argmax, quantified universally. No tie-break or uniqueness is added. The same reserve rule defines the benchmark (4).

Standing assumptions and added hypotheses.

The noise density is continuous on $[-B_n,B_n]$ , with mass one and mean zero, and Assumption 1 holds.
$\|x\|\le1$ almost surely, and $c_{\min}/d\,\|u\|^2<\mathbb E\langle x,u\rangle^2\le c_{\max}/d\,\|u\|^2$ ; the proof uses these eigenvalue bounds (pp. 57, 72–73).
Bids are at most $M$ (p. 14) and pairwise distinct almost surely (p. 20).
Strategies and selections are measurable, $N,d\ge1$ and $T\ge2$ .
Utility-maximizing is pinned as the inequality the proof uses on p. 77: no buyer gains by switching to truthful bidding from the start of any episode on. Every best-response profile satisfies it, and the all-truthful profile does too.
Exploration is a posted price to the chosen buyer.
Lemma 1 adds $f\in C^1(\mathbb R)$ , which its proof uses.
Lemma 2 adds that both indices exceed $-B_n$ ; without that, the argmax is unbounded.
Lemma 3's (45) adds that another buyer wins; as printed it fails when nobody wins.
Corollary 18.2 adds $u_0=0$ .

Ruled out. The constant $C$ comes before every instance, horizon, selection and strategy, so a bound depending on $T$ or on the instance does not count. The policy is CORP as defined, not any reserve-setting rule. The rationality hypothesis is satisfiable.

Infrastructure. A complete development needs the following.

Measurability of the recursive play.
The monopoly price under log-concavity (Proposition 3.1, Lemma 2).
Censored-likelihood estimation with compactly supported noise.
A vector Freedman inequality (Corollary 18.2, reusable).
Covariance concentration for bounded vectors.

Contributions on any milestone are welcome. So is a formal counterexample to the goal in the model as stated, for example with one truthful buyer, uniform noise and the smallest minimizer of (9).

Out of scope. CORP-II and SCORP (Theorems 5.1–5.3, Propositions 11.1–11.2) and the extensions of Appendix 8 are not part of this mission. Proposition 9.1, Lemma 5, Lemma 6 and Theorem 18.1 are not posed (see Significance).

Selected references

N. Golrezaei, A. Javanmard, V. Mirrokni, Dynamic Incentive-Aware Learning: Robust Pricing in Contextual Auctions, Operations Research 69(1), 2021; read as arXiv:2002.11137v1. https://arxiv.org/abs/2002.11137
K. Amin, A. Rostamizadeh, U. Syed, Learning Prices for Repeated Auctions with Strategic Buyers, NeurIPS 2013. https://papers.nips.cc/paper/2013/hash/1e6e0a04d20f50967c64dac2d639a577-Abstract.html
R. Paes Leme, M. Pál, S. Vassilvitskii, A Field Guide to Personalized Reserve Prices, WWW 2016. https://doi.org/10.1145/2872427.2883071
J. A. Tropp, Freedman's inequality for matrix martingales, Electronic Communications in Probability 16, 2011. https://doi.org/10.1214/ECP.v16-1624
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

10 thms3 active usersReviewed

Completed

Markov Chain Operations Research Reinforcement Learning·Captain: mikedeng1

Nonstationary Reinforcement Learning: The Blessing of (More) Optimism II: Per-Step Dynamic Regret of SWUCRL2-CW When the Widened Confidence Region Contains an MDP of Diameter at Most DResearch Paper

Why changing environments matter

A reinforcement-learning agent chooses actions while learning how those actions affect future states. In a stationary model, observations collected long ago remain relevant to the current transition law. In a nonstationary Markov decision process, rewards and transition probabilities may change at each round. Old observations can then bias an estimate even when the agent has collected many samples. The challenge is to keep learning from recent observations without becoming blind to actions that the agent has not tried recently. Cheung, Simchi-Levi and Zhu study this tension for finite-state average-reward learning and introduce confidence widening in their SWUCRL2-CW algorithm Cheung et al., §4.

The paper's broad regret theorems suppress constants inside asymptotic notation. Proposition 2 gives an explicit one-round inequality that exposes the roles of estimation error, temporal variation, confidence widening, and the diameter of a plausible transition model. This mission targets that proposition and the stated auxiliary results used around it Cheung et al., pp. 14, 38–41.

The finite changing MDP

Let $\mathcal S$ be a finite state set. Each state $s$ has a nonempty finite set $\mathcal A_s$ of permitted actions. At round $t$ , taking action $a\in\mathcal A_s$ in state $s$ gives expected reward $r_t(s,a)\in[0,1]$ and moves to state $s'$ with probability $p_t(s'\mid s,a)$ . The one-step variation $B_{r,t}$ is the greatest change $|r_{t+1}(s,a)-r_t(s,a)|$ over permitted pairs; $B_{p,t}$ is the corresponding greatest $\ell_1$ distance between transition rows. These definitions make no stationarity assumption Cheung et al., pp. 6, 33.

At the start $\tau(m)$ of an episode, the algorithm counts visits to each pair in a recent window of length $W$ . It divides empirical sums by $N^+=\max\{1,N\}$ , where $N$ is the visit count. Thus an unvisited pair has estimated reward and transition vector equal to zero. Reward confidence sets lie in $[0,1]$ ; transition confidence sets lie in the probability simplex and use an $\ell_1$ radius enlarged by a nonnegative parameter $\eta$ . Write $\operatorname{rad}_{r,\tau(m)}(s,a)$ and $\operatorname{rad}_{p,\tau(m)}(s,a)$ for their respective radii. The algorithm chooses a stationary policy $\tilde\pi_{\tau(m)}$ and an optimistic model, gain $\tilde\rho_{\tau(m)}$ , and bias $\tilde\gamma_{\tau(m)}$ from extended value iteration Cheung et al., pp. 11–13.

The diameter of a transition model is the largest, over ordered source and target states, of the smallest expected number of transitions needed to reach the target under a stationary policy. Source equal to target means a return time after at least one transition. The round- $t$ optimal gain $\rho_t^*$ is the value of the stationary occupancy-measure linear program for $(r_t,p_t)$ with only permitted actions. From the window's first round through the round before $t$ , let $\operatorname{var}_{r,t}$ and $\operatorname{var}_{p,t}$ be the sums of the corresponding one-step variations Cheung et al., pp. 8, 14, 33.

Formalization targets

The main target is Proposition 2. Condition on the local reward and transition estimation events at $\tau(m)$ . Assume that the widened transition confidence sets contain every permitted row of an MDP of diameter at most $D$ . For a round in which $a_t=\tilde\pi_{\tau(m)}(s_t)$ , the target is

\begin{aligned} \rho_t^*-r_t(s_t,a_t)\le{}&\sum_{s'}p_t(s'\mid s_t,a_t)\tilde\gamma_{\tau(m)}(s')-\tilde\gamma_{\tau(m)}(s_t)+\frac1{\sqrt{\tau(m)}}\\ &+2\operatorname{var}_{r,t}+4D(\operatorname{var}_{p,t}+\eta)\\ &+2\operatorname{rad}_{r,\tau(m)}(s_t,a_t)+4D\operatorname{rad}_{p,\tau(m)}(s_t,a_t). \end{aligned}

The five milestones are the paper's Lemmas 2–5 and displayed inequality (32): a dual-bias span bound, a drift estimate for window averages, bounded optimistic bias, optimism under drift, and a transition-value error bound. Their exact constants are part of the targets Cheung et al., pp. 33, 38–39.

What the result supplies

Proposition 2 separates the per-round change in optimal gain from the cost of the current action. Its first term tracks changes in the optimistic bias along transitions; the other terms identify window drift, reward and transition estimation, and widening. This decomposition can be summed across episodes when analyzing the algorithm. The result has a concrete role even though the later horizon-wide theorem is given in asymptotic notation Cheung et al., pp. 14, 41.

The paper proves these claims mathematically. The mission asks for machine-checked proofs of the explicit statements and for reusable definitions of finite nonstationary MDP variation, window estimators, confidence sets, occupancy gain, and hitting-time diameter. The source's Theorems 1–4 are not posed here: their displayed bounds hide constants in $\widetilde O(\cdot)$ and, in one case, use an unspecified $O(\delta)$ failure probability Cheung et al., pp. 14–25. This proposal supplies statements for solvers; it does not claim that these new statements already have machine-checked proofs.

Where the difficulty lies

The current model need not resemble the model that generated every observation in the window. A direct stationary confidence argument cannot control the resulting temporal error. The challenge is especially visible at a pair with no recent visits: its comparison transition vector is zero, although a genuine transition row has total mass one. The paper's Lemma 3, read literally for every pair, fails in that case. The mission states its positive-count condition explicitly while keeping the proposition and the later optimism and transition milestones valid at unvisited pairs Cheung et al., pp. 12, 38–40.

There is a separate issue with the printed dual-bias lemma. Feasibility alone permits an arbitrarily large dual gain and does not force the asserted $2D$ span bound. The mission adds $\rho\le2$ to Lemma 2 and records the change for audit. The EVI output is represented by its selected-model membership, bias normalization, optimism, and near-optimality properties; this is the contract stated for the algorithm's output, rather than a formal execution of extended value iteration Cheung et al., pp. 13, 33, 35–36.

Formalization scope

States and ambient actions are Fin S and Fin A; permitted actions are state-dependent finite subsets. The setup has $S>1$ , $0<\delta<1$ , $\eta\ge0$ , and a nonempty action set at each state. Time is zero-based in Lean, while the paper's rounds are one-based; in particular its $1/\sqrt{\tau(m)}$ is represented by $1/\sqrt{\tau_m+1}$ . Counts and confidence sets are evaluated at the episode start. Variations continue up to the target round. The estimation events are assumed at the episode start, which is the only time used by these statements.

Hitting times and diameter take values in extended nonnegative reals, so an unreachable target does not acquire a false finite diameter. The diameter includes return times and minimizes over deterministic stationary policies. The confidence-radius product $SA$ counts actual permitted pairs. At an unvisited pair, the comparison averages remain zero and $N^+=1$ ; the large confidence radii under the stated bounds are essential. The local transition event uses the $\ell_1$ error condition: literal membership of the zero comparison vector in a simplex would make the paper's event fail. The printed coordinatewise maxima in Property 1 imply the standard joint-distribution optimism condition used here. The free $(s,a)$ printed in the last radius of Proposition 2 means $(s_t,a_t)$ , as the proof's context confirms Cheung et al., pp. 12, 14, 36, 40–41.

Two milestones carry a pinned hypothesis because the printed statement is false without it: Lemma 2 assumes the dual gain satisfies $\rho\le 2$ (an arbitrary feasible $\rho$ can make the bias span exceed $2D$ ), and Lemma 3 assumes the pair was visited in the episode-start window (at an unvisited pair the comparison averages are zero). Proposition 2 is stated for every round $t\ge\tau(m)$ before the horizon at which the action is the episode policy's choice, which covers the rounds of episode $m$ ; the coefficient $4D$ of $\eta$ is kept as printed.

The witness MDP has genuine probability rows in the widened sets and a diameter bound. The EVI tuple obeys both stated properties, and the chosen action obeys its policy. These conditions prevent an unconstrained bias, a spurious zero diameter, a confidence event at the wrong time, or a reward bound for an unrelated action. The published FiniteMDPLearning model supplies probability rows and rewards in $[0,1]$ ; its different travel-time convention is not substituted for the paper's diameter. Contributions to the MDP linear program, finite-state hitting times, window-average inequalities, and confidence-region geometry are all useful beyond this mission.

Selected references

W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. Preprint; journal DOI.
T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. Article.

10 thms3 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low IV: ℓ1-Regularized Best Subset Selection Satisfies Slow-Rate and Fast-Rate Oracle InequalitiesResearch Paper

Why shrink a best subset?

Best subset selection fits a linear predictor using at most $k$ of $p$ available columns. Its explicit limit on the number of selected variables makes the model easy to interpret, but the search can still fit noise: among many subsets of the same size, one can align unusually well with a noisy response. Mazumder, Radchenko and Dedieu study this effect in Subset Selection with Shrinkage. They add a penalty on the size of the selected coefficients and show how this changes prediction error when the signal-to-noise ratio is low.

An $\ell_1$ penalty is familiar from the Lasso. The estimator here also keeps the subset-size constraint, so its comparison class and its tuning parameter have a different role from those in an unconstrained Lasso. The paper's Theorem 3 gives three deterministic error bounds for this estimator, each valid on a specified event of the Gaussian noise. These bounds are the target of this mission. The separate probability estimates for the events are Theorem 1 of the paper and belong to another mission in this series.

Setting

Let $X\in\mathbb R^{n\times p}$ be a fixed design matrix whose columns have Euclidean norm one. The observation is $y=f^*+\epsilon$ , where $f^*\in\mathbb R^n$ is a fixed mean and the coordinates of $\epsilon$ are independent $N(0,\sigma^2)$ random variables, with $\sigma>0$ . The result below fixes one realized noise vector $\epsilon$ and assumes it lies in an event stated below. No assumption that $f^*$ is itself a linear combination of columns of $X$ is required.

For $1\le k\le p$ , write $B_0(k)=\{\beta\in\mathbb R^p:\|\beta\|_0\le k\}$ , where $\|\beta\|_0$ counts nonzero coordinates. An $\ell_1$ -regularized best subset estimator is any minimizer

\hat\beta_1\in\operatorname*{argmin}_{\beta\in B_0(k)}\bigl\{\|y-X\beta\|_2^2+\lambda\|\beta\|_1\bigr\}.\tag{16}

The objective has no factor $1/2$ . The assertion applies to every minimizer, so tied solutions are covered. The sparse minimum singular value is $\gamma_s=\inf\{\|Xu\|_2/\|u\|_2:u\ne0,\ \|u\|_0\le s\}$ . When $p\ge1$ and $s\ge1$ its domain is nonempty. Write $u_1^\sharp,\ldots,u_p^\sharp$ for the decreasing rearrangement of $|u_1|,\ldots,|u_p|$ .

The paper defines three noise events used here. $\mathcal H$ bounds the largest coordinate of $X^\top\epsilon$ by $\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}$ . On $\mathcal F$ , every $u\in\mathbb R^p$ satisfies

\epsilon^\top Xu\le(4+\sqrt2)\sigma\max\left\{\sum_{j=1}^{p}u_j^\sharp\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|_2\right\}.

On $\mathcal G_s$ , every $u\in B_0(s)$ satisfies $\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|_2$ . Here $\delta_0\in(0,1]$ and all logarithms are natural. These definitions, including the constant in $\mathcal G_s$ , are the printed deterministic events of p. 13.

Formalization targets

Exact slow rate on $\mathcal H$

At $\lambda=2\sigma\sqrt{2\log(2p)}+2\sigma\sqrt{2\log(1/\delta_0)}$ , Theorem 3(A) states

\|f^*-X\hat\beta_1\|_2^2\le\inf_{\beta\in B_0(k)}\bigl[\|f^*-X\beta\|_2^2+2\lambda\|\beta\|_1\bigr]\qquad(\epsilon\in\mathcal H).

Slow rate on $\mathcal F$

For $\lambda\ge(8+2\sqrt2)\sigma\sqrt{\log(2p)}$ , a positive universal constant $C_A$ gives

\|f^*-X\hat\beta_1\|_2^2\le C_A\left[\inf_{\beta\in B_0(k)}\bigl(\|f^*-X\beta\|_2^2+\lambda\|\beta\|_1\bigr)+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal F).

Fast rate on $\mathcal G_{2k}$

For every $\lambda\ge0$ , a positive universal constant $C_B$ gives

\|f^*-X\hat\beta_1\|_2^2\le C_B\left[\inf_{\beta\in B_0(k)}\|f^*-X\beta\|_2^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2 k+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal G_{2k}).

The $k$ multiplying $\gamma_{2k}^{-2}\lambda^2$ distinguishes this rate from the $\ell_2$ -penalized estimator's bound. The three claims together, with their separate tuning conditions, are Theorem 3 on p. 16. The milestones follow the displays of its proof in Supplement B.6, pp. 42–43.

What the result provides

Each inequality compares the prediction of any selected minimizer with that of every sparse competitor. The first bound has an exact leading constant and no additive noise term on $\mathcal H$ . The second keeps a linear penalty term when $\lambda$ meets a fixed noise-dependent threshold. The third replaces the linear term with a quadratic $\lambda$ term controlled by the sparse minimum singular value. This distinguishes regimes in which coefficient shrinkage changes the error rate. The paper also combines deterministic bounds with event probabilities in subsequent corollaries; those probability statements are separate from this goal.

The paper proves Theorem 3. The formalization task is to verify its model definitions, event interpretation and all three inequalities in Lean, with the same constants and quantifiers. The milestone statements isolate the basic inequality, the $\mathcal H$ bound, the rearranged-coordinate bound, the $\mathcal F$ case split and the sparse $\ell_1$ step. A complete proof would also provide reusable finite-dimensional norm and matrix estimates. This mission does not include the paper's numerical experiments, data-driven model-size selection, the $\ell_2$ -penalized estimator, or the event-probability theorem.

Difficulty

The constraint $\|\beta\|_0\le k$ makes the estimator a minimizer over a nonconvex set. A standard unconstrained Lasso argument does not directly supply the paper's bound for every feasible sparse comparator. The slow rates rely on two different noise controls: a coordinatewise bound on $\mathcal H$ and a maximum of a sorted-coordinate term and a prediction-norm term on $\mathcal F$ . The fast rate also needs the sparse minimum singular value to relate coefficient error to prediction error. The constants in these steps matter: replacing the exact first tuning equality or dropping the factor $k$ in the fast rate would state a different theorem.

Formalization scope

Lean uses Fin n → ℝ and Fin p → ℝ for vectors and Matrix (Fin n) (Fin p) ℝ for $X$ . Norms are explicit finite sums, rather than the function type's default supremum norm. The paper's one-based sorted index $j$ is j.val + 1; the sum using $u^\sharp$ is encoded as a maximum over coordinate permutations, which agrees with the decreasing rearrangement. The events are predicates on realized noise vectors. The Gaussian law explains the model but is not needed in these deterministic statements. The estimator is an argmin predicate, never a chosen minimizer.

The universal constants precede all dimensions and data in the Lean goal. The infima in the three displayed bounds are expressed as inequalities for every $\beta\in B_0(k)$ , avoiding the default value of an empty or unbounded real infimum. The standing conditions are $1\le k\le p$ , unit-norm columns, $\sigma>0$ and $0<\delta_0\le1$ . The first slow-rate branch retains the paper's equality for $\lambda$ . The fast branch additionally requires $\gamma_{2k}>0$ or $\lambda=0$ : this makes the $\lambda^2/\gamma_{2k}^2$ term meaningful under Lean's total division, which returns zero at a zero denominator. The displayed events use the paper's original $\mathcal G_s$ constant; this mission makes only a deterministic claim on that event.

The sparse domain for $\gamma_{2k}$ is nonempty under these conditions. All square-root radicands and logarithm arguments in the target are in their intended ranges. The formalization must rule out a universal constant that depends on $n$ , $p$ , $k$ , $X$ or $\lambda$ , and must apply to every minimizer. Contributions to the shared norm inequalities, rearrangement identity and matrix calculations are useful beyond this theorem.

Selected references

Rahul Mazumder, Peter Radchenko and Antoine Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research 71 (2023), arXiv preprint version 4 (2022), arXiv:1708.03288v4. This mission cites the preprint's page and theorem numbering.

9 thms3 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low III: ℓ2-Regularized Best Subset Selection Satisfies Slow-Rate and Fast-Rate Oracle InequalitiesResearch Paper

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors, choosing the $k$ that minimize the residual sum of squares. Mixed-integer optimization made it computable at moderate scale (Bertsimas, King & Mazumder, 2016), which reopened the statistical question of when it should be used. Empirical comparisons (Hastie, Tibshirani & Tibshirani, 2020) found that best subsets predicts poorly when the signal-to-noise ratio (SNR) is low: by fitting the noise exactly within its chosen support it overfits, and shrinkage methods such as the Lasso do better there.

Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty to the cardinality-constrained problem. Their Theorem 2 quantifies the effect of an $\ell_2$ (Euclidean-norm) penalty: it proves prediction-error bounds that are linear in the penalty level and therefore remain small in the low-SNR regime where best subsets fails. This mission formalizes that theorem.

Setting

The data follow the model

y=f^*+\epsilon,

where $y,f^*,\epsilon\in\mathbb R^n$ , $f^*$ is an unknown deterministic mean and $\epsilon$ is a noise vector (in the paper, with independent $N(0,\sigma^2)$ entries, $\sigma>0$ ). The design $X\in\mathbb R^{n\times p}$ is deterministic and its columns have unit Euclidean norm. Write $\|\cdot\|$ for the Euclidean norm, $\|\beta\|_0$ for the number of nonzero coordinates of $\beta$ , and $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$ .

For a model size $k$ and a penalty level $\lambda\ge0$ , the $\ell_2$ -regularized best-subsets estimator is any solution

\hat\beta_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|\quad\text{s.t.}\quad\|\beta\|_0\le k.

The penalty is the norm $\|\beta\|$ , not its square, and the loss carries no factor $1/2$ . The quantity of interest is the prediction error $\|f^*-X\hat\beta_2\|^2$ .

The minimal $s$ -sparse eigenvalue of $X$ is $\gamma_s=\min_{u\neq0,\,u\in B_0(s)}\|Xu\|/\|u\|$ . For $u\in\mathbb R^p$ , $u^\sharp_1\ge\dots\ge u^\sharp_p$ is the non-increasing rearrangement of $|u_1|,\dots,|u_p|$ . Given $\delta_0\in(0,1]$ , three noise events are sets of noise vectors:

\mathcal E_s=\big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\big\},

\mathcal F=\Big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\max\Big(\textstyle\sum_{j=1}^p u^\sharp_j\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|\Big),\ \forall u\in\mathbb R^p\Big\},

\mathcal G_s=\big\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\big\}.

The paper's Theorem 1 shows these events have high probability; Theorem 2 is a deterministic statement on each of them. The symbol $\lesssim$ means "up to a positive universal multiplicative constant", one that does not depend on $n,p,k,X,f^*,\sigma,\lambda$ or $\delta_0$ .

Formalization targets

Goal: Theorem 2 (p. 14)

Let $1\le k\le p$ .

(A) Slow rate. If $\lambda\ge[8+2\sqrt2]\sigma\sqrt{2k\log(ep/k)}$ , then on $\mathcal E_{2k}$

\|f^*-X\hat\beta_2\|^2\le\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+2\lambda\|\beta\|\big],

and on $\mathcal F$

\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+\lambda\|\beta\|\big]+\sigma^2\log(1/\delta_0).

(B) Fast rate. For every $\lambda\ge0$ , on $\mathcal G_{2k}$

\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\|f^*-X\beta\|^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2+\sigma^2\log(1/\delta_0).

The bounds hold for every minimizer $\hat\beta_2$ and for misspecified models: $f^*$ need not lie in the column span of $X$ .

Milestones

The steps of the printed proof (Supplement B.2, pp. 39–40), in the order the proof uses them: the basic inequality (29); the bound (30) on $\mathcal E_{2k}$ and its consequence (31); the dichotomy on $\mathcal F$ , where (30) implies (31) and (32) implies (33); the elementary inequality (34); the basic inequality on $\mathcal G_{2k}$ (p. 40); and the bound of $\lambda\|\beta-\hat\beta_2\|$ through $\gamma_{2k}$ (p. 40).

Significance

The result. The slow-rate bound of part (A) is linear in $\lambda$ . When the signal $\|\beta^*\|$ is small compared with $\sigma$ , the term $\lambda\|\beta^*\|$ is smaller than the rate $\sigma^2 k\log(ep/k)$ that best subsets attains, and the paper's Theorem 4 shows that in this regime the prediction error of best subsets is at least of order $\sigma^2\gamma_k^2k\log(ep/k)$ . Together the two results explain the empirical finding that shrinkage helps best subsets at low SNR. Part (B) shows nothing is lost at high SNR: the fast rate is the minimax rate $\sigma^2k\log(ep/k)$ over $k$ -sparse vectors plus the shrinkage term $\gamma_{2k}^{-2}\lambda^2$ . Combined with Theorem 1, the bounds give the high-probability statements of the paper's Corollaries 1 and 3.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist. The mission produces a checked deterministic core: once the events are granted, every constant ( $8+2\sqrt2$ , the factor $2\lambda$ , the threshold $2k\log(ep/k)$ ) is verified exactly. Together with the companion mission on Theorem 1 it would yield fully checked high-probability oracle inequalities for a cardinality-constrained estimator, which no current formal library contains.

Difficulty

Every step is elementary, but the bookkeeping is exact. The obvious reading "insert the event's inequality into (29)" does not by itself work on $\mathcal F$ : the event's right-hand side is a maximum of a sorted weighted sum and a prediction-norm term, and the first branch has to be compared with $\sqrt{2k\log(ep/k)}\,\|u\|$ for the $2k$ -sparse difference $u=\hat\beta_2-\beta$ , including when $2k$ exceeds $p$ . That comparison is a combinatorial estimate on sorted sums, not a substitution. On $\mathcal G_{2k}$ , the penalty difference $\lambda(\|\beta\|-\|\hat\beta_2\|)$ is not controlled by the event at all and has to be converted into prediction errors through $\gamma_{2k}$ . In both parts the final constant must not depend on $k$ , $p$ or $\delta_0$ .

Formalization scope

All objects are explicit Lean definitions in the namespace SubsetShrink.L2:

vectors are functions on Fin n and Fin p with 0-based indices, and $X$ is a real Matrix (Fin n) (Fin p);
the Euclidean norm, $\|\cdot\|_0$ and the inner product are explicit finite sums, since Mathlib's norm on Fin m → ℝ is the sup norm;
$\sum_j u^\sharp_j\sqrt{\log(2p/j)}$ is encoded as a maximum over permutations, which equals the sorted sum by the rearrangement inequality;
$\gamma_s$ is a real infimum over the nonzero vectors of $B_0(s)$ , a nonempty set when $p,s\ge1$ .

The model consists of $X$ with unit columns, $f^*$ , $\epsilon$ , $\sigma>0$ and $y=f^*+\epsilon$ . The estimator is a predicate that every minimizer satisfies; no minimizer is chosen and existence is not assumed. "On the event" is a hypothesis that the noise vector satisfies the event's printed inequality, so no probability measure appears. $\mathcal G_{2k}$ is the event as printed on p. 13; the correction of its probability bound belongs to the mission on Theorem 1 and does not affect these deterministic statements.

Committed conventions:

each $\lesssim$ is an existential constant $C>0$ quantified before all other data;
an infimum over $B_0(k)$ is stated as a bound for every $\beta\in B_0(k)$ ;
$\delta_0\in(0,1]$ is universally quantified;
the model size satisfies $1\le k\le p$ .

Part (B) assumes $\gamma_{2k}>0$ or $\lambda=0$ . When $\gamma_{2k}=0<\lambda$ the paper's bound is vacuous ( $\gamma_{2k}^{-2}\lambda^2=+\infty$ ), but Lean's $0^{-1}=0$ would turn it into a false claim.

A formalization that lets the constant depend on $k$ , $p$ or $\delta_0$ , fixes a particular minimizer, weakens an event (for example drops "for all $u\in B_0(s)$ "), or computes the infimum as a real ⨅ over an unbounded set would trivialize the theorem and is ruled out.

Not formalized here: the probability bounds of Theorem 1, the $\ell_1$ -penalized Theorem 3, the lower bound of Theorem 4, the data-driven choice of $k$ (Theorem 5), and the corollaries and numerical experiments. These are separate missions or follow-ups. Contributions of reusable lemmas (the rearrangement bound for the sorted sum, properties of $\gamma_s$ , the elementary absorption inequality (34)) are welcome.

Selected references

R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
T. Hastie, R. Tibshirani, R. Tibshirani, Best subset, forward stepwise or Lasso? Analysis and recommendations based on extensive comparisons, Statistical Science 35(4), 2020. https://doi.org/10.1214/19-STS733
P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670

8 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Offline Multi-Action Policy Learning: Generalization and Optimization 2: Depth-L Decision Trees Satisfy log N_H(ε,Π_L) ≤ (2^L−1)log p + 2^L log d + (2^L−1)log(L/ε+1)Research Paper

Motivation

Offline policy learning chooses a treatment rule from logged data: given $n$ observations of features $X_i$ , the action $A_i$ taken and the reward obtained, pick a policy $\pi:\mathcal X\to\{1,\dots,d\}$ from a class $\Pi$ whose expected reward is close to the best in the class. Zhou, Athey and Wager (arXiv:1810.04778v2) bound the regret of their cross-fitted augmented inverse-propensity-weighted learner by a quantity of order $\kappa(\Pi)\sqrt{V_*/n}$ , where $\kappa(\Pi)$ is an entropy integral built from Hamming covering numbers of $\Pi$ . A bound of this kind is only useful for a concrete policy class if $\kappa(\Pi)$ is finite and explicit.

Decision trees are the class the paper uses in practice: they are interpretable, they are the standard object in personalized-treatment applications, and the paper's computational sections (a mixed-integer program and a tree-search algorithm) optimize over them. Lemma 4 of the paper is the bridge between the general regret theory and trees: it bounds the Hamming covering number of the class $\Pi_L$ of depth- $L$ trees, and hence $\kappa(\Pi_L)$ . Covering and complexity bounds for trees in the 0–1 (two-action) setting go back to VC-dimension arguments; the multi-action Hamming-cover version here is the one this paper's regret bound consumes.

Setting

Features are points $x\in\mathbb R^p$ with components $x(1),\dots,x(p)$ ; there are $d$ actions, written $1,\dots,d$ . A deterministic policy is a map $\pi:\mathbb R^p\to\{1,\dots,d\}$ .

Hamming distance and covers. Fix points $x_1,\dots,x_n$ (repetitions allowed). For two policies,

H(\pi_1,\pi_2)=\frac1n\sum_{j=1}^n\mathbf 1\{\pi_1(x_j)\ne\pi_2(x_j)\}.

The $\varepsilon$ -Hamming covering number $N_H(\varepsilon,\Pi,\{x_1,\dots,x_n\})$ is the least $K$ such that some $\pi_1,\dots,\pi_K\in\Pi$ have every $\pi\in\Pi$ within Hamming distance $\varepsilon$ of some $\pi_i$ . The covering number of the class is the worst case over point sets,

N_H(\varepsilon,\Pi)=\sup\{N_H(\varepsilon,\Pi,\{x_1,\dots,x_m\}) : m\ge1\},

and the entropy integral is $\kappa(\Pi)=\int_0^1\sqrt{\log N_H(\varepsilon^2,\Pi)}\,d\varepsilon$ .

Decision trees. A depth- $L$ tree has $L$ layers: $L-1$ layers of branch nodes and a final layer of leaves, so $2^{L-1}-1$ branch nodes and $2^{L-1}$ leaves; a depth-1 tree is a single leaf. A branch node carries a split variable $i\in\{1,\dots,p\}$ and a threshold $b\in\mathbb R$ , and sends $x$ to its left child if $x(i)<b$ and to its right child otherwise. Each leaf carries an action. $\Pi_L$ is the set of policies computed by depth- $L$ trees. In the Lean development these are DTree p d L, DTree.eval and treePolicies p d L; the Hamming layer is hammingDist, hammingCoverNumOn, hammingCoverNum and entropyIntegral.

Formalization targets

Goal: Lemma 4, part 1 (p. 27)

For $p,d,L\ge1$ and $\varepsilon>0$ , $N_H(\varepsilon,\Pi_L)$ is finite and

\log N_H(\varepsilon,\Pi_L)\le(2^L-1)\log p+2^L\log d+(2^L-1)\log\Big(\frac L\varepsilon+1\Big).

Milestones (App. F)

Display (66), p. 67: for any reals $r_1,\dots,r_m$ there are $\lceil L/\varepsilon\rceil$ thresholds $b_i$ such that every indicator $\mathbf 1_b(r)=\mathbf 1\{r<b\}$ is within Hamming distance $\varepsilon/L$ of some $\mathbf 1_{b_i}$ with respect to $r_1,\dots,r_m$ .
App. F, Step 2, p. 69: for any $n\ge1$ points, $p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ depth- $L$ trees $\varepsilon$ -cover $\Pi_L$ , i.e. $N_H(\varepsilon,\Pi_L,\{x_1,\dots,x_n\})\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ .
App. F, Step 2, p. 69: $N_H(\varepsilon,\Pi_L)\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ .

Companion: Lemma 4, part 2 (p. 27)

\kappa(\Pi_L)\le\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1}.

It is posed as printed, as a second theorem of the mission rather than a milestone of the goal.

Significance

The result. Lemma 4 makes the abstract regret theory of the paper concrete: with part 2 it gives Theorem 4, the regret bound $O_p\big((\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1})\sqrt{V_*/n}\big)$ for learning depth- $L$ trees, which for fixed $L,p,d$ is $O_p(\sqrt{V_*/n})$ . The covering bound grows only logarithmically in $1/\varepsilon$ , which is the property the paper's Assumption 3 asks of a policy class. The same counting gives covering bounds for any class of piecewise-constant rules on axis-aligned partitions of bounded depth.

Formalizing it. The result is proved in the paper (App. F) but, as far as known, has no machine-checked proof. The paper omits the induction that combines per-node threshold grids into a cover of whole trees ("a straightforward but lengthy induction (omitted)"), and its appendix counts $2^L-1$ branch nodes where §6.1's trees have $2^{L-1}-1$ . A formal proof fixes both: it supplies the omitted induction and confirms that the printed bound holds for the class actually defined in §6.1. The milestones are reusable statements about threshold indicators and tree covers. The companion part 2 is posed with the printed constant $4/3$ , although the printed derivation evaluates $\int_0^1(L/\varepsilon^2)^{1/4}d\varepsilon$ as $\frac43L^{1/4}$ where the integral equals $2L^{1/4}$ ; whether the printed bound holds is part of what the mission settles.

Difficulty

The one-dimensional step (66) is elementary once the Hamming distance between two threshold indicators is identified with a count of points between the thresholds. The difficulty is in passing from single thresholds to whole trees. Replacing each branch node's threshold independently by its nearest grid threshold, with grids built on all $n$ points, does not give an $\varepsilon$ cover: the errors at different nodes of the same layer add up, and the naive bound is $(2^{L-1}-1)\varepsilon/L$ rather than $\varepsilon$ . The points that reach a node depend on the thresholds above it, so the approximation has to respect the tree structure, while the number of candidate trees must still be counted as a product over nodes. The passage from finite point sets to $N_H(\varepsilon,\Pi_L)$ , which is a supremum over all point sets in $\mathbb N\cup\{\infty\}$ , and the arithmetic with $\lceil L/\varepsilon\rceil$ and real logarithms are routine but must be done in the stated types.

Formalization scope

Features range over all of $\mathbb R^p$ (Fin p → ℝ); the paper's $\mathcal X$ is a bounded subset of $\mathbb R^p$ , and a bound over $\mathbb R^p$ implies the bound over every $\mathcal X\subseteq\mathbb R^p$ . Actions are Fin d, split variables Fin p (0-based); policies are deterministic.
Point sets are sequences Fin m → (Fin p → ℝ) with repetitions allowed, $m\ge1$ ; covers are proper (centres in $\Pi_L$ ). $N_H(\varepsilon,\Pi)$ is in ℕ∞, $\kappa(\Pi)$ a lower Lebesgue integral in ℝ≥0∞ over $(0,1]$ .
Depth follows §6.1: DTree p d 1 are leaves, DTree p d 0 is empty. The bounds are the printed ones, which over-count for this convention; the Lean was not switched to the appendix's convention, which would change $\Pi_L$ .
Standing hypotheses: $p\ge1$ , $d\ge1$ , $L\ge1$ ("Let $L$ be any fixed positive integer"), $\varepsilon>0$ (needed for $\lceil L/\varepsilon\rceil$ ).
The goal asserts finiteness of $N_H(\varepsilon,\Pi_L)$ explicitly. Without it the inequality would be trivially true for an infinite covering number, because Lean's toNat ⊤ = 0 and Real.log 0 = 0. The covering number is an infimum that is $0$ only for an empty class, and $\Pi_L$ is nonempty under the hypotheses, so the cover is not trivialized either.
Not posed: the $O(\log 1/\varepsilon)$ remark of Lemma 4.1 (a remark on the right-hand side); Theorem 4 (p. 28, the combination with the regret theorem, which belongs to the companion mission on regret); the mixed-integer program and tree search of §6.2–6.3 and App. G (computational).

Contributions welcome: proofs of the milestones, the omitted per-node induction as a stand-alone lemma, and the companion part 2.

Selected references

Z. Zhou, S. Athey, S. Wager, Offline Multi-Action Policy Learning: Generalization and Optimization, arXiv preprint, 2018 (v2). https://arxiv.org/abs/1810.04778
L. Breiman, J. Friedman, R. Olshen, C. Stone, Classification and Regression Trees, Wadsworth, 1984. https://doi.org/10.1201/9781315139470
D. Bertsimas, J. Dunn, Optimal classification trees, Machine Learning 106, 1039–1082, 2017. https://doi.org/10.1007/s10994-017-5633-9
S. Athey, S. Wager, Policy Learning With Observational Data, Econometrica 89(1), 133–161, 2021. https://doi.org/10.3982/ECTA15732

6 thms3 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Offline Multi-Action Policy Learning: Generalization and Optimization 1: Cross-Fitted AIPW Policy Learning Has Regret O_p(κ(Π)√(V*/n)) Even with Slowly Converging Nuisance EstimatesResearch Paper

Learning treatment policies from logged data

Many decisions are made by assigning one of several actions to an individual on the basis of observed features: which of $d$ drugs to prescribe, which of several promotions to show, which job-training programme to offer. Experimentation is often costly or unethical, while historical records of past assignments and their outcomes are plentiful. Offline policy learning asks for a rule that maps features to actions, chosen from such observational records, whose expected outcome is close to that of the best rule in a prescribed class. The binary-action case was settled by Kitagawa and Tetenov (2018) with known propensities and by Athey and Wager (2021) with estimated ones; Zhou, Athey and Wager extend the doubly robust approach to $d \ge 2$ actions. This mission formalizes the statistical half of that paper: the regret guarantee of its cross-fitted learner.

Timeline. Robins, Rotnitzky and Zhao (1994) introduced augmented inverse-propensity weighting (AIPW). Dudík, Langford and Li (2011) used doubly robust scores for multi-action policy evaluation and optimization. Chernozhukov et al. (2018) showed that cross-fitting removes the bias of flexible nuisance estimates in semiparametric estimation. Athey and Wager proved $\sqrt n$ -rate regret for binary actions with VC classes. Zhou, Athey and Wager (arXiv 2018; Operations Research, 2023) treat $d$ actions with a Hamming entropy integral as the complexity measure.

Setting

There are $d$ actions, written $1,\dots,d$ and identified with the standard basis vectors of $\mathbb R^d$ , so that for $\gamma\in\mathbb R^d$ the inner product $\langle\pi(x),\gamma\rangle$ is the coordinate $\gamma_{\pi(x)}$ . A draw consists of features $X\in\mathcal X$ , potential outcomes $(Y(1),\dots,Y(d))$ and a logged action $A$ ; only the triple $(X,A,Y)$ with $Y=Y(A)$ is observed. The data are $n$ iid draws.

The model consists of a law $P_X$ of the features and two conditional laws given $X=x$ : one for the outcome vector, one for the action. Given $X$ the two are independent (unconfoundedness). The propensity is $e_a(x)=P(A=a\mid X=x)$ and the mean reward is $\mu_a(x)=\mathbb E[Y(a)\mid X=x]$ . A policy is a map $\pi:\mathcal X\to\{1,\dots,d\}$ from a class $\Pi$ . Its value is $Q(\pi)=\mathbb E[Y(\pi(X))]$ and its regret is $R(\pi)=\sup_{\pi'\in\Pi}Q(\pi')-Q(\pi)$ .

The learner, CAIPWL (Algorithm 1), divides the sample into $K\ge2$ evenly sized folds. For each fold $k$ it fits estimators $\hat\mu^{-k}_a$ , $\hat e^{-k}_a$ on the observed data outside fold $k$ , forms the cross-fitted AIPW score

\hat\Gamma_{i,j}=\hat\mu^{-k(i)}_j(X_i)+\mathbf 1\{A_i=j\}\frac{Y_i-\hat\mu^{-k(i)}_{A_i}(X_i)}{\hat e^{-k(i)}_{A_i}(X_i)},

and returns a maximizer $\hat\pi_{CAIPWL}$ over $\Pi$ of $\hat Q_{CAIPWL}(\pi)=\frac1n\sum_i\hat\Gamma_{i,\pi(X_i)}$ . The oracle score $\Gamma_i$ is the same expression with the true $\mu$ and $e$ ; it gives $\tilde Q(\pi)=\frac1n\sum_i\Gamma_{i,\pi(X_i)}$ . Write $\Delta$ , $\tilde\Delta$ , $\hat\Delta$ for the differences $Q(\pi_1)-Q(\pi_2)$ , $\tilde Q(\pi_1)-\tilde Q(\pi_2)$ , $\hat Q(\pi_1)-\hat Q(\pi_2)$ , and

V_*=\sup_{\pi_a,\pi_b\in\Pi}\mathbb E\big[(\Gamma_{\pi_a(X)}-\Gamma_{\pi_b(X)})^2\big].

The complexity of $\Pi$ is measured through the Hamming distance $H(\pi_1,\pi_2)=\frac1m\#\{j:\pi_1(x_j)\ne\pi_2(x_j)\}$ on points $x_1,\dots,x_m$ . The covering number $N_H(\varepsilon,\Pi)$ is the supremum over all finite point sequences of the least number of policies of $\Pi$ that $\varepsilon$ -cover $\Pi$ in $H$ . The entropy integral is $\kappa(\Pi)=\int_0^1\sqrt{\log N_H(\varepsilon^2,\Pi)}\,d\varepsilon$ .

The assumptions are: overlap, $e_a(x)\ge\eta>0$ ; bounded rewards, $|Y(a)|\le B$ ; Assumption 2, $\mathbb E[(\hat\mu^{-k}_a-\mu_a)^2]\cdot\mathbb E[(\hat e^{-k}_a-e_a)^2]=o(1)/n$ ; and Assumption 3, $N_H(\varepsilon,\Pi)\le C\exp(D\varepsilon^{-\omega})$ with $0<\omega<1/2$ .

Formalization targets

Goal: Theorem 3 in the form of Remark 8, (18), p. 22

R(\hat\pi_{CAIPWL})=O_p\Big(\kappa(\Pi)\sqrt{\tfrac{V_*}{n}}\Big),

read per $n$ : for every $\varepsilon>0$ there are $M>0$ and $N$ with $\mathbb P\big(R(\hat\pi_{CAIPWL})>M\kappa(\Pi)\sqrt{V_*/n}\big)\le\varepsilon$ for all $n\ge N$ . This is the paper's own "simpler way of stating the regret bound in Theorem 3". It fixes the rate and the dependence on $\kappa(\Pi)$ and $V_*$ , but no constants.

Milestones

Lemma 1 (1): the inner product distance $I_\Gamma$ satisfies the triangle inequality.
(48): $\mathbb E[\tilde Q(\pi)]=Q(\pi)$ .
(17): $\hat\Delta-\tilde\Delta=\sum_j(S^j_1+S^j_2+S^j_3)$ , the algebraic split into error terms.
Lemma 3 (pinned): $\sup_{\pi_1,\pi_2\in\Pi}|\hat\Delta-\tilde\Delta|=o_p(n^{-1/2})$ .
Oracle concentration (Lemma 2 as used in (18), pinned): $\sup_{\pi_1,\pi_2\in\Pi}|\tilde\Delta-\Delta|=O_p(n^{-1/2})$ .
(18): $R(\hat\pi)\le\sup_{\pi_1,\pi_2\in\Pi}|\hat\Delta-\Delta|$ for every empirical maximizer.

Printed statements not posed

Theorem 3's explicit display, $R\le(54.4\sqrt2\kappa(\Pi)+435.2+\sqrt{2\log(1/\delta)})\sqrt{V_*/n}$ , together with Theorem 1, Lemma 2 (11) and Theorem 2, is not posed. Lemma 1(2), which the proof of Theorem 1 uses, is false. With three points, $d=2$ , $\pi_0\equiv1$ , $\pi_k$ switching to action 2 at the point $k$ only, and $\gamma_i=(1,0)$ , one gets $N_{I_\Gamma}(0.7)=4>3\ge N_H(0.49)$ .
The $\sqrt{V_*}$ scaling of Theorem 1 fails for interval-switching classes, where $\kappa(\Pi)$ stays bounded, $V_*=2p$ , and the Rademacher complexity is of order $\sqrt{p\log(1/p)}$ .
$54.4\sqrt2(\kappa+8)$ equals $54.4\sqrt2\kappa+435.2\sqrt2$ , not $54.4\sqrt2\kappa+435.2$ .
The $o(1/\sqrt n)$ and $o_p(1/\sqrt n)$ remainders cannot be absorbed into one explicit constant at a fixed probability.
Lemma 1(2) is not posed, being false.

Significance

The theorem shows that a learner can use flexible machine-learning estimates of the propensities and outcome regressions, each converging more slowly than $n^{-1/2}$ , and still attain the regret rate of an oracle that knows them, provided the product of their errors is $o(n^{-1/2})$ . This doubly robust rate condition is what makes cross-fitted AIPW scores usable for policy learning with random forests, boosting or neural-network nuisances. The dependence on $\Pi$ only through $\kappa(\Pi)$ covers the multi-action classes the paper uses later, such as depth- $L$ decision trees.

On formalization: the result is proved on paper, with explicit constants that are not established as printed. No machine-checked proof of any part of it is known. A complete development would give a checked doubly robust policy-learning guarantee with the hypotheses a correct proof needs, stated explicitly. It would also deliver, as by-products, a checked uniform-entropy bound for empirical processes indexed by policy differences and a cross-fitting lemma with fold-wise conditional independence.

Difficulty

Two parts are hard. The oracle concentration needs a chaining (Dudley-type) bound for the empirical process $\{\tilde\Delta(\pi_1,\pi_2)-\Delta(\pi_1,\pi_2)\}$ , indexed by pairs of policies, in which the covering numbers are uniform over point sets and the entropy integrand uses $\varepsilon^2$ . Bounding one fixed pair by a central limit theorem is not enough, because the supremum over $\Pi\times\Pi$ is the whole point. Lemma 3 needs the conditional independence that cross-fitting creates: given the data outside fold $k$ , the terms of fold $k$ are iid with conditional mean zero in the first two error terms of (17). The uniform $o_p(n^{-1/2})$ bound then comes from a localized chaining argument whose radius shrinks with the nuisance errors. A naive argument conditioning on all the data at once loses the mean-zero structure.

Formalization scope

Actions are Fin d; policies are deterministic maps X → Fin d (endnote 3, p. 45), and a class is Pol : Set (X → Fin d). The model is a probability measure PX with two Markov kernels κY, κA, and the joint law is PX ⊗ₘ (κY ×ₖ κA). This builds unconfoundedness into the law. The sample of size $n$ is the product measure on Fin n → Draw X d. Estimators of fold $k$ are functions of the observed triples indexed by {i // fold n i ≠ k}, so they cannot see fold $k$ or unobserved potential outcomes. The regret uses $\sup_{\pi'\in\Pi}Q(\pi')$ in place of $Q(\pi^*)$ . $\kappa(\Pi)$ is an ℝ≥0∞ lower integral, finite under Assumption 3. $O_p$ and $o_p$ are read for each $n$ separately: Definition 8's " $\forall n\ge N$ with probability $1-\varepsilon$ " presupposes one probability space for all $n$ . Bounded support is stated for each $x$ under κY x.

Hypotheses added to the printed ones:

(i) both mean-squared errors tend to $0$ separately, in addition to (3). The proof of Lemma 3 uses separate rates, and with $\hat\mu\equiv0$ , $\hat e=e$ , condition (3) holds while the first term of (17) has exact order $n^{-1/2}$ .
(ii) $|\hat\mu|\le\hat B$ , $\hat e\ge\hat\eta>0$ , and both estimators are measurable.
(iii) the policies are measurable, and the class is permissible: for each $m$ and action pattern, the set of point sequences on which some policy realizes the pattern is measurable.

Without (ii) and (iii), Lean's integrals of non-measurable functions are $0$ and Assumption 2 would be vacuous. The hypotheses are satisfiable: the oracle estimators $\hat\mu=\mu$ , $\hat e=e$ meet every estimator condition, and a finite class of constant policies meets Assumption 3 and permissibility. The degenerate cases $\kappa(\Pi)=0$ or $V_*=0$ force zero regret, so the goal is not trivialized there.

Needed infrastructure: product measures and kernels (Mathlib), and Hamming covering numbers (local, Definition 4). Still to build: uniform-entropy chaining for bounded classes, and Talagrand/Bousquet-type concentration. Contributions are welcome on the chaining bound, the cross-fitting conditional-independence lemma, and the elementary items (48), (17) and Lemma 1(1). These are reusable in any doubly robust estimation mission.

Selected references

Z. Zhou, S. Athey, S. Wager, Offline Multi-Action Policy Learning: Generalization and Optimization, arXiv:1810.04778v2, 2018; Operations Research 71(1), 2023. https://arxiv.org/abs/1810.04778
S. Athey, S. Wager, Policy Learning with Observational Data, Econometrica 89(1), 2021. https://arxiv.org/abs/1702.02896
T. Kitagawa, A. Tetenov, Who Should Be Treated? Empirical Welfare Maximization Methods for Treatment Choice, Econometrica 86(2), 2018. https://doi.org/10.3982/ECTA13288
V. Chernozhukov et al., Double/Debiased Machine Learning for Treatment and Structural Parameters, The Econometrics Journal 21(1), 2018. https://arxiv.org/abs/1608.00060
M. Dudík, J. Langford, L. Li, Doubly Robust Policy Evaluation and Learning, ICML 2011. https://arxiv.org/abs/1103.4601
J. Robins, A. Rotnitzky, L. P. Zhao, Estimation of Regression Coefficients When Some Regressors Are Not Always Observed, JASA 89(427), 1994. https://doi.org/10.1080/01621459.1994.10476818

9 thms3 active usersReviewed

Completed

Algorithmic Game Theory Bandit Algorithms Operations Research·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 2: The ML-IS-UCB Bidding Policy Achieves Expected Regret at Most C√T log³ T for Every Oblivious Private-Value SequenceResearch Paper

Learning to bid in first-price auctions

Display advertising has been moving from second-price to first-price auctions: several exchanges began rolling them out in 2017, and Google Ad Manager completed its move at the end of 2019 (Davies 2019). In a second-price auction bidding one's value is a dominant strategy; in a first-price auction the optimal bid depends on the distribution of the competing bids, which a bidder does not know and must learn from repeated play. Most of the learning literature on auctions takes the seller's side of the second-price auction (reserve prices, e.g. Cesa-Bianchi, Gentile, Mansour 2015); on the bidder's side of the first-price auction, the main prior approach is the cross-learning framework of Balseiro et al. 2019.

Han, Zhou and Weissman (arXiv:2003.09795) study the bidder's problem with the feedback that ad exchanges actually provide, where only the winning price is announced, and with no assumption on the distribution of the competing bids. Their two upper bounds are $\widetilde O(\sqrt T)$ regret: Theorem 1 for iid private values and Theorem 2, the subject of this mission, for values chosen by an oblivious adversary. A matching $\Omega(\sqrt T)$ lower bound holds even under full information (Theorem 9).

Setting

A single bidder plays $T$ rounds. In round $t$ she observes a private value $v_t\in[0,1]$ , bids $b_t\in[0,1]$ , and wins if $b_t\ge m_t$ , where $m_t\in[0,1]$ is the highest other bid (HOB). Her payoff is (1)

r(v_t,b_t;m_t)=(v_t-b_t)\,\mathbb 1(b_t\ge m_t).

The HOBs are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$ ; $G$ may be discrete, continuous or mixed. Feedback is censored: after round $t$ only $\max\{b_t,m_t\}$ is revealed, so $m_t$ is observed only when the bidder loses. The expected reward is $R(v,b)=(v-b)G(b)$ , and the regret of a policy $\pi$ against the value sequence $v=(v_1,\dots,v_T)$ is (3)

R_T(\pi;v)=\sum_{t=1}^T\Big(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Big),

the shortfall against an oracle that knows $G$ . A policy bids in round $t$ as a (possibly randomized) function of $v_1,\dots,v_t$ and of the feedback of rounds $1,\dots,t-1$ . An oblivious adversary fixes the whole value sequence in advance, independently of the bids and the HOBs.

The policy analysed is ML-IS-UCB (Algorithm 4). It restricts bids to the grid $b^i=(i-1)/K$ , $i\in[K]$ , with $K=\lceil\sqrt T\rceil$ ; it splits time into $L=\lceil\log_2T\rceil$ levels after an initialization phase of $T_0=(L+1)\lceil\sqrt T\rceil$ zero bids; and at each level it computes a width $w^\ell_{i,t}$ , an interval-splitting reward estimate $\hat r^\ell_{i,t}$ and a candidate set $\mathcal B^\ell_t$ by the displays (12)–(16).

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $T\ge2$ some policy $\pi$ satisfies, for every value sequence $v\in[0,1]^T$ and every $G$ on $[0,1]$ ,

\mathbb E\big[R_T(\pi;v)\big]\le C\sqrt T\log^3T .

The constant is unspecified, so the goal survives any improvement of the constants below.

The explicit bound: Theorem 7

For every $\gamma\ge3$ , the ML-IS-UCB policy satisfies

\mathbb E\big[R_T(\pi^{\mathrm{ML\text{-}IS\text{-}UCB}};v)\big]\le4+(L+4)\lceil\sqrt T\rceil+80\gamma^{3/2}\log(LKT)(1+\log T)\,L\sqrt T .

Milestones

In the order of the proof (Section 4.3 and Appendix C):

Lemma 7: with probability at least $1-4T^{-3}$ , $|\hat r^\ell_{i,t}-r_{i,t}|\le w^\ell_{i,t}$ for all $i,\ell$ and $T_0<t\le T$ , and $w^\ell_{i,t}$ is bounded by (18) in terms of the true interval probabilities $p_j=G(b^{j+1})-G(b^j)$ .
Lemma 8: on that event the best grid bid is never eliminated, and a round assigned to level $\ell$ has regret at most $8\cdot2^{-\ell}$ against the grid.
Display (19): the grid regret is at most $T_0+8\sum_\ell2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|$ .
Lemma 16: a deterministic counting bound for the sums $\sum_t\sum_{j\ge i(t)}v_j/n^\ell_{j,t}$ .
Lemma 9: $2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|\le10\gamma^{3/2}\log(LKT)(1+\log T)\sqrt T$ .
Theorem 7.

A supporting item, not a milestone, states the quantization step $\max_{b\in[0,1]}R(v,b)\le\max_iR(v,b^i)+1/K$ for the grid of Algorithm 4.

Significance

The result shows that adversarial values cost at most a logarithmic factor relative to iid values in repeated first-price auctions with censored feedback, and that no regularity of $G$ is needed. ML-IS-UCB is also an algorithmic template: its widths are computed before the data of the current level is used, which makes the estimates at each level independent of the bids that select them, and its interval-splitting estimator uses the variance of each interval rather than a uniform bound. Remark 3 notes that replacing the interval probabilities by $1$ gives only $\widetilde O(\sqrt{KT})$ .

All results of the paper are proved in the preprint; none of them is machine-checked. A complete development formalizes a multi-level elimination algorithm with data-dependent level assignment, a Bernstein-type concentration argument for estimates indexed by random sets, and the counting lemma behind the logarithmic factors. Each of these is reusable for other elimination-based bandit algorithms.

Difficulty

The obvious route is a single UCB index per grid bid, (11) on p. 27, built from all past observations through the estimates $\hat p^t_j=\sum_{s\le t}\mathbb 1(b_s\le b^j)\mathbb 1(m_s\in(b^j,b^{j+1}])/\sum_{s\le t}\mathbb 1(b_s\le b^j)$ . It fails because $\hat p^t_j$ is not a normalized binomial variable: each bid depends on the earlier HOBs, so conditioned on the bids the HOBs are no longer independent and $\hat p^t_j$ is not even unbiased. Self-normalized martingale bounds control each $\hat p^t_j$ separately but not the sum $\sum_{j\ge i}\hat p^t_j$ that the reward estimate needs. Algorithm 4 restores conditional independence through its level structure, and Lemma 7 has to make that precise: the sets $\Phi^\ell(t)$ are random, and the bound must hold uniformly over all $(i,\ell,t)$ with a variance term estimated from a held-out sample. Lemma 9 then needs the variance-sensitive width (18); a crude width loses a factor $\sqrt K$ (Remark 3).

Formalization scope

Model. Rounds are Fin T; Lean round $t$ is paper time $t+1$ . The HOB law is a probability measure μG on ℝ with μG [0,1]ᶜ = 0, and $G(x)$ is (μG (Set.Iic x)).toReal; atoms are allowed. The maximum in (3) is a supremum over $[0,1]$ .
Policies. A policy has internal randomness $u\sim\mu_U$ and, for each $u$ , a bidding rule whose round- $t$ bid receives only the values of rounds $\le t$ and the feedback $\max\{b_s,m_s\}$ of rounds $<t$ , enforced by the argument types; bids lie in $[0,1]$ and are jointly measurable. The expectation is a Bochner integral over $u$ and $m\sim G^{\otimes T}$ , and Theorems 2 and 7 also assert integrability, so the integral cannot be a junk value.
Algorithm 4. Grid indices are 0-based ( $b^{i+1}=i/K$ , $b^{K+1}=1$ ); inside the algorithm times are the paper's $1,\dots,T$ . Every quantity $n,w,\hat p,\hat r,\mathcal B$ is defined by its formula for every $(i,\ell,t)$ . The estimators (14) and $\hat p^0$ are computed from the feedback, not from $m$ , and the algorithm recomputes its own past decisions, so it is a censored-feedback rule. "An arbitrary $i$ " is a selection rule depending on the time and the level only. If no level breaks (impossible for $\gamma\ge3$ , $T\ge2$ ) the round goes to level $L$ with bid $0$ .
Hypotheses added to the printed statements, each disclosed in its item: $T\ge2$ in Theorem 2 (the printed bound is $0$ at $T=1$ ); Lemmas 8, 9 and (19) are stated pathwise under the inequalities of Lemma 7 that their proofs use; Lemma 16 assumes that the set contains $\lceil\sqrt T\rceil$ initialization rounds with bid $0$ , which its proof uses; the quantization display is adapted from the grid of Lemma 4 to that of Algorithm 4.
Ruled out. A policy that reads $m_t$ , $G$ or future values, a constant $C$ chosen after $T$ , $v$ or $G$ , a policy chosen after $v$ or $G$ , and an expectation of a non-integrable function would each make the goal trivial; the statements exclude all four.
Needed and welcome. Bernstein and multiplicative Chernoff bounds for binomial variables (Lemmas 14, 15 of the paper are cited from the literature), measurability of the run of the algorithm, and the harmonic-sum bound $\sum_{k=a}^T1/k\le1+\log T$ . Contributions toward any milestone, or alternative proofs of the goal, are welcome.

Selected references

Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
N. Cesa-Bianchi, C. Gentile, Y. Mansour, Regret Minimization for Reserve Prices in Second-Price Auctions, IEEE Transactions on Information Theory 61(1), 2015. https://doi.org/10.1109/TIT.2014.2365772
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
J. Davies, What to know about Google's implementation of first-price ad auctions, Digiday, 2019. https://digiday.com/media/buyers-welcome-auction-standardization-as-google-finally-goes-all-in-on-first-price/

13 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Contextual Inverse Optimization: Offline and Online Learning 2: The Greedy Circumcenter Policy Can Incur Regret Linear in the Horizon from a Pointed Knowledge SetResearch Paper

Learning a cost vector from optimal decisions

In inverse optimization, an observer sees decisions made by an expert who solves an optimization problem, and wants to recover the expert's unknown objective. Besbes, Fonseca and Lobel study a contextual version: in each period a feasible set and a context function are revealed, a learner must act before seeing the expert's choice, and then observes the expert's optimal action. The learner pays the expert's cost of its own action. This models, for example, a platform imitating a dispatcher's routing decisions or a recommender learning a user's trade-offs, where only optimal choices, not costs, are ever observed (Besbes, Fonseca, Lobel, arXiv:2106.14015).

For the one-period (offline) problem the paper shows that the circumcenter policy, which acts as if the unknown cost were the center of the smallest revolution cone containing the set of costs still consistent with the data, is minimax optimal (Theorem 1). The natural online policy is to apply it greedily in every period. This mission formalizes the paper's Theorem 2, which shows that this greedy policy can fail badly: its worst-case regret can grow linearly in the horizon, even when the initial uncertainty is small in a precise geometric sense.

Setting

Costs live in $\mathbb R^d$ and actions in $\mathbb R^n$ . The true cost $c^\star$ lies on the unit sphere $S^d$ . An action set $\mathcal X\in\mathfrak B$ is a nonempty compact subset of $\mathbb R^n$ of diameter at most $1$ ; a context function $f\in\mathfrak F$ is a $1$ -Lipschitz map $\mathbb R^n\to\mathbb R^d$ . The forward problem with cost $c$ has solution set

\psi(c,\mathcal X,f)=\arg\min_{x\in\mathcal X} f(x)'c .

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$ , set to $0$ if either vector is $0$ . The uncertainty angle of a set $C$ is

\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\theta(c,\hat c),

and a circumcenter $\hat c(C)$ is a unit vector attaining this infimum. A set is pointed when $\alpha(C)<\pi/2$ , i.e. it fits inside an open half-space cone.

Online protocol. In periods $t=1,\dots,T$ nature reveals $\mathcal X_t$ and $f_t$ , the learner picks $x^\pi_t\in\mathcal X_t$ , and then an optimal expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ is revealed. Starting from a closed set $C_0\subseteq S^d$ , the knowledge set is

C(\mathcal I_t)=\{c\in C_0:\ c'f_s(x^\star_s)\le c'f_s(x)\ \ \forall x\in\mathcal X_s,\ s<t\},

the regret is $R^\pi_T=\sum_{t=1}^T\big(f_t(x^\pi_t)-f_t(x^\star_t)\big)'c^\star$ , and the worst-case regret $\mathcal{WCR}^\pi_T(C_0)$ is its supremum over $c^\star\in C_0$ and admissible instances. The greedy circumcenter policy chooses $x^\pi_t\in\psi\big(\hat c(C(\mathcal I_t)),\mathcal X_t,f_t\big)$ .

Formalization targets

Goal: Theorem 2 (pp. 13–14)

There is a closed, nonempty, pointed $C_0\subseteq S^3$ such that

\mathcal{WCR}^{\pi_{greedy}}_T(C_0)=\Omega(T).

Concretely: there are $C_0$ and $\kappa>0$ such that for every horizon $T\ge1$ some $c^\star\in C_0$ and admissible $(\mathcal X_t,f_t)$ admit a greedy run, and every greedy run (any circumcenter, any tie-break) has regret at least $\kappa T$ . The constant $\kappa$ is left existential, as the page claims only $\Omega(T)$ .

Milestones (the proof's displayed steps, App-9–App-11)

Lemma 2 (p. 12): a circumcenter exists for every nonempty set, and is unique when the set is pointed and not $\{0\}$ .
Step 1: for $0<\bar\alpha<\pi/2$ and $0\le\varepsilon\le\tan\bar\alpha/2$ , the set $C_{\varepsilon,\bar\alpha}$ , a polyhedral cone cut by three half-spaces and intersected with $S^3$ , has the unique circumcenter

\hat c(C_{\varepsilon,\bar\alpha})=\tfrac{1}{\sqrt{1+\varepsilon^2}}(1,\varepsilon,0).

Step 2: with $C_0=C_{0,\bar\alpha}$ , $f_t=\mathrm{id}$ , $\mathcal X_t=\{\bar x_t,0\}$ , $\varepsilon_t=t\tan\bar\alpha/(2T)$ , the greedy knowledge sets are $C(\mathcal I_t)=C_{\varepsilon_{t-1},\bar\alpha}$ .
Step 3: in that instance, with $\tan\bar\alpha\le 2$ , each period's regret is at least $\sin\bar\alpha/4$ .

Significance

The result separates offline from online learning in this model. Theorem 1 makes the circumcenter the best one-shot guess, yet Theorem 2 shows that one-shot optimality says nothing about information collection: a greedy learner can keep choosing actions that are wrong by a fixed margin while the revealed expert actions cut away only slivers of the knowledge set. This is the reason the paper introduces its EllipsoidalCones algorithm, which acts greedily on an enlarged ellipsoidal-cone superset and attains logarithmic regret for pointed initial sets. Theorem 2 is the lower bound that makes that design necessary.

On the formal side, the paper's proof is complete but compressed; it asserts the circumcenter of a three-generator spherical polygon "using Definition 2" and leaves the induction's geometric inclusions to the reader. A machine-checked version fixes the normalization of the circumcenter and the quantitative condition behind " $\varepsilon^2\le1$ ", and gives a reusable formal treatment of uncertainty angles and circumcenters, which the paper's other results (Theorem 1, Theorem 3, Lemma 10) all use. No result of the paper has a formal statement or proof on Prove2Me yet.

Difficulty

The arithmetic of Step 3 is elementary once the knowledge sets are known. The difficulty is in Steps 1 and 2. Identifying the circumcenter of $C_{\varepsilon,\bar\alpha}$ requires a minimax argument over the whole sphere: one must show that no other unit vector has a smaller maximal angle to the three extreme rays, and that the minimizer is unique, which rests on Lemma 2. The greedy policy is defined through this minimizer, so without uniqueness nothing can be said about its actions. Step 2 then needs an exact description of each knowledge set: showing that the new half-space makes the previous one redundant inside $C_0$ requires the sign information carried by the other constraints. A naive bound on the regret that ignores the knowledge-set dynamics fails, because a priori the policy might learn $c^\star$ after a few periods.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), so norms, diameters and Lipschitz constants are Euclidean. The angle uses the paper's convention $\theta(c,0)=\theta(0,\hat c)=0$ ; Mathlib's InnerProductGeometry.angle is not used. Action sets are required to be nonempty (otherwise no action exists). Periods are $0$ -based in Lean: Lean period $t$ is the paper's period $t+1$ , and Lean's knowledge set at $t$ is the paper's $C(\mathcal I_{t+1})$ . The construction and the goal are in dimension $d=3$ , as in the proof; the goal holds for every action dimension $n\ge1$ .

The worst-case regret is never written as a real supremum, whose junk values would decide the statement. The lower bound is stated by exhibiting the instance. A run of the greedy policy is a predicate quantifying over every circumcenter choice and every minimizer, and nature's sequences are arbitrary. Two pins relative to the page: the printed circumcenter $(1,\varepsilon,0)$ is normalized as in Step 3, and Step 3 assumes $\tan\bar\alpha\le2$ , which the page's " $\varepsilon^2\le1$ " needs (the goal uses $\bar\alpha=\pi/4$ ).

Two trivializations are ruled out. Without pointedness the claim holds for $C_0=S^3$ with antipodal costs, so $\alpha(C_0)<\pi/2$ is part of the goal. A bound over all runs would hold vacuously if no run existed, so the goal also asserts that a greedy run exists.

A complete development needs spherical geometry of polyhedral cones (extreme rays, angles to a cone), continuity of the uncertainty-angle objective for Lemma 2, and elementary trigonometry. The Geometry and Online definitions are shared with the other missions of this series and are reusable for any work on inverse optimization or learning from revealed preferences. Proofs of any milestone are welcome, as are alternative arguments for Lemma 2.

Selected references

O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023 (preprint used here; published in Operations Research, 2025). https://arxiv.org/abs/2106.14015
M. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
R. K. Ahuja, J. B. Orlin, Inverse Optimization, Operations Research 49(5), 2001. https://doi.org/10.1287/opre.49.5.771.10607

9 thms3 active usersReviewed

Completed

Algorithmic Game Theory Bandit Algorithms Operations Research·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 1: With IID Private Values a Bidding Policy Achieves Expected Regret at Most C√T log^2.5 TResearch Paper

Motivation

Most display advertising is sold in first-price auctions: the highest bidder wins and pays its own bid. Since the industry's move away from second-price formats around 2019, a bidder can no longer bid its value and must instead learn how much to shade its bid, from data about how the other bidders behave. A demand-side platform faces this problem millions of times a day with very little information. When it wins it pays its bid and learns nothing about the competition beyond the fact that it won; when it loses it sees only the winning price.

Han, Zhou and Weissman (arXiv:2003.09795v7, Operations Research 2025) cast this as an online learning problem and gave the first bidding policies with $\tilde O(\sqrt T)$ regret against an arbitrary unknown distribution of competing bids. This mission is the first of a series of six on that paper. It covers the case of stochastic private values, and the route to it through a general class of contextual bandits.

Setting

A single bidder takes part in $T$ rounds. In round $t$ she observes a private value $v_t\in[0,1]$ , bids $b_t\in[0,1]$ , and the highest other bid (HOB) is $m_t\in[0,1]$ . She wins iff $b_t\ge m_t$ , so her payoff is $r(v_t,b_t;m_t)=(v_t-b_t)\mathbb 1(b_t\ge m_t)$ . The HOBs are iid with an unknown CDF $G$ on $[0,1]$ ; no continuity or shape assumption is made, and atoms are allowed. The values $v_1,\dots,v_T$ are iid with an unknown distribution $F$ on $[0,1]$ , independent of the HOBs.

Feedback is censored: at the end of round $t$ only the winning bid $y_t=\max\{b_t,m_t\}$ is revealed. A policy $\pi$ chooses $b_t$ from its own internal randomness, $v_1,\dots,v_t$ and $y_1,\dots,y_{t-1}$ . With the expected reward $R(v,b)=(v-b)G(b)$ , the regret is

R_T(\pi;v)=\sum_{t=1}^T\Big(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Big),

the gap to an oracle that knows $G$ .

The paper reaches its bound through partially ordered contextual bandits. These are contextual bandits with $M$ contexts and $K$ actions, rewards in $[0,1]$ , and a feedback graph $G$ on the actions. Playing $a$ reveals the rewards of $a$ and its out-neighbours under every context (cross learning). The graph is a transitively closed DAG, so it induces a partial order $\preceq_G$ on actions. There is also a partial order $\preceq_{\mathcal C}$ on contexts along which some choice of optimal action is monotone (Definitions 2 and 3). Algorithm 3 is an arm-elimination algorithm for this class. The auction becomes such a bandit when values are clipped to the grid $\mathcal C=\{1/M,\dots,1\}$ and bids are restricted to $\mathcal A=\{1/K,\dots,1\}$ : a bid $b$ reveals $\mathbb 1(m_t\le b')$ for every $b'\ge b$ .

Formalization targets

Goal: Theorem 1

\exists\,C>0\ \ \forall\,T\ge2\ \ \exists\,\pi\ \ \forall\,F,G:\qquad \mathbb E\big[R_T(\pi;v)\big]\le C\sqrt T\,\log^{2.5}T .

The policy may depend on $T$ but not on $F$ or $G$ , and $C$ is absolute. The goal leaves the policy unspecified. That makes it the weakest stable form of the paper's result: any later policy with a better logarithmic factor still proves it.

Milestones, in attack order

Lemma 5 (p. 20): the largest maximiser $b^\star(v)$ of $R(v,\cdot)$ over the grid $\mathcal A$ is non-decreasing in $v$ .
Lemma 4 (p. 20): pathwise, quantization costs at most $(2/M+1/K)T$ regret.
Lemma 3.1 (p. 19): for iid $X_1,\dots,X_T$ in a finite poset of width $\beta$ , $\mathbb E\sum_t(1+\sum_{s<t}\mathbb 1(X_s\preceq X_t))^{-1}\le\beta(1+\log T)^2$ .
Lemma 2 (p. 18): with probability $1-\delta$ , Algorithm 3's minimum counts satisfy $N^{t-1}_{c_t}\ge\sum_{s<t}\mathbb 1(c_s\preceq_{\mathcal C}c_t)/(\alpha\log(MKT^2/\delta))-1$ .
Theorem 5, iid contexts (p. 18): $\mathbb E[R_T]\le1+24\sqrt{\alpha\beta T\log(2T)\log(2MKT^2)\log(2MKT^3)}(1+\log T)$ .
Corollary 1, iid values (p. 20): Algorithm 3 on the quantized auction with $M=K=\lceil\sqrt T\rceil$ , $\delta=1/(2T)$ has expected regret $O(\sqrt T\log^{2.5}T)$ . This is the explicit policy behind the goal.

Significance

The result. Theorem 1 shows that a bidder facing an arbitrary unknown competition distribution can learn to bid as well as the oracle up to $\tilde O(\sqrt T)$ . That rate is optimal up to logarithms: mission 3 of the series formalizes the $\Omega(\sqrt T)$ lower bound. Theorem 5 is of independent interest. For partially ordered contextual bandits with iid contexts, the regret depends on the widths $\alpha,\beta$ of the two orders and not on the numbers $M,K$ of contexts and actions. Mission 5 of the series shows that this fails for adversarial contexts.

Formalizing it. The results are proved in the paper, with full proofs in its Appendix C; none of them has a machine-checked proof. Beyond the theorems, the mission produces a reusable model of repeated auctions with censored feedback, with policies that are non-anticipating by construction. It also produces a definition of contextual bandits with graph feedback and cross learning, and an executable definition of an elimination algorithm with randomized exploration. Lemmas 3, 4 and 5 are self-contained and need no bandit machinery.

Difficulty

The obvious approach discretizes and runs one bandit algorithm per context. That gives regret $\tilde O(\sqrt{MT})$ and, after balancing against the quantization error of Lemma 4, only $\tilde O(T^{2/3})$ . Reaching $\sqrt T$ requires information to flow across contexts. Lemma 2 says that a round with a small context feeds the minimum counts of every larger context. Lemma 3 turns this into a bound on the sum of confidence widths that depends on the width $\beta$ of the context order and not on $M$ . Lemma 2 is a statement about a randomized algorithm whose active sets depend on the whole past, and its proof uses the uniform choice among the sources of the active set together with the extra elimination rule ( $\star\star$ ). The step from a high-probability bound to an expectation over iid contexts must keep the contexts independent of the rewards and of the algorithm's randomness.

Formalization scope

Time and grids. Rounds are Fin T: paper round $t$ is index $t-1$ . The grids (6) are finite sets of reals. Context $i$ and action $j$ of Fin M, Fin K stand for $(i+1)/M$ and $(j+1)/K$ . The paper's $M=K=T^{1/2}$ are $\lceil\sqrt T\rceil$ .
HOB law. $G$ is a probability measure on $\mathbb R$ carried by $[0,1]$ , with $G(x)=\mu_G((-\infty,x])$ . Atoms are allowed.
Policies. A policy has an internal probability space. Its round- $t$ bid takes the values as Fin (t+1) → ℝ and the feedback $\max\{b_s,m_s\}$ as Fin t → ℝ. It never sees $m$ , $G$ or $F$ . The expectation is an integral against $\mu_U\otimes F^{\otimes T}\otimes G^{\otimes T}$ .
Integrability. Every expected-regret bound also asserts that the regret is integrable. This rules out the trivializing reading in which a non-measurable policy has expected regret $0$ (Lean's value of a non-integrable integral).
Horizon. Theorem 1 and Corollary 1 start at $T\ge2$ : at $T=1$ the printed bound is $0$ , but an uninformed first bid has positive regret.
Algorithm 3. The algorithm is a deterministic function of the contexts, the reward vectors and one uniform $u_t\in[0,1]$ per round. The uniform choice in ( $\star$ ) is the $\lfloor u_tn\rfloor$ -th of the $n$ candidates. The topological ordering of the contexts is an argument, and every theorem quantifies over all such orderings. An active set emptied off the good event has minimum count $+\infty$ , and the algorithm then plays action $0$ .
Definition 3. " $a^\star(c)=\arg\max_aR_{c,a}$ " is read as some selection of maximisers that is monotone. The independence numbers enter as upper bounds.
Probabilities. "With probability at least $1-\delta$ " means the failure set has measure at most $\delta$ . Lemma 2 is stated for every fixed context sequence.
Rewards in Corollary 1. The quantized auction rewards lie in $[-1,1]$ , and Algorithm 3 runs on them as printed. The formalization does not claim that they are a Definition 2 instance.

Not stated here: the adversarial parts of Theorem 5 and Corollary 1, Lemma 3.2, and the contextual form of Lemma 1. Proof contributions are welcome at every level. Useful infrastructure includes an anytime concentration bound for running means under adaptive sampling (the contextual Lemma 1) and Dilworth's theorem for finite posets (the step from $\beta=1$ to general $\beta$ in Lemma 3). Lemmas 3, 4 and 5 can be attacked first and independently.

Selected references

Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
N. Alon, N. Cesa-Bianchi, O. Dekel, T. Koren, Online Learning with Feedback Graphs: Beyond Bandits, COLT 2015. https://arxiv.org/abs/1502.07617
S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
R. P. Dilworth, A Decomposition Theorem for Partially Ordered Sets, Annals of Mathematics 51(1), 1950. https://doi.org/10.2307/1969503

12 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Contextual Inverse Optimization: Offline and Online Learning 1: The Circumcenter Policy Has Offline Worst-Case Regret at Most sin α(C(D)), or 1 When α(C(D)) ≥ π/2, and No Policy Does BetterResearch Paper

Motivation

Inverse optimization asks for the objective of an optimization problem when only its optimal decisions are observed. It was formalized for linear programs by Ahuja and Orlin (Operations Research 2001) and has since been used to infer costs, preferences and utilities from observed choices, for instance in routing, pricing and the imitation of expert planners (see the survey discussion in Chan, Lee and Terekhov, Management Science 2019, and the noisy-data setting of Aswani, Shen and Siddiq, Operations Research 2018).

Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) study a contextual version: the problems a decision-maker faces change from instance to instance, and the observed expert decisions constrain a fixed but unknown cost vector. Their question is not how to estimate the cost, but which decisions to take so that the loss against the expert is as small as possible in the worst case. This mission formalizes the answer in the offline setting, where a finite data set is given in advance. The text used is the arXiv preprint v3 (1 July 2023); all theorem numbers refer to it.

Setting

Actions live in $\mathbb R^n$ and costs in $\mathbb R^d$ , both with the Euclidean norm, and $d\ge2$ . The unknown cost $c^\star$ lies on the unit sphere $S^d=\{c:\|c\|=1\}$ .

An instance is a pair $(\mathcal X,f)$ : a feasible set $\mathcal X\in\mathcal B$ , i.e. a nonempty compact subset of $\mathbb R^n$ with diameter at most $1$ , and a context function $f\in\mathcal F$ , i.e. a $1$ -Lipschitz map $\mathbb R^n\to\mathbb R^d$ . Given a cost $c$ , the forward problem is

\psi(c,\mathcal X,f)=\operatorname*{arg\,min}_{x\in\mathcal X} f(x)'c,

a set of minimizers.

The offline data are $\mathcal D=\{(\mathcal X_i,f_i,x^\star_i)\}_{i=1}^N$ with $x^\star_i\in\psi(c^\star,\mathcal X_i,f_i)$ . The costs compatible with them form the knowledge set

C(\mathcal D)=\{c\in S^d:\ c'f_i(x^\star_i)\le c'f_i(x)\ \ \forall x\in\mathcal X_i,\ i=1,\dots,N\}.

A policy maps the data and a new instance $(\mathcal X,f)$ to an action $x^\pi\in\mathcal X$ , and its regret on the instance is $(f(x^\pi)-f(x^\star))'c^\star$ with $x^\star\in\psi(c^\star,\mathcal X,f)$ . The worst-case regret $\mathcal{WCR}^\pi(\mathcal D)$ is the supremum of the regret over $c^\star\in C(\mathcal D)$ , $\mathcal X\in\mathcal B$ and $f\in\mathcal F$ .

The angle between two vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$ , with $\theta(c,0)=\theta(0,\hat c)=0$ . The uncertainty angle of a set $C$ is

\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\ \theta(c,\hat c),

and a circumcenter $\hat c(C)$ is a point of $S^d$ attaining the infimum. Geometrically, $\alpha(C)$ is the aperture of the narrowest revolution cone containing $C$ and $\hat c(C)$ is its axis. The circumcenter policy answers an instance with any $x^\pi\in\psi(\hat c(C(\mathcal D)),\mathcal X,f)$ . Write $g(a)=\mathbf 1\{a<\pi/2\}\sin a+\mathbf 1\{a\ge\pi/2\}$ .

Formalization targets

Goal: Theorem 1 (offline minimax regret), p. 12

For every realizable data set,

\mathcal{WCR}^{\pi}(\mathcal D)\ \le\ g\big(\alpha(C(\mathcal D))\big)

for the circumcenter policy $\pi$ , whatever circumcenter and whatever minimizer it picks. Conversely, for every $\bar\alpha\in[0,\pi]$ there is an information set $C\subseteq S^d$ with $\alpha(C)=\bar\alpha$ on which every policy suffers regret at least $g(\bar\alpha)$ on some instance. The upper bound and the lower bound are one statement.

Milestones

Lemma 1 (p. 11). For a proxy cost $c^\pi\in S^d$ and a true cost $c^\star\in S^d$ , the worst-case regret over instances and over minimizers $x^\pi\in\psi(c^\pi,\mathcal X,f)$ is attained and equals $g(\theta(c^\star,c^\pi))$ :

\mathcal L(c^\pi,c^\star)=\begin{cases}\sin\theta(c^\star,c^\pi)&\theta(c^\star,c^\pi)<\pi/2,\\1&\text{otherwise.}\end{cases}

Lemma 2 (p. 12). Every nonempty $C\subseteq\mathbb R^d$ has a circumcenter; it is unique when $C\setminus\{0\}\neq\emptyset$ and $\alpha(C)<\pi/2$ .

Significance

Theorem 1 identifies the minimax offline regret of contextual inverse optimization with a single geometric number of the knowledge set, $\sin\alpha(C(\mathcal D))$ (or $1$ ), and shows that one explicit policy, acting as if the cost were the circumcenter, attains it uniformly over all instances. It reduces the design of offline policies to computing a circumcenter, and it is the benchmark that the paper's online analysis (§4–§5) compares against: the online policies are judged by how fast they shrink the uncertainty angle.

The results are proved in the paper (App-3–App-9). To our knowledge none of them has a machine-checked proof. Formalizing them yields a verified statement of the minimax value, a reusable notion of uncertainty angle and circumcenter for arbitrary subsets of $\mathbb R^d$ , and the exact tightness of the bound, including the regime $\alpha\ge\pi/2$ where nature can force the maximal regret.

Difficulty

The upper bound is not a direct consequence of the definitions: the regret involves an arbitrary compact action set and an arbitrary $1$ -Lipschitz context, and the only link between the circumcenter's choice and $c^\star$ is that $x^\pi$ is optimal for the wrong cost. Lemma 1 is where this link is turned into an angle, and its value must be matched exactly, not up to constants. Lemma 2 requires care because the objective $\hat c\mapsto\sup_{c\in C}\theta(c,\hat c)$ is a supremum over an arbitrary, possibly non-closed, set and the angle convention at $0$ breaks continuity. The lower bound must hold for every policy, including ones that exploit tie-breaking, so the hard instance must be chosen after the policy.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin d). The angle vecAngle is defined directly with value $0$ when either argument is $0$ ; Mathlib's InnerProductGeometry.angle (which is $\pi/2$ there) is not used. $\alpha$ is a real infimum over the sphere of a real supremum over $C$ ; the angles lie in $[0,\pi]$ , so both are genuine when $C$ is nonempty. Action sets are nonempty compact sets of diameter at most $1$ (nonemptiness is added: an empty feasible set has no action), contexts are $1$ -Lipschitz, and data are indexed by Fin N.

Committed conventions and pins:

$d\ge2$ is the paper's standing assumption (p. 7). $n\ge1$ is added on Lemma 1 and on Theorem 1: in $\mathbb R^0$ every regret is $0$ and the lower bounds would be false.
Theorem 1's upper bound assumes realizable data (some $c_0\in S^d$ explains every observation), as the paper's data model does; this makes $C(\mathcal D)$ nonempty.
Worst-case regrets are never written as real suprema. The upper bound quantifies over every $c^\star\in C(\mathcal D)$ , instance, circumcenter, policy minimizer and expert minimizer. Lemma 1 is stated with IsGreatest, and the lower bound of Theorem 1 in attained form, which implies the paper's statement about the supremum.
In the lower bound the quantifiers are ordered as in the paper: the set $C$ , then the policy (any map from instances to feasible actions), then nature's instance.

A formalization that bounds the regret only for one selected minimizer of the forward problem, or that chooses the hard instance before the policy, proves a different and weaker theorem and is excluded.

The development needs: compactness and lower semicontinuity on the sphere (existence of a circumcenter), elementary spherical geometry for the uniqueness and for $\sin\theta$ as the value of a two-point instance, and monotonicity of $g$ on $[0,\pi]$ . The angle, uncertainty angle and circumcenter definitions are reusable for the online missions of this series. Proofs of the two lemmas are the natural first contributions.

Selected references

O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv preprint v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015v3
R. K. Ahuja, J. B. Orlin, Inverse optimization, Operations Research 49(5):771–783, 2001. https://doi.org/10.1287/opre.49.5.771.10607
T. C. Y. Chan, T. Lee, D. Terekhov, Inverse optimization: closed-form solutions, geometry, and goodness of fit, Management Science 65(3):1115–1135, 2019. https://doi.org/10.1287/mnsc.2017.2992
A. Aswani, Z.-J. Shen, A. Siddiq, Inverse optimization with noisy data, Operations Research 66(3):870–892, 2018. https://doi.org/10.1287/opre.2017.1705
R. Henrion, A. Seeger, Inradius and circumradius of various convex cones arising in applications, Set-Valued and Variational Analysis 18(3–4):483–511, 2010. https://doi.org/10.1007/s11228-010-0150-z

5 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantum Algorithms and Learning Theory — Part II 7: Identifying a codeword state needs Ω(k) copiesTextbook

Motivation

This mission develops Chapter 7 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

For a matrix $M\in\mathbb F_2^{n\times k}$ of rank $k$ (the generator matrix of an $[n,k,d]_2$ linear code) and $x\in\{0,1\}^k$ define the codeword state

|\psi_x\rangle=\frac{1}{\sqrt n}\sum_{i\in[n]}|i,(Mx)_i\rangle .

For every rate $c_1>0$ there is a constant $c_0>0$ such that the following holds for all $n,k$ and all rank- $k$ matrices $M\in\mathbb F_2^{n\times k}$ with $k\ge c_1 n$ : if a measurement (POVM $\{N_y\}_{y\in\{0,1\}^k}$ ) on $T$ copies identifies $x$ from $|\psi_x\rangle^{\otimes T}$ , for $x$ drawn uniformly from $\{0,1\}^k$ , with average success probability

\frac{1}{2^k}\sum_{x\in\{0,1\}^k}\operatorname{Tr}\!\big(N_x\,|\psi_x\rangle\langle\psi_x|^{\otimes T}\big)\ \ge\ \frac45,

then $T\ge c_0\,k$ .

This improves the Holevo-type bound $\Omega(k/\log n)$ to the optimal $\Omega(k)$ for constant-rate codes, showing that codeword fingerprint states cannot be identified from few copies.

Formalization Note " $k=\Omega(n)$ " is read as a fixed rate $k\ge c_1 n$ , and the constant of $\Omega(k)$ may depend on $c_1$ only. Identifying the state means outputting $x$ , which is equivalent since $x\mapsto Mx$ is injective for rank $k$ . The code distance $d$ plays no role and is not a hypothesis.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

Theorem 7.3.1: Barnum–Knill: the pretty good measurement is at most quadratically worse than optimal.
Claim 7.3.5: Fourier coefficients of f composed with a linear map over F2.
Claim 7.3.6: The maximum of (c/√t)^t on [1, c²] is e^{c²/(2e)} (for c ≥ √e).
Fact 7.3.7: Binary entropy: H(ε) = O(ε log 1/ε) and 1 − H(1/2+ε) ≤ 2ε²/ln 2 + O(ε⁴).
Fact 7.3.8: Binomial coefficients and their partial sums are at most 2^{nH(·/n)}.
Fact 7.3.9: Helstrom bound for guessing a uniform bit from |ψ_b⟩, and its corollary.
Fact 7.3.10: Subadditivity of von Neumann entropy.
Lemma 7.4.1: Quantum PAC learners of a non-trivial class need Ω(log(1/δ)/ε) examples.
Lemma 7.4.2: Quantum agnostic learners of a non-trivial class need Ω(log(1/δ)/ε²) examples.
Theorem 7.4.3: Classical PAC sample complexity is Ω(d/ε + log(1/δ)/ε).
Theorem 7.4.4: Classical agnostic sample complexity is Ω(d/ε² + log(1/δ)/ε²).
Theorem 7.4.5: ε-average agnostic learners need (d/ε²)(1/62 − log(2d+2)/(4d)) samples.
Theorem 7.4.6: Quantum PAC sample complexity lower bound (information-theoretic).
Theorem 7.4.7: Quantum agnostic sample complexity lower bound (information-theoretic).
Claim 7.5.2: Eigenvalues of an XOR-convolution matrix are scaled Fourier coefficients.
Claim 7.5.3: Diagonal of √A in terms of Fourier coefficients of f.
Lemma 7.5.4: Fourier coefficients of (1 − β|z|/m)^T are nonnegative and small.
Claim 7.5.5: Counting index sequences whose basis vectors sum to S.
Theorem 7.5.6: Optimal quantum PAC sample complexity lower bound.
Lemma 7.5.7: PGM success bound for the PAC hard ensemble.
Theorem 7.5.8: Optimal quantum agnostic sample complexity lower bound.
Lemma 7.5.9: PGM success bound for the agnostic hard ensemble.
Theorem 7.6.1: Quantum PAC lower bound under random classification noise.
Theorem 7.6.2: Identifying a codeword state needs Ω(k) copies.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08. https://ir.cwi.nl/pub/27536/Thesis_S_Arunachalam.

30 thms3 active usersReviewed

Completed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

Distribution-Free Contextual Dynamic Pricing 2: Every Algorithm Has Expected Regret at Least C₀ C_p T₀ on Some Perturbed Linear Bandit with Perturbation C_pResearch Paper

Motivation

Dynamic pricing asks a seller to post prices to a stream of customers and learn demand from purchase decisions alone. Luo, Sun and Liu study the contextual version in which a customer's valuation is linear in a covariate vector plus noise with an unknown distribution (arXiv:2109.07340v2; Mathematics of Operations Research, 2024). Their DIP policy estimates the linear part, discretizes the remaining price residual, and then runs an upper-confidence-bound rule on the discretized problem. Because the linear part is only estimated, the discretized problem is not an ordinary linear bandit: its reward parameter drifts from period to period by an amount controlled by the estimation error. The paper calls this a perturbed linear bandit (PLB) and proves an upper bound for it whose dominant extra term is linear in the perturbation size times the horizon.

This mission formalizes the matching statement: no algorithm can avoid that linear term. It is the paper's Proposition 2 (p. 22), proved in its Appendix A (pp. 44–46).

Setting

Fix a dimension $d$ . A perturbed linear bandit with perturbation constant $C_p$ consists of parameters $\xi_1,\xi_2,\ldots\in\mathbb R^d$ , finite action sets $\mathcal A_1,\mathcal A_2,\ldots\subset\mathbb R^d$ and noise variables $\eta_1,\eta_2,\ldots$ , with $\|\xi_s-\xi_t\|_\infty\le C_p$ for all periods $s,t$ . In period $t$ an algorithm $\mathcal A^*$ sees the action set $\mathcal A_t$ and the history of its past actions and rewards, plays $A_t\in\mathcal A_t$ , and observes the reward

Z_t=\langle\xi_t,A_t\rangle+\eta_t .

The algorithm may randomize. The parameters $\xi_t$ are never observed.

For a central parameter $\tilde\xi\in\mathbb R^d$ the paper defines the parameter set

PB(\tilde\xi,C_p)=\{\xi\in\mathbb R^d:\ \|\xi-\tilde\xi\|_\infty\le C_p/2\},

so any sequence in $PB(\tilde\xi,C_p)$ has perturbation at most $C_p$ .

The PLB regret over $T_0$ periods compares each action with the best action of the current period:

R^{PLB}_{T_0}(\mathcal A^*)=\sum_{t=1}^{T_0}\Big(\max_{a\in\mathcal A_t}\langle\xi_t,a\rangle-\langle\xi_t,A_t\rangle\Big)\ \ge 0 .

The expectation $\mathbb E$ is over the algorithm's randomness and the noise.

Formalization targets

Goal: Proposition 2 (p. 22)

For every $\tilde\xi$ with positive entries (and $d\ge2$ ) there is $C_0>0$ depending only on $\tilde\xi$ such that for every $C_p\ge0$ with $C_p/2<\min_i\tilde\xi_i$ and every algorithm $\mathcal A^*$ there are parameters $\xi_t\in PB(\tilde\xi,C_p)$ and action sets $\mathcal A_t$ with

\mathbb E\big(R^{PLB}_{T_0}(\mathcal A^*)\big)\ \ge\ C_0\,C_p\,T_0\qquad\text{for all }T_0\ge1 .

The formal statement also records that the constructed instance is a PLB with perturbation $C_p$ , that its action sets are nonempty, and that every action has a single nonzero entry with $|\langle\xi_t,a\rangle|\le1$ , which places the hard instance inside the class covered by the paper's upper bound (Lemma 3, Conditions 1 and 3).

Milestones

Two-point construction (proof of Proposition 2, p. 44). With $C=C_p/2$ , two coordinates $j_u\ne j_v$ , $u=\tilde\xi_{j_u}$ , $v=\tilde\xi_{j_v}$ , actions $U=e_{j_u}/(u+C)$ , $V=e_{j_v}/(v+C)$ and parameters $\xi_u,\xi_v$ obtained from $\tilde\xi$ by moving the two coordinates by $\mp C$ , $\pm C$ :

\xi_u,\xi_v\in PB(\tilde\xi,C_p),\qquad\langle\xi_u,U\rangle=\tfrac{u-C}{u+C}\le1=\langle\xi_v,U\rangle,\qquad\langle\xi_v,V\rangle=\tfrac{v-C}{v+C}\le1=\langle\xi_u,V\rangle .

Per-period bound (pp. 45–46). If $u\le v$ , $A$ is a random action in $\{U,V\}$ , and $\xi_t=\xi_u$ when $P(A=U)\ge1/2$ and $\xi_t=\xi_v$ otherwise, then

\mathbb E(r_t)\ \ge\ C_0C_p,\qquad C_0=\frac1{4v}.

Significance

The result. Lemma 3 of the paper bounds the regret of its M-LinUCB algorithm on a PLB by a $\sqrt{T_0}$ -type term plus $2a_{\max}C_pT_0$ . Proposition 2 shows that the second term is not an artefact of the analysis: an adversary who may move the parameter inside a box of width $C_p$ forces every algorithm to pay order $C_pT_0$ . In the pricing application the perturbation is proportional to the estimation error $\|\hat\theta-\theta_0\|_1$ of the linear part, so the lower bound explains why the paper's pricing regret bound (Theorem 1) carries a term linear in the accumulated estimation error. The result also separates the PLB from the zero-perturbation linear bandit, where $\tilde O(\sqrt{T_0})$ regret is achievable.

Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof requires an explicit model of randomized, history-dependent algorithms interacting with an adversarially chosen but deterministic parameter sequence, which the mission supplies. The model and the two-point construction are reusable for other two-hypothesis lower bounds in linear and contextual bandits.

Difficulty

The obvious argument fixes one hard instance and shows that every algorithm suffers on it. That fails: for a fixed parameter sequence, an algorithm that always plays the optimal action of that sequence has zero regret. The instance must therefore be chosen after the algorithm, and it must be chosen period by period, because the law of the period- $t$ action depends on the rewards of periods $1,\dots,t-1$ , which depend on the parameters already chosen. The parameters must nevertheless be deterministic: the adversary may react to the law of the algorithm's action, not to its realization. Making this recursive construction precise, together with the measurability needed for "the probability that $A_t=U$ " to be meaningful, is the main formal work. The arithmetic of each period is elementary.

A second point concerns the dimension: the construction needs two distinct coordinates, and for $d=1$ the statement fails, since every parameter in $PB(\tilde\xi,C_p)$ is then positive and playing the largest action has zero regret.

Formalization scope

Model. Arms are coordinates Fin d (0-based); periods are 1-based. Vectors are Fin d → ℝ, and $\|\cdot\|_\infty$ is Mathlib's sup norm on that type. Action sets are finite sets (Finset). The maximum over an empty action set is set to $0$ ; every statement requires nonempty action sets.
Algorithms. An algorithm is a decision rule that maps a sample point $\omega$ of a probability space (its internal randomness), the past actions and rewards, and the current action set to an action of that set; it is jointly measurable in $\omega$ and the history. The trajectory $(A_t,Z_t)$ is defined recursively from the rule, the parameters, the action sets and the noise. Since the rule sees all of $\omega$ , it may also depend on the noise; this only enlarges the class over which the lower bound holds.
Noise. The goal quantifies over every measurable noise process. The paper's PLB asks for conditionally sub-Gaussian noise; since $\eta\equiv0$ is allowed, the formal statement is stronger than the printed existence statement, and the paper's proof uses no property of the noise.
Instance. The parameters and action sets are deterministic and are chosen after the algorithm, the probability space and the noise. The constant $C_0$ is chosen after $\tilde\xi$ and before $C_p$ , the algorithm and $T_0$ , which is the formal content of "only dependent on $\tilde\xi$ ".
Added hypotheses. $d\ge2$ (necessary, see above) and $C_p\ge0$ (otherwise $PB(\tilde\xi,C_p)$ is empty).
Expectation. Expected regret is the lower Lebesgue integral of the nonnegative regret, so no integrability convention can make the bound hold vacuously. The bound is positive whenever $C_p>0$ ; a formalization in which the expectation could collapse to a default value, or the algorithm class could be empty, is ruled out (the class contains every fixed-choice rule).
Source. The source is the arXiv v2 preprint (6 March 2023); the paper's proofs are in its Appendix A.

Contributions welcome: proofs of the two milestones, the measurability of the recursively defined actions, and the summation step from the per-period bound to the goal.

Selected references

Y. Luo, W. W. Sun, Y. Liu, Distribution-Free Contextual Dynamic Pricing, Mathematics of Operations Research, 2024. Preprint arXiv:2109.07340v2; DOI 10.1287/moor.2023.1369.
Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS, 2011. link
T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

5 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

A Single Timescale Stochastic Approximation Method for Nested Stochastic Optimization: NASA with Stepsizes 1/√N Drives the Expected Stationarity Measure E[V(x_R, z_R)] Below C/(√N − 1)Research Paper

Motivation

Many learning and risk-averse decision problems minimize a function of an expectation that is itself passed through another function: $F(x)=f(g(x))$ with $g(x)=\mathbb E[G(x,\xi)]$ . Examples are mean–deviation risk measures, stochastic variational inequalities rewritten as minimization, and policy evaluation in reinforcement learning. Only noisy samples of $g$ , of its Jacobian and of $\nabla f$ are available, and the plug-in estimate $\nabla g(x)^\top\nabla f(G)$ of $\nabla F(x)$ is biased because $f$ is nonlinear. Classical stochastic gradient analysis does not apply directly.

Timeline of sample complexities for smooth nonconvex two-level problems, measured by the number of samples needed to reach an $\varepsilon$ -stationary point:

2017 — Wang, Fang and Liu (Math. Program.) introduce stochastic compositional gradient descent with two time scales; the unconstrained nonconvex rate is $O(\varepsilon^{-4})$ in their measure.
2017 — Wang, Liu and Fang (JMLR) accelerate it to $O(\varepsilon^{-2.25})$ for smooth unconstrained problems, still with two time scales.
2019–2020 — Ghadimi, Ruszczyński and Wang (arXiv:1812.01094, SIAM J. Optim. 2020) propose NASA, a single-time-scale method with one sample per iteration, and prove $O(\varepsilon^{-2})$ for constrained problems. This mission formalizes that result.

Setting

Problem (1.1) is

\min_{x\in X} F(x)=f(g(x)),

where $f:\mathbb R^m\to\mathbb R$ and $g:\mathbb R^n\to\mathbb R^m$ are continuously differentiable, $X\subseteq\mathbb R^n$ is closed and convex, and nothing is convex. Assumption 2 asks that $f$ , $g$ , $\nabla f$ , $\nabla g$ be Lipschitz with constants $L_f,L_g,L_{\nabla f},L_{\nabla g}$ ; then $\nabla F$ is Lipschitz with $L_{\nabla F}=L_g^2L_{\nabla f}+L_fL_{\nabla g}$ . $F^*$ is the infimum of $F$ over $X$ .

For $\beta>0$ the subproblem solution is $\bar y(x,z,\beta)=\operatorname{argmin}_{y\in X}\{\langle z,y-x\rangle+\frac\beta2\|y-x\|^2\}=\Pi_X(x-z/\beta)$ , with $\Pi_X$ the Euclidean projection. A pair $(x,z)$ is judged by the optimality measure

V(x,z)=\|\bar y(x,z,1)-x\|^2+\|z-\nabla F(x)\|^2,

which vanishes exactly when $z=\nabla F(x)$ and $-\nabla F(x)$ lies in the normal cone to $X$ at $x$ .

The NASA method (Algorithm 1) keeps three sequences: iterates $x^k\in X$ , gradient averages $z^k$ and value averages $u^k$ . With parameters $a,b>0$ , regularization $\beta>0$ and stepsizes $\tau_k\in(0,1/a]$ :

x^{k+1}=x^k+\tau_k(\bar y(x^k,z^k,\beta)-x^k),\quad z^{k+1}=(1-a\tau_k)z^k+a\tau_k[J^{k+1}]^\top s^{k+1},\quad u^{k+1}=(1-b\tau_k)u^k+b\tau_kG^{k+1}.

Assumption 1 governs the oracle. Given $\mathcal F_k$ , the outputs $G^{k+1}$ , $J^{k+1}$ and $s^{k+1}$ are conditionally unbiased for $g(x^{k+1})$ , $\nabla g(x^{k+1})$ and $\nabla f(u^k)$ . Their second moments are bounded by $\sigma_G^2,\sigma_J^2,\sigma_s^2$ , and $s^{k+1}$ , $J^{k+1}$ are conditionally independent. The analysis rests on the merit function $W(x,z,u)=a(F(x)-F^*)-\eta(x,z)+\frac\gamma2\|g(x)-u\|^2$ , where $\eta$ is the optimal value of the subproblem.

Formalization targets

Goal: Theorem 2(c), (3.37)

With $a=b=1$ , $\beta=\big(\frac{(1+\alpha)^2}{\alpha}L_g^2+\frac\alpha4\big)L_{\nabla f}$ for some $\alpha>0$ , $\tau_0=1$ , $\tau_k=1/\sqrt N$ for $k\ge1$ , $N\ge2$ , and $R$ uniform on $\{1,\dots,N-1\}$ :

\mathbb E[V(x^R,z^R)]\le\frac4{\sqrt N-1}\Big(\frac2{\alpha L_{\nabla f}}\big[\max(L_1,L_2)+\max(1,\beta^2)\big]\big[W(x^0,z^0,u^0)+\hat\sigma^2\big]+\sigma_J^2\sigma_s^2\Big).

The constants $L_1,L_2$ (3.32) and $\hat\sigma^2$ are explicit in the problem data. This is the paper's headline rate, and every other statement of the mission feeds it.

Milestones

Lemma 1: $\|\bar y(x,z,1)-x\|\le\max(1,\beta)\|\bar y(x,z,\beta)-x\|$ .
Lemma 2: $\nabla F$ is $L_{\nabla F}$ -Lipschitz.
Lemma 3: $\eta$ has an $L_{\nabla\eta}$ -Lipschitz gradient in $(x,z)$ .
(3.21): $\langle z,d\rangle+\beta\|d\|^2\le0$ for the subproblem step $d$ .
Lemma 4: the pathwise descent inequality $c\sum\tau_k(\|d^k\|^2+\|g(x^k)-u^k\|^2)\le W(x^0,z^0,u^0)+\sum r^{k+1}$ .
Proposition 1(a): moment bounds on $z^k$ and $d^k$ .
Proposition 1(b): $\sum\mathbb E[r^{k+1}]\le\hat\sigma^2\sum\tau_k^2$ .
(3.29): $V(x,z)\le\max(1,\beta^2)\|d\|^2+\|z-\nabla F(x)\|^2$ .
Theorem 2(a): the weighted gradient-tracking error.
Theorem 2(b): the bound on $\mathbb E[V(x^R,z^R)]$ for general admissible stepsizes.

Significance

The result. Theorem 2(c) gives $\mathbb E[V(x^R,z^R)]\le\varepsilon$ after $O(\varepsilon^{-2})$ iterations with one oracle call each. That matches the complexity of stochastic gradient descent on single-level smooth nonconvex problems, so the nested structure costs only constants. The bound holds with constraints, and $z^R$ comes with a certified estimate of $\nabla F(x^R)$ . The same merit-function technique underlies later single-time-scale methods for multi-level and conditional stochastic optimization.

Formalizing it. The result is proved on paper, not formalized. A machine-checked proof requires the whole chain, Lemma 4 through Theorem 2, to be stated with constants that the argument actually supports. Several printed constants do not meet that bar (see Formalization scope), so the formalization also certifies a corrected version of the theorem. The deterministic milestones (Lemmas 1–3, (3.21), (3.29)) are general facts about Euclidean projections and value functions of strongly convex subproblems, and other projected-gradient developments can reuse them.

Difficulty

The obvious approach fails. Analyzing $F(x^k)$ alone does not work because the step uses $z^k$ , a biased and correlated estimate of $\nabla F(x^k)$ , and its error does not vanish at a single time scale. The analysis instead tracks the coupled potential $W$ . Each of its three terms needs a different tool: the descent lemma for $F$ , the smoothness of the value function $\eta$ (Lemma 3, which needs differentiability of a parametric minimum), and a recursion for $u^k$ . These pieces must combine under the single coupling condition (3.16). The probabilistic part is delicate as well. The cross terms vanish only in expectation, they require conditional independence of $J^{k+1}$ and $s^{k+1}$ , and their integrability is not automatic. Theorem 2(a) adds a weighted unrolling of the $z$ -recursion through the products $\Gamma_k$ and the summation condition (3.30).

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). Jacobians are continuous linear maps with the operator norm, and $\nabla g(x)^\top$ is the adjoint. The projection is a function $P$ with the published predicate SpectralProjGrad.Shared.IsProjOnto X P, and $\bar y(x,z,\beta)=P(x-\beta^{-1}z)$ . $\eta$ is the subproblem objective evaluated at $\bar y$ , and Lemma 3 places $(x,z)$ in the $L^2$ product WithLp 2 (ℝⁿ × ℝⁿ). $F^*$ is sInf over $X$ , and $F$ is assumed bounded below on $X$ . The regularization $\beta_k\equiv\beta$ and the stepsizes are deterministic.

The randomness lives on a standard Borel probability space. Assumption 1 is stated with respect to any filtration to which $x^k,z^k,u^k$ are adapted, which includes the paper's natural filtration. It requires square-integrable oracle outputs, so that no conditional-expectation hypothesis is vacuous. Statements printed with conditional expectations on the left and constants on the right (Proposition 1, Theorem 2(a)) are stated in total expectation, which is what the proofs establish. Every conclusion about an expectation includes the integrability of the integrand, so a bound cannot hold because a non-integrable integral defaults to $0$ . $\mathbb E[V(x^R,z^R)]$ is the $\tau$ -weighted average of $\mathbb E[V(x^k,z^k)]$ over $k=1,\dots,N-1$ (3.34). Lemma 4 is deterministic: it holds along every path of the recursions, whatever the oracle outputs. The recursions tie $y^k$ to the projection and $z^k,u^k$ to the oracle outputs, so the goal cannot be satisfied by arbitrary sequences or by a vacuous oracle.

Corrections to printed constants, each stated in the item's Formalization Note:

(3.18): the noise term of $r^{k+1}$ carries $\gamma b^2$ , not $b^2$ . The printed Lemma 4 has a counterexample.
(3.26): $\hat\sigma^2$ uses $aL_{\nabla F}$ , $\max(\sigma_J^2\sigma_s^2,\|z^0\|^2)/\beta^2$ (the $k=0$ term) and $\gamma b^2\sigma_G^2$ .
(3.33): the coefficient of $\max(1,\beta^2)\hat\sigma^2$ is $1/c$ , not $a\bar c/c$ . The two agree when $a\bar c=1$ .
(3.37): the denominator is $\alpha L_{\nabla f}$ , not $\alpha L_{\nabla F}$ , since the proof sets $c=\alpha L_{\nabla f}/4$ . The proof also fixes $\gamma=\alpha L_{\nabla f}$ in $W$ and $\hat\sigma^2$ .
Proposition 1(a): the bound $\mathbb E\|z^k\|^2\le\sigma_J^2\sigma_s^2$ is false conditionally on $\mathcal F_{k-1}$ and is stated in expectation.
Hypotheses the proofs use but the statements omit: $\tau_k\le1$ , $b\tau_k\le1$ , $a\beta\ge c$ and $\gamma b\ge2c$ , $\tau_0=1/a$ (Theorem 2(a),(b)), $N\ge2$ , and $L_{\nabla f}>0$ .

The second claim (3.38) of Theorem 2(c) is excluded: its printed constant is smaller than what the proof gives. Theorem 3 (asymptotics) and the ASA variant of §4 are out of scope. Contributions are welcome at every milestone. Solvers will need Euclidean projection characterizations, differentiability of the squared distance to a convex set, conditional-independence product rules for conditional expectations, and Abel-type summation for the $\Gamma_k$ weights.

Selected references

S. Ghadimi, A. Ruszczyński, M. Wang, A Single Time-Scale Stochastic Approximation Method for Nested Stochastic Optimization, arXiv:1812.01094v2, 2019; SIAM J. Optim. 30(1), 2020. https://arxiv.org/abs/1812.01094
M. Wang, E. X. Fang, H. Liu, Stochastic compositional gradient descent: algorithms for minimizing compositions of expected-value functions, Math. Program. 161, 2017. https://doi.org/10.1007/s10107-016-1017-3
M. Wang, J. Liu, E. X. Fang, Accelerating stochastic composition optimization, JMLR 18(105), 2017. https://jmlr.org/papers/v18/16-504.html
S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
A. Ruszczyński, Nonlinear Optimization, Princeton University Press, 2006.

14 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Stochastic Gradient Descent, Weighted Sampling, and the Randomized Kaczmarz Algorithm: SGD with Step γ < 1/sup L Has E‖x_k − x⋆‖² ≤ [1 − 2γμ(1 − γ sup L)]^k ‖x₀ − x⋆‖² + γσ²/(μ(1 − γ sup L))Research Paper

Motivation

Stochastic gradient descent (SGD) minimizes an objective that is an expectation, $F(x) = \mathbb E_{i\sim\mathcal D} f_i(x)$ , by stepping along the gradient of one randomly drawn component at a time. It is the workhorse of large-scale machine learning, where $F$ is an average loss over training examples, and it also contains the randomized Kaczmarz method for linear systems, where each component is a single squared residual $\frac12(\langle a_i, x\rangle - b_i)^2$ (Strohmer & Vershynin 2009).

For smooth, strongly convex objectives, the question is how fast a fixed step size drives the iterates to the minimizer $x_\star$ , and how the rate depends on the smoothness constants $L_i$ of the components. Bach & Moulines (2011) showed that an iteration count scaling with the squared conditioning $\mathbb E L_i^2/\mu^2$ suffices. Needell, Srebro and Ward (arXiv:1310.5715v5, Theorem 2.1) replaced this by a dependence that is linear in the uniform conditioning $\sup L/\mu$ . Their theorem is the base of the rest of the paper: Corollary 2.2 (choice of step size), the importance-sampling results of Section 3 (weighting components by $L_i$ ), and the Kaczmarz rates of Section 5 are all derived from it.

Timeline:

1951, Robbins and Monro: stochastic approximation.
2009, Strohmer and Vershynin: expected linear convergence of randomized Kaczmarz with rows sampled proportionally to their squared norms.
2011, Bach and Moulines: fixed-step SGD on strongly convex smooth objectives, with an iteration count of order $\log(\varepsilon_0/\varepsilon)(\mathbb E L_i^2/\mu^2 + \sigma^2/(\mu^2\varepsilon))$ .
2013–2015, Needell, Srebro and Ward: the bound below, linear in $\sup L/\mu$ , and its importance-sampling and Kaczmarz corollaries.

Setting

Let $\mathcal D$ be a probability distribution, the source distribution, on an arbitrary measurable index space $I$ . Let $\mathcal H$ be a real Hilbert space (for example $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$ ), and let $f_i : \mathcal H \to \mathbb R$ , $i \in I$ , be a family of functions. The objective is

F(x) = \mathbb E_{i\sim\mathcal D} f_i(x),

and $x_\star$ is a minimizer of $F$ . The paper assumes:

each $f_i$ is convex and differentiable, and its gradient $\nabla f_i$ is Lipschitz with constant $L_i$ : $\|\nabla f_i(x) - \nabla f_i(y)\|_2 \le L_i\|x - y\|_2$ ;
$F$ is $\mu$ -strongly convex: $\langle x - y, \nabla F(x) - \nabla F(y)\rangle \ge \mu\|x - y\|_2^2$ for all $x, y$ .

The number $\sup L$ is an almost-sure upper bound on $L_i$ , and the residual is

\sigma^2 = \mathbb E\|\nabla f_i(x_\star)\|_2^2,

which vanishes exactly when $x_\star$ is a stationary point of every component (the realizable case).

The SGD iterates with fixed step size $\gamma$ start at $x_0 \in \mathcal H$ and follow (2.2):

x_{k+1} = x_k - \gamma\nabla f_{i_k}(x_k),

where $i_0, i_1, \dots$ are drawn independently from $\mathcal D$ . The iterate $x_k$ is a random point that depends on $i_0, \dots, i_{k-1}$ . In Lean these objects are objective D f, residual D f xstar, iidLaw D (the law of the index sequence) and sgdIter f γ x0 k ω in the namespace SGDKaczmarz.SGD.

Formalization targets

Goal: Theorem 2.1, (2.4)

If $0 < \gamma < 1/\sup L$ , then for every $k \ge 0$

\mathbb E\|x_k - x_\star\|_2^2 \le \Bigl[1 - 2\gamma\mu(1 - \gamma\sup L)\Bigr]^k\|x_0 - x_\star\|_2^2 + \frac{\gamma\sigma^2}{\mu(1 - \gamma\sup L)},

where the expectation is over the sampling of $\{i_k\}$ . The constants are the paper's; nothing is left unfixed.

Milestones

In the order of the paper's proof (Appendix A):

(A.1): at a minimizer $x_\star$ of a function with $L$ -Lipschitz gradient, $\frac{1}{2L}\|\nabla f(x) - \nabla f(x_\star)\|_2^2 \le f(x) - f(x_\star)$ ;
Lemma A.1 (co-coercivity): $\|\nabla f(x) - \nabla f(y)\|_2^2 \le L\langle x - y, \nabla f(x) - \nabla f(y)\rangle$ ;
the pathwise one-step bound on $\|x_k - x_\star - \gamma\nabla f_i(x_k)\|_2^2$ ;
unbiasedness: $\mathbb E\nabla f_i(x) = \nabla F(x)$ ;
the expected one-step recursion $\mathbb E\|x_{k+1} - x_\star\|_2^2 \le (1 - 2\gamma\mu(1 - \gamma\sup L))\|x_k - x_\star\|_2^2 + 2\gamma^2\sigma^2$ for $\gamma \le 1/\sup L$ ;
the unrolled recursion, with the finite geometric sum $2\sum_{j<k}(1 - 2\gamma\mu(1 - \gamma\sup L))^j\gamma^2\sigma^2$ .

Significance

The bound has two terms: a contraction at rate $1 - 2\gamma\mu(1 - \gamma\sup L)$ and a floor proportional to $\gamma\sigma^2$ . Choosing $\gamma$ to balance them (Corollary 2.2) gives an iteration count of order $\log(\varepsilon_0/\varepsilon)(\sup L/\mu + \sigma^2/(\mu^2\varepsilon))$ , linear rather than quadratic in the conditioning. In the realizable case $\sigma^2 = 0$ it is a pure linear rate. Reweighting the distribution by $L_i$ turns $\sup L$ into the average $\bar L = \mathbb E L_i$ (Section 3), and specializing to least squares yields convergence rates for randomized Kaczmarz with uniform, weighted and hybrid row selection (Section 5). These consequences are stated in terms of Theorem 2.1, so a formal version of the theorem is the prerequisite for formalizing any of them.

The result is proved on paper (Appendix A.2). The work here is to formalize that proof: co-coercivity in a Hilbert space, differentiation of $F = \mathbb E f_i$ under the expectation, and the passage from a conditional one-step bound to the unconditional bound over an i.i.d. sequence. To our knowledge no machine-checked proof of Theorem 2.1 exists. The platform has formal results on projected SGD with decaying steps and on the finite-sum Kaczmarz iteration, which state different results.

Difficulty

The one-step algebra is routine once co-coercivity is available. What is hard is making the expectation rigorous. On the page, " $\mathbb E\|x_{k+1} - x_\star\|^2$ " in the recursion is an expectation over the index $i_k$ alone, with $x_k$ held fixed. Iterating it requires that $x_k$ be a measurable function of $i_0, \dots, i_{k-1}$ , that $i_k$ be independent of it, and that expectations of possibly non-integrable nonnegative quantities be handled without junk values. The unbiasedness step $\mathbb E\nabla f_i = \nabla F$ is a differentiation under the integral sign in a possibly infinite-dimensional space, and it needs a dominating bound that comes from the almost-sure bound on $L_i$ together with the finiteness of $\sigma^2$ . A tempting shortcut, assuming $\nabla f_i(x_\star) = 0$ for every $i$ , gives only the realizable special case $\sigma^2 = 0$ and is not the theorem.

Formalization scope

Space. $\mathcal H$ is a complete real inner-product space with its Borel σ-algebra and a second-countable topology (every separable Hilbert space, including $\mathbb R^d$ ). Separability makes the iterates random variables.
Gradients. These are Mathlib's gradient. Assumption (1) is LipschitzWith (L i) (gradient (f i)) with L i : ℝ≥0, together with Differentiable ℝ (f i) and ConvexOn ℝ Set.univ (f i) for every $i$ .
The objective. $F$ is the Bochner integral $x \mapsto \int f_i(x)\,d\mathcal D$ , under the hypothesis that $i \mapsto f_i(x)$ is integrable for every $x$ . The gradient maps $i \mapsto \nabla f_i(x)$ are assumed measurable.
Strong convexity. Assumption (2) is stated in the paper's gradient-monotone form for gradient (objective D f). Differentiability of $F$ is not assumed separately: it follows whenever $\sigma^2 < \infty$ (milestone "unbiasedness").
The constant $\sup L$ . It is any real number with $L_i \le \sup L$ almost surely. This is equivalent to the paper's essential supremum, because the bound is increasing in $\sup L$ .
Step-size conditions. $\gamma < 1/\sup L$ is written γ * supL < 1 (and $\gamma \le 1/\sup L$ as γ * supL ≤ 1), with $0 < \gamma$ and $0 < \mu$ .
Expectations. $\mathbb E\|x_k - x_\star\|^2$ and $\sigma^2$ are lower Lebesgue integrals in $[0,\infty]$ : the first over the infinite product law Measure.infinitePi of the index sequence, the second over $\mathcal D$ . A non-integrable iterate therefore cannot satisfy the bound vacuously, and $\sigma^2 = \infty$ makes the right side $\infty$ , which is the paper's meaning.
Indexing. $x_0$ is the initial point and $x_k$ is the point after $k$ steps.
Hypotheses. The co-coercivity lemma carries convexity of $f$ , which its proof uses and without which it is false. No hypothesis such as $\nabla f_i(x_\star) = 0$ , $\sigma^2 < \infty$ or $\mu \le \sup L$ is added to the goal.

Infrastructure that a complete development needs, and that is reusable beyond this mission:

co-coercivity of gradients of smooth convex functions on Hilbert spaces;
differentiation under the expectation for families with uniformly Lipschitz gradients;
the tower property for a measurable recursion driven by Measure.infinitePi.

Contributions of any of these as separate lemmas are welcome.

Selected references

D. Needell, N. Srebro, R. Ward, Stochastic gradient descent, weighted sampling, and the randomized Kaczmarz algorithm, arXiv:1310.5715v5, 2015 (Mathematical Programming 155, 2016). https://arxiv.org/abs/1310.5715v5
F. Bach, E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, NIPS 2011. https://hal.science/hal-00608041
T. Strohmer, R. Vershynin, A randomized Kaczmarz algorithm with exponential convergence, J. Fourier Anal. Appl. 15(2):262–278, 2009. https://doi.org/10.1007/s00041-008-9030-4
H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22:400–407, 1951. https://doi.org/10.1214/aoms/1177729586
Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

8 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Modern Introduction to Online Learning XI: Constrained Online Convex Optimization Reduces to Unconstrained Learning on Distance-Penalized Surrogate LossesTextbook

Motivation

An online learner repeatedly chooses a point, observes a loss, and is judged by the difference between its accumulated loss and that of a fixed competitor. In practice, an available learner may operate on a broad feasible set $W$ , while the application permits decisions only in a smaller set $V$ . Replacing each output by a feasible point changes the learner's losses, so its existing regret guarantee no longer directly applies. Chapter 12 of Orabona's text develops reductions that use the learner as a black box: they change the feedback sent to it and recover a guarantee for the constrained predictions.

The chapter treats Euclidean and other norms, Bregman projections, sleeping experts, and the separation of magnitude from direction. This mission focuses on its first general construction, Theorem 12.5. It is useful when the internal update of the learner is unavailable or when a solver wants to reuse one unconstrained algorithm across several constraint sets. The theorem gives four explicit surrogate losses and an explicit bound on their subgradient norms. Orabona, Chapter 12 also explains how its distance based construction relates to regret matching on the simplex.

Setting

Work in a finite-dimensional real vector space $E$ with an arbitrary norm $\|\cdot\|$ . Its continuous dual consists of real-valued linear functionals; $g(v)$ is the pairing and $\|g\|_*$ is the dual norm. Let $V\subseteq W\subseteq E$ , with $V$ nonempty, closed, and convex. The distance to $V$ and the generalized projection are

d_V(z)=\min_{y\in V}\|z-y\|, \qquad \Pi_V(z)=\{x\in V:\|z-x\|=d_V(z)\}.

The minimum exists under these assumptions. A projection need not be unique for an arbitrary norm; the construction accepts any $x_t\in\Pi_V(z_t)$ . In round $t$ , an underlying learner outputs $z_t\in W$ , the reduction predicts $x_t\in V$ , and the environment reveals a real-valued loss $\ell_t$ . Choose a subgradient $g_t$ of $\ell_t$ at $x_t$ that satisfies the subgradient inequality for competitors in $V$ . Choose any full-space subgradient $q_t\in\partial d_V(z_t)$ . For a fixed $u\in V$ , the constrained regret is

\operatorname{Regret}_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).

The surrogate losses are functions passed back to the learner. Their four formulas are the distance-penalized linear loss, its linear form using $q_t$ , a distance penalty activated only when $g_t(x_t-z_t)>0$ , and that activated penalty's linear form. Each is defined on the ambient space, then used on $W$ . The projection rule and the selected subgradients are the only information the reduction needs from a run.

Formalization targets

Constrained regret from surrogate regret

For each of the four choices $k$ in Theorem 12.5 and every $u\in V$ , the goal is

\operatorname{Regret}_T(u) \le \sum_{t=1}^{T}\bigl(\widetilde\ell_t^{(k)}(z_t) -\widetilde\ell_t^{(k)}(u)\bigr).

The theorem is pathwise: it applies to any sequence of predictions $z_t$ that the underlying learner could produce. No particular learner or regret rate is built into the target. Equation (12.2) isolates the linearized regret term that each surrogate must cover. The four clauses of Lemma 12.2 establish convexity, the exact Lipschitz constant, the zero subgradient on $V$ , and the subdifferential characterization outside $V$ .

Surrogate subgradient size

The companion clause of Theorem 12.5 says that every full-space subgradient $\widetilde g_t$ of a surrogate at a point of $W$ satisfies

\|\widetilde g_t\|_*\le 2\|g_t\|_*.

The factor $2$ is part of the printed result. It applies to all four choices, including the branches at which the activation term vanishes.

Significance

The result transfers a regret guarantee from an algorithm working on $W$ to feasible decisions in $V$ through a loss transformation. The norm bound makes this transfer quantitative for algorithms whose guarantees depend on subgradient magnitudes: the new losses have controlled scale. Lemma 12.2 is reusable apart from online learning, because it describes distance and subgradients for a closed convex set in any finite-dimensional normed geometry.

Orabona presents these as established mathematical results in Theorem 12.5 and Lemma 12.2. The work here is to give them auditable Lean statements and, subsequently, machine-checked proofs. The chapter's Bregman projection, sleeping-experts, and magnitude/direction reductions are separate results; this proposal leaves them for later missions or additions. A proof of the present goal would make the first black-box reduction reusable without depending on a specific unconstrained learner's implementation.

Difficulty

Simply projecting $z_t$ into $V$ leaves an extra term in the linearized regret: the old learner was evaluated at $z_t$ while the actual loss was incurred at $x_t$ . An arbitrary correction to the feedback can cover that term while destroying convexity or greatly enlarging gradients. The four formulas balance both requirements, and the two activated formulas must also handle the boundary case $x_t=z_t$ , where a normalized direction would otherwise divide by zero. Generalized projections create another issue: an argument cannot silently assume one canonical nearest point when the norm is not Euclidean.

Formalization scope

Lean uses a finite-dimensional real normed space and represents dual vectors as continuous linear functionals. Their operator norm is the book's dual norm. The distance is Metric.infDist; nonemptiness keeps its value meaningful, and closedness plus finite dimensionality supplies an attained minimum. Projection is a relation, so all valid choices are covered. Sequences start at index $1$ ; index $0$ is unused, and the horizon is explicitly at least one. The original losses are real-valued on the ambient space, with the subgradient inequality required only for comparators in $V$ . The distance and surrogate subgradients use the full-space inequality. This matters when $W$ has empty interior: a relative subgradient on $W$ can have an arbitrary normal component and would make the printed norm bound false.

The underlying algorithm is abstracted by its sequence $z_t\in W$ ; its surrogate regret is exactly the sum on the right of the goal. $W$ is allowed to be strictly larger than $V$ , so the statement retains the constraint-reduction content. The normalized direction in the third and fourth surrogates appears only in the branch with $g_t(x_t-z_t)>0$ , which implies $x_t\ne z_t$ . Contributions toward the distance-function lemmas, the surrogate inequalities, and the gradient bound all support the goal. The same geometric definitions can also support later reductions based on other projections.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 12, pp. 192–205. arXiv

9 thms3 active usersReviewed

Missions

The Power of Subsampling in Submodular Maximization: SampleGreedy is a (p+1)²/p-approximation for non-negative submodular maximization over p-extendible systemsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 7)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamic Pricing with Unknown Non-Parametric Demand and Limited Price Changes: The SLPE Policy Has Regret O(√T log T log log T) on Its Concentration Event and Makes O(log log T) Price ChangesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 and Corollary 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models: The Adaptive-Confidence Trisection Policy Has N-Independent Regret at Most C√TResearch Paper

Learning which products to offer

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Geometric Deep Learning IX: Message-Passing GNNs Are No More Powerful Than the Weisfeiler–Lehman Test — Equal Colour Histograms Force Equal OutputsTextbook

Motivation

Setting

Formalization targets

Goal: GNNs are bounded by WL

Milestones

Companion: reaching the bound

Significance

Difficulty

Formalization scope

Selected references

Geometric Deep Learning VIII: An RNN Seeded at a Fixed Point h⁽⁰⁾ = R(0, h⁽⁰⁾) Is Equivariant to Left Shifts of a Zero-Padded Input SequenceTextbook

Why sequence boundaries matter

RNN runs and padded sequences

Formalization targets

What the result supplies

The boundary difficulty

Formalization scope

Selected references

Geometric Deep Learning III: An n × n Matrix Commutes with the Cyclic Shift S if and only if It Is Circulant, So Convolution Is Shift EquivarianceTextbook

Why convolution, and why the shift

Setting

Formalization targets

Goal: commuting with the shift characterises circulant matrices

Milestones, in attack order

Companion: the Convolution Theorem

Significance

Difficulty

Formalization scope

Selected references

Speculative Actions: A Lossless Framework for Faster Agentic Systems: Exact Expected Runtime Ratio of k-Branch Speculation Under Exponential LatenciesResearch Paper

Motivation

Setting

Formalization targets

Random-runtime identities

Proposition 1

Significance

Difficulty

Formalization scope

Selected references

Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination: The Partial Identification Set of Demographic Disparity Is the Closed Interval with Fréchet–Hoeffding EndpointsResearch Paper

Why the disparity is uncertain

Observed information and compatible joints

Formalization targets

What the result gives

Central difficulty

Formalization scope

Selected references

Exact slow rate on $\mathcal H$

Slow rate on $\mathcal F$

Fast rate on $\mathcal G_{2k}$