Optimization

Motivation

Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the simplest matrix consistent with a set of linear observations, where "simplest" means "of least rank". Given a linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ and a vector $b\in\mathbb R^p$, the affine rank minimization problem is

$$\min_X\ \operatorname{rank}(X)\quad\text{s.t.}\quad \mathcal A(X)=b .$$

This problem is NP-hard in general: it contains the problem of finding the sparsest solution of a linear system as the special case of diagonal matrices. A standard heuristic, popularized in control by Fazel, Hindi and Boyd, replaces the rank by the nuclear norm $\|X\|_*$, the sum of the singular values, which is the convex envelope of the rank on the unit ball of the operator norm. The resulting problem is a semidefinite program and can be solved efficiently.

Recht, Fazel and Parrilo (arXiv:0706.4138, SIAM Review 2010) gave the first general conditions under which this heuristic provably returns the minimum-rank solution. Their argument transfers the compressed sensing theory of Candès and Tao (Decoding by linear programming, 2005) and Candès, Romberg and Tao from sparse vectors and the $\ell_1$ norm to low-rank matrices and the nuclear norm. This mission formalizes the paper's deterministic recovery theorem (Section 3).

Setting

Matrices are real $m\times n$ matrices. For matrices $X,Y$ of the same size, $\langle X,Y\rangle=\operatorname{Tr}(X^{\top}Y)=\sum_{i,j}X_{ij}Y_{ij}$ is the trace inner product. With $\sigma_1(X)\ge\sigma_2(X)\ge\dots\ge0$ the singular values of $X$, the three norms used are the operator norm $\|X\|=\sigma_1(X)$, the Frobenius norm $\|X\|_F=\sqrt{\langle X,X\rangle}=(\sum_i\sigma_i(X)^2)^{1/2}$, and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$.

A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by $p$ measurement matrices $A_1,\dots,A_p$ through $\mathcal A(X)_i=\langle A_i,X\rangle$; $\|\mathcal A(X)\|$ is the Euclidean norm of the vector $\mathcal A(X)\in\mathbb R^p$.

For an integer $r$, the $r$-restricted isometry constant $\delta_r(\mathcal A)$ (Definition 3.1) is the smallest $\delta\ge0$ with

$$(1-\delta)\,\|X\|_F\le\|\mathcal A(X)\|\le(1+\delta)\,\|X\|_F\qquad\text{for every } X \text{ with } \operatorname{rank}X\le r .$$

Fix a matrix $X_0$ of rank at most $r$, put $b=\mathcal A(X_0)$, and consider the nuclear norm minimization problem

$$X^*:=\arg\min_X\ \|X\|_*\quad\text{s.t.}\quad\mathcal A(X)=b. \tag{3.1}$$

Formalization targets

Goal: Theorem 3.3

If $r\ge1$ and $\delta_{5r}(\mathcal A)<\tfrac1{10}$, then $X^*=X_0$; precisely,

$$\forall X\in\mathbb R^{m\times n}:\quad \mathcal A(X)=\mathcal A(X_0)\ \text{ and }\ \|X\|_*\le\|X_0\|_*\ \Longrightarrow\ X=X_0 .$$

The statement holds for every linear map, every $m,n,p$ and every $X_0$ of rank at most $r$. The constant $1/10$ is the paper's; the paper notes (p. 14) that its derivation is chosen for simplicity and is not optimal.

Milestones, in the paper's order

