Probability

From conditional motion to a marginal probability path

Flow matching models a changing probability distribution using a time-dependent velocity field. A conditional model specifies a density and a velocity separately for each conditioning point. The mathematical question is whether those conditional descriptions determine a velocity for the mixture distribution. This mission concerns the continuity-equation formulation of Theorem 1 of Lipman, Chen, Ben-Hamu, Nickel, and Le, Flow Matching for Generative Modeling (ICLR 2023). The source is arXiv:2210.02747v2, Section 3.1 and Appendix A.

Densities, velocities, and probability flux

Fix a natural number $d$ and let $E=\mathbb R^d$. The conditioning distribution $Q$ is a Borel probability measure on $E$. At time $t$, position $x$, and conditioning point $z$, write $\rho(t,x,z)$ for the conditional density and $v(t,x,z)\in E$ for the conditional velocity. The variable $x$ is integrated against Lebesgue measure; $z$ is integrated against $Q$. These roles remain distinct even though both variables take values in the same space.

The conditional flux is $F(t,x,z)=\rho(t,x,z)v(t,x,z)$. The marginal density, marginal flux, and marginal velocity are defined by

$$p(t,x)=\int_E\rho(t,x,z)\,dQ(z),\qquad J(t,x)=\int_E F(t,x,z)\,dQ(z),\qquad u(t,x)=p(t,x)^{-1}J(t,x).$$

These definitions express equations (6) and (8) using a probability measure rather than a data-density function. This representation also allows discrete conditioning distributions. Every conditional density is strictly positive and normalized on $0\leq t\leq1$, jointly measurable in $(x,z)$, and integrable in $z$ at each fixed $(t,x)$.

The divergence of a differentiable vector field is the sum of the diagonal entries of its derivative. A density and velocity satisfy the classical continuity equation when their flux is spatially differentiable and the density has time derivative equal to minus that divergence.

Formalization targets

The goal asserts that $p(t,\cdot)$ is a positive probability density for every $t\in[0,1]$ and that

$$\partial_t p(t,x)+\operatorname{div}_x\bigl(p(t,x)u(t,x)\bigr)=0\qquad(0<t<1,\ x\in E).$$

The hypotheses require the conditional continuity equation for $Q$-almost every conditioning point, at each interior time and spatial point. They also specify a sufficient local domination package for differentiation under the integral. This is an explicit classical interpretation of the regularity qualification in the proof of Theorem 1.

Four supporting targets isolate the mathematical assertions used by this formulation: the probability-density property of equation (6); time differentiation under the conditioning integral; spatial divergence under the conditioning integral; and the velocity/flux identity corresponding to equation (8). The source contains these equations and operations rather than separately numbered supporting lemmas, so the milestone titles identify the relevant equation or proof passage.

What completing the formalization provides

The deliverable is a checked interface for passing from a measurable family of conditional continuity equations to the continuity equation of its mixture. It records which variables are differentiated, which measure is used for averaging, where positivity is needed, and which assumptions justify each analytic operation. The time and spatial differentiation lemmas are stated for general measures and integrands, making them reusable outside this particular probability model.

The mathematical result is already proved in the cited paper. The uploaded theorem items are open formalization targets, with explicit proof placeholders. Successful local compilation checks their types and imports; it does not establish their conclusions. The definition module contains no proof placeholders.

Analytic obligations

Pointwise differentiability of every conditional function does not by itself justify differentiating an integral over the conditioning variable. The regularity predicates therefore require a neighborhood independent of that variable, an integrable bound for the derivative norm throughout that neighborhood, and almost-everywhere measurability of the integrand and derivative. Time and space receive separate predicates because their derivatives take values in different spaces.

There is also a distinction between density normalization in $x$ and integrability in $z$ at a fixed position. The formal assumptions record both. A probability measure on the conditioning space does not make every measurable function integrable. These conditions prevent the totalized Bochner integral from silently supplying a default value where an intended integral fails to exist.

Formalization scope

Space is represented by Fin d → ℝ, with its standard finite-product Borel structure and Lebesgue measure. Its norm is the standard product norm used by mathlib. All finite dimensions, including dimension zero, are included. Time-dependent functions are defined on all real times, while density assumptions apply on the closed unit interval and derivative conclusions apply on its interior. No endpoint time derivative is asserted.

The regularity package is one sufficient realization of the source's Leibniz-rule assumption, not a claim to the weakest possible hypotheses. Conditional continuity equations may hold almost everywhere in the conditioning variable; their exceptional sets may depend on the fixed time and position. Spatial differentiability of the marginal flux is part of the conclusion, so the equation cannot be satisfied merely through the default value of an undefined derivative.

The target is the PDE formulation. It does not assert existence of a global ODE flow, uniqueness of transported measures, or equality with a flow pushforward. Those require a separate transport development. It also asserts no endpoint approximation to a data distribution and no theorem about optimization, neural networks, or Gaussian paths. No marginal continuity equation or differentiation–integration interchange is assumed as an input.

Required infrastructure consists of Bochner integration, finite-dimensional differentiation, finite sums of derivative coordinates, and product-measure integration. Contributions may prove the supporting targets or the goal directly while preserving their statements and the distinction between classical PDE and flow-transport claims.

Selected references

• Yaron Lipman, Ricky T. Q. Chen, Heli Ben-Hamu, Maximilian Nickel, and Matt Le. Flow Matching for Generative Modeling. ICLR 2023. arXiv:2210.02747v2, Section 2, Section 3.1, Theorem 1, equations (6), (8), and (26), and Appendix A's proof of Theorem 1.
• mathlib contributors. ParametricIntegral.lean, revision 0df444a360eaa60ab8c11dca51a86af692955474. Differentiation under the integral.

Motivation

The fundamental theorem of Mission IV says that a class of binary classifiers is PAC learnable exactly when its VC-dimension is finite. That leaves out classes one would like to learn, such as all polynomial classifiers over the line, whose VC-dimension is infinite although each degree separately is learnable. Chapter 7 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) relaxes the definition. In nonuniform learnability (Definition 7.1) the sample size may depend on the hypothesis the learner is competing with: the learner must, for every $h \in H$, eventually do as well as $h$ up to $\epsilon$, but how soon may depend on $h$. The chapter's main result (Theorem 7.2) characterizes the nonuniformly learnable classes of binary classifiers as the countable unions of agnostic PAC learnable classes. The learning rule behind it is Structural Risk Minimization (SRM): write $H = \bigcup_n H_n$, weight the pieces, and minimize the empirical risk plus a confidence term that grows with the index (Theorems 7.3–7.5). Applied to a countable class described by a prefix-free code, SRM becomes the Minimum Description Length rule and yields a quantitative form of Occam's razor (Lemma 7.6, Theorem 7.7). The chapter closes the circle with a No-Free-Lunch result for the relaxed notion (Remark 7.2, Exercise 7.5).

Setting

