All missions

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

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

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

Companion results

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Timeline:

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

Setting

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

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

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

Formalization targets

Goal: Theorem 1 (pp. 37–38)

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

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

A complete development needs the following:

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

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

Selected references

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

Motivation

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

Setting

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

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

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

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

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

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

Formalization targets

Steps of the proof

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

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

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

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

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

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

Goal: Theorem 4

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 1 (p. 3)

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Why expected regret needs a lower bound

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

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

Models, algorithms and the coefficient

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

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

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

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

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

Formalization targets

Localized DEC lower bound

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

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

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

Supporting targets

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

What the result supplies

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

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

Where the difficulty lies

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

Formalization scope

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

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

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

Selected references

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

Motivation

Hypergraph Turán problems ask how many edges a $k$-uniform hypergraph on $n$ vertices can have without containing a fixed sub-hypergraph. For graphs ($k=2$) the theory is well developed; for $k\ge 3$ exact answers are rare and are known mostly for small, dense configurations such as the Fano plane or expanded triangles. Paths are the natural sparse test case. For graphs, Erdős and Gallai (1959) showed that a graph on $n$ vertices without a path of length $\ell$ has at most $\frac12(\ell-1)n$ edges. For hypergraphs there are several notions of path: Berge paths (Győri, Katona and Lemons, 2010), loose paths (Mubayi and Verstraëte, 2007, asymptotic bounds) and the most restrictive notion, linear paths. The case of two edges was solved by Frankl (1977), and the case $\ell<k$ asymptotically by Frankl and Füredi (1987).

Füredi, Jiang and Seiver (arXiv:1108.1247v1, published in Combinatorica 34 (2014), doi:10.1007/s00493-014-2838-4) determined the Turán number of every $k$-uniform linear path exactly, for $k\ge4$ and $n$ large, together with the unique extremal families. It is one of the few exact hypergraph Turán results for an infinite family of forbidden hypergraphs.

Setting

The vertex set is $[n]=\{1,\dots,n\}$. A family $\mathcal F$ is a set of subsets of $[n]$; it is $k$-uniform if $\mathcal F\subseteq\binom{[n]}{k}$, the set of all $k$-element subsets.

A linear path of length $\ell$ is a sequence of distinct sets $F_1,\dots,F_\ell$ such that

$$|F_i\cap F_{i+1}|=1\ \text{ for each } i,\qquad F_i\cap F_j=\emptyset\ \text{ whenever } |i-j|>1.$$

The $k$-uniform linear path of length $\ell$ is written $\mathbb P^{(k)}_\ell$; a family contains it if some $\ell$ of its members form a linear path. The Turán number $\mathbf{ex}_k(n,\mathbb P^{(k)}_\ell)$ is the maximum size of a $k$-uniform family on $[n]$ that does not contain $\mathbb P^{(k)}_\ell$.

Two counting functions describe the answer:

$$f(n,k,t)=\sum_{i=1}^{t}\binom{n-i}{k-1},\qquad g(n,k,t)=f(n,k,t)+\binom{n-t-2}{k-2}.$$

For a set $S\subseteq[n]$ of $t$ elements, $f(n,k,t)$ is the number of $k$-sets meeting $S$ (the star family of $S$), and $g(n,k,t)$ adds the $k$-sets of $[n]\setminus S$ that contain two fixed vertices $u,v$ (the even family).

The proof is phrased in the language of the delta-system method: $s$-stars (sets pairwise meeting in a common kernel), the kernel degree $\deg^*_{\mathcal F}(W)$ (the largest $s$ for which an $s$-star with kernel $W$ exists), $(k,s)$-homogeneous families (k-partite families whose intersections follow a single intersection-closed pattern $\mathcal J$ of subsets of $[k]$, each intersection being the kernel of an $s$-star), the rank of $\mathcal J$, the kernel graph of $\mathcal F$, and the $k$-blowup $H^{(k)}$ of a graph $H$.

Formalization targets

Goal: Theorem 2.4

For every $k\ge 4$ and $t\ge1$ there is $n_0$ such that for all $n\ge n_0$:

$$\mathbf{ex}_k(n,\mathbb P^{(k)}_{2t+1})=f(n,k,t),\qquad \mathbf{ex}_k(n,\mathbb P^{(k)}_{2t+2})=g(n,k,t),$$

and in each case a $k$-uniform, path-free family of that size is exactly the star family of some $t$-set $S$ (odd case), respectively the even family of some $t$-set $S$ and two distinct vertices $u,v\notin S$ (even case).

Milestones

In the order the proof uses them:

