All missions

Why oscillating coefficients matter

An equation driven by fractional Brownian motion can respond to a rapidly varying coefficient even when that coefficient has no useful pointwise limit. Hairer and Li study this issue for fractional Brownian motion with Hurst index above one half. Their Section 3 isolates a deterministic averaging statement: if the time antiderivatives of the coefficients approach those of a limiting coefficient in a suitable negative Hölder norm, the solutions approach the limiting solution in probability. This statement supplies a common target for averaging models whose fast variables have very different origins. The authors use it later with mixing fast processes, and also present a quasi-periodic example. The result and its role in the paper are stated in Hairer and Li, Section 3.

The problem sits at the boundary of two familiar views of differential equations. A pathwise Young equation is defined from individual sufficiently regular paths, whereas the available estimates for the oscillating coefficient and the fractional Brownian driver involve probability and conditional expectation. The mission records the precise point where these descriptions meet. It treats the published article, rather than a preprint, and targets its Theorem 3.13.

Driver, coefficients, and solutions

An $m$-dimensional fractional Brownian motion $B=(B^1,\ldots,B^m)$ with index $H$ is a centered Gaussian process with independent coordinates and covariance

The paper works with a two-sided process and $1/2<H<1$. It uses a version whose sample paths are locally $\beta$-Hölder for every $\beta<H$. The mission names that version condition separately, because the covariance law alone does not select particular sample paths. The relevant past sigma algebra at time $s$ is generated by increments $B_u-B_v$ with $u,v\le s$. These conventions come from pp. 1826 and 1831–1832 of the article.

For a path $x$ on $[0,T]$, write $|x|_\alpha$ for its homogeneous Hölder seminorm and $|x|_\infty$ for its supremum norm. The norm on $C^\alpha[0,T]$ is $|x|_\infty+|x|_\alpha$. A Young integral $\int_s^t f_r\,db_r$ is the limit of left-point sums over partitions of $[s,t]$ as the largest cell shrinks to zero. A Young solution from $x_0$ is an $\alpha$-Hölder path satisfying its integral equation at every time, with value $x_0$ at time zero. Here $BC^2$ means bounded, twice continuously differentiable maps with bounded derivatives through order two; $C^{\zeta,2}$ means $\zeta$-Hölder in time with values in $BC^2$. These are the paper's conventions on pp. 1829 and 1835–1838.

The negative Hölder bound $|f|_{-\kappa,\gamma}\le K$ means that the time antiderivative of $f$ has increments bounded by $K|t-s|^{1-\kappa}$, and that the difference of those increments at spatial points $x,y$ is bounded by $K|t-s|^{1-\kappa}|x-y|^\gamma$. Both bounds apply on the time window in question when $|t-s|\le1$. This is equation (3.12) in the article. It measures cancellation over time; it does not require $f(t,x)$ itself to be small.

Formalization targets

The goal is the $dB$ part of Theorem 3.13. Let $f_n$ be $C^{\zeta,2}$, let the limiting $\bar f$ be autonomous and in $BC^2$, and suppose $|f_n-\bar f|_{-\kappa,\gamma}\to0$. The exponents satisfy $1/2<\alpha<H-\kappa$, $H-\kappa>1/2$, $H-\kappa+\gamma\alpha>1$, and $\alpha<\zeta\le1$. For Young solutions with the same starting point,

the target is

The milestone list follows the statements used around this target: the Hölder composition estimate of Lemma 2.1, the RKHS estimate of Lemma 3.3, the fractional Brownian integral estimate of Lemma 3.4, the stochastic sewing lemma of Lemma 3.5, the Young case of (3.18) from Lemmas 3.10 and 3.12, the Kolmogorov inclusions (3.24), and the deterministic stability estimate of Lemma 2.2. Each is a separate formal theorem. The authors' proofs follow their statements in Sections 2 and 3 and the Appendix; Lemma 3.5 is quoted from Lê, Theorem 2.1 without proof in the article.

What the result provides

The target gives convergence of entire solution paths in a Hölder topology, in probability. In the paper, this lets a model-specific estimate of the negative Hölder distance be used to conclude convergence of the corresponding dynamical system. Theorem A is obtained by adding such an estimate for a stationary mixing fast process; the deterministic statement here isolates the part independent of that model. These uses are described in Sections 1 and 3.

The published paper proves the result. This mission asks for machine-checked proofs of the stated Lean theorems. Its reusable work would include a pathwise Young integral over arbitrary partitions, Hölder norms that retain the value $+\infty$, a two-sided vector fractional Brownian motion interface, and stochastic estimates for time-dependent integrands. The goal and milestones in this proposal are statements with proof placeholders; the local build checks their types, not their proofs.

Main obstruction