The framework is that of Missions I, II and IV: examples in a domain $Z$, a hypothesis type with a class $H$, a loss $\ell$, risk $L_D$ and empirical risk $L_S$, learners as functions of the sample, the uniform convergence property with an explicit rate $m^{UC}_H$, agnostic PAC learnability, and for binary classification the 0–1 loss, the VC-dimension and pointwise separability. The new module adds Definition 7.1 with an explicit rate $m^{NUL}$ and, as in Definition 3.4, learners whose outputs lie in $H$; the same notion for a family of learners indexed by the confidence $\delta$, since the SRM and MDL rules take $\delta$ as an input; the rate $\epsilon_n(m,\delta) = \inf\{\epsilon \in (0,1) : m^{UC}_{H_n}(\epsilon,\delta) \le m\}$ of Equation (7.1), which is meaningful only when that set is nonempty; the index $n(h) = \min\{n : h \in H_n\}$ of Equation (7.4); the SRM rule as a minimizer of $L_S(h) + \epsilon_{n(h)}(m, w(n(h))\delta)$ over the admissible hypotheses, those whose index has positive weight and a defined rate; prefix-free description languages $d : H \to \{0,1\}^*$ and the MDL rule; and shattering of an infinite set.

Formalization targets

Goal: Theorem 7.2

For a class $H$ of measurable binary classifiers over a domain with measurable singletons, every subclass of which is pointwise separable, $H$ is nonuniformly learnable if and only if there are classes $H_n$ with $\bigcup_n H_n = H$, each agnostic PAC learnable.

Milestones

Theorem 7.3. If $H = \bigcup_n H_n$ is nonempty and each $H_n$ has the uniform convergence property, then $H$ is nonuniformly learnable (general loss).

Theorem 7.4. For weights $w(n) \in [0,1]$ with partial sums at most $1$, uniformly convergent pieces $H_n$ with rates $m^{UC}_{H_n}$, $\delta \in (0,1)$, any $D$ and any $m$: with probability at least $1-\delta$, for every $n$ with $w(n) > 0$ at which $\epsilon_n(m, w(n)\delta)$ is defined and every $h \in H_n$, $|L_D(h) - L_S(h)| \le \epsilon_n(m, w(n)\delta)$.

Theorem 7.5. With $w(n) = 6/(\pi^2 n^2)$ and $H_0 = \emptyset$, every family of learners implementing the SRM rule satisfies the nonuniform guarantee with rate $m^{NUL}(\epsilon,\delta,h) = m^{UC}_{H_{n(h)}}(\epsilon/2,\ 6\delta/(\pi n(h))^2)$.

Lemma 7.6 (Kraft). For a prefix-free set $S$ of binary strings, every finite subfamily satisfies $\sum_{\sigma} 2^{-|\sigma|} \le 1$.

Theorem 7.7. For a prefix-free description language on a class with a $[0,1]$-valued loss, $m \ge 1$ and $\delta > 0$: with probability at least $1-\delta$, every $h \in H$ satisfies $L_D(h) \le L_S(h) + \sqrt{(|h| + \ln(2/\delta))/(2m)}$.

Further items: nonuniform learnability is implied by agnostic PAC learnability (§7.1); a nonuniformly learnable class of binary classifiers is a countable union of classes of finite VC-dimension (Exercise 7.5 (1)–(2)); a class shattering an infinite set admits no countable cover by classes of finite VC-dimension (Exercise 7.5 (3)) and is not nonuniformly learnable; over an infinite domain the class of all measurable classifiers is not nonuniformly learnable (Remark 7.2).

Significance

Theorem 7.2 is the second characterization theorem of the book's Part I and the one that explains why model selection works: any class that can be stratified into learnable pieces is learnable in the nonuniform sense, with the price of not knowing the index paid in sample size rather than in principle. SRM is the abstract form of every penalized learning rule, and the MDL bound of Theorem 7.7 is the cleanest instance, a bound in which the only property of the hypothesis that matters is the length of its description. Remark 7.2 shows the relaxation is not free: even nonuniformly, no learner handles all classifiers over an infinite domain.

Nothing here is machine-checked. The chapter's arguments are short but they combine everything before them: Hoeffding, the union bound with weights, the VC lower bound of Corollary 6.4 and the fundamental theorem. Three places where the book's statements need care are recorded in the formalization: the rate $\epsilon_n$ is an infimum that may be undefined for small $m$; the SRM rule takes $\delta$ as an input and so is a family of learners; and the fundamental theorem's uniform-convergence direction needs a measurability condition, which appears in Theorem 7.2 as hereditary pointwise separability.

Difficulty

The relaxation remark is a direct comparison of two definitions. Kraft's inequality is the coin-tossing argument of the book or an induction on the maximal length: it is the intended entry point. Theorem 7.4 is Theorem 7.3's engine: for each index and each $\epsilon$ in the set of Equation (7.1), the uniform convergence property bounds the failure by $w(n)\delta$; the passage from "every $\epsilon$ in the set" to the infimum uses continuity of the outer measure along an increasing union; the union over $n$ uses countable subadditivity and the partial-sum condition. Theorem 7.5 is Theorem 7.4 on the good event together with the two inequalities of the book's proof, using that the target is admissible when $m \ge m^{UC}_{H_{n(h)}}(\epsilon/2, w(n(h))\delta)$ and that admissibility of the SRM output gives the bound for it. Theorem 7.3 asks for a single learner: SRM with a confidence schedule $\delta_m \to 0$ chosen so that, for each fixed index, the rate at level $\delta_m$ eventually falls below any $\epsilon$, together with an approximate minimizer within $1/m$; the target hypothesis is admissible for $m$ large. Theorem 7.7 is Theorem 7.4 with singleton pieces and the weights $2^{-|h|}$, a one-sided Hoeffding bound for each $h$, and Kraft's inequality. Exercise 7.5 (3) is the combinatorial construction of the book's hint, disjoint finite subsets $K_n$ of the shattered set with $|K_n| > \mathrm{VCdim}(H_n)$ and a labeling that no $H_n$ realizes. The first half of Theorem 7.2 is Corollary 6.4 applied to the nonuniform learner at fixed $\epsilon_0, \delta_0$, with constants chosen so that the two probability bounds actually contradict; the second half is the fundamental theorem on each piece followed by Theorem 7.3.

Formalization scope

Learners output hypotheses in $H$, in Definition 7.1 as in Definition 3.4. The rate $\epsilon_n$ is an infimum over the set of Equation (7.1), and every statement that uses it is guarded by the nonemptiness of that set; the weight $w(n)$ may be $0$, and $H_0 = \emptyset$ encodes the book's indices $1, 2, \dots$. The SRM rule minimizes over admissible hypotheses, and an SRM family is one that returns an admissible minimizer whenever some hypothesis is admissible, which is the book's assumption that the argmin is attained (automatic for the 0–1 loss). Theorem 7.4's sum condition is on partial sums, and Kraft's inequality is on finite subfamilies, so no divergent series is silently zero. Theorem 7.7 assumes a $[0,1]$-valued loss and $m \ge 1$. The binary-classification results assume measurable singletons and measurable hypotheses; Theorem 7.2 also assumes every subclass pointwise separable, which every class over a countable domain satisfies. Definition 7.8 (consistency) and the Memorize algorithm of §7.4 are not stated.

