Statistics

Motivation

How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite-$H$) right is the foundation the rest of the book's guarantees build on.

Setting

A learner sees a sample $S = (x_1,\dots,x_m)$ drawn i.i.d. from a fixed but unknown distribution $D$ on an instance space $X$, labeled by an unknown target concept $c$ drawn from a concept class $C$; a hypothesis $h$ from a fixed hypothesis set $H$ is judged by its generalization error $R(h) = \Pr_{x\sim D}[h(x)\ne c(x)]$ (Definition 2.1) against its empirical error $\hat R_S(h) = \frac1m\sum_i \mathbb 1_{h(x_i)\ne c(x_i)}$ (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most $\epsilon$ with probability at least $1-\delta$, for every accuracy $\epsilon$ and confidence $\delta$ and every distribution $D$ — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.

Formalization targets

Theorem 2.5 (consistent case, milestone). If $H$ is finite and algorithm $A$ always returns a hypothesis consistent with the target concept on the training sample ($\hat R_S(h_S)=0$), then $\Pr_{S\sim D^m}[R(h_S)\le\epsilon]\ge1-\delta$ whenever $m \ge \frac1\epsilon(\log|H|+\log\frac1\delta)$.

Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis $h:X\to\{0,1\}$ and any $\delta>0$, with probability at least $1-\delta$, $R(h) \le \hat R_S(h) + \sqrt{\log(2/\delta)/(2m)}$.

Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set $H$ and any $\delta>0$, with probability at least $1-\delta$, simultaneously for every $h\in H$,

Significance

Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency requirement — the typical case in practice, where no hypothesis in $H$ perfectly fits the training data — while paying only an additive $\log|H|$ price inside the square root, via a union bound over $H$ applied to Corollary 2.11's per-hypothesis concentration bound. It is also the template every later generalization bound in the book refines: Chapter 3 replaces $\log|H|$ with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's Rademacher-complexity bound is the direct machine-independent generalization of the same argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.

Difficulty

Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over $|H|$ hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample $S$ and the target hypothesis $h$ kept in the right relationship — $h$ fixed, $S$ random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the $\forall h\in H$ quantifier placed inside the probability event (a single sample $S$ must work for every $h$ at once), not outside it (which would only assert each $h$'s bound holds with high probability for a sample chosen depending on $h$) — the difference between a uniform convergence bound and $|H|$ separate, weaker statements. Definition 2.3's "polynomial function $\mathrm{poly}(\cdot,\cdot,\cdot,\cdot)$" is a genuine formalization judgment call, addressed below.

Formalization scope

GeneralizationError/EmpiricalError are typed generally over $X, Y$ (matching Definition 2.1/2.2's own general statement, "$h : X\to Y$"), since Theorem 2.5 itself is stated for general $Y$, not just $Y=\mathrm{Bool}$; Corollary 2.11 and Theorem 2.13 specialize to $h : X\to\mathrm{Bool}$, matching their own explicit "$h:X\to\{0,1\}$" (Corollary 2.11) and the surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample $S\sim D^m$ is modeled as the identity random variable on the product-measure space $(\mathrm{Fin}\ m \to X,\ \mathrm{Measure.pi}(\lambda\_.\ D))$ in both Corollary 2.11 and Theorem 2.13, matching the book's own $S\sim D^m$ notation exactly. IsPACLearnable (Definition 2.3) makes "polynomial function" precise as a function bounded above by $K\cdot(a+b+n+s+1)^k$ for some constants $K>0$, $k\in\mathbb N$, uniform in its (nonnegative) arguments — the standard reading of "polynomial in its arguments" in the absence of a ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint entirely (stating only "there is some threshold function") would silently weaken Definition 2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved concept class admits some (possibly super-polynomial) sample-complexity threshold — this is exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no upper bound on $\delta$ is added anywhere the book itself leaves it unrestricted (the theorems remain true, if vacuous, for $\delta>1$). Not formalized: the "efficiently PAC-learnable" running-time clause of Definition 2.3 (a second, independent polynomial-time condition on $A$ not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding statement Corollary 2.11 is immediately derived from by solving for $\epsilon$, making it redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked example (Example 2.4–2.9), which illustrates the framework rather than proving a new general result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle machinery to encode only the specific two-dimensional geometric argument rather than the general finite-$H$ theorems — is exactly what this mission avoids by drafting Theorems 2.5 and 2.13 in their general, hypothesis-set-agnostic form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 2.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association 58(301), 1963, 13-30.

Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.

Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective

where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.

Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has no spurious local minima — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.

Motivation

Stochastic programs and chance-constrained models in operations research contain expectations of the form

where $\xi$ is a random input under an unknown distribution $P_0$, $x$ is a decision and $h$ is a known loss. In practice $P_0$ is seen only through i.i.d. data $\xi_1,\dots,\xi_n$. Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.

The usual answer, for divergence-based sets on a finite support of size $k$, sets the radius from a $\chi^2_{k-1}$ quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as $k$ grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for $Z_0(x)$. The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).

Timeline:

• 1988: Owen proves the empirical likelihood theorem for a mean (−2 log of the profile likelihood ratio tends to $\chi^2_1$), the nonparametric analogue of Wilks' theorem.
• 2013: Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen calibrate $\varphi$-divergence balls on a finite support with $\chi^2_{k-1}$ quantiles.
• 2016: Lam (this paper) connects the empirical Burg-ball DRO to empirical likelihood, with pointwise (Theorem 2) and uniform (Theorem 4) coverage.
• 2016–2021: Duchi, Glynn and Namkoong (arXiv:1610.03425) develop the general $f$-divergence version and exact coverage of optimal values.

Setting

Data: $\xi_1,\xi_2,\dots$ are i.i.d. random elements of a measurable space $\Xi$ under $P_0$. A decision $x\in\mathbb R^m$ is fixed, and $h(x;\cdot):\Xi\to\mathbb R$ is measurable with $0<\operatorname{Var}_0 h(x;\xi)<\infty$.

The empirical Burg-entropy divergence ball of radius $\eta$ is the set of weight vectors on the $n$ data points

with $\log 0=-\infty$. It is the $\varphi$-divergence ball around the uniform weights $1/n$ for the Burg generator $\varphi(t)=-\log t+t-1$. Let $\chi^2_{1,1-\alpha}$ be the $(1-\alpha)$-quantile of the $\chi^2_1$ law, i.e. $P(Y^2\le\chi^2_{1,1-\alpha})=1-\alpha$ for $Y\sim N(0,1)$. The empirical DRO bounds are

For a sample $z\in\mathbb R^n$ and a value $\mu$, the profile empirical likelihood statistic is

equal to $+\infty$ when no weight vector is feasible.

Formalization targets

Goal: Theorem 2 (p. 11)

The event is two-sided and joint. No rate is claimed.

Milestones

• Proposition 2 (p. 23). For every data vector and $\kappa\ge0$,

• Theorem 1, the empirical likelihood theorem (p. 10). $-2\log R(Z_0(x))\Rightarrow\chi^2_1$.
• The pointwise steps of the paper's proof of Theorem 1 (the proof of Theorem 5 with a one-point index set): Lemma 3 (p. 38), $\max_{i\le n}|Y_i|=o(n^{1/2})$ a.s. for square-integrable i.i.d. $Y_i$; the closed form (49)–(50) (pp. 25–26) of the optimal weights; the multiplier bound (52) (p. 27); the expansion (68) (p. 30), $-2\log R=n s^{-1}\bar h^2+o_p(1)$.

Significance

Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius $\chi^2_{1,1-\alpha}/(2n)$ yields an asymptotically exact $(1-\alpha)$ confidence interval for an expected loss, independently of the support size of $\xi$. Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on $-2\log R$ transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.

The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point $\{x\}$ and its generator is $2\varphi$ with radius $\chi^2_{1,1-\alpha}$; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to $|Y_i|$.

Difficulty

Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining $-2\log R$, which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier $\lambda$ that solves a nonlinear equation; to expand $-2\log R$ one must first show $\lambda=O_p(n^{-1/2})$, which requires controlling the largest observation by Lemma 3 together with the law of large numbers for $s$, and then bound the cubic Taylor remainder of $\log(1+\lambda\tilde h_i)$ uniformly in $i$. A direct appeal to the central limit theorem for the sample mean does not suffice, since $-2\log R$ is an implicitly defined optimal value, not a smooth function of the mean.

Formalization scope

• The sample is a sequence ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from $0$; the size-$n$ sample is fun i : Fin n => h x (ξ i ω).
• The moment assumption is MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is $1$.
• The quantile is pinned by gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with $0<\alpha<1$; it is not a free parameter, and it is not the normal quantile.
• The upper bound is the published GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius $\rho/n$, so $\rho=q/2$); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.
• The Burg generator is $+\infty$ at $t\le0$, and the statistic elStat minimizes over strictly positive weights with the empty infimum equal to $+\infty$. Lean's junk value $\log 0=0$ therefore never enters: a formalization with $w_i\ge0$ and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For $n\ge1$ the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.
• The decision set $\Theta$ is dropped (the statements are pointwise in $x$). Theorem 1 is stated as convergence of distribution functions at every $t$, which is equivalent to $\Rightarrow\chi^2_1$ since the limit is continuous. Proposition 2 is stated for general $\kappa\ge0$ and every data vector, as displayed on p. 11. Milestones (49)–(50), (52), (68) are the one-point ($\Theta=\{x\}$) specialisations of the proof of Theorem 5.
• Probabilities of events are outer probabilities; no measurability of events is assumed, as the paper ignores these issues (p. 14).
• Not posed: the headline Theorem 4 (uniform calibration over $\Theta$ by the quantile of a $\chi^2$-process supremum), Theorem 5 and Lemma 2, which need Donsker classes and weak convergence in $\ell^\infty(\Theta)$, for which Mathlib has no substrate.

Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.

Selected references

• H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019. https://arxiv.org/abs/1605.09349v1
• A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
• A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of robust optimization: a generalized empirical likelihood approach, Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425

Motivation

Data-driven decision making with side information ("prescriptive analytics") chooses a decision $z$ after observing a context $x = x_0$, using a training set of past pairs $(x, y)$. A common recipe estimates the conditional expected cost $\mathbb E[L(z, y) \mid x = x_0]$ with a local learning method, such as Nadaraya–Watson kernel regression or nearest neighbours, and then minimizes the estimate over $z$ (Ban and Rudin 2019; Bertsimas and Kallus 2020). Such estimate-then-optimize decisions are known to be optimistically biased: the minimized estimate tends to understate the cost that the decision incurs on new data.

Bertsimas and Van Parys (arXiv:1711.09974v2) robustify these formulations against distributions near the empirical one, measured by a relative-entropy bootstrap distance. They show that this choice protects the decision against disappointment on resampled (bootstrap) data at an exponential rate. A robust formulation is only usable if it can be computed. This mission concerns the paper's computational result for the Nadaraya–Watson case: the robust budget, a supremum over a set of distributions, equals a two-variable convex dual program.

Setting

The training data have finitely many distinct points, the support $\Omega_n$. A distribution on $\Omega_n$ is a vector $D = (D_i)_{i \in \Omega_n}$ with $D_i \ge 0$ and $\sum_i D_i = 1$; their set is $\mathcal D_n$. Fix a context $x_0$ and a decision $\bar z$. Each support point $i = (\bar x_i, \bar y_i)$ carries a weight $w_i = w_n(\bar x_i, x_0) > 0$ and a loss $\ell_i = L(\bar z, \bar y_i)$.

The Nadaraya–Watson estimate at $D$ (equation (19)) is the weighted average

The bootstrap distance (Definition 6, equation (27)) is the relative entropy

with $0\log 0 = 0$ and $B(D', D) = +\infty$ when $D'$ puts mass on a point where $D$ vanishes. For a reference distribution $D$ and a radius $r$, the bootstrap robust Nadaraya–Watson budget (equation (24) with $R = B$ and $k(n) = n$) is

For the nearest-neighbours variant, nested neighbourhoods $N^0 \subseteq N^1 \subseteq \dots \subseteq N^n = \Omega_n$ define a partial robust budget $c^j_n$ (equation (25)), with two extra linear constraints tying the mass of $N^j$ and $N^{j-1}$ to $k/n$ and $(k-1)/n$.

Formalization targets

Goal: Lemma 2

For every $D \in \mathcal D_n$ and every radius $r \in \mathbb R$,

No hypothesis on $r$ is imposed. For $r < 0$ both sides are $-\infty$, and for $r = 0$ both equal $E^n_D[\ell]$.

Milestones

The milestones follow the proof in Appendices B.3 and B.8:

1. The estimate $E^n_D[\ell]$ is the maximum of a linear program in $(s, P)$ with the single feasible point $P = sD$ (B.3).
2. Corollary 1: for any distance $R$, $c_n$ equals the perspective program $\sup_{s > 0, P} \sum_i w_i \ell_i P_i$ subject to $s\,R(P/s, D) \le s\,r$, $\sum_i P_i = s$ and $\sum_i w_i P_i = 1$.
3. The Fenchel step: $\sup_{\lambda \ge 0}(\lambda b - \nu\lambda\log\lambda) = \nu e^{b/\nu - 1}$.
4. Strong duality for $r > 0$: the program of Corollary 1 with $R = B$ equals $\inf\{\alpha : \exists \beta, \nu > 0,\ r\nu + \nu\sum_i D_i e^{((\ell_i - \alpha)w_i + \beta)/\nu - 1} \le \beta\}$.
5. Elimination of $\beta$: such a $\beta$ exists if and only if $\nu \log \sum_i e^{(\ell_i-\alpha)w_i/\nu} D_i + r\nu \le 0$.
6. Lemma 1 (companion): the analogous dual (32) of the partial nearest-neighbours budget, assuming Slater's condition $\inf\{B(D', D) : D' \in \mathcal D^j_n\} < r$.

Significance

The robust budget is a supremum over a $|\Omega_n|$-dimensional set of distributions, and the decision minimizes it over $\bar z$, which is a min–max problem. Lemma 2 replaces the inner supremum by an infimum over two scalars $(\alpha, \nu)$, so the robust prescription becomes a single minimization over $(\bar z, \alpha, \nu)$. When $L$ is convex in $\bar z$, that minimization is an exponential-cone program. The paper's numerical section (§5) solves its robust formulations in exactly this form. Lemma 1 plays the same role for the nearest-neighbours formulation, with one dual program per neighbourhood.

The results are proved in the paper (Appendices B.3, B.7, B.8) by a Lagrangian computation. As far as we know, none of them has been machine-checked. A formalization adds three things. It handles reference distributions $D$ with zeros, which the page's computation divides by. It covers the full range of radii, including $r \le 0$, where Slater's condition fails. And it records the corrected sign of the minimizing multiplier $\beta^\star$. The linear-objective special case without the ratio and with a strictly positive reference, $\max\{v^\top p : D(p\|q) \le \beta\} = \inf_{\lambda > 0} \lambda \log \sum_j q_j e^{v_j/\lambda} + \beta\lambda$, is already proved on the platform (Nilim–El Ghaoui, RobustMDP.EntropyInner.kl_ball_inner_problem_dual, with its multiplier elimination RobustMDP.EntropyInner.mu_elimination). Both are included as supporting references.

Difficulty

The obvious route is to apply the known entropic duality formula to the robust budget directly. That route fails because the objective $E^n_{D'}[\ell]$ is a ratio of two linear functions of $D'$, not a linear function. The ratio is quasi-linear, and Lagrangian duality does not apply to it as it stands. The paper first lifts it to a linear objective over the cone $(s, P) = (s, sD')$ (Corollary 1). The entropy constraint then becomes the perspective $s\,B(P/s, D) \le s\,r$, and duality is applied to this lifted program. A second difficulty is that the reference $D$ may vanish on part of the support. The ball then lives on a face of the simplex, and every step must respect the convention $B = +\infty$ off the support of $D$. Finally, strong duality needs a Slater point, which exists only for $r > 0$. The cases $r \le 0$ of the goal have to be handled separately.

Formalization scope

The support $\Omega_n$ is a finite type ι, and $\mathcal D_n$ is stdSimplex ℝ ι. Covariates, responses and the distance of Definition 2 do not appear: only the weights w : ι → ℝ (positive) and the losses L z : ι → ℝ of a fixed decision enter. Losses are real-valued, a restriction of the paper's $\mathbb R_+ \cup \{+\infty\}$, while nonnegativity is not required. The conventions are the following.

• $B$ is EReal-valued: it is $+\infty$ when the first argument charges a zero of the second, and $0 \log 0 = 0$.
• All suprema and infima are in EReal: the supremum of the empty set is $-\infty$ and the infimum of the empty set is $+\infty$.
• Dual variables satisfy $\nu > 0$. The page's $\nu \in \mathbb R_+$ admits $\nu = 0$ only as the perspective limit, and the infimum over $\alpha$ is unchanged.
• In the perspective programs, $P/s \in \mathcal D_n$ is stated explicitly.
• The neighbourhood chain is a monotone family of finite sets with $N^0 = \emptyset$ and $N^n = \Omega_n$.

Several formalizations would make the statements trivial, and each is ruled out:

• a real-valued $B$, whose finite junk values enlarge the ball when $D$ has zeros;
• real sSup/sInf, which return $0$ on empty or unbounded sets;
• $\nu \ge 0$ with Lean's $x/0 = 0$, which makes every $\alpha$ feasible;
• a positivity hypothesis on $D$, which the lemma does not have.

A complete development needs the following:

• Gibbs' inequality and continuity of $B$ on the simplex;
• Lagrangian (or Fenchel) duality for a convex program with one entropic constraint and linear constraints;
• the perspective of relative entropy;
• the one-dimensional conjugate of $\lambda \log \lambda$.

The duality and conjugate lemmas are reusable for any KL-ball robust program. Contributions are welcome on each milestone, on bridges from the published RobustMDP.EntropyInner theorems to the setting here (they agree with $B$ when the reference is positive), and on the $r \le 0$ cases of the goal.

Selected references

• D. Bertsimas and B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021 (Math. Program., 2021). https://arxiv.org/abs/1711.09974v2
• G.-Y. Ban and C. Rudin, The big data newsvendor: practical insights from machine learning, Operations Research 67(1), 2019. https://doi.org/10.1287/opre.2018.1757
• D. Bertsimas and N. Kallus, From predictive to prescriptive analytics, Management Science 66(3), 2020. https://doi.org/10.1287/mnsc.2018.3253
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg and G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

Motivation

Boosting combines many weak classifiers into a strong one by refitting, again and again, to reweighted data. AdaBoost (Freund and Schapire, 1997) and its confidence-rated variant Real AdaBoost (Schapire and Singer, 1999) were introduced through the theory of online learning. Friedman, Hastie and Tibshirani (2000) recast them as stagewise fitting of an additive model $F(x) = \sum_m f_m(x)$ by minimizing the exponential criterion $J(F) = E\,e^{-yF(x)}$, where $y\in\{-1,1\}$ is the class label. In that view Real AdaBoost minimizes $J(F+f)$ exactly over the new term $f$ at each stage.

The same paper proposes Gentle AdaBoost (Algorithm 4, §4.4), which replaces the exact minimization by a single Newton step. Its increments are bounded, and the authors report that it often matches or beats Real AdaBoost and LogitBoost, especially when numerical stability is an issue. The paper's stagewise view of boosting led on to gradient boosting (Friedman, 2001). This mission formalizes the paper's justification of the algorithm: its population version takes Newton steps on $E\,e^{-yF(x)}$.

Setting

A feature $x$ ranges over a measurable space $X$. The label $y$ takes values in $\{-1,1\}$, and $(x,y)$ has a joint probability law $\nu$ on $X\times\{-1,1\}$. Conditional expectations given $x$, written $E(\cdot\mid x)$, are integrals against the conditional law $\nu(\cdot\mid x)$ of $y$ given $x$, and $P = P(y=1\mid x)$.

The algorithm maintains a current additive fit $F : X\to\mathbb R$, starting from $F = 0$. For a new term $f(x)$, the conditional exponential criterion is

a function of the real number $f(x)$ for each fixed $x$.

The weight attached to an observation is $w(x,y) = e^{-yF(x)}$. The weighted conditional expectation (p. 347) is

and $P_w(y=b\mid x) = E_w[1_{[y=b]}\mid x]$ are the weighted class probabilities.

Gentle AdaBoost (Algorithm 4) repeats three steps: fit $f_m$ by weighted least squares of $y$ on $x$ with weights $w$, update $F \leftarrow F + f_m$, and update $w \leftarrow w\,e^{-yf_m(x)}$ with renormalization. In the population version the weighted least-squares fit is the weighted conditional mean, so one step is

For comparison with LogitBoost the paper uses the symmetric logistic $p(x) = e^{F(x)}/(e^{F(x)}+e^{-F(x)})$ and the 0/1 response $y^* = (y+1)/2$.

Formalization targets

Goal: Result 4

For every $x$, with $s(x) = -E(e^{-yF(x)}y\mid x)$ and $H(x) = E(e^{-yF(x)}\mid x)$: $s(x)$ is the first derivative of $J(F(x)+f(x))$ at $f(x)=0$, $H(x)$ is the second derivative, $H(x)>0$, and

This is the paper's Result 4, "the Gentle AdaBoost algorithm (population version) uses Newton steps for minimizing $Ee^{-yF(x)}$", in the precise form its Derivation gives.

Milestones

1. The Derivation's derivatives:

2. The Newton update: $F(x) + E(e^{-yF(x)}y\mid x)/E(e^{-yF(x)}\mid x) = F(x) + E_w(y\mid x)$.
3. The update as weighted class probabilities: $E_w(y\mid x) = P_w(y=1\mid x) - P_w(y=-1\mid x)$.
4. The range: $E_w(y\mid x) \in [-1,1]$.
5. Display (37):

6. Display (38): the LogitBoost increment $\tfrac12 E(y^*-p(x)\mid x)/E(p(x)(1-p(x))\mid x)$ equals $\tfrac12 (P-p(x))/(p(x)(1-p(x)))$.

Significance

The result. Result 4 places Gentle AdaBoost alongside LogitBoost (Result 3) as a Newton method. Real AdaBoost (Result 2) and Gentle AdaBoost minimize the same criterion, but one solves the stagewise problem exactly and the other takes one Newton step. Displays (37) and (38) then put Gentle AdaBoost and LogitBoost in the same coordinates $P$ and $p(x)$. The two updates are close when $p(x)\approx \tfrac12$. LogitBoost's update can be unbounded as $p(x)$ approaches $0$ or $1$, while Gentle AdaBoost's always stays in $[-1,1]$. This is the paper's explanation for the stability of Gentle AdaBoost.

Formalizing it. The result is proved on the page by direct calculation. No machine-checked version is known to exist. The mission produces a formal account of the population algorithm on an arbitrary joint law, through Mathlib's disintegration of a measure on $X\times\{-1,1\}$, and of the Newton-step identity. It also gives a reusable treatment of the paper's weighted conditional expectation $E_w$ in the conditional-kernel language. The same objects appear in the other missions of this series (Real AdaBoost, LogitBoost).

Difficulty

The calculus on the page is short. The work is in the setting. "Differentiate the criterion with respect to $f(x)$" has to mean differentiating an integral against the conditional law of $y$ given $x$ with respect to a parameter, with the derivative established, not read off a formula. A plain derivative equation proves nothing at a point where the function is not differentiable. The second derivative needs the first derivative as a function of $t$, not only its value at $0$. The Newton step divides by $H(x)$, so its positivity must be established before the identity has content. Finally, (37) requires recovering $P(y=-1\mid x) = 1-P$ from the conditional law being a probability measure, and the second equality in (37) holds only for the symmetric logistic.

Formalization scope

Labels are Bool (true for $y=1$, false for $y=-1$); $y$ is sgn b and $y^*$ is ystar b. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν], and $E(\cdot\mid x)$ is the Bochner integral against ν.condKernel x, a probability measure on the two-point type. Every statement holds for every $x$. No almost-everywhere qualifier, integrability or measurability hypothesis is needed, and none is added. The kernel is unique only almost everywhere, and the statements hold for the chosen version. They use only the fact that it is a Markov kernel. The definitions file fixes the conditional criterion condCritAt, the weighted conditional expectation wCondExp with weight $e^{-yF(x)}$, the weighted class probabilities wProb, the population step gentleStep, and the symmetric logistic symLogistic. All of these are written exactly as on the page.

Derivatives are HasDerivAt statements. The second derivative is the derivative at $0$ of an explicit first-derivative function, which is itself shown to be the derivative at every point. $H(x)>0$ is a conclusion of the goal, never a hypothesis. Several formalizations would trivialize the claims and are ruled out. The criterion is the integral against the conditional law, not a closed form $\eta e^{-F-t}+(1-\eta)e^{F+t}$ in a free parameter $\eta$. No bare deriv equation and no division by an unproved nonzero quantity is used. The logistic is the symmetric $e^{F}/(e^{F}+e^{-F})$, not $1/(1+e^{-F})$, which differs by a factor $2$ in $F$ and makes (37) false. The sample version of Algorithm 4 (trees, terminal-node averages) is not formalized.

Welcome contributions: proofs of the milestones, general lemmas on differentiating integrals over finite label spaces with respect to a parameter, and lemmas connecting condKernel on Bool with the closed forms in $P$.

Selected references

• J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
• R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
• J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451

Motivation

Boosting combines many weak classifiers into a strong one by refitting, round after round, to a reweighted version of the training data. Freund and Schapire's AdaBoost was introduced as a procedure, with guarantees on the training error, and for several years it was not clear what statistical model it fitted. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) answered this by showing that boosting is stagewise additive modelling: each round adds one term to an additive function $F(x) = \sum_m f_m(x)$ so as to improve a population criterion.

Section 4.3 of that paper takes the step from interpretation to design. If boosting is stagewise fitting of an additive logistic model, one can choose the criterion directly: the Bernoulli log-likelihood. The resulting procedure, LogitBoost (Algorithm 3), fits at each round a weighted least-squares regression to a working response, exactly as iteratively reweighted least squares fits a logistic regression. Result 3 states that this is no accident: in the population, LogitBoost's update is a Newton step on the expected log-likelihood. The same Newton reading reappears in gradient boosting with logistic loss, where each terminal node of a tree takes one Newton step (Friedman 2001).

Timeline:

• 1997: Freund and Schapire, AdaBoost (J. Comput. Syst. Sci. 55).
• 1999: Schapire and Singer, Real AdaBoost with confidence-rated predictions (Mach. Learn. 37).
• 2000: Friedman, Hastie and Tibshirani, the statistical view; LogitBoost and Result 3.
• 2001: Friedman, gradient boosting machines (Ann. Statist. 29).

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability measure on $X\times\{0,1\}$, the joint law of a feature $x$ and a 0/1 response $y^*$. Write $E(\cdot\mid x)$ for the conditional expectation given $x$, an integral against the regular conditional distribution of $y^*$ given $x$.

A current fit is a function $F : X\to\mathbb R$. The symmetric logistic model (30) represents $P(y^*=1\mid x)$ by

For an update $f(x)$, the expected log-likelihood (31) is

whose integrand is the Bernoulli log-likelihood $y^*\log p + (1-y^*)\log(1-p)$ of $y^*$ under the model.

For a positive weight $w$, the weighted conditional expectation is $E_w(g\mid x) = E(wg\mid x)/E(w\mid x)$. LogitBoost (Algorithm 3), population version, computes the working response and weight

fits $f(x) = E_w(z\mid x)$ (the population weighted least-squares regression of $z$ on $x$), and updates $F(x)\leftarrow F(x)+\tfrac12 f(x)$.

Formalization targets

Goal: Result 3

Fix $x$ and let $\ell_x(t) = E[\,2y^*(F(x)+t) - \log(1+e^{2(F(x)+t)})\mid x]$. Then $\ell_x$ has first derivative $s(x)$ and second derivative $H(x)$ at $t=0$,

$H(x)\neq0$, and the population LogitBoost update equals the Newton update:

Milestones

1. (31): the integrand of $E\,l(F+f)$ is the Bernoulli log-likelihood of the symmetric logistic model.
2. (32): the first derivative $s(x)$.
3. (33): the second derivative $H(x)$.
4. (34)–(35): $F(x) - H(x)^{-1}s(x) = F(x) + \frac12 \frac{E(y^*-p(x)\mid x)}{E(p(x)(1-p(x))\mid x)} = F(x)+\frac12E_w\big(\frac{y^*-p(x)}{p(x)(1-p(x))}\,\big|\,x\big)$.
5. (36): the Newton update solves $\min_{f(x)} E_{w(x)}\big(F(x)+\frac12 z - (F(x)+f(x))\big)^2$.

Significance

The result. Result 3 explains what LogitBoost computes: a stagewise Newton–Raphson ascent of the expected Bernoulli log-likelihood, one coordinate $F(x)$ at a time. It makes the working response and the weights of Algorithm 3 the score and curvature of the likelihood, and reduces each round to a weighted least-squares problem (36) that any regression method can solve.

Formalizing it. The result is proved on the page by a short calculation, and no machine-checked version exists. The mission produces a formal account of the population algorithm on an arbitrary joint law, with conditional expectations taken through a regular conditional distribution, the derivatives stated with differentiability, and the Newton step identified exactly, including the constants $2$, $-4$ and $\tfrac12$ that the symmetric parametrization forces.

Difficulty

The algebra is short; the formal content is in keeping every object honest. The derivatives are of a conditional expectation in a parameter, so differentiation must pass through the integral against the conditional law. The second derivative needs the first derivative as a function of $t$, not only its value at $0$. The Newton step divides by $H(x)$, which must be shown nonzero from $0<p(x)<1$ rather than assumed. A tempting shortcut, replacing the conditional expectation of the log-likelihood by its closed form in a free probability parameter, removes the joint law from the statement and is ruled out.

Formalization scope

• Labels are Bool, with $y^*(\texttt{true}) = 1$ and $y^*(\texttt{false})=0$. The joint law is a probability measure ν on X × Bool; $E(\cdot\mid x)$ is the integral against Mathlib's ν.condKernel x. Every statement is for every $x$, conditional on $x$ as in the Derivation; because the label space is finite, no integrability or measurability hypotheses are needed.
• The symmetric logistic is written exactly as (30), $e^{t}/(e^{t}+e^{-t})$, not as $1/(1+e^{-t})$, which differs by a factor $2$ in $t$ and would change every constant.
• The conditional log-likelihood is defined as an integral against the conditional law, not by its closed form with a free parameter.
• Derivatives are stated with HasDerivAt, never with deriv, which returns $0$ at non-differentiable points; $H(x)\neq0$ is a conclusion, so the division in the Newton step cannot silently return $0$.
• The weighted conditional expectation takes its weight as an explicit argument; here it is $p(x)(1-p(x))$.
• In (36) the page writes $E_{w(x)}$ without "$\mid x$"; it is read as the conditional weighted expectation, since the Derivation conditions on $x$ throughout.
• Out of scope: the data version of Algorithm 3 (regression trees, the $z_{\max}$ threshold and the weight floor of pp. 352–353), which are implementation choices, and the multiclass algorithm (§5).

Contributions welcome: differentiation of finite conditional expectations in a parameter, and derivative facts for the symmetric logistic, both reusable across the other missions of this series.

Selected references

• J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
• R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
• J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451

Motivation

The residual life time of a lifetime $X$ at age $t$ is the excess $X - t$ given survival, $X > t$. How it behaves at great ages is a question in reliability (remaining life of an item that has already lasted long), in insurance and demography (remaining life at old age), and in the peaks-over-threshold method of extreme value statistics, where exceedances over a high threshold are modelled by a generalized Pareto law.

Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974) 792–804) determined every possible limit law of the suitably normed residual life as $t \to \infty$, and their domains of attraction. For continuous limits, the classical sufficient conditions are von Mises' conditions (1936) on the derivative of $(1 - F)/F'$. Section 4 of the paper goes further: it gives inequalities that hold at every finite age $t \ge t_0$, not only in the limit. This mission formalizes that finite-$t$ result, the Corollary to Theorem 7.

Timeline: von Mises (1936) gives sufficient conditions for domains of attraction of extreme value laws; Balkema and de Haan (1974) prove the limit theorems for residual life and the finite-$t$ bounds formalized here; Pickands (1975, Ann. Statist. 3, 119–131) proves the corresponding approximation by the generalized Pareto law for excesses, the result now known as the Pickands–Balkema–de Haan theorem.

Setting

Let $X$ be a real random variable with distribution function $F$. The residual life distribution function at age $t$ is

Assume $F$ has a positive, differentiable density $F'$ for $t \ge t_0$, and define the norming function

the reciprocal of the hazard rate. The normed residual life is $(X - t)/a(t)$ given $X > t$, with distribution function $P\{(X - t)/a(t) \le x \mid X > t\} = F_t(x\,a(t))$.

The comparison laws are the distribution functions $\Pi_{0,c}$, $c \in \mathbb R$, all vanishing for $x < 0$:

• for $c > 0$, $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $x \ge 0$ (a generalized Pareto law);
• for $c = 0$, $\Pi_{0,0}(x) = \Pi(x) = 1 - e^{-x}$ for $x \ge 0$ (the exponential law);
• for $c < 0$, $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $0 \le x \le |c|^{-1}$, and $1$ beyond (bounded support).

Formalization targets

Goal: the Corollary to Theorem 7

If $c \ge 0$ and $\varepsilon \ge 0$ satisfy $|c - a'(t)| \le \varepsilon$ for $t \ge t_0$, then

Milestones

1. The bounds (13): if $c_1 \le a' \le c_2$ on $[t_0, \infty)$, then $1 + c_1 x \le a(t + x a(t))/a(t) \le 1 + c_2 x$ for $t \ge t_0$, $x \ge 0$.
2. The exponential representation

3. Theorem 7: if $c_1 \le a'(t) \le c_2$ for $t \ge t_0$, then

4. $\sigma(u) = u^{-2}(e^{-u} - 1 + u) = \int_0^1\int_0^t e^{-us}\,ds\,dt$ is positive and decreasing.
5. Lemma 4: $0 \le -(\partial/\partial c)\Pi_{0,c}(x) < 1$ for $c > -1$, $x \ne 0$, $cx \ne -1$.
6. $|\Pi_{0,c}(x) - \Pi_{0,c_0}(x)| \le |c - c_0|$ for $c \ge 0$ and all real $c_0$, $x$.

The goal is the Corollary because it is the paper's final statement of Section 4: a single parameter $c$ and a single error $\varepsilon$, with no limit taken. Theorem 7 is the stronger two-parameter sandwich it rests on.

Significance

The result. Theorem 7 and its Corollary are a quantitative, non-asymptotic form of the von Mises condition $\frac{d}{dt}\frac{1-F(t)}{F'(t)} \to c$. If the derivative of the reciprocal hazard stays within $\varepsilon$ of $c$ from age $t_0$ on, then at every such age the normed excess distribution is uniformly within $\varepsilon$ of the generalized Pareto (or exponential) law $\Pi_{0,c}$. Letting $\varepsilon \to 0$ along $t_0 \to \infty$ recovers convergence to $\Pi_{0,c}$, and the bound itself quantifies the error of the generalized Pareto approximation used in threshold-exceedance modelling.

Formalizing it. The result is proved in the paper (1974), with short proofs. To our knowledge no part of it has a machine-checked proof. The mission produces checked versions of the theorem, the corollary and the elementary lemmas about the family $\Pi_{0,c}$: its monotonicity and Lipschitz dependence on the parameter $c$, including across the case change at $c = 0$. Those facts about the generalized Pareto family are reusable in any formal development of extreme value statistics.

Difficulty

The analytic content is elementary, but several steps hide case analysis. The Lipschitz bound in $c$ requires the derivative of $\Pi_{0,c}(x)$ in $c$ across $c = 0$, where the formula changes from $1 - (1+cx)^{-1/c}$ to $1 - e^{-x}$, and across the boundary $cx = -1$ of the support when $c < 0$, where the function is not differentiable. The bound $-\partial_c \Pi_{0,c} < 1$ is not a crude estimate: it reduces to the comparison $\sigma(u) < \sigma(-\psi)$ for the function $\sigma(u) = u^{-2}(e^{-u} - 1 + u)$, which needs its strict monotonicity on all of $\mathbb R$, including $u = 0$ where the closed form is undefined. In Theorem 7 the lower bound $1 + c_1 x$ in (13) becomes negative for $c_1 < 0$ and large $x$; this is exactly where the comparison law $\Pi_{0,c_1}$ reaches $1$, and the argument must handle it. The orientation is easy to get wrong: the upper bound $c_2$ on the derivative gives the lower bound $\Pi_{0,c_2}$, since $\Pi_{0,c}(x)$ decreases in $c$.