1. Theorem 3.2 (p. 12): if $\delta_{2r}<1$, then $X_0$ is the only matrix of rank at most $r$ with $\mathcal A(X)=b$.
2. (2.1) (p. 6): $\|X\|\le\|X\|_F\le\|X\|_*\le\sqrt r\,\|X\|_F\le r\,\|X\|$ whenever $\operatorname{rank}X\le r$.
3. Lemma 2.3 (p. 9): if $AB^{\top}=0$ and $A^{\top}B=0$, then $\|A+B\|_*=\|A\|_*+\|B\|_*$.
4. Lemma 3.4 (pp. 12–13): every $B$ splits as $B=B_1+B_2$ with $\operatorname{rank}B_1\le2\operatorname{rank}A$, $AB_2^{\top}=0$, $A^{\top}B_2=0$ and $\langle B_1,B_2\rangle=0$.
5. (3.3)–(3.4) (p. 13): for the error $R=R_0+R_c$ of a minimizer, $\|R_c\|_*\le\|R_0\|_*$.
6. (3.5)–(3.6) (p. 13): a matrix splits into pairwise orthogonal pieces of rank at most $3r$ whose Frobenius norms, from the second piece on, sum to at most $\|M\|_*/\sqrt{3r}$.
7. Monotonicity (p. 12): $\delta_r\le\delta_{r'}$ for $r\le r'$.
8. (3.7) (p. 14): $\|\mathcal A(R)\|\ge\big((1-\delta_{5r})-\tfrac9{11}(1+\delta_{3r})\big)\|R_0\|_F$, with a positive factor whenever $9\delta_{3r}+11\delta_{5r}<2$.

Significance

Theorem 3.3 is a deterministic certificate: it separates the question "does nuclear norm minimization recover low-rank matrices?" into a property of the measurement map alone, with an absolute constant independent of $m$, $n$, $r$ and $p$. Section 4 of the same paper then shows that random maps with i.i.d. Gaussian or Bernoulli entries satisfy $\delta_{5r}<1/10$ with high probability once $p$ is of order $r(m+n)\log(mn)$, so a matrix with $mn$ entries is determined by far fewer measurements than entries and is found by a semidefinite program.

The theorem is proved in the paper, and the sparse-vector analogue has been formalized on this platform (HighDimProb.SparseRecovery.rip_implies_exact_recovery, from Vershynin's textbook; CandesTao.Decoding.decoding_by_lp). The matrix version is not formalized. A machine-checked proof needs the basic theory of singular values for rectangular real matrices (the norm comparisons (2.1), additivity of the nuclear norm, the triangle inequality for the nuclear norm, and block decompositions via the singular value decomposition), most of which Mathlib lacks in this form. That infrastructure is reusable for every nuclear-norm result on the platform.

Difficulty

For sparse vectors the analogous proof splits the error vector by its support, and every step is coordinatewise. For matrices there is no common basis: the error $R$ and the target $X_0$ have different singular vectors, and the restricted isometry inequality controls only matrices of low rank. The first obstacle is therefore to split $R$ into a piece of rank at most $2\operatorname{rank}X_0$ and a piece whose row and column spaces are orthogonal to those of $X_0$, so that the nuclear norm is additive. The second is that the triangle inequality, additivity and the norm chain (2.1) for the nuclear norm are themselves nontrivial statements about singular values. Applying the restricted isometry inequality directly to $R$ fails, because $R$ need not have low rank.

Formalization scope

• Matrices are Matrix (Fin m) (Fin n) ℝ; rank is Matrix.rank; transpose is Xᵀ. The norms and the inner product are opNorm, frobeniusNorm, nuclearNorm and traceInner of the published module HighDimStat_MatrixRank_Core, which defines the nuclear norm as the sum of the square roots of the eigenvalues of $X^{\top}X$.
• The map $\mathcal A$ is given by Xs : Fin p → Matrix (Fin m) (Fin n) ℝ and evaluated by observationOp; measNorm Xs X is $\|\mathcal A(X)\|$.
• ripConst Xs r is the infimum of the admissible $\delta\ge0$; the set is nonempty and closed, so the infimum is attained. It is defined for every $r$, not only $1\le r\le m$, since the goal uses $\delta_{5r}$. The paper's normalization $m\le n$ is not assumed.
• The goal assumes $\operatorname{rank}X_0\le r$ rather than $=r$ (equivalent by monotonicity of $\delta$). Its conclusion quantifies over all feasible $X$ with $\|X\|_*\le\|X_0\|_*$, so it does not depend on a choice of arg min. A formalization that fixes some minimizer unrelated to $b$, or only asserts the existence of a minimizer equal to $X_0$, would be trivial and is excluded.
• Milestone (3.5)–(3.6) is stated existentially, listing the properties of the singular value blocks that the proof uses, because Mathlib has no ordered rectangular singular value decomposition. Milestone (3.7) makes explicit the orthogonality $\langle R_0,R_1\rangle=0$ that the paper uses silently.

Welcome contributions: a rectangular SVD with ordered singular values, the triangle inequality and duality for nuclearNorm, and the attainment and monotonicity lemmas for ripConst.

Selected references

• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Review 52(3), 471–501, 2010. https://doi.org/10.1137/070697835 ; preprint arXiv:0706.4138v1. https://arxiv.org/abs/0706.4138
• E. J. Candès, T. Tao, Decoding by Linear Programming, IEEE Trans. Inform. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
• E. J. Candès, J. Romberg, T. Tao, Stable Signal Recovery from Incomplete and Inaccurate Measurements, Comm. Pure Appl. Math. 59(8), 2006. https://doi.org/10.1002/cpa.20124
• M. Fazel, Matrix Rank Minimization with Applications, PhD thesis, Stanford University, 2002.
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §10.5. https://doi.org/10.1017/9781108231596

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

$$J(F(x)+f(x)) = E\big(e^{-y(F(x)+f(x))}\mid x\big),$$

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

$$E_w\big[g(x,y)\mid x\big] = \frac{E[w(x,y)\,g(x,y)\mid x]}{E[w(x,y)\mid x]},$$

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

$$F(x) \leftarrow F(x) + E_w(y\mid x),\qquad w(x,y) = e^{-yF(x)}.$$

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

$$F(x) + E_w(y\mid x) = F(x) - \frac{s(x)}{H(x)}.$$

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:

$$\frac{\partial J}{\partial f(x)}\Big|_{0} = -E(e^{-yF(x)}y\mid x),\qquad \frac{\partial^2 J}{\partial f(x)^2}\Big|_{0} = E(e^{-yF(x)}\mid x).$$

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):

$$\frac{E(e^{-yF(x)}y\mid x)}{E(e^{-yF(x)}\mid x)} = \frac{e^{-F(x)}P - e^{F(x)}(1-P)}{e^{-F(x)}P + e^{F(x)}(1-P)} = \frac{P-p(x)}{(1-p(x))P + p(x)(1-P)} \in [-1,1].$$

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

Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time, the problem written $R\,|\,|\sum w_jC_j$ in the three-field notation, is one of the basic NP-hard models of machine scheduling. Each job may take a different time on each machine, as when heterogeneous processors, plants or crews serve the same pool of tasks, and the objective rewards finishing important jobs early. For a single machine the problem is solved exactly by Smith's ratio rule (Smith, 1956). With several unrelated machines the problem is strongly NP-hard and the question is how close to the optimum a polynomial-time algorithm can come.

Timeline of the guarantees for $R\,|\,|\sum w_jC_j$:

• Lenstra, Shmoys and Tardos (1990) gave an LP-based 2-approximation for the makespan on unrelated machines; their assignment variables $a_{ij}$ are the ones used here.
• Hall, Schulz, Shmoys and Wein (1997) gave constant-factor approximations for $\sum w_jC_j$ on unrelated machines via time-indexed and interval-indexed LP relaxations.
• Schulz and Skutella (conference version 1999, journal 2002) obtained $3/2+\varepsilon$ by randomized rounding of a time-indexed LP.
• Skutella (J. ACM 2001), the paper of this mission, gave a convex quadratic relaxation in assignment variables alone and a $3/2$-approximation by randomized rounding, with a short analysis.
• Bansal, Srinivasan and Svensson (2016) improved $3/2$ to $3/2-\varepsilon$ for a small constant $\varepsilon>0$; later work lowered the constant further.

Setting

There are $n$ jobs $j\in J$ and $m$ machines $i$. Job $j$ has a weight $w_j\ge 0$ and a processing time $p_{ij}>0$ on machine $i$. A schedule assigns each job to one machine and orders the jobs on every machine; the completion time $C_j$ of a job is the time at which it finishes when each machine works without idle time.

For a fixed assignment, Smith's ratio rule orders each machine optimally. Fix for each machine $i$ the total order $j\prec_i k$ iff $w_j/p_{ij}>w_k/p_{ik}$, ties broken by index. Under an assignment $\sigma$ the completion time of $j$ is

$$C_j(\sigma)=p_{\sigma(j)j}+\sum_{k\prec_{\sigma(j)}j,\ \sigma(k)=\sigma(j)}p_{\sigma(j)k},$$

and the problem is to minimize $\mathrm{val}(\sigma)=\sum_jw_jC_j(\sigma)$ over all assignments.

With $a_{ij}\in\{0,1\}$ indicating that $j$ runs on $i$, the problem is the integer quadratic program (IQP) with objective

$$Z_{QP}(a)=c^Ta+\tfrac12a^TDa,\qquad c_{ij}=w_jp_{ij},$$

where $D$ is symmetric with entry $w_jp_{ik}$ at $((i,j),(i,k))$ for $k\prec_ij$ and zero across machines and on the diagonal. Relaxing $a_{ij}\in\{0,1\}$ to $a\ge 0$ with $\sum_ia_{ij}=1$ gives (QP). Raising the diagonal gives the convex program (CQP), with objective $Z_{CQP}(a)=\tfrac12c^Ta+\tfrac12a^T(D+\operatorname{diag}(c))a$. Adding the lower bound $c^Ta$ gives (CQP′):

$$\min Z\quad\text{s.t.}\quad \textstyle\sum_ia_{ij}=1,\ \ a\ge 0,\ \ Z\ge Z_{CQP}(a),\ \ Z\ge c^Ta .$$

Randomized rounding of a fractional $\bar a$ sends job $j$ to machine $i$ with probability $\bar a_{ij}$, the choices being pairwise independent across jobs, and then orders every machine by $\prec_i$.

Formalization targets

Goal: (CQP′) is a relaxation, and rounding loses at most 3/2

For every instance with $p>0$, $w\ge 0$:

$$\forall\sigma:\ (a^\sigma,\ \mathrm{val}(\sigma))\ \text{is feasible for (CQP′)},$$ $$\forall(\bar a,Z)\ \text{feasible for (CQP′)}:\quad \mathbb E\Bigl[\sum_jw_jC_j\Bigr]\le\tfrac32 Z .$$

The first part makes $Z^*_{CQP'}$ a lower bound on the optimum. The second is Lemma 2.8. Together they are Corollary 2.9 and the value guarantee of the $3/2$-approximation.

Milestones

In attack order:

• Lemma 2.2: $\mathbb E[C_j]=\sum_i(\Pr[j\mapsto i]p_{ij}+\sum_{k\prec_ij}\Pr[j,k\mapsto i]p_{ik})$ for any random assignment.
• Theorem 2.1: rounding a feasible $\bar a$ has expected value exactly $Z_{QP}(\bar a)$.
• Corollary 2.3: (IQP) and (QP) have the same optimum.
• The positive semidefiniteness of $D+\operatorname{diag}(c)$ and Lemma 2.4: $a\mapsto(1-\gamma)c^Ta+\tfrac12a^T(D+2\gamma\operatorname{diag}(c))a$ is convex for all instances iff $\gamma\ge\tfrac12$.
• The identity $Z_{QP}=Z_{CQP}+\tfrac12(c^Ta-a^T\operatorname{diag}(c)a)$ and Theorem 2.6 a), the factor $2$ for (CQP).
• Lemma 2.8, the integrality step of Theorem 2.10, and Corollary 2.11, the bound $(1+c^T\bar a/(2Z))Z$.

Significance

The result gives a $3/2$-approximation for $R\,|\,|\sum w_jC_j$ from a relaxation with only $mn$ variables, without time indexing, so its size does not depend on the processing times. The same convexification, adapted to time slots, yields the factor 2 with release dates (§3 of the paper). The equality of Theorem 2.1 makes the analysis exact: the loss of rounding is exactly the gap between $Z_{QP}$ and the convex objective. The relaxation also bounds the power of preemption (§4), and for identical machines it connects scheduling to Max-$k$-Cut (§6).

All these results are proved in the paper; none is known to be formalized. A formal development adds:

• a checked model of Smith-sequenced assignment schedules;
• the expectation calculus for pairwise independent rounding;
• the positive-semidefiniteness argument of Lemma 2.4;
• a precise statement of what the $3/2$ guarantee says when complexity is set aside.

Difficulty

Two steps resist the obvious approach.

Positive semidefiniteness. $D$ alone is indefinite: two jobs with unit data give the block $\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$. Positive semidefiniteness of $D+\operatorname{diag}(c)$ holds only because the jobs on each machine are ordered by Smith's ratio. A generic matrix argument that ignores this ordering fails, and the "only if" half of Lemma 2.4 needs a specific family of instances.

Exact expectations under pairwise independence. Theorem 2.1 is an equality that uses only the one- and two-job marginals. A proof that silently assumes full independence of the choices proves a different statement. A proof that drops the product condition on pairs is false: with correlated choices the expected value differs from $Z_{QP}$.

Formalization scope

Jobs and machines are Fin n and Fin m; vectors in $\mathbb R^{mn}$ are functions on Fin m × Fin n and $D$ is a Matrix over that type. The order $\prec_i$ is cross-multiplied ($w_jp_{ik}>w_kp_{ij}$, or equality and $j<k$), which equals the page's ratio definition because $p>0$.

Standing assumptions of p. 2 are hypotheses of every theorem: $p_{ij}>0$ and $w_j\ge0$. Hypotheses added relative to the page:

• Corollary 2.11 assumes $Z>0$, which its fraction presupposes;
• the integrality step of Theorem 2.10 assumes integral $p$ and $w$, as the page's proof does.

Optimum. The scheduling optimum $Z^*$ is the minimum of $\mathrm{val}$ over assignments, by Smith's rule (p. 7, cited by the paper, not reproved). "Within a factor $\alpha$ of the optimum" is stated as a bound against the value of every assignment, so no optimum is presupposed.

Rounding. Randomized rounding is any nonnegative weight $\mu$ of total mass 1 on assignments, with $\Pr_\mu[j\mapsto i]=\bar a_{ij}$ and $\Pr_\mu[j\mapsto i,\,k\mapsto h]=\bar a_{ij}\bar a_{hk}$ for $j\ne k$. The product weight satisfies this.

Not formalized. Polynomial running time, solvability of (CQP′) within additive error $\varepsilon$ (ellipsoid method), and derandomization by conditional probabilities. Theorem 2.10 is formalized as the existence of an outcome in the support of the rounding with the $3/2$ guarantee.

Trivializing formalization ruled out. A bound $\mathbb E\le\tfrac32Z$ for an arbitrary number $Z$ says nothing about schedules. The goal therefore also states that every schedule is feasible for (CQP′) at its own value, so $Z$ is a genuine lower bound on the optimum.

Contributions welcome. A complete development needs:

• linearity of expectation over a finite weight on assignments;
• the computation of Lemma 2.2;
• a positive-semidefiniteness criterion via principal minors or a direct sum-of-squares decomposition of $a^T(D+\operatorname{diag}(c))a$;
• convexity of quadratic forms with PSD matrices.

The rounding calculus and the PSD lemma are reusable for §§3–4 of the same paper. Alternative proofs of Lemma 2.4 are welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22(3), 1997. https://doi.org/10.1287/moor.22.3.513
• A. S. Schulz, M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM Journal on Discrete Mathematics 15(4), 2002. https://doi.org/10.1137/S0895480199357078
• N. Bansal, A. Srinivasan, O. Svensson, Lift-and-round to improve weighted completion time on unrelated machines, STOC 2016. https://doi.org/10.1145/2897518.2897572

Motivation

Minimizing a submodular set function is one of the central tractable problems of combinatorial optimization. Minimum cuts in graphs and hypergraphs, matroid intersection and partition, the rank of a matroid union, and many problems in facility location, image segmentation and machine learning are special cases or subroutines of it. The question is algorithmic: given only a value oracle for $f$, find a set $U$ with $f(U) = \min_W f(W)$ using a number of operations bounded by a polynomial in $|V|$ alone, independent of the size of the values of $f$ (strongly polynomial).

Timeline.

• 1981. Grötschel, Lovász and Schrijver showed with the ellipsoid method that submodular functions can be minimized in strongly polynomial time (Combinatorica 1, 1981). The method is not combinatorial.
• 1985. Cunningham gave a combinatorial pseudo-polynomial algorithm for submodular function minimization (Combinatorica 5, 1985).
• 1999–2000. Two combinatorial strongly polynomial algorithms appeared independently: Iwata, Fleischer and Fujishige (J. ACM 48, 2001), and Schrijver, the paper of this mission (J. Combin. Theory Ser. B 80, 2000).

Schrijver's algorithm is the one usually taught. Its proof uses only the greedy vectors of $f$, a reachability digraph and a lexicographic potential.

Setting

Let $V = \{1,\dots,n\}$ and let $f$ be a real function on all subsets of $V$ that is submodular:

$$f(Y) + f(Z) \ge f(Y\cap Z) + f(Y\cup Z) \qquad (Y, Z \subseteq V),$$

normalized so that $f(\emptyset)=0$. For $x \in \mathbb R^V$ and $U \subseteq V$ write $x(U) = \sum_{v\in U} x(v)$. The base polytope is $B_f = \{x \in \mathbb R^V : x(U) \le f(U)\ \forall U,\ x(V) = f(V)\}$.

For a total order $\prec$ on $V$ let $v_\prec = \{u : u \prec v\}$. The greedy vector of $\prec$ is $h^\prec(v) = f(v_\prec\cup\{v\}) - f(v_\prec)$. A lower ideal of $\prec$ is a set closed under taking $\prec$-smaller elements. The interval $(s,t]_\prec$ is $\{v : s \prec v \preceq t\}$. For $s \prec u$, the order $\prec^{s,u}$ is obtained from $\prec$ by moving $u$ to the position just before $s$. The vector $\chi^u$ is the incidence vector of $u$.

The algorithm keeps a point $x = \lambda_1 h^{\prec_1} + \dots + \lambda_k h^{\prec_k}$ with $\lambda_i > 0$ and $\sum_i \lambda_i = 1$; initially $x = h^\prec$ for an arbitrary order. It forms the digraph $D = (V, A)$, where $A = \{(u,v) : u \prec_i v \text{ for some } i\}$, and the sets $P = \{x > 0\}$ and $N = \{x < 0\}$.

• Case 1: $D$ has no path from $P$ to $N$. The algorithm returns the set $U$ of vertices that can reach $N$.
• Case 2: there is such a path. Let $d(v)$ be the distance from $P$ to $v$ in $D$. The algorithm picks $t \in N$ maximizing $(d(t), t)$, then the largest $s$ with $(s,t)\in A$ and $d(s) = d(t)-1$, then an order $\prec_1$ maximizing $|(s,t]_{\prec_1}|$.
  • It finds $\delta \ge 0$ with $h^{\prec_1} + \delta(\chi^t - \chi^s)$ a convex combination of the $h^{\prec_1^{s,u}}$, $u \in (s,t]_{\prec_1}$.
  • It moves $x$ toward $y = x + \lambda_1\delta(\chi^t-\chi^s)$ as far as $x(t) \le 0$ allows.
  • It reduces the new convex decomposition to at most $|V|$ terms, dropping $\prec_1$ if $x'(t) < 0$.

Formalization targets

Goal: correctness, well-definedness and the iteration bound

For every submodular $f$ with $f(\emptyset)=0$:

$$\text{(i) in Case 1, } f(U) \le f(W)\ \forall W \subseteq V;\quad \text{(ii) every Case 2 state has a successor};\quad \text{(iii) every run has } m \le |V|^6 \text{ iterations}.$$

Part (iii) is the opening claim of §5 (p. 352), and part (i) is display (16) (p. 351). Part (ii) states that the description of §4 can always be carried out, and it keeps (iii) from holding vacuously.

Milestones

In order: the diminishing-returns inequality (9); $h^\prec(U) = f(U)$ on lower ideals and $h^\prec \in B_f$ (§2); the comparison (8) of $h^{\prec^{s,u}}$ with $h^\prec$; the subroutine (12); the Case 1 certificate (16); existence of a Case 2 iteration (§4, p. 352); the location (22) of new arcs; monotonicity (20) of distances; and the lexicographic decrease (21) of $(d(t), t, s, \alpha, \beta)$ while $d$ stays fixed.

Significance

The result. The theorem gives a submodular minimizer after a number of iterations bounded by a polynomial in $|V|$. Each iteration makes polynomially many oracle calls and arithmetic operations, so the algorithm is strongly polynomial. The same exchange-and-potential scheme underlies later improvements (Fleischer–Iwata's push-relabel variant, Iwata–Orlin, Orlin's $O(n^5)$ bound). Section 6 of the paper, the companion mission, transfers the result to submodular functions on ring families.

Formalizing it. The result is proved and has been in textbooks for twenty years. It has no machine-checked proof that we know of, in Lean or elsewhere, and Mathlib has no submodular minimization. A complete development yields a verified correctness and termination proof for a nontrivial combinatorial algorithm on the base polytope. It also yields reusable facts about greedy vectors and lower ideals, and a worked example of a lexicographic-potential termination argument.

Difficulty

Correctness (16) is short once $h^\prec(U) = f(U)$ on lower ideals is available. The difficulty is termination. A single iteration can increase $x$ at $t$ and decrease it at $s$, and it adds new orders and so new arcs. Neither $|N|$ nor $x(N)$ need improve monotonically, and the obvious potentials fail. The argument needs the precise structure of the new arcs (22): every new arc lies inside the interval $[s,t]$ of $\prec_1$, and that gives both the monotonicity of distances (20) and the strict lexicographic decrease (21). The choice rule for $t$ and $s$ ("largest") is what makes (21) hold. An arbitrary choice can cycle. Well-definedness also takes work: it combines (12) with a Carathéodory reduction over the hyperplane $x(V) = f(V)$.

Formalization scope

• Ground set and values. $V$ is Fin n and subsets are Finset (Fin n). Values are real; the paper allows any ordered field. "Largest" in the choice of $t$ and $s$ is the order of Fin n.
• Orders and states. A total order is a permutation $\sigma$ read as a position map: $u \prec v$ iff $\sigma(u) < \sigma(v)$. The order $\prec^{s,u}$ is characterized relationally (IsMoved). A state is a list of (order, weight) pairs.
• Distances. Distances take values in $\mathbb N \cup \{\infty\}$, with $\infty$ for unreachable vertices.
• Standing assumptions. Submodularity (the platform definition NonmonotoneSubmod.Shared.Submodular) and $f(\emptyset) = 0$ are the paper's standing assumptions of §2 and §4. Milestones that do not need $f(\emptyset)=0$ omit it.
• Iterations as a relation. An iteration is a relation Step that admits every choice the paper leaves open: any subroutine output $\delta$, any maximizing index, and any Carathéodory reduction. The reduced decomposition may only use orders $\prec_i$ ($i \ne 1$), each $\prec_1^{s,u}$ at most once, and $\prec_1$ only when $x'(t) = 0$.
• Not formalized. The value oracle, "strongly polynomial time" and the number of oracle calls are not formalized, because there is no machine model. Only the iteration count is.
• No trivial reading. A Step relation that is never satisfiable would make the bound vacuous. Part (ii) of the goal rules this out, and the goal does not mention $d$, $\alpha$, $\beta$ or the matrix of §3.
• Contributions welcome. Proofs of the milestones, general lemmas on greedy vectors and lower ideals (reusable for any base-polytope development), and a Carathéodory lemma for convex combinations in an affine hyperplane.

Selected references

• A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000) 346–355. https://doi.org/10.1006/jctb.2000.1989
• S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001) 761–777. https://doi.org/10.1145/502090.502096
• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• W. H. Cunningham, On submodular function minimization, Combinatorica 5 (1985) 185–192. https://doi.org/10.1007/BF02579361
• J. B. Orlin, A faster strongly polynomial time algorithm for submodular function minimization, Math. Program. 118 (2009) 237–251. https://doi.org/10.1007/s10107-007-0189-2