Trivializing readings are excluded: outputs in $H$ keep the risk an honest integral, the rate is never a junk infimum of the empty set, and the failure events are bounded in outer measure. Welcome contributions: a reusable weighted union bound over a countable family of uniform-convergence events, the continuity argument for the infimum rate, and the shattered-set combinatorics of Exercise 7.5.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 7. doi:10.1017/CBO9781107298019
• V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. doi:10.1007/978-1-4757-2440-0
• J. Rissanen, Modeling by shortest data description, Automatica 14(5), 1978. doi:10.1016/0005-1098(78)90005-5
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
• L. G. Kraft, A device for quantizing, grouping, and coding amplitude modulated pulses, MSc thesis, MIT, 1949.

Motivation

Missions I and II of this series showed that finite hypothesis classes are learnable, with and without the realizability assumption, by empirical risk minimization. Chapter 5 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) asks the converse question: is prior knowledge, in the form of a restricted hypothesis class, really necessary? Could there be a universal learner, an algorithm that, given enough examples from any distribution, outputs a predictor of low risk? The No-Free-Lunch theorem (Theorem 5.1) answers no: for binary classification with the 0–1 loss over a domain $X$, for every learning algorithm and every training-set size $m$ smaller than $|X|/2$ there is a distribution on which the learner fails with probability at least $1/7$, even though that distribution is perfectly predictable by some function $f$, so that another learner (ERM over $\{f\}$) succeeds. The consequence for the framework is Corollary 5.2: over an infinite domain, the class of all functions is not PAC learnable. This is the first lower bound of the book and the reason the rest of it is about the complexity of hypothesis classes rather than about universal algorithms.

Setting

The framework is the UnderstandingML_Framework module of Mission I, cited as a reference. Binary classification over a domain $X$ uses examples in $X \times \{0,1\}$, hypotheses $h : X \to \{0,1\}$ and the 0–1 loss, so the risk of $h$ under a distribution $D$ over $X \times \{0,1\}$ is $L_D(h) = D(\{(x,y) : h(x) \ne y\})$, computed as the integral of the 0–1 loss. A learner is a function from samples of each size to hypotheses, and a sample of size $m$ has the law $D^m$. PAC learnability of a class $H$ (Definition 3.1) requires a sample-complexity function $m_H$ and a learner $A$ such that for every $\epsilon, \delta \in (0,1)$, every distribution $D$ over $X$ and every measurable labeling function $f$ realizable by $H$, samples of size $m \ge m_H(\epsilon,\delta)$ yield $L_{(D,f)}(A(S)) \le \epsilon$ with probability at least $1-\delta$.

Two conventions specific to this mission. The domain $X$ is assumed to have measurable singletons (the book's Remark 3.1 assumes away measurability issues); this makes the finitely supported distributions of the proof honest probability measures and makes every $L_D(h)$ under them a genuine integral. And "$m$ smaller than $|X|/2$" is written $2m < |X|$ in the extended natural numbers, so that an infinite domain satisfies it for every $m$.

Formalization targets

Goal: Theorem 5.1 (No-Free-Lunch)

Let $A$ be any learning algorithm for binary classification with respect to the 0–1 loss over a domain $X$ with measurable singletons, and let $m$ be a training-set size with $2m < |X|$. Then there exists a probability distribution $D$ over $X \times \{0,1\}$ such that

1. there is a measurable $f : X \to \{0,1\}$ with $L_D(f) = 0$;
2. there is a measurable set $E$ of samples of size $m$ with $D^m(E) \ge 1/7$ on which $L_D(A(S)) \ge 1/8$.

Milestones

Lemma B.1 (Appendix B). If $Z$ takes values in $[0,1]$ and $E[Z] = \mu$, then for every $a \in (0,1)$, $P[Z > 1-a] \ge (\mu - (1-a))/a$, and consequently $P[Z > a] \ge (\mu - a)/(1-a) \ge \mu - a$.

Equation (5.2). Under the hypotheses of Theorem 5.1 there are $D$ and a measurable $f$ with $L_D(f) = 0$ and $\mathbb{E}_{S \sim D^m}[L_D(A(S))] \ge 1/4$.

Corollary 5.2. For an infinite domain $X$ with measurable singletons, the class of all functions $X \to \{0,1\}$ is not PAC learnable.

Two further items: Exercise 5.1, the passage from an expectation of at least $1/4$ to a probability of at least $1/7$ of exceeding $1/8$ for a $[0,1]$-valued variable; and Exercise 5.3, the $k$-fold version of Equation (5.2), with bound $1/2 - 1/(2k)$ when $km \le |X|$, $k \ge 2$ and $X$ is nonempty.

Significance

The No-Free-Lunch theorem is the book's first impossibility result and the conceptual pivot of Part I: it shows that learnability is a property of the pair (hypothesis class, learner) and not of the learner alone, and it motivates the bias–complexity tradeoff of §5.2 and the VC-dimension of Chapter 6, whose lower bound (Theorem 6.7, the "only if" direction of the fundamental theorem) is proved by the same symmetrization argument. Corollary 5.2 is the statement that the class of all functions has infinite sample complexity, the negative half of the characterization of learnable classes.

Nothing here is machine-checked. The proof is combinatorial and elementary but has real content for a formalization: a finite subset $C$ of the domain, the $2^{2m}$ labelings of $C$, the uniform distribution on $C$ labeled by each of them, an exchange of a maximum, an average and a minimum over labelings and sample sequences, and a pairing argument on labelings that differ at exactly one unseen point. Lemma B.1 is a reverse Markov inequality for bounded variables that later chapters also use.

Difficulty

Lemma B.1 is Markov's inequality applied to $1 - Z$ and is the entry point; Exercise 5.1 is its instance with $a = 1/8$ and $\mu \ge 1/4$, giving $(1/4 - 1/8)/(7/8) = 1/7$, together with the inclusion of $\{\theta > 1/8\}$ in $\{\theta \ge 1/8\}$. Theorem 5.1 follows from Equation (5.2) and Exercise 5.1 once one knows that $S \mapsto L_D(A(S))$ is, under the finitely supported $D^m$, almost everywhere equal to a measurable function with values in $[0,1]$; the set $E$ is the intersection of the event with the finite support of $D^m$, which is measurable because singletons are. Equation (5.2) is the heart of the mission. One picks $C \subseteq X$ of size $2m$ (available because $2m < |X|$), lets $D_i$ be uniform on $C$ labeled by the $i$-th function $f_i : C \to \{0,1\}$ extended by $0$ off $C$, and computes $\mathbb{E}_{S \sim D_i^m}[L_{D_i}(A(S))]$ as an average over the $(2m)^m$ sequences of instances, which requires identifying $D_i^m$ as a finitely supported measure on sequences, that is, the product of finitely supported measures. The inequalities (5.4)–(5.6) exchange max, average and min and restrict to the unseen points, and the pairing argument shows that for each unseen point the average over $i$ of the indicator that $A$ errs on it is exactly $1/2$. Exercise 5.3 is the same argument with $|C| = km$, where at least $(k-1)m$ points are unseen. Corollary 5.2 takes $\epsilon < 1/8$, $\delta < 1/7$, $m = m_H(\epsilon,\delta)$ and a set $C$ of size $2m$ in the infinite domain, and derives the contradiction from Theorem 5.1 via the identification of $L_D$ for $D$ uniform on $C$ labeled by $f$ with the true error $L_{(D_X, f)}$ of Definition 3.1, where $D_X$ is uniform on $C$; the case $m = 0$ is handled separately with a single point.

Formalization scope

The items are stated in the joint-distribution form of the book's Chapter 5, with $D$ over $X \times \{0,1\}$ and $L_D$ the risk under the 0–1 loss, rather than in the $(D, f)$ form of Definition 3.1; Corollary 5.2 is the bridge and is stated with the framework's PACLearnable. Witness labeling functions are required to be measurable, because a non-measurable $f$ would make $L_D(f) = 0$ true by Lean's convention for non-integrable functions rather than by content. Clause (2) of Theorem 5.1 is stated in the inner form (a measurable set of probability at least $1/7$ inside the event) rather than as a lower bound on the outer measure of the event, which for a non-measurable event would be the weaker statement. The size condition uses ENat.card, so infinite domains satisfy it. Learners are deterministic functions of the sample; the book's argument goes through for randomized learners by averaging, but the framework does not model them.

Trivializing readings are excluded: the distribution must be a probability measure, the failing set must be measurable with an honest lower bound, and the witness $f$ must be measurable. Welcome contributions: the finitely supported product law on sequences, the averaging identity (5.3), and the pairing argument on labelings of $C$.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 5 and Appendix B. doi:10.1017/CBO9781107298019
• D. H. Wolpert, W. G. Macready, No free lunch theorems for optimization, IEEE Transactions on Evolutionary Computation 1(1), 1997. doi:10.1109/4235.585893
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

Motivation

Mission I of this series set up the statistical learning framework of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) and proved, in the book's Chapters 2 and 3, that finite classes are PAC learnable under the realizability assumption. Chapter 4 removes that assumption. Its idea is the one that organizes the rest of the theory: if the empirical risks $L_S(h)$ of all hypotheses in $H$ are simultaneously close to their true risks $L_D(h)$, then minimizing $L_S$ over $H$ is nearly as good as minimizing $L_D$ over $H$, whatever the distribution $D$ is. A sample with that property is called $\epsilon$-representative (Definition 4.1), and a class for which representative samples are guaranteed at some sample size is said to have the uniform convergence property (Definition 4.3). Lemma 4.2 turns representativeness into a guarantee for ERM, Corollary 4.4 turns uniform convergence into agnostic PAC learnability, Hoeffding's inequality (Lemma 4.5) gives uniform convergence for a single hypothesis, and a union bound gives it for a finite class: Corollary 4.6, the capstone, says every finite class with a loss in $[0,1]$ is agnostic PAC learnable by ERM with sample complexity $\lceil 2\log(2|H|/\delta)/\epsilon^2 \rceil$.

