Probability

Motivation

Many optimization problems in simulation-based design, reinforcement learning and machine learning can be evaluated but not differentiated. Their objective is an expectation $f(x) = \mathbb E[F(x,\xi)]$ that can only be sampled through noisy function values $F(x,\xi)$. Gradients may be unavailable because the model is a black box, a simulator, or a legacy code. Methods for this setting are called zeroth-order or derivative-free stochastic methods. The objective $f$ is often nonconvex, so the realistic target is an approximately stationary point, $\|\nabla f(x)\|^2 \le \epsilon$, not a global minimizer.

Ghadimi and Lan (arXiv:1309.5549; SIAM J. Optim. 23(4), 2013) gave the first complexity bounds for stochastic zeroth-order methods on nonconvex problems. Their randomized stochastic gradient free (RSGF) method combines two ingredients. The first is the Gaussian smoothing and random finite-difference estimator of Nesterov and Spokoiny (Found. Comput. Math. 17, 2017; preprint 2011). The second is a randomized stopping rule that outputs an iterate chosen at random along the trajectory. The resulting bound has become the standard reference point for derivative-free nonconvex stochastic optimization.

Timeline:

• 1952: Kiefer and Wolfowitz introduce finite-difference stochastic approximation.
• 2011: Nesterov and Spokoiny analyze Gaussian random gradient-free oracles for convex and deterministic nonconvex problems.
• 2013: Ghadimi and Lan prove the nonconvex stochastic rate of the RSGF method (Theorem 3.2) and its $O(n/\epsilon^2)$ complexity (Corollary 3.3).

Setting

Let $\mathbb R^n$ be Euclidean space and let $\xi$ be a random vector with distribution $P$ on a measurable space $\Xi$. The problem is

$$f^* := \inf_{x\in\mathbb R^n}\Big\{ f(x) := \int_\Xi F(x,\xi)\,dP(\xi) \Big\}. \tag{3.1}$$

The sample functions $F(\cdot,\xi)$ lie in $\mathcal C^{1,1}_L(\mathbb R^n)$ almost surely: they are differentiable, and their gradients are $L$-Lipschitz. Two assumptions describe the noise. Assumption A1 concerns the first-order oracle $G(x,\xi) = \nabla_x F(x,\xi)$: it is unbiased, $\mathbb E[G(x,\xi)] = \nabla f(x)$, and has variance at most $\sigma^2$. Assumption A3 says the zeroth-order oracle is unbiased, $\mathbb E[F(x,\xi)] = f(x)$.

For a smoothing parameter $\mu > 0$ and an $n$-dimensional standard Gaussian vector $u$, the Gaussian smoothing of $f$ is $f_\mu(x) = \mathbb E_u[f(x+\mu u)]$ (3.3). The RSGF method starts from $x_1$ and uses stepsizes $\gamma_k$. At step $k$ it draws a fresh sample $\xi_k$ and a fresh Gaussian direction $u_k$, forms the zeroth-order estimator

$$G_\mu(x_k,\xi_k,u_k) = \frac{F(x_k+\mu u_k,\xi_k) - F(x_k,\xi_k)}{\mu}\,u_k, \tag{3.12}$$

and sets $x_{k+1} = x_k - \gamma_k G_\mu(x_k,\xi_k,u_k)$ (3.13). The output is $x_R$, where the random iteration count $R \in \{1,\dots,N\}$ has the probability mass function

$$P_R(k) = \frac{\gamma_k - 2L(n+4)\gamma_k^2}{\sum_{j=1}^N[\gamma_j - 2L(n+4)\gamma_j^2]}. \tag{3.15}$$

In the Lean development, $f$ is objective P F, $G_\mu$ is szoGrad (the published RandomGradFree.Shared.oracle applied to $F(\cdot,\xi)$), and $f_\mu$ is the published RandomGradFree.Shared.smoothing. The smoothing parameter is μs, because μ names the probability measure.

Formalization targets

Goal: Theorem 3.2 a)

Let $0 < \gamma_k < 1/[2(n+4)L]$ for $k = 1,\dots,N$, with $N \ge 1$, and let $D_f^2 = 2(f(x_1)-f^*)/L$. Then

$$\frac1L\,\mathbb E\|\nabla f(x_R)\|^2 \le \frac{D_f^2 + 2\mu^2(n+4)\big(1 + L(n+4)^2\sum_{k=1}^N(\frac{\gamma_k}{4} + L\gamma_k^2)\big) + 2(n+4)\sigma^2\sum_{k=1}^N\gamma_k^2}{\sum_{k=1}^N[\gamma_k - 2L(n+4)\gamma_k^2]}. \tag{3.16}$$

The stepsizes are left free, so every stepsize policy specializes the goal.

Companions

• Theorem 3.2 b), (3.17): for convex $f$ with a minimizer $x^*$, the bound on $\mathbb E[f(x_R) - f^*]$.
• Corollary 3.3, (3.26): for the constant stepsizes (3.24) and $\mu \le D_f/((n+4)\sqrt{2N})$,

$$\frac1L\,\mathbb E\|\nabla f(x_R)\|^2 \le \frac{12(n+4)LD_f^2}{N} + \frac{4\sigma\sqrt{n+4}}{\sqrt N}\Big(\tilde D + \frac{D_f^2}{\tilde D}\Big).$$

Milestones

The milestones follow the paper's proof.

• Properties of the smoothing. These are Theorem 3.1 a)–c): $f_\mu$ has an $L$-Lipschitz gradient given by (3.4), $|f_\mu - f| \le \frac{\mu^2}{2}Ln$ (3.5), the gradient bound (3.6), and the second-moment bound (3.7). Three of these are already on the platform and are referenced. Two consequences follow, (3.9) and (3.11).
• Unbiasedness, (3.14): the estimator $G_\mu$ is unbiased for $\nabla f_\mu$.
• The proof chain of Theorem 3.2. The pathwise descent inequality (3.19), the martingale identity (3.20) and the conditional second-moment bound (3.21) combine into the weighted bound (3.23). The $R$-weighting identity converts (3.23) into (3.16).

Significance

The theorem shows that function values alone suffice to find approximately stationary points of nonconvex stochastic programs. The price is a factor of the dimension $n$: with constant stepsizes the RSGF method needs $O(n/\epsilon^2)$ iterations, against $O(1/\epsilon^2)$ for the first-order RSG method. The randomized output rule and the analysis through $f_\mu$ are reused in later zeroth-order methods, including two-phase variants, mirror-descent variants and variance-reduced schemes.

The result is proved in the paper. It is not formalized anywhere known to this mission. The platform already holds parts of the Gaussian-smoothing theory from the Nesterov–Spokoiny series, but only for convex problems with exact function values. This mission adds:

• the nonconvex form of the second-moment bound (3.7);
• the gradient-approximation bound (3.6);
• the stochastic sampling model with conditional expectations;
• the first machine-checkable statement of a nonconvex stochastic zeroth-order rate.