Motivation

The scheduling problem $R\,|\,r_j\,|\sum C_j$ asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.

The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).

Timeline.

• 1991: Papadimitriou and Yannakakis define MaxSNP and L-reductions, and show that MAX3SAT with a bounded number of occurrences per variable is MaxSNP-complete.
• 1998: Hoogeveen, Schuurman and Woeginger prove that $R\,|\,|\sum w_jC_j$ and $R\,|\,r_j\,|\sum C_j$ are MaxSNP-hard, by a reduction from a MaxSNP-hard variant of 3-dimensional matching.
• 2001: Skutella (§7, pp. 32–33) gives a shorter reduction from 3-OCCURRENCE MAX3SAT, the variant of MAX3SAT in which every variable occurs at most three times (MaxSNP-hard, see Ausiello et al. 1999, Corollary 8.15).

Setting

An instance $I$ of 3-OCCURRENCE MAX3SAT has $n$ variables and $m$ clauses. Each clause is a set of one to three literals (a variable $x$ or its negation $\neg x$), and each variable occurs at most three times in total. A truth assignment $t$ gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. $\#(t)$ denotes the number of satisfied clauses, and $\mathrm{OPT}_{\mathrm{SAT}}(I)=\max_t \#(t)$.

The scheduling instance $R(I)$ has $n+m$ jobs and $2n$ machines.