Setting

The framework is the UnderstandingML_Framework module of Mission I, cited here as a reference. A domain $Z$ is a measurable space, hypotheses form a type with a class $H$, and a loss $\ell : H \times Z \to \mathbb{R}$ is given. The risk is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h,z)$, the empirical risk on $S = (z_1,\dots,z_m)$ is $L_S(h) = \frac1m \sum_i \ell(h, z_i)$, and a sample of size $m$ has the product law $D^m$. A hypothesis is an ERM hypothesis for $S$ if it lies in $H$ and minimizes $L_S$ over $H$; a learner is a function from samples of each size to hypotheses, and an ERM learner returns an ERM hypothesis on every sample.

$S$ is $\epsilon$-representative with respect to $H$, $\ell$ and $D$ if $|L_S(h) - L_D(h)| \le \epsilon$ for every $h \in H$. $H$ has the uniform convergence property with the function $m^{UC}_H$ if for every $\epsilon, \delta \in (0,1)$ and every distribution $D$ over $Z$, a sample of $m \ge m^{UC}_H(\epsilon, \delta)$ i.i.d. examples is $\epsilon$-representative with probability at least $1 - \delta$. $H$ is agnostic PAC learnable with the function $m_H$ and the learner $A$ if $A$ returns hypotheses in $H$ and, for every $\epsilon, \delta \in (0,1)$, every $D$ and every $m \ge m_H(\epsilon,\delta)$, $L_D(A(S)) \le \min_{h' \in H} L_D(h') + \epsilon$ with probability at least $1 - \delta$ over $S \sim D^m$. As in Mission I, "with probability at least $1-\delta$" is an upper bound $\delta$ on the outer measure of the failure event, "$\min_{h' \in H} L_D(h') + \epsilon < L_D(h)$" is written as "$\exists h' \in H$, $L_D(h') + \epsilon < L_D(h)$", and sample-complexity functions are carried explicitly rather than as minimal functions.

Formalization targets

Goal: Corollary 4.6

Let $H$ be a finite hypothesis class, $Z$ a domain and $\ell : H \times Z \to [0,1]$ a loss function whose sections $\ell(h,\cdot)$ are measurable. Then

1. $H$ has the uniform convergence property with the function $m^{UC}_H(\epsilon,\delta) = \lceil \log(2|H|/\delta)/(2\epsilon^2) \rceil$;
2. every ERM learner for $H$ is an agnostic PAC learner with the function $m_H(\epsilon,\delta) = \lceil 2\log(2|H|/\delta)/\epsilon^2 \rceil$, which is $m^{UC}_H(\epsilon/2,\delta)$;
3. if $H$ is nonempty, $H$ is agnostic PAC learnable.

Milestones

Lemma 4.2. If $S$ is $\epsilon/2$-representative and $h_S$ is an ERM hypothesis for $S$, then $L_D(h_S) \le L_D(h) + \epsilon$ for every $h \in H$.

Corollary 4.4. If $H$ has the uniform convergence property with $m^{UC}_H$, then every ERM learner for $H$ is an agnostic PAC learner with the function $(\epsilon,\delta) \mapsto m^{UC}_H(\epsilon/2, \delta)$, and $H$ is agnostic PAC learnable as soon as an ERM learner exists.