Pointwise control of $f_n-\bar f$ is unavailable: a rapidly oscillating function can be large at most times and still have small time antiderivatives. Applying a pathwise Young stability estimate directly to $f_n-\bar f$ therefore leaves a coefficient norm that need not tend to zero. The integral estimate must connect cancellation measured by $|\cdot|_{-\kappa,\gamma}$ with $L^p$ bounds on the driven equation. The dependence on the past of the fractional Brownian motion makes this step more delicate than an estimate for a deterministic integrand. The required estimates and their domains appear in Lemmas 3.4–3.12.

Formalization scope

Time is $\mathbb R$ for the two-sided driver; coefficient and solution assertions use $[0,T]$ with $T>0$. State spaces are finite-dimensional real Euclidean spaces. The goal takes $H\in(1/2,1)$ from the standing setting of Section 3.1, and it assumes the locally Hölder version of $B$ described on p. 1826. The solutions are required almost surely to satisfy the Young equation from the same $x_0$. This requirement fixes the processes to the equations; the convergence claim cannot be obtained by choosing arbitrary paths. Probability of the norm event uses the measure of that set, and the conclusion is convergence in probability in the full $C^\alpha$ norm.

The Lean definitions use $[0,\infty]$ for path and process seminorms, so unbounded suprema are not replaced by a default real value. The negative Hölder hypothesis uses real bounds $K_n\to0$ instead of an infimum that could be meaningless on an empty class. The Young integral quantifies over every monotone partition and the mesh limit of its left-point sums. The fBm definition includes Gaussianity, means, and every cross-coordinate covariance; its path version is explicit. Interval integrals in the coefficient bound are applied to time-continuous coefficients in the goal. Lemmas 3.4 and 3.10 use the increment filtration, the case needed for this theorem.

The paper's Lemma 2.2 needs a common initial value for its homogeneous-seminorm estimate; the formal statement includes it and records the printed issue. The paper writes the limiting coefficient with a time argument but uses an autonomous coefficient in (3.23), which the goal adopts. This proposal covers the $dB$ equation. The final $dt$ extension in Theorem 3.13 and the conditional-expectation estimate (3.19) remain outside its current items. Contributions that close these gaps, or supply a general conditional Wiener integral matching the article's notation, would extend the development.

Selected references

• M. Hairer and X.-M. Li, Averaging dynamics driven by fractional Brownian motion, Annals of Probability 48(4), 2020, 1826–1860. DOI.
• K. Lê, A stochastic sewing lemma and applications, 2018, arXiv:1810.10500, cited as [23] in Hairer and Li. arXiv.

Motivation

Principal component analysis (PCA) asks for the $j$-dimensional affine subspace that best fits a cloud of $n$ points in $\mathbb R^d$ in the least-squares sense. When $n$ is very large, or the points arrive as a stream or are spread over many machines, one wants to replace the data by a small summary on which the cost of every candidate subspace can still be evaluated, up to a factor $1+\varepsilon$. Such a summary is a coreset. Coresets for the $j$-subspace problem are the building block of the streaming and distributed PCA and projective clustering algorithms of Feldman, Schmidt and Sohler (SIAM J. Comput. 49(3), 2020), whose sizes depend on $j$ and $\varepsilon$ only, not on $n$ or $d$.

For linear subspaces (through the origin) the paper's Theorem 17 gives a deterministic coreset of $m=O(j/\varepsilon)$ points read off the singular value decomposition. Data are rarely centred, though, and subtracting the mean before the computation does not survive the union of coresets with different means (p. 616). Section 4 of the paper repairs this: Theorem 19 gives a coreset for affine $j$-subspaces whose points already carry the mean, at the price of doubling the size and weighting the points. This mission formalizes Theorem 19.

Setting

A data set of $n$ points in $\mathbb R^d$ is a matrix $A\in\mathbb R^{n\times d}$ whose rows $A_{i*}$ are the points. For a nonempty set $C\subseteq\mathbb R^d$ and a point $p$, $\operatorname{dist}(p,C)=\inf_{c\in C}\|p-c\|_2$. The cost of $C$ is

and for weights $w_1,\ldots,w_r\ge0$ on the rows of $S\in\mathbb R^{r\times d}$ the weighted cost is $\sum_i w_i\operatorname{dist}^2(S_{i*},C)$. The squared Frobenius norm is $\|M\|_F^2=\sum_{i,k}M_{ik}^2$.

A singular value decomposition (SVD) of $A$ is a factorization $A=U\Sigma V^T$ with $U\in\mathbb R^{n\times n}$ and $V\in\mathbb R^{d\times d}$ orthogonal and $\Sigma\in\mathbb R^{n\times d}$ rectangular diagonal with nonnegative, nonincreasing diagonal entries $\sigma_1\ge\sigma_2\ge\cdots$. $\Sigma^{(m)}$ keeps the first $m$ diagonal entries and sets the rest to $0$; the $m$-rank approximation is $A^{(m)}=U\Sigma^{(m)}V^T$ (Definition 1).

The mean row is $\mu(A)=\frac1n\sum_iA_{i*}$ and the centred matrix is $A'=A-\mathbb 1\cdot\mu(A)$, whose rows are $A_{i*}-\mu(A)$.