• Every variable $x$ has a true machine and a false machine, and one v-job. The v-job is released at time $0$, has processing time $4$ on the two machines of $x$, and cannot run anywhere else.
• Every clause $c$ has one c-job, released at time $3$, with processing time $0$. It may run on the false machine of $x$ when $x$ occurs in $c$, on the true machine of $x$ when $\neg x$ occurs in $c$, and nowhere else.

A schedule $S$ gives every job $j$ a machine and a start time $S_j\ge r_j$, with no two jobs on one machine overlapping. Its value is the total completion time $\mathrm{VAL}(S)=\sum_j (S_j+p_j)$. The truth assignment $\mathrm{SAT}(S)$ sets $x$ true exactly when the v-job of $x$ runs on the true machine. $\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ is the minimum of $\mathrm{VAL}$ over feasible schedules.

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

$R(I)$ has an optimal schedule $S_0$, and

$$\mathrm{VAL}(S_0)=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I),\qquad \mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{VAL}(S_0)$$

for every feasible schedule $S$. These are the two conditions of an L-reduction, with constants $\alpha=32$ and $\beta=1$.

Milestones

1. Lemma 7.1 a) (p. 32): $\#(\mathrm{SAT}(S))\ge 4n+4m-\mathrm{VAL}(S)$ for every feasible $S$.
2. Lemma 7.1 b) (p. 33): $\mathrm{OPT}_{\mathrm{SCH}}(R(I))=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)$.
3. The two counting facts of the proof of Theorem 7.2: $\mathrm{OPT}_{\mathrm{SAT}}(I)\ge m/2$ and $n\le 3m$.
4. The first L-reduction condition: $\mathrm{OPT}_{\mathrm{SCH}}(R(I))\le 12m+4m\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I)$.
5. The second L-reduction condition: $\mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{OPT}_{\mathrm{SCH}}(R(I))$.