Lemma 4.5 (Hoeffding's inequality). For a probability measure $D$, a measurable $\theta$ with $a \le \theta \le b$ almost surely and mean $\mu = \int \theta\,dD$, and $\epsilon > 0$,

$$D^m\Big[\Big|\tfrac1m \textstyle\sum_{i=1}^m \theta(\omega_i) - \mu\Big| > \epsilon\Big] \le 2\exp\!\big(-2m\epsilon^2/(b-a)^2\big).$$

Significance

Chapter 4 is where the book's account of learnability becomes distribution-free in the agnostic sense: nothing is assumed about $D$ beyond being a probability distribution, and the guarantee is relative to the best hypothesis in the class. Lemma 4.2 and Corollary 4.4 are the reduction that every later generalization bound in the book (VC dimension, Rademacher complexity, covering numbers, compression) plugs into: prove uniform convergence, get ERM learnability. Corollary 4.6 is the first instance, and its $\log|H|/\epsilon^2$ dependence, against the $\log|H|/\epsilon$ of the realizable case, is the standard illustration of the price of agnosticism. Hoeffding's inequality is stated in the form the book uses everywhere afterward, for the product law of one distribution, with an almost-sure range bound and the mean written as an integral.

Nothing here is machine-checked. Mathlib has no Hoeffding inequality for sums of i.i.d. bounded variables on a product measure in this form, so Lemma 4.5 is a genuine contribution; its proof in the book's Appendix B goes through Hoeffding's lemma on the moment generating function of a bounded centered variable and the Chernoff bounding method, both of which will be needed by the concentration results of later missions.

Difficulty

Lemma 4.2 is three inequalities on real numbers and is the intended entry point. Corollary 4.4 is Lemma 4.2 applied on the complement of the failure event of uniform convergence at $\epsilon/2$: the failure set of the learner is contained in the failure set of representativeness, and outer measure is monotone. Hoeffding's inequality is the substantial item: one needs the moment generating function bound $\mathbb{E}\,e^{\lambda(\theta-\mu)} \le e^{\lambda^2(b-a)^2/8}$ (Lemma B.7 of the book, by convexity of the exponential on $[a,b]$), independence of the coordinates under Measure.pi to factor the expectation of the product, Markov's inequality, and the optimization over $\lambda$; the two tails are treated separately and added. The degenerate cases are genuine: for $m = 0$ the bound is $2$ and the claim holds trivially, and for $a = b$ Lean's convention $x/0 = 0$ makes the bound $2$ again. Corollary 4.6 combines Hoeffding for each $h \in H$ with a union bound over the finite class and an arithmetic step showing that $m \ge \log(2|H|/\delta)/(2\epsilon^2)$ gives $2|H|e^{-2m\epsilon^2} \le \delta$; the empty class makes the uniform convergence clause vacuous. The second and third clauses of the goal then follow from Corollary 4.4, the third by exhibiting an ERM learner, which exists for a nonempty finite class by choosing a minimizer of $L_S$.

Formalization scope

The four items live in the general loss framework, not the binary-classification special case, because the chapter is stated for an arbitrary loss; Mission I's IsRepresentative and HasUniformConvergenceWith already carry the chapter's definitions, so no new definition module is introduced. Losses in Corollary 4.6 are real-valued with the range condition $\ell(h,z) \in [0,1]$ for every $z$ and measurability of $\ell(h,\cdot)$ for $h \in H$, which is what the book's "$\ell : H \times Z \to [0,1]$" and Remark 3.1 give. The book's "$m_H(\epsilon,\delta) \le \cdots$" is stated as "the guarantee holds with the function $\lceil \cdots \rceil$", the same convention as Mission I. In Corollary 4.4 the ERM clause is universal over ERM learners, matching "the ERM paradigm is a successful agnostic PAC learner" for every choice of minimizer; the existence of an ERM learner is a separate hypothesis for the learnability clause because a class with no minimizers on some sample has no ERM rule. Hoeffding's inequality is on i.i.d. coordinates of Measure.pi; the book's "$E[\theta_i] = \mu$" is the definition of $\mu$ rather than an assumption.

Trivializing readings are excluded: the failure events are bounded in outer measure, so measurability of the events is not a loophole; representativeness is required for every $h \in H$; the sample-complexity functions are the book's, with ceilings. Welcome contributions: Hoeffding's lemma on bounded centered variables, the factorization of the moment generating function under Measure.pi, and a reusable union bound over a finite class.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 4 and Appendix B. doi:10.1017/CBO9781107298019
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 1963. doi:10.1080/01621459.1963.10500830
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013, Chapter 2. doi:10.1093/acprof:oso/9780199535255.001.0001

Motivation

Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than $\log(|H|/\delta)/\epsilon$ (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function $m_H(\epsilon, \delta)$, restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.

Setting

A domain $Z$ of examples, a class $H$ of hypotheses and a loss $\ell : H \times Z \to \mathbb{R}$. The risk of $h$ under a distribution $D$ is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h, z)$ and its empirical risk on $S = (z_1, \dots, z_m)$ is $L_S(h) = \frac1m\sum_i \ell(h, z_i)$; a sample is drawn i.i.d., $S \sim D^m$; an ERM hypothesis minimizes $L_S$ over $H$; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are $(x, f(x))$ with $x \sim D$ over $X$ and $f$ a labeling function, and the true error is $L_{(D,f)}(h) = D(\{x : h(x) \ne f(x)\})$; the realizability assumption says some $h^\star \in H$ has $L_{(D,f)}(h^\star) = 0$. $H$ is PAC learnable if some sample-complexity function $m_H$ and algorithm guarantee, for all $\epsilon, \delta \in (0,1)$, all $D$ and all realizable $f$, true error at most $\epsilon$ with probability at least $1 - \delta$ from $m \ge m_H(\epsilon, \delta)$ examples; agnostic PAC learnability with respect to a loss asks instead for $L_D(h) \le \min_{h' \in H} L_D(h') + \epsilon$ for every distribution over $Z$.

Formalization targets

Goal: Corollary 3.2

Every finite hypothesis class is PAC learnable with sample complexity

$$m_H(\epsilon, \delta) \le \Big\lceil \frac{\log(|H|/\delta)}{\epsilon} \Big\rceil,$$

by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.

Milestone

Corollary 2.3: under realizability, with $m \ge \log(|H|/\delta)/\epsilon$ examples, every ERM hypothesis has true error at most $\epsilon$ with probability at least $1 - \delta$.

Significance

Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most $(1 - \epsilon)^m \le e^{-\epsilon m}$, and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count $|H|$ by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.

Difficulty

The milestone needs that, for a fixed measurable hypothesis whose true error exceeds $\epsilon$, the product law gives the event "zero empirical risk" probability at most $(1-\epsilon)^m$; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with $f$, followed by $1 - \epsilon \le e^{-\epsilon}$, the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.

Formalization scope

The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least $1 - \delta$"; the comparison with $\min_{h' \in H} L_D(h')$ is written without an infimum. Sample-complexity functions are carried explicitly: the book's $m_H$ as the minimal such function is not defined, and "$m_H \le f$" is stated as "the learner satisfies the guarantee with the function $f$". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: $\epsilon > 0$, $\delta \in (0,1)$, $H$ finite (and nonempty for the learner to exist).

Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all $\epsilon, \delta$. Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 2–4. doi:10.1017/CBO9781107298019
• L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
• V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. doi:10.1007/978-1-4757-2440-0
• D. Haussler, Decision theoretic generalizations of the PAC model for neural net and other learning applications, Information and Computation 100(1), 1992. doi:10.1016/0890-5401(92)90010-D

Motivation

Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than $k$-CNF and $k$-DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.

Setting

The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution $D$, the product law of a sample of $m$ labeled examples, the error $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \neq c(x)]$, and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an $(\alpha, \beta)$-Occam algorithm outputs a consistent hypothesis of size at most $(n \cdot \mathrm{size}(c))^\alpha m^\beta$ with $0 \le \beta < 1$. The set cover problem asks for a minimum subcollection of a collection $\mathcal{S}$ of subsets of a finite universe $U$ that covers $U$; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A $k$-decision list is a sequence of conditions, each a conjunction of at most $k$ literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.

Formalization targets