Algorithm 1, subspace-Coreset$(A,j,\varepsilon)$, sets $m=\min\{n,d,j+\lceil j/\varepsilon\rceil-1\}$, returns the matrix $S$ of the first $m$ rows of $\Sigma^{(m)}V^T$ (all other rows are zero), the weights $w_i=1$, and $\Delta=\|A-A^{(m)}\|_F^2$.

Algorithm 2, affine-$j$-subspace-Coreset$(A,j,\varepsilon)$, runs Algorithm 1 on $A'$, obtaining $(S',\Delta)$ with $m=|S'|$, and returns

together with $\Delta$.

Formalization targets

Goal: Theorem 19 (p. 617)

Let $n\ge1$, $j\in[1,d-1]$ and $\varepsilon>0$, and let $(S,\Delta,w)$ be the output of Algorithm 2 for any SVD of $A'$. Then $S\in\mathbb R^{(2m)\times d}$, $m\le j+\lceil j/\varepsilon\rceil-1$, $\Delta\ge0$, and for every affine $j$-dimensional subspace $C$ of $\mathbb R^d$,

Milestones

1. Theorem 17 (p. 615): for any SVD of $A$, the output of Algorithm 1 satisfies $\operatorname{dist}^2(A,L)\le\sum_{i=1}^m\operatorname{dist}^2(S_{i*},L)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A,L)$ for every $j$-dimensional linear subspace $L$.
2. Lemma 18 (p. 616): if $\mu(M)=\vec0$, $L$ is a linear $j$-subspace and $t\in L^\perp$, then $\operatorname{dist}^2(M,t+L)=\operatorname{dist}^2(M,L)+n\|t\|^2$.
3. Display (7) (p. 618): with $S''=\sqrt{m/n}\,[S';-S']$, $\operatorname{dist}^2(A',L)\le\frac n{2m}\operatorname{dist}^2(S'',L)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A',L)$ for every linear $j$-subspace $L$.

Theorem 17 rests on Corollary 16 and Claim 3 of the paper; those are milestones of the companion mission Turning Big Data into Tiny Data … I and are not posed again here.

Significance