Significance

The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that $R\,|\,r_j\,|\sum C_j$ is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift $k\mapsto 4n+4m-k$.

Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of $R(I)$ and optimal truth assignments of $I$, and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.

Difficulty

The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time $3$ without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by $4n+4m-\#(\mathrm{SAT}(S))$. The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.

Formalization scope

Variables and clauses are Fin n and Fin m; here $n$ and $m$ count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for $x$ and b = false for $\neg x$, and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and $\mathrm{VAL}$ is a real number; $\#$ and $\mathrm{OPT}_{\mathrm{SAT}}$ are natural numbers cast to the reals, so no natural-number subtraction occurs. $\mathrm{OPT}_{\mathrm{SCH}}$ is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.

Two conventions are fixed that the page leaves implicit:

• Every clause has between one and three literals. An empty clause would leave its c-job with no machine, so $R(I)$ would have no schedule, and "at least $m/2$" would fail.
• Every variable occurs at least once. The bound $n\le 3m$, and with it the constant $32$, needs this: a variable that occurs nowhere adds $4$ to $\mathrm{OPT}_{\mathrm{SCH}}$ and nothing to $\mathrm{OPT}_{\mathrm{SAT}}$.

Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy $S_j+p_j\le S_k$ or $S_k+p_k\le S_j$. Under this rule a c-job at time $3$ conflicts with a v-job running over $[0,4)$, but several c-jobs may share a start time. Reading jobs as half-open intervals $[S_j,S_j+p_j)$ would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.

Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of $R$ and $\mathrm{SAT}$; the weighted variant for $R\,|\,|\sum w_jC_j$ in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of $R(I)$ (v-jobs at time $0$, c-jobs at time $3$ or $4$), and on the existence of optimal schedules.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2), 206–242, 2001. https://doi.org/10.1145/375827.375840
• J. A. Hoogeveen, P. Schuurman, G. J. Woeginger, Non-approximability results for scheduling problems with minsum criteria, IPCO 1998, LNCS 1412, 353–366. https://doi.org/10.1007/3-540-69346-7_27
• C. H. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
• G. Ausiello, P. Crescenzi, G. Gambosi, V. Kann, A. Marchetti-Spaccamela, M. Protasi, Complexity and Approximation, Springer, 1999. https://doi.org/10.1007/978-3-642-58412-1
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306

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

$$p(x) = \frac{e^{F(x)}}{e^{F(x)}+e^{-F(x)}}.$$

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

$$E\,l(F+f) = E\Big[2y^*\big(F(x)+f(x)\big) - \log\big(1+e^{2(F(x)+f(x))}\big)\Big],$$

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

$$z = \frac{y^*-p(x)}{p(x)(1-p(x))},\qquad w(x) = p(x)(1-p(x)),$$

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$,

$$s(x) = 2E\big(y^*-p(x)\mid x\big),\qquad H(x) = -4E\big(p(x)(1-p(x))\mid x\big),$$

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

$$F(x) + \tfrac12E_w(z\mid x) = F(x) - H(x)^{-1}s(x).$$

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