Goal: Theorem 2.2 (Occam's Razor, cardinality version)

For a finite hypothesis class $H$, a target $c$, a distribution $D$ and $0 < \epsilon \le 1$, the probability that a sample of $m$ examples is consistent with some $h \in H$ of error greater than $\epsilon$ is at most $|H|(1 - \epsilon)^m$; hence

$$m \ge \frac{1}{\epsilon}\Big(\ln|H| + \ln\frac{1}{\delta}\Big)$$

makes this probability at most $\delta$, and any algorithm that outputs a consistent hypothesis from $H$ has error greater than $\epsilon$ with probability at most $|H|(1-\epsilon)^m$.

Milestones

Theorem 2.1 (an $(\alpha, \beta)$-Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant $a$); the greedy set-cover bound of §2.3 ($|U_i| \le (1 - 1/\mathrm{opt})^i|U|$ and $\mathrm{opt}\ln|U|$ sets cover); the improved conjunction bound of §2.2; Theorem 2.3 ($k$-decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).

Significance

Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, $k$-CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of $|H|$. Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.

Difficulty

Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than $\epsilon$, the product law gives the event "consistent with all $m$ examples" probability at most $(1 - \epsilon)^m$, which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where $h$ agrees with $c$; the union bound over $H$ and the elementary inequality $(1 - \epsilon)^m \le e^{-\epsilon m}$ finish. Theorem 2.1 adds only the count of binary strings of length at most $K$ and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of $U$ restricted to the uncovered elements has at most $\mathrm{opt}$ sets, so one of them, hence the greedy choice, covers a $1/\mathrm{opt}$ fraction; the covering clause needs the strict inequality $1 - 1/\mathrm{opt} < e^{-1/\mathrm{opt}}$. Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.

Formalization scope

Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant $b$ is $1$ with natural logarithms; Theorem 2.1's constant $a$ is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every $k$ with the $k$-conjunctions as conditions, so that its hypothesis is a $k$-decision list rather than the expansion the book sketches for $k > 1$. The conjunction count is $3^n + 1$, including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and $m$ on both sides). Hypotheses: $0 < \epsilon \le 1$, $0 < \delta$ (and $\delta < 1$ where $\ln(1/\delta)$ must be nonnegative).

Trivializing readings are excluded: the bad-consistent event is over all of $H$, the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 2. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
• V. Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4(3), 1979. doi:10.1287/moor.4.3.233
• R. L. Rivest, Learning decision lists, Machine Learning 2(3), 1987. doi:10.1007/BF00058680
• D. Haussler, Quantifying inductive bias: AI learning algorithms and Valiant's learning framework, Artificial Intelligence 36(2), 1988. doi:10.1016/0004-3702(88)90002-1

Motivation

Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least $1 - \delta$ over the sample, misclassifies a fresh example with probability at most $\epsilon$; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.

Setting

The instance space is a measurable space $X$, a concept is a function $c : X \to \{0, 1\}$, and the target distribution $D$ is a probability measure on $X$. The error of a hypothesis $h$ is $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \ne c(x)]$. A sample of $m$ examples is $S = ((x_1, c(x_1)), \dots, (x_m, c(x_m)))$ with the $x_i$ independent draws from $D$; a learning algorithm is a function from samples to hypotheses; it has the $(\epsilon, \delta)$ guarantee on a class $C$ if for every $c \in C$ and every $D$ the probability that its hypothesis has error greater than $\epsilon$ is at most $\delta$; $C$ is PAC learnable using $H$ if for all $\epsilon, \delta \in (0, 1/2)$ some sample size and algorithm with hypotheses in $H$ achieve the guarantee. For $X = \{0,1\}^n$ a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all $2n$ literals and deletes every literal contradicted by a positive example. For $X = \mathbb{R}^2$ the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion $a \mapsto a'$ records for each triple $(u, v, w)$ of literals the value $u \vee v \vee w$.

Formalization targets

Goal: Theorem 1.2

Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on $\{0,1\}^n$ and $\epsilon, \delta > 0$, the elimination hypothesis is consistent with every sample labeled by the target, and with

$$m \ge \frac{2n}{\epsilon}\Big(\ln 2n + \ln\frac{1}{\delta}\Big)$$

examples its error exceeds $\epsilon$ with probability at most $\delta$; hence conjunctions are PAC learnable using conjunctions.

Milestones

Theorem 1.1 (rectangles by the tightest fit, $m \ge (4/\epsilon)\ln(4/\delta)$) and Theorem 1.4 (3-CNF formulae by elimination over the $(2n)^3$ expanded variables, the hypothesis being itself a 3-CNF formula).

Significance

Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.

Difficulty

The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals $z$ of $p(z) = \Pr[c(a) = 1 \wedge z = 0 \text{ in } a]$, and that a literal with $p(z) \ge \epsilon/2n$ survives $m$ independent examples with probability at most $(1 - \epsilon/2n)^m$; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality $1 - x \le e^{-x}$. The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip $\{y \ge t^*\}$ with $t^*$ the supremum of the heights at which the strip has weight at least $\epsilon/4$ and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.

Formalization scope

The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least $1 - \delta$" and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is $\{0,1\}^n$ as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so $N = (2n)^3$ is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: $\epsilon > 0$, $0 < \delta < 1$; the sample bounds are as printed, with natural logarithms.

Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all $\epsilon, \delta$. Welcome contributions: the product-law bound $\Pr[\text{a fixed event of probability} \ge p \text{ is missed by all } m \text{ examples}] \le (1 - p)^m$, the union bound over literals, and the pushforward identity for the expanded sample.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 1. doi:10.7551/mitpress/3897.001.0001
• L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• L. Pitt, L. G. Valiant, Computational limitations on learning from examples, Journal of the ACM 35(4), 1988. doi:10.1145/48014.63140

Why the policy class is not up for debate

Every model in Chapters 5 and 6 of Axsäter's Inventory Control assumes at the outset that the ordering policy is of $(R,Q)$ or $(s,S)$ type. Section 6.2 asks whether better policies exist and answers, for the case in which there are no ordering costs but every order must be a multiple of a fixed batch quantity $Q$, that none do: Proposition 6.1, "an $(R,Q)$ policy is optimal", with a proof the book attributes to Chen (2000). For $Q = 1$ it is the optimality of an order-up-to-$S$ policy in the absence of ordering costs, and for continuous or Poisson demand it transfers to $(s,S)$ policies, which are then the same thing. The proposition is the one place in the book where a policy is compared against every feasible alternative rather than against other members of its own family, and its proof is short enough to be given in full, which makes it the natural capstone of Chapter 6.

Setting

Demand is compound Poisson: customers arrive according to a Poisson process with rate $\lambda$ and each demands an integral number of units, with sizes $D_0, D_1, \dots$ independent and identically distributed with law $f$ on the positive integers, independent of the arrival process. The book's standing assumption that not all demands are multiples of some integer larger than one is kept. Writing $T_n$ for the $n$-th arrival time, $N(t)$ for the number of arrivals by time $t$ and $S_n = D_0 + \dots + D_{n-1}$, the total demand by time $t$ is $S_{N(t)}$.

The replenishment lead-time $L$ is constant and $D(L)$, the demand over a lead-time, has law $D$. A holding cost $h > 0$ and a shortage cost $b_1 > 0$ per unit and time unit are charged. There are no ordering costs, but all orders must be multiples of a given batch quantity $Q \ge 1$ and can only be triggered by customer demands. A policy is therefore any rule $m$ that decides at each demand epoch how many batches to order; with initial position $y_0$ the inventory position evolves as $y_{n+1} = y_n - D_n + m_nQ$ (Eq. 6.22), and $y_t = y_{N(t)}$.

The standard argument of Sect. 5.3.2 gives the cost rate at time $t + L$ as