1. the star and even families are path-free and have $f$ and $g$ members (lower bound);
2. Lemma 3.1, Füredi's intersection semilattice lemma;
3. Lemma 3.3 and Proposition 3.4, the rank bound $|\mathcal F^*|\le\binom np$;
4. Lemma 3.6 and Corollary 3.7, the structure of patterns of rank $k$ and $k-1$;
5. Theorem 3.8, blowups of trees in homogeneous families of rank $k$ or type 2;
6. Theorem 3.9, the canonical partition of a path-free family;
7. Lemmas 4.2–4.4, from kernel graphs to blowups, the edge count $(k-1)|\mathcal F|\le e(H')\binom{n-2}{k-2}$, and the Erdős–Gallai circumference bound;
8. Theorem 4.5, $\mathbf{ex}_k(n,\mathbb P_{2t+2}^{(k)})\le t\binom{n-1}{k-1}+O(n^{k-2})$;
9. the bound (1), $\mathbf{ex}_k(n,\mathbb P^{(k)}_\ell)\le(k-1)(\ell-1)\binom{n-1}{k-1}$ for every $n$;
10. Erdős' matching theorem for large $n$ (Theorem 1.1) and the $r$-intersecting Erdős–Ko–Rado theorem;
11. Claims 2–3 of §5: a near-extremal family has a $t$-set joined in the kernel graph to all but $O(\sqrt n)$ vertices.

Significance

The theorem gives the exact extremal number and the unique extremal configuration for every linear path when $k\ge4$, and its proof yields a stability statement (Theorem 5.1 of the paper): a path-free family of nearly extremal size is close to a star family. The method is the standard template for exact results on sparse hypergraphs: delta-system decomposition, an asymptotic bound from a graph theorem applied to a kernel graph, then stability and cleaning.

The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: Mathlib has the intersecting Erdős–Ko–Rado theorem ($r=1$) but not the $r$-intersecting version with uniqueness for large $n$, not Erdős' matching theorem, not the Erdős–Gallai circumference theorem, and no delta-system machinery. A formalization would produce reusable libraries for each of these, and the first machine-checked exact hypergraph Turán number for an infinite family.

Difficulty

The obvious argument — bound the number of members through each vertex and sum — gives only $O(n^{k-1})$ with a wrong leading constant, because a path-free family can have $t$ vertices of almost full degree. Exactness needs three layers that do not reduce to one another. First, the intersection semilattice lemma (Lemma 3.1) is a deep structural theorem with a doubly exponential constant; it is cited, not proved, in the paper. Second, the asymptotic bound passes through the Erdős–Gallai circumference theorem, itself a nontrivial graph result. Third, the exact value requires a stability argument with several error terms ($O(n^{k-3/2})$, $O(\sqrt n)$) that must be balanced, followed by Erdős' matching theorem and the 2-intersecting Erdős–Ko–Rado theorem for large $n$, both with uniqueness. The structural lemmas of §§3–4 are elementary but involve greedy embeddings in which disjointness of the new vertices has to be maintained carefully.

Formalization scope

Vertices are Fin n; families are Finset (Finset (Fin n)); $k$-uniformity is 𝓕 ⊆ univ.powersetCard k. A linear path is an injective map Fin ℓ → Finset (Fin n) into the family with consecutive members meeting in exactly one vertex and non-consecutive members disjoint. The Turán number is a Finset.sup of cardinalities over all path-free $k$-uniform subfamilies, a finite attained maximum for $\ell\ge1$; at $\ell=0$ the feasible set is empty and Lean returns zero, which no theorem here uses. Partitions into $k$ parts are part maps Fin n → Fin k; stars are finsets of distinct petals; the rank is a minimum computed with sInf, exact because intersection patterns consist of proper subsets of $[k]$. "Sufficiently large $n$" and every $O(\cdot)$ are explicit existential constants chosen before $n$ and the family.

Hypotheses added relative to the page: Theorem 3.8 assumes the homogeneous family is nonempty (the empty family is homogeneous for every pattern, and the proof starts from a member). Lemma 4.2 states $k\ge2$, implicit in the paper's definition of a blowup using $k-2$ new vertices; it excludes a false zero-threshold case at $k=0$. Lemma 4.3 is stated for an arbitrary choice of a vertex $c(F)\in F$ in each member, a generalization of the printed lemma, whose proof uses only $c(F)\in F$. Bound (1) is posed for $k\ge2$. Claims 2–3 are stated stand-alone with the $t$-set $S$ existentially quantified.

Trivializing formalizations are ruled out: the goal asserts the value and the uniqueness of the extremal family, the Turán number is a true maximum rather than a junk supremum, the linear path requires intersections of size exactly one and disjointness of non-consecutive members, and all constants are quantified before $n$.

Needed infrastructure: the delta-system method (Lemma 3.1), Erdős–Gallai for circumference, Erdős' matching theorem and $r$-intersecting Erdős–Ko–Rado for large $n$. Each is reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• Z. Füredi, T. Jiang, R. Seiver, Exact solution of the hypergraph Turán problem for k-uniform linear paths, Combinatorica 34 (2014). arXiv:1108.1247, doi:10.1007/s00493-014-2838-4
• Z. Füredi, On finite set-systems whose every intersection is a kernel of a star, Discrete Math. 47 (1983) 129–132. doi:10.1016/0012-365X(83)90081-X
• P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959) 337–356. doi:10.1007/BF02024498
• P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965) 93–95.
• P. Erdős, C. Ko, R. Rado, Intersection theorems for systems of finite sets, Quart. J. Math. Oxford 12 (1961) 313–320. doi:10.1093/qmath/12.1.313
• P. Frankl, Z. Füredi, Exact solution of some Turán-type problems, J. Combin. Theory Ser. A 45 (1987) 226–262. doi:10.1016/0097-3165(87)90016-7
• D. Mubayi, J. Verstraëte, Minimal paths and cycles in set systems, European J. Combin. 28 (2007) 1681–1693. doi:10.1016/j.ejc.2006.07.008