Difficulty

The first idea is to treat the RSGF method as the first-order RSG method run on $f_\mu$ with the unbiased estimator $G_\mu$, and to quote the RSG bound. This fails, because the variance $\mathbb E\|G_\mu - \nabla f_\mu\|^2$ has no uniform bound: by (3.7) it grows with $\|\nabla f(x_k)\|^2$ at the random iterate. The analysis has to carry that term along and absorb it into the left side, which is where the weights $\gamma_k - 2L(n+4)\gamma_k^2$ come from. It must also move between $\nabla f_\mu$ and $\nabla f$ through (3.6) at a cost polynomial in $n$.

On the formal side, three obstacles stand out.

• The Gaussian moment estimates behind (3.6) and (3.7) need bounds on $\mathbb E\|u\|^p$ up to $p = 6$ for a standard Gaussian vector.
• Conditional expectations with respect to $\sigma(\zeta_{[k-1]})$ are taken at random iterates that depend on the past, so independence of the fresh samples must be used carefully.
• Integrability must be established for every quantity before expectations can be manipulated.

Formalization scope

• Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The constants $(n+3)$, $(n+4)$, $(n+6)$ use the same natural number $n$. The Gaussian is Mathlib's stdGaussian.
• Iterates. They are indexed from $1$, and $R$ takes values in $\{1,\dots,N\}$.
• Optimal values. $f^*$ is the infimum of $f$ (IsGLB), with $f$ bounded below. The paper's $f^*_\mu := \min f_\mu$ (3.10) is read as an infimum, since the minimum need not be attained.
• Smoothness. $F(\cdot,\xi) \in \mathcal C^{1,1}_L$ is required for $P$-almost every $\xi$, as on the page.
• Assumption A1 is stated at every point $x$ for $G = \nabla_x F$.
• Assumption A3 is the definition of $f$, with $F(x,\cdot)$ integrable.

The following are explicit additions; the paper leaves them implicit.

• Sampling. The samples $\xi_k \sim P$ and $u_k \sim \mathcal N(0,I_n)$ are measurable and mutually independent, and $R$ is independent of all of them.
• Measurability and integrability. $F$ is jointly measurable, and $\nabla_x F(x,\cdot)$ is integrable.
• Stepsizes are positive.
• Corollary 3.3 assumes $\sigma > 0$.

Every conclusion about an expectation also asserts the integrability of its integrand. A non-integrable function has Lean integral $0$, so a bound without this conjunct could hold for the wrong reason.

The goal is stated about the objects of the method only: $F$, $P$, $f$, the run (3.12)–(3.13), $R$ and the constants. It does not mention $f_\mu$, $\Delta_k$ or the filtration, so it cannot be discharged by choosing an auxiliary object.

A complete development needs:

• Gaussian moment bounds and differentiation under the Gaussian integral;
• conditional expectation with respect to the natural filtration of an independent sequence;
• the descent lemma for $\mathcal C^{1,1}_L$ functions.

The Gaussian-smoothing lemmas (3.6), (3.7) and (3.9) are reusable by any zeroth-order mission. Contributions of proofs of individual milestones are welcome, as are alternative proofs of (3.7) without Nesterov's bound.

Selected references

• S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4):2341–2368, 2013. Preprint arXiv:1309.5549v1, the version cited here. https://arxiv.org/abs/1309.5549
• Y. Nesterov and V. Spokoiny, Random gradient-free minimization of convex functions, Found. Comput. Math. 17:527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23(3):462–466, 1952. https://doi.org/10.1214/aoms/1177729392

Learning parities under differential privacy

Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) requires a randomized algorithm's output distribution to change little when one individual's record is changed. PAC learning asks an algorithm to output, from i.i.d. labeled examples, a hypothesis whose error is small with high probability. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith (arXiv:0803.0924v3; SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090) asked which concept classes can be learned under both requirements at once. All theorem, page and display numbers in this mission are those of the arXiv v3.

Their generic learner (§3, the subject of mission I of this series) learns every finite class privately with a polynomial number of examples, but its running time is exponential in the representation size for classes such as parity. Parity functions are the standard example of a class that is learnable efficiently by linear algebra and not learnable with statistical queries (Kearns, 1998; Blum et al., 1994), a model that was then the main known source of efficient private learners (Blum, Dwork, McSherry and Nissim, 2005). Section 4 of the paper gives an efficient private PAC learner for parity. The result separates efficient private learning from statistical-query learning, and the local (randomized-response) model from the centralized one (missions III–V).

Setting