$$g(y_t), \qquad g(k) = -b_1(k - \mu') + (h+b_1)\sum_{j=1}^{k} j\,\Pr[D(L) = k - j],$$

the expected holding-plus-shortage cost rate of an inventory level $k - D(L)$ (Eq. 6.20), which is convex in $k$ with $g(k) \to \infty$ as $|k| \to \infty$. The band cost is $\bar g(y) = \sum_{j=1}^{Q} g(y+j)$ and $R$ denotes an integer minimizing $\bar g$. The $(R,Q)$ policy orders, as soon as the position is at or below $R$, the smallest number of batches that brings it above $R$; its position lives in the band $\{R+1, \dots, R+Q\}$ from the first order on. The performance measure is the long-run average cost rate $\frac{1}{T}\int_0^T g(y_{t-L})\,\mathrm{d}t$ as $T \to \infty$.

Formalization targets

Goal — Proposition 6.1

Almost surely, (1) for every policy $m$ and every $y_0$,

$$\liminf_{T\to\infty} \frac{1}{T}\int_0^T g\big(y^{m}_{t-L}\big)\,\mathrm{d}t \;\ge\; \frac{\bar g(R)}{Q},$$

and (2) the $(R,Q)$ policy attains it:

$$\frac{1}{T}\int_0^T g\big(y^{(R,Q)}_{t-L}\big)\,\mathrm{d}t \;\longrightarrow\; \frac{\bar g(R)}{Q}.$$

Supporting targets

Lemma 6.1, that $x \mapsto g(z + xQ)$ is convex and minimized at the representative of $z$ in the band; the closed form of the $(R,Q)$ position, $y_0 - S_n$ until the first order and the band representative of $y_0 - S_n$ afterwards; the uniform occupation of the band by the reduced process $y_t'$, the book's "the steady state distribution can be shown to be uniform", and its consequence that the long-run average of $g(y_t')$ is $\bar g(R)/Q$; Proposition 5.1 in the same ergodic form for the $(R,Q)$ policy; and the two halves of the goal as separate statements.

Significance

The result itself. Proposition 6.1 is what licenses the two-parameter policies on which the rest of the book's single-echelon theory is built, and it does so for the practically important case of batch ordering (pallets, containers, production lots). Its proof also explains why the policy works: the only quantity a policy controls is the residue class of the inventory position modulo $Q$, which no policy can influence, and the position within that class, which the $(R,Q)$ policy always sets to the cheapest possible value. The book extends the same reasoning to other cost structures and to periodic review.

Formalizing it. The proposition is a theorem about the class of all policies, and the book's proof is pathwise: Lemma 6.1 compares any policy with the reduced process instant by instant, and an ergodic statement about the reduced process does the rest. Formalizing it therefore forces the policy class, the demand process and the long-run average to be written down exactly, which the book never does. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The pointwise comparison is elementary once Lemma 6.1 is available, and Lemma 6.1 is discrete convexity. The difficulty is entirely in the ergodic statement: that the reduced position $y_t' =$ (the band representative of $y_0 - S_{N(t)}$) spends a fraction $1/Q$ of the time at each point of the band, almost surely. In discrete time this is the convergence of occupation frequencies for an irreducible random walk on $\mathbb{Z}/Q\mathbb{Z}$ with step law $f$ modulo $Q$, where irreducibility is exactly the aperiodicity assumption on $f$, and the book's double-stochasticity argument (Eq. 5.33-5.34) identifies the uniform law as stationary. Passing to continuous time adds the exponential holding times: the time average is the arrival average weighted by i.i.d. holding times independent of the walk, which a strong law of large numbers turns back into the discrete statement. Mathlib has the strong law and the exponential law but no ergodic theorem for finite Markov chains, so that is the groundwork a solver must build. The naive route through the stationary distribution of the embedded chain at demand epochs is not enough on its own: for pure Poisson demand that chain is periodic, and the book itself notes it.

Formalization scope

A CompoundPoissonDemand on a probability space packages the rate, the size law with $f_0 = 0$ and the aperiodicity condition, and two sequences of random variables, the gaps and the sizes, with their laws (expMeasure lam, the given pmf), independence within each sequence, and independence between the sequences. Arrival times are partial sums of the gaps, count t is the supremum of $\{n : T_n \le t\}$, and cumDemand n is the partial sum of the sizes. A policy is a function m : ℕ → Ω → ℕ with no measurability requirement; ipPath and ipAt are the position after the $n$-th demand and at time $t$; rqIP and rqOrders are the $(R,Q)$ policy, with a theorem identifying rqOrders as a policy in the general sense. avgCost is $\frac{1}{T}\int_0^T g(y_{t-L})\,\mathrm{d}t$ with $y_s = y_0$ for $s < 0$. The cost function $g$ is sPolicyCost from the previous mission, applied to a DiscreteDemand that the hypotheses tie to the process as the law of the demand in $(0, L]$.

Conventions: $Q \ge 1$, $L \ge 0$, $h, b_1 > 0$; $R$ is any minimizer of $\bar g$ (it exists by the divergence of $g$, proved in the previous mission); $y_0$ is arbitrary. count and the interval integral take junk values on the null set where arrivals do not tend to infinity, which the almost-sure conclusions absorb. "$\liminf \ge c$" is stated as "for every $\varepsilon > 0$, eventually $\ge c - \varepsilon$", avoiding a liminf on $\mathbb{R}$ that could be junk.

Two readings that would trivialize the goal are excluded: the lower bound is over every rule, not over stationary or measurable ones, and the achievability half is a genuine limit, not a bound. The demand model and the occupation-frequency theorems are reusable for Proposition 10.1 and the batch-ordering models of Sect. 10.5; contributions establishing the ergodic theorem for irreducible chains on a finite cyclic group are welcome and would close most of this mission.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.3.1 and 6.2.1. DOI 10.1007/978-3-319-15729-0
• Fangruo Chen, Optimal Policies for Multi-Echelon Inventory Problems with Batch Ordering, Operations Research 48(3), 2000, pp. 376-389. DOI 10.1287/opre.48.3.376.12427
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal $(r,Q)$ Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4), 1992, pp. 808-813. DOI 10.1287/opre.40.4.808
• Evan L. Porteus, Foundations of Stochastic Inventory Theory, Stanford University Press, 2002.

Two decisions that are usually taken separately

An $(R,Q)$ policy has two parameters. Chapter 4 of Axsäter's Inventory Control chooses the batch quantity $Q$ from a deterministic model, and Chapter 5 chooses the reorder point $R$ from a stochastic one with $Q$ held fixed; the book presents this two-step practice as an adequate approximation. Section 6.1 asks what is lost by it and shows how to optimize both parameters jointly in one stochastic model. For discrete demand the answer, due to Federgruen and Zheng (1992), is an algorithm of remarkable simplicity: increase $Q$ one unit at a time, keep the reorder point optimal along the way by a one-line rule, and stop at the first $Q$ for which the cost goes up. The claim that this stopping rule finds the global optimum over all pairs $(R, Q)$ is the capstone of Sect. 6.1.1.1 and the goal of this mission. The same idea is reused in the book for $(s,S)$ policies (Sect. 6.1.1.2) and, in continuous form, for normally distributed demand (Sect. 6.1.2).

Setting

An item is controlled by a continuous review $(R,Q)$ policy with integral reorder point $R$ and batch quantity $Q \ge 1$. Demand is discrete and stationary; the lead-time demand $D(L)$ takes values in the nonnegative integers with probabilities $p_j = \Pr[D(L) = j]$ and has a finite mean $\mu'$. The average demand per unit of time is $\mu$. Costs are a holding cost $h$ and a shortage cost $b_1$, both per unit and time unit, and an ordering cost $A$ per batch.

The building block is the cost of an $(S-1,S)$ policy that keeps the inventory position at a fixed integer $k$. By the standard argument of Sect. 5.3.2 the inventory level a lead-time later is $k - D(L)$, and the average holding and shortage cost rate is (Eq. 6.3)

$$g(k) \;=\; -b_1\,(k - \mu') + (h + b_1)\sum_{j=1}^{k} j\,\Pr[D(L) = k - j].$$

Under the $(R,Q)$ policy the inventory position is uniformly distributed on $\{R+1, \dots, R+Q\}$ (Proposition 5.1), so the total average cost rate is (Eq. 6.4)

$$C(R, Q) \;=\; \frac{A\mu}{Q} + \frac{1}{Q}\sum_{k=R+1}^{R+Q} g(k),$$

and $C(Q) = \min_R C(R,Q)$ (Eq. 6.5), attained at an optimal reorder point $R^{*}(Q)$. The ready rate $S_3(R) = \Pr[IL > 0] = \frac{1}{Q}\sum_{k=R+1}^{R+Q}\Pr[D(L) \le k-1]$ links the cost to service: raising the reorder point by one unit changes the cost by $-b_1 + (h + b_1)S_3(R+1)$ (Eq. 5.60).

Formalization targets

Goal — the Federgruen-Zheng stopping rule is optimal

Let $Q^{*} \ge 1$ be the smallest batch quantity with $C(Q^{*}+1) \ge C(Q^{*})$ and let $R^{*}$ be an optimal reorder point for $Q^{*}$. Then

$$C(R^{*}, Q^{*}) \;\le\; C(R, Q) \qquad\text{for all } R \in \mathbb{Z},\ Q \ge 1.$$

Supporting targets

The increment identity $g(k+1) - g(k) = -b_1 + (h+b_1)\Pr[D(L) \le k]$; convexity of $g$ on $\mathbb{Z}$ together with $g(k) \to \infty$ as $|k| \to \infty$; Eq. (5.60) and the convexity of $C(\cdot, Q)$ in $R$; Eq. (5.61), that the largest $R$ with $S_3(R) \le b_1/(h+b_1)$ is optimal for its $Q$; existence of an optimal $R$ for every $Q$; the recursion (6.6)-(6.7), $R^{*}(Q+1) \in \{R^{*}(Q) - 1, R^{*}(Q)\}$ chosen by comparing $g(R^{*}(Q))$ with $g(R^{*}(Q)+Q+1)$, and $C(Q+1) = C(Q)\frac{Q}{Q+1} + \min\{g(R^{*}(Q)), g(R^{*}(Q)+Q+1)\}\frac{1}{Q+1}$; the equivalence $C(Q+1) \ge C(Q) \iff \min\{\cdot\} \ge C(Q)$ and the monotonicity of that minimum in $Q$; and the existence of some $Q$ at which the costs stop decreasing.

Significance

The result itself. Joint optimization typically enlarges the batch and lowers the reorder point relative to the two-step procedure, and the book's Example 6.1 puts the resulting cost saving at a few percent. The Federgruen-Zheng procedure makes the exact joint optimum for discrete demand as cheap to compute as the two-step approximation, because each step of the recursion evaluates $g$ at two points. It is the exact benchmark against which the book's approximate techniques for normal demand (Sects. 6.1.2 and 6.1.3) are judged, and its structural core, that the optimal window of $Q$ consecutive inventory positions grows one neighbour at a time, is the discrete-convexity fact behind the whole of Sect. 6.1.

Formalizing it. The mathematics is settled. What the mission produces is a Lean development in which the steps the book marks "evident" and "obvious" are separate statements: that the recursion preserves optimality, that the marginal cost of enlarging the batch is monotone, and that a minimum over $R$ exists at all. None of the statements has a machine-checked proof yet.

Difficulty

The obvious first idea, to argue that $C(Q)$ is convex in $Q$ and stop at its first increase, does not work as stated: $C(Q)$ is a minimum over $R$ of a ratio and is not convex in general. What is true, and what the proof uses, is that the marginal cost $(Q+1)C(Q+1) - QC(Q)$ is nondecreasing, because it equals the smaller of the two $g$-values adjacent to the optimal window. Establishing the recursion (6.6) is where discrete convexity is needed: one must show that the best window of $Q+1$ consecutive positions is obtained from the best window of $Q$ by adding a neighbour, which fails for non-convex $g$. The window sums $R \mapsto \sum_{k=R+1}^{R+Q} g(k)$ are themselves convex in $R$ with increments $g(R+Q+1) - g(R+1)$, and the argument compares a competing window with the optimal one through the end terms. The remaining steps are finite algebra and an induction on $Q$ from $Q^{*}$.

Formalization scope

A DiscreteDemand is a function $p : \mathbb{N} \to \mathbb{R}$ with $p \ge 0$, $\sum p = 1$ and a summable first moment; $\Pr[D(L) \le k]$ is a finite sum over $0 \le j \le k$, empty for $k < 0$. The reorder point ranges over $\mathbb{Z}$ and the batch quantity over $\mathbb{N}$, with $Q \ge 1$ assumed in every statement because Lean's division by $0$ is $0$. Convexity of a function on $\mathbb{Z}$ is stated as nondecreasing increments, and divergence as Tendsto g (cocompact ℤ) atTop.

$C(Q)$ enters the goal as a function CQ together with the hypothesis that CQ Q is the least value of $R \mapsto C(R, Q)$; the stopping index $Q^{*}$ is characterized by the two conditions that define "the smallest $Q$ with $C(Q+1) \ge C(Q)$", and $R^{*}$ by optimality at $Q^{*}$. That these objects exist is the content of two separate items, so the goal is not vacuous: a minimum over $R$ exists for every $Q$ because $g \to \infty$, and the costs cannot decrease forever because the average of the $Q$ smallest values of $g$ tends to infinity. The positivity of $A$ and $\mu$ is the book's setting and is assumed where it appears.

The uniform inventory position of Proposition 5.1, which needs the book's assumption that not all demands are multiples of an integer larger than one, is taken as given in the cost formula (6.4), as the book does; the proposition itself is the subject of the next mission of this series. The definitions are reusable for the $(s,S)$ optimization of Sect. 6.1.1.2 and for the multi-echelon batch-ordering results of Sect. 10.5; contributions formalizing the Zheng-Federgruen $(s,S)$ algorithm on top of them are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.9.1 and 6.1.1. DOI 10.1007/978-3-319-15729-0
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal $(r,Q)$ Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4), 1992, pp. 808-813. DOI 10.1287/opre.40.4.808
• Yu-Sheng Zheng and Awi Federgruen, Finding Optimal $(s,S)$ Policies Is About as Simple as Evaluating a Single Policy, Operations Research 39(4), 1991, pp. 654-665. DOI 10.1287/opre.39.4.654
• Paul Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.