The result. Theorem 19 gives a deterministic summary of $2m\le2(j+\lceil j/\varepsilon\rceil-1)$ weighted points and one scalar that preserves the cost of every affine $j$-subspace within $1+\varepsilon$, for arbitrary data, with no assumption on the mean. Because its points carry the mean, coresets of different data sets can be merged, which the merge-and-reduce streaming constructions of the paper's later sections need. Any $(1+\varepsilon')$-approximate PCA solution computed on the coreset is then a $(1+\varepsilon)(1+\varepsilon')$-approximate solution for the full data.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any coreset theorem, exists on the platform. A complete development would produce the cost identities for sums of squared distances to linear and affine subspaces in Lean, the effect of centring and orthogonal translation on these costs, and the use of the SVD truncation as a summary, all of which are reusable for other PCA, low-rank approximation and projective clustering results.

Difficulty

The obvious construction, centring the data, computing the linear coreset of the centred data and adding the mean back, fails: the linear coreset $S'$ need not have mean $\vec0$, and translating a subspace by $t\perp L$ changes the cost of a point set by a multiple of $\|t\|^2$ that depends on the number of points (p. 617). The paper's construction has to match both the mean and the total weight of the original data while keeping the linear-subspace guarantee, and the formal proof has to carry this through the reduction of an arbitrary affine subspace to a linear one plus an orthogonal translation. Beneath it lies Theorem 17, which needs the SVD-based estimate of the companion mission (Corollary 16) and the passage from the $n$-row matrix $A^{(m)}=U\Sigma^{(m)}V^T$ to the $m$ nonzero rows of $\Sigma^{(m)}V^T$. Distances to subspaces in Lean are infima over sets, so the identities $\operatorname{dist}^2(A,L)=\|AY\|_F^2$ for an orthonormal basis $Y$ of $L^\perp$ must themselves be established.

Formalization scope

• Representation. Points are rows of Matrix (Fin n) (Fin d) ℝ, read as points of EuclideanSpace ℝ (Fin d). $\operatorname{dist}$ is Metric.infDist. Linear $j$-subspaces are Submodules of finrank $j$; affine ones are AffineSubspaces whose direction has finrank $j$, and $t+L$ is AffineSubspace.mk' t L. The SVD and $A^{(m)}$ are the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every statement holds for an arbitrary SVD; none is chosen.
• Pinned hypotheses and readings.
  1. The page's "$\Delta>0$" (Theorems 17 and 19) is false when $\operatorname{rank}A'\le m$, for instance when all points coincide; the statements claim $\Delta\ge0$.
  2. $n\ge1$ is added to Theorem 19 and (7), since Algorithm 2 divides by $n$.
  3. "subspace-Coreset$(P,j,\varepsilon)$" is read with $P=A$.
  4. Theorem 17's $S\in\mathbb R^{m\times d}$ is the first $m$ rows of $\Sigma^{(m)}V^T$, as the text before it says, although Algorithm 1, line 3 writes the whole matrix.
  5. Lemma 18's "affine $j$-dimensional subspace $L$" is a linear subspace: the lemma uses $L^\perp$, and the proof of Theorem 19 applies it to linear $L$.
  6. Theorem 19's affine subspace $C$ is also required to be nonempty; this follows from $j\ge1$ and guards against Mathlib's convention that the distance to $\emptyset$ is $0$.
• Conventions. $m\le j+\lceil j/\varepsilon\rceil-1$ is written $m+1\le j+\lceil j/\varepsilon\rceil$. Diagonal positions of $\Sigma$ are 0-based in Lean. The $2m$ output rows are $\mu+\sqrt{m/n}\,S'_{i*}$ followed by $\mu-\sqrt{m/n}\,S'_{i*}$. Weights are the real number $n/(2m)$ with $m=|S'|$, not the cap $j+\lceil j/\varepsilon\rceil-1$.
• Not trivializable. The goal quantifies over affine, not linear, subspaces; the coreset is built from an SVD of the centred matrix $A'$ and $\Delta$ is the residual of $A'$, so neither the mean nor the centring can be dropped; and no hypothesis is vacuous (any data matrix with any of its SVDs satisfies them).
• Not formalized. The running-time clauses ("$O(\min\{nd^2,dn^2\})$ time") and §4.1 (weighted inputs).
• Welcome contributions. Lemmas computing $\operatorname{dist}^2$ to subspaces via orthogonal projections, invariance of these costs under orthogonal maps, and the cost identity for symmetric point sets.

Selected references

• D. Feldman, M. Schmidt, C. Sohler, Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering, SIAM J. Comput. 49(3):601–657, 2020. https://doi.org/10.1137/18M1209854
• P.-A. Absil, J. Malick, Projection-like Retractions on Matrix Manifolds, SIAM J. Optim. 22(1):135–158, 2012 (source of the published SVD definition used here). https://doi.org/10.1137/100802529

Motivation

An online decision maker often sees information about a customer, patient, or request before choosing an action. A bandit with covariates models this setting when the reward of every available action is initially unknown and only the reward of the chosen action is observed. A method must learn which action works best for which covariates while paying for exploratory choices. Perchet and Rigollet studied this problem for smooth reward functions and measured how quickly a policy can approach the performance of an oracle that knows every arm's mean reward Perchet and Rigollet, 2013.

A fixed grid divides the covariate space at one resolution everywhere. It can spend pulls distinguishing arms in regions where their difference is already large, while leaving too few observations in regions where they are close. Adaptively binned successive elimination (ABSE) instead refines a region only while several arms remain plausible there. The paper proves a regret rate controlled jointly by the smoothness of the reward functions and the probability of encountering near ties. Its Theorem 5.1 is the target of this mission.

Setting

There are $K\ge2$ arms and covariates $X_t$ in the unit cube $\mathcal X=[0,1]^d\subset\mathbb R^d$, with $d\ge1$. At time $t$, the policy sees $X_t$, chooses an arm, and sees that arm's reward. The random vectors consisting of the covariate and all potential arm rewards are independent across times. Covariates have a common probability law $P_X$ with a density between constants $0<\underline c\le\overline c$. Every reward lies in $[0,1]$; for arm $i$ its conditional mean given $X_t=x$ is $f^{(i)}(x)\in[0,1]$. The paper does not require the complete reward vectors to be identically distributed across time. These conventions come from §3.1, pp. 10–11.

At $x$, write $f^*(x)=\max_i f^{(i)}(x)$. Write $f^\sharp(x)$ for the largest mean strictly below $f^*(x)$, and set $f^\sharp(x)=f^*(x)$ when every arm ties. The difference $f^*(x)-f^\sharp(x)$ is the positive gap wherever a genuinely suboptimal arm exists. The smoothness condition requires $|f^{(i)}(x)-f^{(i)}(x')|\le L\|x-x'\|^\beta$ for every arm, with the Euclidean norm, $0<\beta\le1$, and $L>0$. The margin condition, with $\alpha>0$, $0<\delta_0<1$, and $C_0>0$, says

These are the assumptions defining the paper's class $\mathcal M^K_{\mathcal X}(\alpha,\beta,L)$ §3.2, pp. 12–13.

ABSE starts with the whole cube. Each live dyadic cell runs a copy of successive elimination on its inherited arms. One round pulls each remaining arm once. After a complete round, an arm is eliminated if its empirical mean falls more than twice the radius $U(s,n|B|^d)$ below the largest empirical mean, where $|B|$ is the cell's side length and $U$ uses $\overline{\log}(x)=\max\{\log x,1\}$. The cell splits after its specified stopping round if it has at least two active arms and is below the maximum depth $k_0$. Each child receives the survivors. The policy takes $d,\beta,L,K,n$ as parameters and uses the current covariate and rewards it actually observed Policy 3, p. 22.

Formalization targets

Goal: Theorem 5.1, finite margin exponent

The goal is the finite-$\alpha$ part of Theorem 5.1, p. 22. Fix $d\ge1$, $0<\beta\le1$, $L>0$, $\alpha>0$ with $\alpha\beta\le d$, $0<\delta_0<1$, $C_0>0$ and $0<\underline c\le\overline c$. There is one constant $C>0$, depending on these parameters but not on $K$, $n$ or the machine, such that for every $K\ge2$, every $n\ge K\log K$ and every machine of the class,

Here $\widetilde\pi$ is ABSE and $R_n$ is its cumulative regret against an arm of maximum conditional mean at each covariate. The goal asserts the shape of the rate with an unspecified constant, which is the paper's form.

Milestones

In attack order:

1. Lemma A.1 (p. 28): a maximal Hoeffding–Azuma inequality, $\mathbb P\{\exists t\le T:\bar Z_t\ge\sqrt{2(b-a)^2t^{-1}\log(4T/(\delta t))}\}\le\delta$ for bounded martingale differences.
2. (5.3) (p. 21): $\ell_B\le C_\ell|B|^{-2\beta}\,\overline{\log}(n|B|^{2\beta+d})$, the number of rounds a cell spends before it may split.
3. (5.10) (p. 26): if arm $i$ has gap above $8c_0|B|^\beta$ at a point of $B$, then the cell mean of the arm $\check\imath$ that is best at that point exceeds the cell mean of $i$ by at least $\tfrac32\varepsilon_{B,\ell_B}$.
4. The display before (5.6) (p. 25): $\sum_{|B|=2^{-k}}q_B\le c_2 2^{k(d-\beta\alpha)}$, where $q_B$ is the conditional probability of a near tie inside $B$.
5. (5.5) (p. 24): the pathwise decomposition $r_n^{\mathrm{born}}(B)=r_n^{\mathrm{live}}(B)+\sum_{B'\in\mathrm{burst}(B)}r_n^{\mathrm{born}}(B')$ of regret along the tree.
6. Theorem 5.1, $\alpha=\infty$ (p. 22): when the margin region $\{0<f^\star-f^\sharp\le\delta_0\}$ has probability zero, $\mathbb E R_n(\widetilde\pi)\le CK\log n$.

Significance

The result provides a performance guarantee for a policy that adapts its spatial resolution to observed evidence, under a class of nonparametric reward functions. It permits a direct comparison with a fixed-bin policy under the same smoothness and margin conditions. The paper proves the rate and discusses optimality in a minimax sense when $K=2$ §5, pp. 22–27. This mission asks for a machine-checked proof of the stated finite-$\alpha$ regime; the Lean goal and milestones are currently open statements, so the paper's proof is the mathematical source rather than a completed formal proof.

A completed development would make the stochastic model, adaptive policy, cell geometry, and concentration estimates reusable for other contextual bandit analyses.

Difficulty

The main difficulty is the feedback loop between decisions and observations. A cell receives samples only when the covariate lands there, and its available arms depend on eliminations in its ancestors. Applying an ordinary concentration inequality to a fixed sequence of arm rewards does not by itself justify the bound at these random birth and stopping times. The formal proof must track the inherited active sets and the samples collected after each birth, then combine local error bounds across the tree. The appendix's maximal inequality controls a range of round counts; the regret argument also uses the small probability of covariates with nearly tied arm means §5, pp. 23–27 and Lemma A.1, p. 28.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) and a probability measure on its unit cube. The lower density bound ensures every valid dyadic cell has positive probability, so its conditional mean is defined by a real quotient. A consistent half-open boundary assignment turns the paper's cells, which are specified up to Lebesgue-null boundaries, into a partition on every path. The policy is a recursive state machine: at time $t$ it receives $X_t$, chooses an arm from its prior state, and updates with only the reward of that arm. It does not receive the unknown means or any unobserved potential reward. The existential constant in the goal is quantified before $K$, $n$, the sample space, and the machine.

The finite-$\alpha$ goal includes $\alpha\beta\le d$. The printed theorem omits it, although the proof uses it. Without it, a two-arm machine with constant means $1$ and $0$ has regret from the policy's first exploratory round, while the printed bound tends to zero when $\alpha$ is large. The $\alpha=\infty$ clause reads the margin condition as $P_X(0<f^\star-f^\sharp\le\delta_0)=0$, the limit of $C_0\delta^\alpha$ for $\delta<1$, because the page does not define it. The (5.3) milestone uses $\overline{\log}$: the printed ordinary logarithm can be nonpositive at a finest cell, while the left side is a positive integer. The cell parameter $T_B=n|B|^d$ and bursting after a full round follow Policy 3 and the proof where nearby prose or pseudocode differs. Lemma A.1 adds $\mathbb EZ_1=0$ and $a<b$, both implicit on the page. The constants $c_2$ and $C_\ell$ are existential and placed after the class parameters, because the page's explicit $c_2=c_1^\alpha/\underline c$ omits the margin constant $C_0$.

The probabilistic error displays (5.6)–(5.9) and (5.11)–(5.14) are not milestones. They are statements about the events $\mathcal A_B=\{\underline{\mathcal I}_B\subseteq\mathcal I_B\subseteq\bar{\mathcal I}_B\}$ and $\mathcal G_B$, which the page leaves undefined for cells that are never born or never finish $\ell_B$ rounds. The decomposition (5.8) also leaves out arms of $\underline{\mathcal I}_B$ that were eliminated at an ancestor of $B$. A faithful encoding of these events is welcome as a contribution.

A complete proof needs measurable recursive policies, conditional expectations and independence, dyadic-cell volume and nesting facts, concentration for arm observations at adaptive times, and sums over tree depths. Contributions establishing these interfaces and the paper's intermediate bounds are welcome. The result must apply to every machine in the stated class. Each of the following would change the theorem: a policy that reads the unknown $f^{(i)}$ or unobserved rewards (the oracle has zero regret), a constant chosen after the machine, a covariate law that is not a probability measure on the cube, Hölder continuity in the sup norm instead of the Euclidean norm, or dropping the density lower bound (cells of zero mass would make $\bar f_B$ a junk value). The paper's proofs are in §5 (pp. 23–27) and its Appendix (p. 28).

Selected references

• Jean-Yves Audibert and Alexandre B. Tsybakov, Fast learning rates for plug-in classifiers, Annals of Statistics 35(2):608–633, 2007, DOI:10.1214/009053606000001217.
• Eyal Even-Dar, Shie Mannor and Yishay Mansour, Action elimination and stopping conditions for the multi-armed bandit and reinforcement learning problems, Journal of Machine Learning Research 7:1079–1105, 2006, jmlr.org/papers/v7/evendar06a.
• Philippe Rigollet and Assaf Zeevi, Nonparametric bandits with covariates, COLT 2010, pp. 54–66, arXiv:1003.1630.
• Vianney Perchet and Philippe Rigollet, The multi-armed bandit problem with covariates, Annals of Statistics 41(2):693–721, 2013, pinned arXiv:1110.6084v3, DOI:10.1214/13-AOS1101.

Motivation

First-order hyperbolic systems of balance laws $z_t+\Lambda(z,x)z_x+f(z,x)=0$ model open-channel flow (the Saint-Venant equations), gas pipelines, traffic and heat exchangers. In most of these applications the state can be acted on only at one end of the domain, so stabilizing an equilibrium is a boundary control problem. For $2\times2$ systems without source term ($f=0$), static boundary feedback built from a Lyapunov function works (Coron–Bastin–d'Andréa-Novel 2008); with a source term, Lyapunov functions of the diagonal form $\int_0^1z^{\mathsf T}Q(x)z\,dx$ can fail (Bastin and Coron 2011, recalled in Remark 1 of the paper). Backstepping, introduced for parabolic equations by Krstic and Smyshlyaev, replaces the search for a Lyapunov function by an invertible integral change of variables that maps the linearized plant to a target system whose stability is evident.

Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013) design such a feedback for the linearization of a $2\times2$ quasilinear system and prove that it stabilizes the nonlinear system locally in $H^2$. This mission formalizes that main result, Theorem 4.1.

Setting

The state is $z(x,t)=(z_1,z_2)\in\mathbb R^2$ on $x\in[0,1]$, $t\ge0$, governed by

The standing assumptions (§2) are: $\Lambda$, $f$, $G_0$ are $C^2$; $\Lambda(0,x)=\operatorname{diag}(\Lambda_1(x),\Lambda_2(x))$ with $\Lambda_1>0>\Lambda_2$ on $[0,1]$; $f(0,x)=0$; $G_0(0)=0$. Write $f_{ij}=\partial f_i/\partial z_j(0,x)$ and $q=G_0'(0)$; the paper treats $q\ne0$.

The scaling $w=\Phi z=(\varphi_1z_1,\varphi_2z_2)$, $\varphi_1=\exp\int_0^xf_{11}/\Lambda_1$, $\varphi_2=\exp\int_0^xf_{22}/\Lambda_2$, removes the diagonal of the linearization, which becomes $w_t=\Sigma w_x+Cw$ with $\Sigma=\operatorname{diag}(-\epsilon_1,\epsilon_2)$, $\epsilon_1=\Lambda_1$, $\epsilon_2=-\Lambda_2$, and $C$ antidiagonal with entries $c_1=-f_{12}\varphi_1/\varphi_2$, $c_2=-f_{21}\varphi_2/\varphi_1$. The kernels $K^{vu},K^{vv}$ solve a pair of first-order hyperbolic equations on the triangle $\mathcal T=\{0\le\xi\le x\le1\}$ with boundary data on its diagonal and on the edge $\xi=0$ ((3.32), (3.33), (3.36), (3.37)). The gain is $k(x)=(\varphi_1(x)K^{vu}(1,x),\varphi_2(x)K^{vv}(1,x))/\varphi_2(1)$.

The closed loop adds a dynamic extension:

with $d_1,d_2>0$, $d_1\ne d_2$, and $a(0)$, $b(0)$ determined by the initial profile $z_0$ through two linear functionals $P_1(z_0)$, $P_2(z_0)$. The norm is $\|z\|_{H^2}=\|z\|_{L^2}+\|z_x\|_{L^2}+\|z_{xx}\|_{L^2}$ on $[0,1]$.

Formalization targets

Goal: Theorem 4.1

For every $0<\lambda<2\min(d_1,d_2)$ there are $\delta,c>0$ such that every classical solution with $\|z_0\|_{H^2}\le\delta$ satisfying the compatibility conditions (4.16), (4.18) obeys

Milestones, in the order the proof uses them

Write $\gamma=(\alpha,\beta)=\mathcal K[\Phi z]=\Phi z-\int_0^xK(x,\xi)\Phi z(\xi)d\xi$ for the full $2\times2$ kernel $K$, $\eta=\gamma_t$, $\theta=\gamma_{tt}$, and $\|\gamma\|_\infty=\sup_x(|\alpha|+|\beta|)$.

1. $H^2$ equivalence (p. 12): $\|\gamma\|_{H^2}$ and $\|z\|_{H^2}$ are equivalent.
2. Proposition 5.1: for $V_1=\int_0^1\gamma^{\mathsf T}D\gamma$ and small $\|\gamma\|_\infty$, $\dot V_1\le-\lambda_1V_1-\lambda_2(\alpha^2(1,t)+\beta^2(0,t))+C_1V_1^{3/2}+C_2\|\gamma_x\|_\infty V_1+C_3(a^2+b^2)$.
3. Lemma B.6: the sup and $L^2$ norms of $\eta$ and $\gamma_x$ are comparable.
4. Proposition 5.3: for $V_2=\int_0^1\eta^{\mathsf T}R[\gamma]\eta$, $\dot V_2\le-\lambda_3V_2-\lambda_4(\eta_1^2(1,t)+\eta_2^2(0,t))+K_1V_2\|\eta\|_\infty+K_2(a^2+b^2)$.
5. Proposition 5.4: for $V_3=\int_0^1\theta^{\mathsf T}R[\gamma]\theta$ and small $\|\gamma\|_\infty+\|\eta\|_\infty$, $\dot V_3\le-\lambda_5V_3-\lambda_6(\theta_1^2(1,t)+\theta_2^2(0,t))+K_1V_3V_2^{1/2}+K_2V_2V_3^{1/2}+K_3V_3^{3/2}+K_4\|\eta\|_\infty\eta_2^2(0,t)+K_5(a^2+b^2)$.
6. Proposition B.5: the norms of $\theta$ and $\gamma_{xx}$ are comparable.

Significance

Theorem 4.1 shows that a feedback computed entirely from the linearization, by solving linear kernel equations, is a valid local stabilizer of the quasilinear system in $H^2$, the natural space for classical $C^1$ solutions of quasilinear hyperbolic systems. The dynamic extension $(a,b)$ is what makes the result usable: without it, the static feedback imposes artificial compatibility conditions (4.17), (4.19) on the initial data.

The result is proved in the paper (§5 and Appendix B); none of it is machine-checked. A formal proof needs a rigorous treatment of the Volterra transformation and its inverse in $H^2$, the three-level Lyapunov argument ($V_1$, $V_2$, $V_3$), and the comparison of these functionals with the $H^2$ norm. The formalization also records corrections to the printed formulas: the sign of $\varphi_2$ in (4.1), the entries of $C$ in (4.7), the initial values (4.26), and the admissible decay rates (see below).

Difficulty

The obvious argument — the linear closed loop is exponentially stable, so the nonlinear one is locally stable — fails for hyperbolic systems: the nonlinear terms $\Lambda_{NL}(w,x)w_x$ contain a derivative of the state, so they are not small in $L^2$ relative to $\|w\|_{L^2}$, and an $L^2$ estimate does not close. One must control $\gamma$, $\gamma_t$ and $\gamma_{tt}$ simultaneously, each with its own Lyapunov functional whose weight $R[\gamma]$ depends on the state, and exchange time derivatives for space derivatives through the equation, which is possible only while $\|\gamma\|_\infty$ and $\|\gamma_t\|_\infty$ stay small.

Formalization scope

States are Fin 2 → ℝ, matrices Matrix (Fin 2) (Fin 2) ℝ, indices 0-based. A solution is one $C^2$ function $z:\mathbb R\times\mathbb R\to\mathbb R^2$ (space first) with the PDE imposed on $[0,1]\times[0,\infty)$ and the boundary conditions for $t\ge0$; this is the theorem restricted to classical solutions, since Mathlib has no Sobolev spaces. Global existence is not asserted. Coefficient functions are defined on all of $\mathbb R$ with global $C^2$ regularity and sign conditions on $[0,1]$. $H^1$, $H^2$ norms are sums of $L^2$ norms, as on p. 11; $\|\cdot\|_\infty$ uses $|\alpha|+|\beta|$.

Added or corrected relative to the page, all disclosed in the items:

• $q\neq0$ (the case the paper proves; $q=0$ is a remark);
• $\varphi_2=\exp(+\int f_{22}/\Lambda_2)$, $c_1=-f_{12}\varphi_1/\varphi_2$, $c_2=-f_{21}\varphi_2/\varphi_1$, $a(0)=(P_2-d_2P_1)/(d_1-d_2)$, $b(0)=(d_1P_1-P_2)/(d_1-d_2)$;
• $0<\lambda<2\min(d_1,d_2)$ instead of "every $\lambda>0$", which fails for fixed $d_1,d_2$ because $a(t)=a(0)e^{-d_1t}$;
• milestones take a full $C^2$ kernel (the page's claim via Theorem A.2, guaranteed for $C^3$ data); the goal takes only $C^1$ kernels $K^{vu},K^{vv}$;
• Proposition 5.3's last term is $K_2(a^2+b^2)$ (printed $K_2b^2$).
• Proposition 5.4 is stated for closed-loop solutions of class $C^3$, since $\dot V_3$ involves $\gamma_{ttt}$.

Trivializing formalizations are ruled out: $\delta$, $c$ and every milestone constant are quantified after the data and before the solution; the kernels are pinned down by all their equations and boundary conditions (unique by Theorem A.1 of the paper); the corrected $a(0)$, $b(0)$ are the ones every classical solution has, so no small initial profile is excluded; and the $H^2$ norm contains $\|z_{xx}\|_{L^2}$.

Not formalized: Lemma 5.2 (its printed bound (5.38), $\|\gamma\|_\infty(1+\|\gamma_x\|_\infty)$, fails for profiles with small $\|\gamma\|_\infty$ and large $\|\gamma_x\|_\infty$, and (5.37) compares a matrix with a scalar), and Lemmas B.1–B.4, B.7, B.8. Contributions of a reusable theory of Volterra integral transformations on $[0,1]$ with $C^2$ kernels, and of the comparison between sup and $L^2$ norms of solutions of hyperbolic systems, are welcome.

Selected references

• J.-M. Coron, R. Vazquez, M. Krstic, G. Bastin, Local Exponential H² Stabilization of a 2 × 2 Quasilinear Hyperbolic System Using Backstepping, arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013. https://arxiv.org/abs/1208.6475v1
• G. Bastin, J.-M. Coron, On boundary feedback stabilization of non-uniform linear 2 × 2 hyperbolic systems over a bounded interval, Systems and Control Letters 60, 2011, pp. 900–906 (reference [1] of arXiv:1208.6475v1). https://arxiv.org/abs/1208.6475v1
• M. Krstic, A. Smyshlyaev, Boundary Control of PDEs: A Course on Backstepping Designs, SIAM, 2008. https://doi.org/10.1137/1.9780898718607
• J.-M. Coron, G. Bastin, B. d'Andréa-Novel, Dissipative boundary conditions for one-dimensional nonlinear hyperbolic systems, SIAM J. Control Optim. 47(3), 2008. https://doi.org/10.1137/060650222

Motivation

The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.

The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters $q_N$ and $f_N$ separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.

Setting

For each size $N$, let $H_N=(h_{ij})$ be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance $1/N$. Their higher moments obey

The sparsity parameter $q_N$ lies between $(\log N)^{3\xi_N}$ and $C\sqrt N$, and the logarithmic parameter satisfies $1+a_0\le\xi_N\le A_0\log\log N$, with $a_0>0$ and $A_0\ge10$. Define $e_N=N^{-1/2}(1,\ldots,1)$ and the noncentered matrix $A_N=H_N+f_N|e_N\rangle\langle e_N|$, where $0\le f_N\le N^C$. The projection $|e_N\rangle\langle e_N|$ has every entry equal to $1/N$. These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.

For a complex number $z=E+i\eta$ with $\eta>0$, the resolvents are $G(z)=(H_N-zI)^{-1}$ and $\widetilde G(z)=(A_N-zI)^{-1}$. Their normalized traces are $m(z)=N^{-1}\operatorname{Tr}G(z)$ and $\widetilde m(z)=N^{-1}\operatorname{Tr}\widetilde G(z)$. The comparison object is the semicircle density $\rho_{\mathrm{sc}}(x)=(2\pi)^{-1}\sqrt{[4-x^2]_+}$ and its Stieltjes transform $m_{\mathrm{sc}}(z)=\int_{\mathbb R}\rho_{\mathrm{sc}}(x)/(x-z)\,dx$. Put $\kappa_E=\bigl||E|-2\bigr|$ and $D=\{E+i\eta:|E|\le\Sigma,\ 0<\eta\le3\}$ for a fixed $\Sigma\ge3$. These definitions appear in Section 2, pp. 7–9.