For $d \ge 1$ and $r \in \{0,1\}^d$, the parity function $c_r(x) = r \odot x$ is the inner product of $r$ and $x$ modulo 2; PARITY is $\{c_r : r \in \{0,1\}^d\}$. A database is $z = (z_1,\dots,z_n)$ with $z_i = (x_i, y_i) \in \{0,1\}^d \times \{0,1\}$. Two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$, identified with the law $A(z)$ of its output, is $\varepsilon$-differentially private if $\Pr[A(z) \in S] \le e^{\varepsilon}\Pr[A(z') \in S]$ for all neighbors $z, z'$ and all sets $S$ of outputs. $\mathrm{Lap}(s)$ is the Laplace distribution with density $\frac{1}{2s}e^{-|x|/s}$.

For $S \subseteq [n]$, $V_S \subseteq \mathbb Z_2^d$ is the solution space of the linear system $\{x_i \odot r = y_i : i \in S\}$. The basic learner $\mathcal A(z,\varepsilon)$ outputs $\bot$ with probability $1/2$; otherwise it puts each $i \in [n]$ into $S$ independently with probability $p = \varepsilon/4$ and outputs $c_{r^*}$ for $r^*$ uniform in $V_S$, or $\bot$ if $V_S = \emptyset$.

The amplified learner $\mathcal A^*(z,\varepsilon,\alpha,\beta)$ sets $\beta' = \beta/2$, $\alpha' = \alpha/5$, $k = \lceil\log_{4/3}(1/\beta')\rceil$, $n' = \lceil cd/(\varepsilon\alpha')\rceil$, $s = \lceil (c'k/(\alpha'\varepsilon))\log_2(k/\beta')\rceil$ for constants $c, c'$. If $n \le kn' + s$ it returns "insufficient samples". Otherwise it runs $\mathcal A$ on $k$ disjoint blocks of $n'$ examples, obtaining $h_1,\dots,h_k$. It perturbs each training error on the next $s$ examples by independent $\mathrm{Lap}(k/(s\varepsilon))$ noise and outputs the $h_j$ with the least perturbed error.

For a distribution $\mathcal X$ on $\{0,1\}^d$ and a target $c_r$, the error of $c_{r'}$ is $\mathrm{err}(c_{r'}) = \Pr_{x\sim\mathcal X}[c_{r'}(x) \ne c_r(x)]$, and probabilities of the learner's success are over $x_1,\dots,x_n \sim \mathcal X$ i.i.d., $z_i = (x_i, c_r(x_i))$, and the learner's coins.

Formalization targets

Goal: Theorem 4.4

There are constants $c, c', C > 0$ such that for all $d \ge 1$, $0 < \varepsilon \le 1/2$, $\alpha, \beta \in (0,1/2)$: $\mathcal A^*(\cdot,\varepsilon,\alpha,\beta)$ is $\varepsilon$-differentially private on databases of every size, and

$$n \ge C\,\frac{(d + \log_2(1/\beta))\log_2(1/\beta)}{\varepsilon\alpha} \implies \Pr\big[\mathcal A^* \text{ outputs } h^* \text{ with } \mathrm{err}(h^*) \le \alpha\big] \ge 1-\beta$$

for every distribution $\mathcal X$ and every target $c_r$. When $\log_2(1/\beta) \le d$ the bound is the paper's $O(d\log(1/\beta)/(\varepsilon\alpha))$. The constants are fixed before all other parameters. The goal is literally the conjunction of Lemma 4.5 and Lemma 4.6.

Milestones

$$\text{Thm 2.3 (Laplace mechanism)},\quad \text{Claim 2.2 (composition)},\quad \text{Thm A.1 (Chernoff)},\quad \text{Occam's razor for } |H| = 2^d,$$ $$\text{Lemma 4.1: } n \ge \tfrac{8}{\varepsilon\alpha}(d\ln 2 + \ln 4) \Rightarrow \Pr[\mathcal A(z,\varepsilon) = h,\ \mathrm{err}(h)\le\alpha] \ge \tfrac14,$$ $$|V_T| \le 2|V_{T\cup\{i\}}| \text{ if } V_{T\cup\{i\}} \ne \emptyset,\quad \text{Claim 4.3},\quad \text{Lemma 4.2 (}\mathcal A\text{ private)},\quad \text{Lemma 4.5 (}\mathcal A^*\text{ private)},\quad \text{Lemma 4.6 (}\mathcal A^*\text{ learns)}.$$

Significance

The theorem shows that the restriction to private algorithms does not separate efficient learnability from statistical-query learnability: parity is efficiently and privately PAC learnable, yet not SQ learnable. Its sample complexity exceeds the non-private $O((d + \ln(1/\beta))/\alpha)$ by a factor $O(\ln(1/\beta)/\varepsilon)$ (remark, p. 18). The private amplification step (private model selection with Laplace-perturbed test errors) is a general technique that converts any private learner with constant success probability into a private PAC learner.

The result is proved in the paper; none of it is machine-checked as far as we know. The mission produces a formal library of the basic privacy calculus (Laplace mechanism, composition and post-processing), the $\mathbb Z_2$ solution-space estimate behind the privacy of $\mathcal A$, and the analysis of both learners. Formalizing it also repairs the paper's statement: the printed sample bound fails when $\log(1/\beta)$ is large compared with $d$ (see the scope section), and the base of the logarithm defining $k$ is misprinted.

Difficulty

The obvious private learner, "solve the linear system on all examples and output a random solution", is not private. One changed example can make the system inconsistent and turn every hypothesis output into failure, so the output law on neighboring databases differs by an unbounded factor. Two devices restore privacy: subsampling each example with probability $\varepsilon/4$, and failing with probability $1/2$ unconditionally. The privacy proof then needs a quantitative fact about $\mathbb Z_2$: adding one consistent equation at most halves the solution space. The proof must also handle databases labeled by no parity at all, where solution spaces are empty.

Utility has its own difficulty. The amplified learner selects among candidates through noisy test errors, so three failure events (no good candidate, unrepresentative test set, large Laplace noise) must be bounded together. The sizes $k$, $n'$, $s$ must also be shown to fit inside the claimed sample bound.

Formalization scope

• Bits are ZMod 2; $\{0,1\}^d$ is Fin d → ZMod 2; $c_r(x)$ is dotProduct r x. Databases are Fin n → (Fin d → ZMod 2) × ZMod 2, with 0-based indices.
• An algorithm is the law of its output. $\mathcal A$'s output is Option (Fin d → ZMod 2) (none = $\bot$). $\mathcal A^*$'s output is "insufficient samples", $\bot$, or a hypothesis $c_r$. Every set of outputs is measurable, and differential privacy is required for all measurable sets.
• The distribution $\mathcal X$ is a PMF on the finite set $\{0,1\}^d$. The probability over the examples is a finite sum weighted by $\prod_i \mathcal X(x_i)$, and $\bot$ has error 1.
• Corrections and explicit hypotheses. (1) $k = \lceil\log_{4/3}(1/\beta')\rceil$: the printed base $3/4$ gives $k \le 0$, and the proof needs $(3/4)^k \le \beta'$. (2) Sizes are ceilings; $\log$ is base 2 and $\ln$ is natural, as on p. 8. (3) Privacy is stated for $0 < \varepsilon \le 1/2$: the proof of Lemma 4.2 uses $\varepsilon \le 1/2$, and its step $2p/(1-p) + 1 \le \varepsilon + 1$ fails beyond that. Utility statements need only $0 < \varepsilon \le 4$, so that $p = \varepsilon/4$ is a probability. (4) The printed bound $O(d\log(1/\beta)/(\varepsilon\alpha))$ is false when $\log(1/\beta) \gg d$, because $\mathcal A^*$ refuses unless $n > kn' + s$ and $s$ grows like $\log^2(1/\beta)/(\varepsilon\alpha)$. Utility is therefore stated with the bound $C(d + \log_2(1/\beta))\log_2(1/\beta)/(\varepsilon\alpha)$, the order of $kn' + s$, which equals the printed order whenever $\log_2(1/\beta) \le d$. The privacy conjunct does not depend on the sample bound. (5) A $\bot$ candidate does not take part in the argmin, and ties go to the least index. (6) Lemma 4.1 assumes $\alpha \le 1/2$, which its proof uses. (7) Claim 4.3 is stated in product form (no division). (8) Theorem 2.3 takes any positive bound $\Delta$ on the global sensitivity.
• "Efficiently" (polynomial running time) is not modelled.
• Ruling out trivial readings. The constants $c, c', C$ are existentially quantified once, outside every other quantifier. A constant chosen after $d$, $\varepsilon$, $\alpha$, $\beta$ would make the utility claim trivial. Success requires an actual hypothesis output, so "insufficient samples" and $\bot$ are failures. Privacy quantifies over all databases, not only consistently labeled ones.
• Reused results: ComputationalLearning.chernoff_bounds (Theorem A.1) and ComputationalLearning.occam_cardinality (Occam's razor), both proved on the platform.
• Contributions welcome: proofs of the privacy calculus (Theorem 2.3, Claim 2.2) for general use, the $\mathbb Z_2$ halving lemma, and the utility analysis. The first two are reusable well beyond this mission.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. DOI 10.1007/11681878_14
• A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical Privacy: The SuLQ Framework, PODS 2005. DOI 10.1145/1065167.1065184
• M. Kearns, Efficient Noise-Tolerant Learning from Statistical Queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351
• A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly Learning DNF and Characterizing Statistical Query Learning Using Fourier Analysis, STOC 1994. DOI 10.1145/195058.195147
• M. Kearns, U. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994. DOI 10.7551/mitpress/3897.001.0001

Motivation

Draw $n$ independent fair bits $X$, compute a one-bit summary $f(X)$, and send the bits through independent binary symmetric channels with crossover probability $\varepsilon$, producing $Y$. Which summary tells the receiver the most about $Y$? Kumar and Courtade conjectured that a single coordinate, $f(X)=X_1$, is optimal: $I(f(X);Y)\le 1-h_2(\varepsilon)$ bits for every Boolean $f$, in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.

This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1970–1976 — Hypercontractivity on the cube (Bonami, Ann. Inst. Fourier 1970; Gross, Amer. J. Math. 1975; Beckner, Annals 1975); Mrs. Gerber's lemma (Wyner–Ziv, IEEE TIT 1973).
• 2013–2014 — Kumar and Courtade pose the conjecture and prove a coordinatewise sum bound.
• 2016 — High-noise results: Ordentlich, Shayevitz and Weinstein for balanced functions (ISIT 2016); Samorodnitsky for all Boolean functions in a dimension-independent high-noise range (IEEE TIT 2016).
• 2018 — Pichler, Piantanida and Matz prove coordinate optimality when the observation is also reduced to one bit (Ann. Appl. Probab. 2018).
• 2020–2023 — Barnes–Özgür's symmetrized reformulation (ISIT 2020); Li–Médard on fixed-mean optimizers (IEEE TIT 2021); Yu's $\Phi$-stability (PTRF 2023).
• 2025–2026 — Chen, Gohari and Nair's differential (entropy-production) approach; independent preprints announcing proofs by Chen, Gohari, Javanmard, Lin, Mirrokni, Nair and Woodruff (arXiv:2609.24931), Ky and Tran (arXiv:2609.24184), Mahdavifar and Beirami (arXiv:2609.26444), and a bias-retaining finite-noise bound by Kramer and Saglam.
• September 2026 — The OpenAI preprint (Theorems 1.1 and 1.3, Corollary 1.2, pp. 1–4).

Setting

Let $\Omega_n=\{-1,1\}^n$ with uniform measure; information is in nats unless stated. For $r\in[-1,1]$ put

$$L=\log2,\quad H(r)=-\tfrac{1+r}2\log\tfrac{1+r}2-\tfrac{1-r}2\log\tfrac{1-r}2,\quad \psi(r)=L-H(r),$$

with $0\log0=0$; $\psi^{-1}$ is the increasing branch $[0,L]\to[0,1]$. A soft channel is $u:\Omega_n\to[-1,1]$, the conditional mean of an auxiliary sign $U$ given $X$; its information is $I(u)=H(\mathbb Eu)-\mathbb EH(u)=I(U;X)$. For $\rho\in[-1,1]$ let $Y_i=X_iZ_i$ with independent signs $\mathbb EZ_i=\rho$, and let $T_\rho u(y)=\mathbb E[u(X)\mid Y=y]$, so $I(T_\rho u)=I(U;Y)$. For an interior field $g:\Omega_n\to(-1,1)$ with $m=\mathbb Eg$, the production is $D(g)=\mathbb E[\operatorname{atanh}(g)\,Ng]$ with $Ng=\frac12\sum_i(g-g\circ\mathrm{flip}_i)$; the rate $F$ is defined by $F(\psi(r))=r\operatorname{atanh}r$; $S(I)=F(I)-2I$ (zero for $I<0$); $B_m(I)=2I+(1-m^2)S\bigl(L-\frac{H(m)-I}{1-m^2}\bigr)$.

Formalization targets

Milestone: Courtade–Kumar inequality in bits (Corollary 1.2, p. 2)

For $n\ge1$, $0\le\varepsilon\le\frac12$ and every Boolean $f$ on $\{0,1\}^n$,

$$I_2(f(X);Y)\le 1-h_2(\varepsilon),$$

with equality for every coordinate $x\mapsto x_i$ and its complement.

Goal: the soft contraction package (Theorem 1.1, p. 1; Corollary 1.2, p. 2; Theorem 1.3, p. 4)

The goal OAI.SoftChannel204.fullMain is the conjunction of:

1. Theorem 1.1. For all $n$, $u:\Omega_n\to[-1,1]$, $\rho\in[-1,1]$:

$$I(T_\rho u)\le\psi\bigl(|\rho|\,\psi^{-1}(I(u))\bigr),$$

with equality for every soft coordinate $u(x)=a x_i$, $|a|\le1$; and $I(U;Y)=I(T_\rho u)$ for the joint law of $(U,Y)$. 2. Corollary 1.2. For Boolean $f$ with $m=\mathbb Ef$ and $r_m=\psi^{-1}(H(m))$: $I(f(X);Y)\le\psi(|\rho|r_m)\le\psi(|\rho|)$, strictly below $\psi(|\rho|)$ when $0<|m|<1$ and $0<|\rho|$; coordinates and their negations attain $\psi(|\rho|)$; and the bits conversion $\psi(1-2\varepsilon)/L=1-h_2(\varepsilon)$. 3. Theorem 1.3. For every interior $g$: $D(g)\ge\max\{B_m(I(g)),F(I(g))\}\ge F(I(g))$.

Significance

The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.

Formalizing it. All objects are finite sums over $\{-1,1\}^n$, so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about $F$ and $S$ (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.

Difficulty

The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile $\Phi_m(I)=F(I)$ fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean $m$ as well. The preprint uses the maximum of two profiles, $B_m$ and $F$; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound $D(g)\ge2I(g)$ from the log-Sobolev inequality does not suffice; the nonlinear surplus above $2I$ is where the difficulty lies.

Formalization scope

• Cube n = Fin n → Bool, averages are finite sums divided by $2^n$, logs are natural; sign maps Bool to $\pm1$.
• psiInv is Function.invFunOn psi (Icc 0 1); since $\psi$ is strictly increasing on $[0,1]$ and $I(u)\in[0,L]$, this is the paper's branch.
• noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of $(1\pm\rho)/2$, which is $T_\rho$. Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is $0$.
• F is stated as psiInv s * artanh (psiInv s) and is only used on $[0,L)$; for interior $g$, $|m|<1$ and $0\le I(g)<H(m)\le L$, so reserve and hybrid are evaluated in their source domain.
• All results hold for every $n\ge0$; the attainment statements quantify over i : Fin n. The milestone (separate definition file) uses the crossover form with bits.

Selected references

• OpenAI, Sharp binary-information contraction on the discrete cube, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf
• T. A. Courtade, G. R. Kumar, Which Boolean functions maximize mutual information on noisy inputs?, IEEE Trans. Inf. Theory 60 (2014). https://doi.org/10.1109/TIT.2014.2326877
• G. R. Kumar, T. A. Courtade, Which Boolean functions are most informative?, ISIT 2013. https://doi.org/10.1109/ISIT.2013.6620221
• A. Samorodnitsky, On the entropy of a noisy function, IEEE Trans. Inf. Theory (2016). https://doi.org/10.1109/TIT.2016.2584625
• O. Ordentlich, O. Shayevitz, O. Weinstein, An improved upper bound for the most informative Boolean function conjecture, ISIT 2016. https://doi.org/10.1109/ISIT.2016.7541349
• G. Pichler, P. Piantanida, G. Matz, Dictator functions maximize mutual information, Ann. Appl. Probab. (2018). https://doi.org/10.1214/18-AAP1384
• L. Yu, On the $\Phi$-stability and related conjectures, Probab. Theory Relat. Fields (2023). https://doi.org/10.1007/s00440-023-01209-5
• A. Gohari, C. Nair, Outer bounds for multiuser settings: the auxiliary receiver approach, IEEE Trans. Inf. Theory (2022). https://doi.org/10.1109/TIT.2021.3128136
• Z. Chen, A. Gohari, A. Javanmard, et al., A proof of the most informative Boolean function conjecture, arXiv:2609.24931 (2026). https://arxiv.org/abs/2609.24931
• V. K. Ky, T. Tran, Dictators are most informative, arXiv:2609.24184 (2026). https://arxiv.org/abs/2609.24184
• H. Mahdavifar, A. Beirami, The most informative bit and beyond, arXiv:2609.26444 (2026). https://arxiv.org/abs/2609.26444
• S. G. Bobkov, P. Tetali, Modified logarithmic Sobolev inequalities in discrete settings, J. Theoret. Probab. (2006). https://doi.org/10.1007/s10959-006-0016-3

Motivation

Many learning tasks run on data about people: medical records, purchase histories, survey answers. A learner whose output reveals too much about any one training example is unusable on such data, however accurate it is. Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) makes "reveals too much" precise: changing one individual's record may change the probability of any outcome of the algorithm by at most a factor $e^{\varepsilon}$.

Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith asked which concept classes can be learned under this constraint, and at what cost in examples. This mission formalizes their first answer (§3 of the paper): every finite concept class can be learned privately in the agnostic model, with a sample size that grows only logarithmically in the size of the class. The result is the private counterpart of the cardinality version of Occam's razor (Kearns and Vazirani, An Introduction to Computational Learning Theory, 1994, p. 35). The paper appeared in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; all indices below are those of arXiv:0803.0924v3.

The learner is an instance of the exponential mechanism of McSherry and Talwar (FOCS 2007), which selects an output with probability exponentially weighted by a quality score.

Setting

A database of size $n$ over a domain $D$ is a vector $z=(z_1,\dots,z_n)\in D^n$. Databases $z,z'$ are neighbors if they differ in exactly one entry. A randomized algorithm $A$ is described by the law $A(z)$ of its output on each input. It is $\varepsilon$-differentially private (Definition 2.1) if

$$\Pr[A(z)\in S]\le e^{\varepsilon}\Pr[A(z')\in S]$$

for all neighbors $z,z'$ and all measurable sets $S$ of outputs.

Learning uses a finite set $X$ of examples and labels $\{0,1\}$. A hypothesis is a map $h:X\to\{0,1\}$, and $H$ is a finite nonempty class of hypotheses; in the theorem $H=C_d$, the concept class itself. Data are drawn i.i.d. from an arbitrary probability distribution $P$ on $X\times\{0,1\}$ (the agnostic setting, Definition 2.5). The error of $h$ is $\mathrm{err}(h)=\Pr_{(x,y)\sim P}[h(x)\neq y]$, and $\mathrm{OPT}=\min_{f\in H}\mathrm{err}(f)$. On a database $z=((x_i,y_i))_{i\le n}$ the score is $q(z,h)=-|\{i:y_i\neq h(x_i)\}|$ and the training error is $\mathrm{err}_T(h)=-q(z,h)/n$.

The exponential mechanism $\mathcal A^{\varepsilon}_q$ outputs $h\in H$ with probability proportional to $\exp(\varepsilon q(z,h)/2)$. In Lean these objects are IsDP, err, OPT, score, errT and expMech in the namespace PrivLearn.Generic.

Formalization targets

Goal: Theorem 3.4 (generic private learner)

There is an absolute constant $C>0$ such that for every finite $X$, every finite nonempty $H$, every $\varepsilon>0$ and all $\alpha,\beta\in(0,1/2)$:

1. $\mathcal A^{\varepsilon}_q$ is $\varepsilon$-differentially private on databases of every size;
2. for every distribution $P$ on $X\times\{0,1\}$ and every

$$n\ \ge\ C\Big(\ln|H|+\ln\tfrac1\beta\Big)\max\Big\{\tfrac1{\varepsilon\alpha},\tfrac1{\alpha^2}\Big\},$$

the mechanism run on $n$ i.i.d. samples from $P$ satisfies

$$\Pr\big[\mathrm{err}(\mathcal A^{\varepsilon}_q(z))>\mathrm{OPT}+\alpha\big]\le\beta .$$

The constant is left unspecified, as the paper's $O(\cdot)$ leaves it. The qualitative first sentence of Theorem 3.4 (classes of size $\exp(\mathrm{poly}(d))$ are privately agnostically learnable) follows at once, because then $\ln|H|$ is polynomial in $d$.

Milestones

• Lemma 3.3: $\mathcal A^{\varepsilon}_q$ is $\varepsilon$-differentially private.
• Theorem A.2: for i.i.d. $X_i\in[a,b]$ with mean $\mu$, $\Pr[|\frac1n\sum_iX_i-\mu|\ge\delta]\le2\exp(-2\delta^2n/(b-a)^2)$.
• Uniform convergence (proof of Theorem 3.4, p. 11): $\Pr[\exists h\in H:\ |\mathrm{err}(h)-\mathrm{err}_T(h)|\ge\rho]\le2|H|e^{-2n\rho^2}$.
• Exponential weights (proof of Theorem 3.4, p. 12): if $|\mathrm{err}(h)-\mathrm{err}_T(h)|<\rho$ for all $h\in H$, then $\mathcal A^{\varepsilon}_q(z)$ outputs some $h$ with $\mathrm{err}_T(h)\ge\mathrm{OPT}+2\rho$ with probability at most $|H|e^{-\varepsilon n\rho/2}$.
• Corollary 3.6: the same guarantee with $\ln|H|$ replaced by $\mathrm{VCDIM}(C_d)\cdot\ln|X|$.

Significance

Theorem 3.4 shows that privacy costs little in sample complexity when computation is unconstrained. Any class that some learner with polynomially long output can learn is learnable privately from polynomially many examples. The non-private agnostic bound is $O((\log|C_d|+\log(1/\beta))/\alpha^2)$; the private one is larger by a factor $O(\alpha/\varepsilon)$ when $\alpha>\varepsilon$, and is the same otherwise (Remark, p. 12). The theorem is the baseline the rest of the paper refines: an efficient private learner for parity (§4) and the equivalence of local privacy with statistical query learning (§5). It also underlies later work on the sample complexity of private learning, such as Beimel, Kasiviswanathan and Nissim (TCC 2010).

The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a checked statement of the exponential mechanism's privacy and of its learning guarantee with an explicit dependence on $|H|$, $\varepsilon$, $\alpha$ and $\beta$. It also provides a reusable bounded i.i.d. Hoeffding inequality (Theorem A.2) in the form learning theory uses. Formalizing the proof with any explicit constant is welcome. The constant $6$ printed at the end of the proof does not, by itself, make the last inequality close (the two error terms add to more than $\beta$), so a correct constant is a genuine contribution.

Difficulty

Privacy and accuracy pull in opposite directions. Empirical risk minimization, the obvious learner, is not private: replacing one example can change which hypothesis minimizes the training error, and the output then changes with probability one. Smoothing the choice must not destroy accuracy, and the accuracy argument must hold simultaneously for every hypothesis in the class, with the mechanism's randomness and the sample's randomness combined into one failure probability. In Lean the measure-theoretic bookkeeping is non-trivial: the output is a measure on a function space, the failure probability integrates the mechanism's law against the product measure $P^n$, and the privacy bound must hold for every measurable event, not only for single hypotheses.

Formalization scope

• Databases are vectors Fin n → X × Bool, indexed from $0$; neighbors differ in exactly one coordinate.
• Algorithms are output laws: $\mathcal A^{\varepsilon}_q(z)$ is the measure $\sum_{h\in H}p_z(h)\,\delta_h$ on X → Bool with the product σ-algebra. It is a probability measure because $H$ is nonempty and all weights are positive; the theorems assume $H$ nonempty, and the definition does not build normalization in.
• Privacy is required on every measurable set of outputs and for every database size $n$, with no assumption on how the data arise.
• The example domain is a finite type with the discrete σ-algebra (the paper's $X_d$ has representations of size at most $d$). The goal quantifies it over Type so that the absolute constant can precede it.
• Labels are Bool, standing for $\{0,1\}$. Logarithms are natural (Real.log), as in the paper's $\ln$.
• Parameters are $\varepsilon>0$ and $\alpha,\beta\in(0,1/2)$ as in Definitions 2.4 and 3.1. The failure event is the strict $\mathrm{err}(h)>\mathrm{OPT}+\alpha$, as on p. 11, and OPT is the minimum over $H=C_d$.
• $O(\cdot)$ is formalized as one absolute constant $C>0$ quantified before the domain, the class, the distribution and all parameters. A constant chosen after them would make the statement trivially true.
• Theorem A.2 assumes measurable, mutually independent, pairwise identically distributed variables with values in $[a,b]$ at every point. It makes no assumption $n\ge1$ or $a<b$; in those cases the right side is $2$ by Lean's division conventions.
• Corollary 3.6 uses the platform's VC dimension ComputationalLearning.vcDim (Kearns–Vazirani's Definition 9, the same notion as the paper's Definition 3.5) and references the platform's proved Sauer lemma.

Contributions welcome: proofs of any milestone, a measurable-structure library for finite output laws, and a general exponential-mechanism privacy theorem from which Lemma 3.3 follows.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. DOI 10.1007/11681878_14
• F. McSherry, K. Talwar, Mechanism Design via Differential Privacy, FOCS 2007. DOI 10.1109/FOCS.2007.66
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. DOI 10.1080/01621459.1963.10500830
• M. Kearns, U. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994. DOI 10.7551/mitpress/3897.001.0001
• A. Beimel, S. P. Kasiviswanathan, K. Nissim, Bounds on the Sample Complexity for Private Learning and Private Data Release, TCC 2010. DOI 10.1007/978-3-642-11799-2_26

Motivation

Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.

This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.

Setting

A consumer who buys at price $p$ learns a valuation $V$, drawn independently from a law $\nu$ with finite mean $\mu = EV$, and then either keeps the product or returns it for the refund $r$. Keeping is optimal when $V \ge r$. Write

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r),$$

for the probabilities of keeping and returning. A consumer's expected utility from buying is $E\max(V,r)$, which is therefore the reservation price: all consumers buy if $p \le E\max(V,r)$ and none buys otherwise (the demand rule (6)). Market demand $X \ge 0$ has distribution function $F$ and $\bar F = 1 - F$; a stock $q \ge 0$ sells $E\min(X,q)$ in expectation when consumers buy, and nothing when they do not. Write $S(p,q,r)$ for these expected sales. The production cost is $c$, leftover and returned units are salvaged at $s$, and $0 \le s < c < \mu$.

The total supply chain profit is

$$\Pi_T(p,q,r) = [(p-s)\bar G(r) + (p-r)G(r)]\,S(p,q,r) - (c-s)q. \tag{15}$$

A manufacturer sells to a retailer, who sets $p$, $q$ and (except in Proposition 4) $r$. The contracts are:

• standard buy-back $(w,b)$: wholesale price $w$, credit $b$ per leftover unit; the retailer earns (14);
• differentiated buy-back $(w,b,l)$: credit $b$ per unsold unit and $b-l$ per returned unit; the retailer earns

$$\Pi_R(p,q,r) = [(p-b)\bar G(r) + (p-r-l)G(r)]\,S(p,q,r) - (w-b)q; \tag{31}$$

• direct-to-manufacturer returns with a buy-back $(w,b)$: consumers return to the manufacturer, who sets $r$; the profits are (19) and (21);
• sales rebate $(w,u)$: a rebate $u$ per unit sold, returned or not; the retailer earns (25).

The supply chain optimum, from Proposition 2 of the paper, is

$$p^{SC} = E\max(V,s), \qquad \bar F(q^{SC}) = \frac{c-s}{E\max(V,s)-s}, \qquad r^{SC} = s.$$

Formalization targets

Goal: Proposition 3 (p. 16)

For $\phi \in [0,1]$ and $\bar\phi = 1-\phi$, the differentiated buy-back

$$w = \phi c + \bar\phi\,E\max(V,s), \qquad b = \phi s + \bar\phi\,E\max(V,s), \qquad b - l = s$$

makes the supply chain optimum a retailer optimum and gives the retailer the share $\phi$:

$$\Pi_R(p,q,r) \le \Pi_R(p^{SC},q^{SC},r^{SC}) \ \ \forall p, r,\ q \ge 0, \qquad \Pi_R(p^{SC},q^{SC},r^{SC}) = \phi\,\Pi_T(p^{SC},q^{SC},r^{SC}),$$

and the contract is implementable: $w \ge b$, $l \ge 0$, $b - l \ge s$.

Milestones

1. Under a standard buy-back the retailer's optimal refund is $r^* = b$ (Sec. 5.1, p. 15).
2. Under (31) the retailer's optimum is $p^* = E\max(V,b-l)$, $\bar F(q^*) = (w-b)/(E\max(V,b-l)-b)$, $r^* = b-l$ (proof of Proposition 3, p. 27).
3. Under (16)–(18), $w - b = \phi(c-s)$ and $E\max(V,b-l) - b = \phi[E\max(V,s)-s]$ ((32)–(33)).
4. At $(E\max(V,s), q, s)$ the retailer earns $\phi\,\Pi_T$ ((34)–(39)).
5. Retailer plus manufacturer profit under direct returns is $\Pi_T$ (Sec. 5.3, p. 17).
6. Proposition 4: with direct-to-manufacturer returns and the buy-back (22)–(23), the chain optimum is a Nash equilibrium between retailer and manufacturer, with retailer share $\phi$.
7. Proposition 5: the sales rebate $u = \frac{E\max(V,s)-s}{c-s}(w-c)$ makes the chain optimum a retailer optimum.
8. With a rebate paid on kept units only, the retailer's optimal refund is $r^* = s - u < s$ (Sec. 5.4, p. 19).

Significance

The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases ($\phi = 0$, atoms in the valuation law) that the paper does not discuss.

Difficulty

Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in $p$ and $r$, and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at $V = r$ matter. The second is a newsvendor problem in $q$ for an arbitrary demand law: the paper writes the optimal stock as $\bar F^{-1}$ of a fractile, which presumes a continuous, strictly increasing $F$, whereas here $F$ may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is $\phi\,\Pi_T$, so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to $\Pi_T$. In Proposition 4 the manufacturer's deviation to a refund below $s$ acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when $V \ge s$ almost surely, so that case needs its own argument.

Formalization scope

Prices, refunds, costs, quantities and profits are real numbers. The valuation law $\nu$ is a probability measure on $\mathbb R$ with integrable identity (a strict generalization of the paper's density $g$); $\bar G(r) = \nu([r,\infty))$ and $G(r) = \nu((-\infty,r))$, matching the rule "keep iff $V \ge r$". The demand law $D$ is a probability measure on $\mathbb R$ with $D((-\infty,0)) = 0$, and $E\min(X,q)$ is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in $p$. Optimization is over all real $p$ and $r$ and all $q \ge 0$, nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes $\Pi_T$ is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of $D$ is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis $w \ge s$, implied by the paper's range $w \ge c$ (p. 19) and necessary: for $w < s$ the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as $\phi\,\Pi_T$, or in which the optimization is restricted to $r = s$, would make the goal trivial and is excluded: (31) is stated with free $w$, $b$, $l$, and the contract enters only through hypotheses.

The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 ; published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities (the buy-back contract), Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166

Motivation

Financial institutions, insurers and engineers who manage the risk of a decision describe it by a statistic of the loss distribution that the decision induces. The value-at-risk (VaR) at confidence level $\beta$, the $\beta$-quantile of the loss, became an industry and regulatory standard in the 1990s, but it is not subadditive and behaves erratically as a function of the decision when the loss distribution has atoms, as it always does in scenario-based models. The conditional value-at-risk (CVaR), roughly the average of the losses beyond VaR, was proposed as a replacement that is coherent in the sense of Artzner, Delbaen, Eber and Heath and that can be optimized.

In an earlier paper (Rockafellar and Uryasev, 2000) the same authors showed, for loss distributions with continuous distribution functions, that CVaR is the minimum value of an explicit convex function of one real variable, and that VaR is a minimizer. That formula turned CVaR minimization over a portfolio into a linear program and is the reason CVaR is used in practice. The paper formalized here (Rockafellar and Uryasev, Research Report #2001-5, 2001, published in J. Banking & Finance 2002) defines CVaR for general loss distributions, discrete ones included, and proves that the minimization formula survives.

Timeline.

• 1997–1999: Artzner, Delbaen, Eber and Heath introduce coherent risk measures; VaR fails subadditivity.
• 2000: Rockafellar and Uryasev prove the minimization formula for continuous loss distributions.
• 2001–2002: the present paper, Theorem 10: the formula holds for every integrable loss once CVaR is defined as the mean of the $\beta$-tail distribution. Acerbi and Tasche (2002) give an equivalent "expected shortfall" formulation.

Setting

A decision $x$ lies in a set $X\subseteq\mathbb R^n$; an uncertain outcome $y\in\mathbb R^m$ has a Borel probability law $P$ that does not depend on $x$. The loss is $z=f(x,y)$, where $f$ is continuous in $x$ on $X$, measurable in $y$, and $E\{|f(x,y)|\}<\infty$ for each $x\in X$. A confidence level $\beta\in(0,1)$ is fixed.

• The distribution function of the loss is $\Psi(x,\alpha)=P\{y\mid f(x,y)\le\alpha\}$, with left limit $\Psi(x,\alpha^-)=P\{y\mid f(x,y)<\alpha\}$.
• The $\beta$-VaR is $\alpha_\beta(x)=\min\{\alpha\mid\Psi(x,\alpha)\ge\beta\}$ and the upper $\beta$-VaR is $\alpha^+_\beta(x)=\inf\{\alpha\mid\Psi(x,\alpha)>\beta\}$.
• The $\beta$-tail distribution is the probability measure on $\mathbb R$ with distribution function

$$\Psi_\beta(x,\alpha)=\begin{cases}0,&\alpha<\alpha_\beta(x),\\ \dfrac{\Psi(x,\alpha)-\beta}{1-\beta},&\alpha\ge\alpha_\beta(x).\end{cases}$$

• The $\beta$-CVaR $\phi_\beta(x)$ is the mean of the $\beta$-tail distribution.
• The upper $\beta$-CVaR is $\phi^+_\beta(x)=E\{f(x,y)\mid f(x,y)>\alpha_\beta(x)\}$, defined when $\Psi(x,\alpha_\beta(x))<1$, and $\lambda_\beta(x)=[\Psi(x,\alpha_\beta(x))-\beta]/[1-\beta]$.
• Finally

$$F_\beta(x,\alpha)=\alpha+\frac{1}{1-\beta}\,E\big\{[f(x,y)-\alpha]^+\big\},\qquad[t]^+=\max\{0,t\}.$$

When $\Psi(x,\cdot)$ jumps across $\beta$ at $\alpha_\beta(x)$, the tail distribution keeps only the part $\lambda_\beta(x)$ of that atom needed to give the tail total mass one: the atom is split.

Formalization targets

Goal: Theorem 10 (fundamental minimization formula)

For each $x\in X$: $F_\beta(x,\cdot)$ is finite and convex (hence continuous), and

$$\phi_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha),\qquad \operatorname{argmin}_\alpha F_\beta(x,\alpha)=[\alpha_\beta(x),\alpha^+_\beta(x)],$$

the minimum being attained and the argmin a nonempty closed bounded interval; in particular $\phi_\beta(x)=F_\beta(x,\alpha_\beta(x))$.

Milestones, in attack order

1. The note after Definition 3: $\Psi_\beta(x,\cdot)$ is a distribution function, so the $\beta$-tail distribution exists; its mean is finite.
2. Proposition 6: $\phi_\beta(x)=\lambda_\beta(x)\alpha_\beta(x)+[1-\lambda_\beta(x)]\phi^+_\beta(x)$ when $\Psi(x,\alpha_\beta(x))<1$, and $\phi_\beta(x)=\alpha_\beta(x)$ otherwise.
3. $F_\beta(x,\cdot)$ is finite and convex.
4. The one-sided derivatives (31): $\partial^+F_\beta/\partial\alpha=[\Psi(x,\alpha)-\beta]/(1-\beta)$ and $\partial^-F_\beta/\partial\alpha=[\Psi(x,\alpha^-)-\beta]/(1-\beta)$.
5. Bounded level sets, and $\operatorname{argmin}_\alpha F_\beta(x,\alpha)=\{\alpha\mid\Psi(x,\alpha^-)\le\beta\le\Psi(x,\alpha)\}$, a nonempty closed bounded interval.
6. The least element of that set is $\alpha_\beta(x)$ and the greatest is $\alpha^+_\beta(x)$.

A companion item states Corollary 7: $\phi_\beta(x)\ge\alpha_\beta(x)$, strictly when $\Psi(x,\alpha_\beta(x))<1$.

Significance

Theorem 10 is what makes CVaR computable and optimizable. Since $\phi_\beta(x)=\min_\alpha F_\beta(x,\alpha)$, minimizing CVaR over $x\in X$ is the joint minimization of $F_\beta(x,\alpha)$ over $(x,\alpha)$; with a finite scenario set and a loss linear in $x$, that is a linear program, and VaR comes out as a by-product. The convexity and sublinearity of CVaR in $x$ (Corollary 11), its coherence (Corollary 12) and the equivalence of CVaR-constrained and CVaR-penalized problems (Theorem 14) are all derived from it. The formula is the basis of CVaR portfolio optimization software and of a large literature on risk-averse stochastic programming.

The result has been proved since 2001 and is not open. To our knowledge it has no machine-checked proof with CVaR defined independently: the CVaR items already on Prove2Me take $\min_\alpha F_\beta$ as the definition of CVaR, which makes (28) true by definition. This mission produces a formal proof that the tail-mean definition, with its atom splitting, agrees with the minimization formula for every integrable loss, together with reusable facts about one-sided derivatives of $\alpha\mapsto E[f-\alpha]^+$ and the argmin of the Rockafellar–Uryasev function.

Difficulty

The minimization side is elementary convex analysis in one variable once the one-sided derivatives are known; computing them requires passing a limit under the expectation, with the jumps of $\Psi(x,\cdot)$ handled separately for right and left limits. The step that does not follow from that analysis is the identification of the minimum value with $\phi_\beta(x)$. When the loss has an atom at $\alpha_\beta(x)$ that straddles level $\beta$, neither $E\{f\mid f\ge\alpha_\beta(x)\}$ nor $E\{f\mid f>\alpha_\beta(x)\}$ equals the minimum value; only the mean of the distribution with the split atom does. The obvious approach, proving the formula for continuous laws and passing to a limit, does not deliver the identity at the level of the defined objects; the identity has to be proved directly from the definition of the tail distribution, through Proposition 6.

Formalization scope

• The outcome space is $\mathbb R^m$ (Fin m → ℝ) with its Borel σ-algebra and a probability measure P. The paper's support set $Y\subseteq\mathbb R^m$ is not modelled: a law on $Y$ is a law on $\mathbb R^m$ concentrated on $Y$, and no statement uses $Y$.
• Probabilities are real numbers (P.real). $\Psi(x,\alpha^-)$ is $P\{f(x,\cdot)<\alpha\}$, as the paper defines it in (2).
• $\alpha_\beta(x)$ is the published MultistageStochastic.valueAtRisk P (f x) β (a real infimum, referenced, not redefined); $\alpha^+_\beta(x)$ is a real infimum. Both are meaningful because $P$ is a probability measure and $0<\beta<1$, and those hypotheses are carried wherever they appear.
• The $\beta$-tail distribution is a probability measure on $\mathbb R$ whose distribution function is $\Psi_\beta(x,\cdot)$, chosen when one exists (it is then unique); $\phi_\beta(x)$ is its mean. Milestone 1 establishes existence and integrability.
• "Minimum" is attainment: $\phi_\beta(x)$ is the least element of the range of $F_\beta(x,\cdot)$. The argmin is the set of global minimizers. "Finite" is integrability of $[f(x,\cdot)-\alpha]^+$ for each $\alpha$.
• One-sided derivatives are derivatives within $[\alpha,\infty)$ and $(-\infty,\alpha]$. The display (31) as printed on p. 14 has $\alpha_\beta(x)$ in place of $\alpha$; the formalization follows the derivation on p. 15.
• The goal and Corollary 7 carry all standing assumptions of §2; milestones assume only what they use (integrability, measurability of the single loss $f(x,\cdot)$), which makes them stronger.

Defining CVaR as $\min_\alpha F_\beta(x,\alpha)$, or as the quantile average, or by formula (21), would make the goal or a milestone true by definition; CVaR is defined here as the mean of the $\beta$-tail distribution, and any such redefinition is ruled out.

A complete development needs: right-continuity and limits of distribution functions, dominated convergence for the difference quotients of $\alpha\mapsto E[f-\alpha]^+$, the uniqueness of a probability measure on $\mathbb R$ with given distribution function, and one-variable convex analysis linking one-sided derivatives to minimizers. The derivative and argmin lemmas are reusable for any Rockafellar–Uryasev-type objective. Proofs of any milestone, and Lean lemmas that bridge valueAtRisk (stated with ENNReal) and P.real, are welcome.

Selected references

• R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Research Report #2001-5, ISE Dept., University of Florida, April 2001; published in Journal of Banking & Finance 26 (2002) 1443–1471. https://doi.org/10.1016/S0378-4266(02)00271-6
• R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
• C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26 (2002) 1487–1503. https://doi.org/10.1016/S0378-4266(02)00283-2
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173