Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Every stability result in Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) — the throughput optimality of the dynamic backpressure algorithm (Theorem 4.5), the utility-optimal Lyapunov drift bound of Chapter 5, the energy-constrained control algorithm of Chapter 6 — is proved the same way: exhibit a drift condition on a quadratic Lyapunov function of the queue backlog vector, then invoke one fixed abstract lemma to conclude stability and an explicit congestion bound. That fixed lemma, Lyapunov drift stability (Lemma 4.1, adapted from Kingman [67], Loynes [87] and Neely, Modiano & Li [110]), is the engine this mission formalizes — the single result the rest of the book's algorithm-specific theorems are instances of.
A network of queues has backlog vector process on slots , on a common probability space . The quadratic Lyapunov function is . A single queue's backlog sequence (read as ) is strongly stable if ; a network is strongly stable if every one of its queues is. The conditional drift of given the current backlog vector, , measures how the aggregate squared backlog is expected to change over one slot, conditioned on where the network currently is — formalized via Mathlib's conditional expectation on the -algebra generated by .
This is the weakest, most general level: a bounded-outside-a-compact-region drift condition implies both a qualitative stability conclusion and a quantitative congestion bound, with no mention of any particular algorithm, arrival distribution, or network topology.
Lyapunov drift stability is the one lemma every later result in this book's method reduces to: Chapter 4's own Theorem 4.5 (backpressure throughput optimality) applies it directly to the dynamic backpressure algorithm's per-slot optimality property; the book explicitly notes ("This drift inequality is in the exact form for application of the Lyapunov drift lemma... proving the result", p. 57) that once a drift bound of this shape is established, the stability conclusion is free. The T-slot version (Lemma 4.2) extends the reach of the method to settings — Markov-modulated channels, non-i.i.d. arrivals — where no single slot need have negative drift.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov drift, max-weight, differential backlog, backpressure — the one Lyapunov-drift hit, a Foster-Lyapunov hitting-time bound for a finite-state MDP with an absorbing target state, is a different mathematical object from a vector queue backlog with no absorbing state, and is not reused). This mission is the first formalization of the book's stability engine.
The obvious first idea is to bound directly via the one-step queueing recursion and telescope. This fails for the same reason it fails in Chapter 3: expectation does not commute with . Lemma 4.1's actual content is a genuine Foster–Lyapunov drift argument on the aggregate quadratic quantity , not a per-queue linear one — the quadratic form is what turns a one-sided drift condition into a bound on itself (via the elementary inequality of Lemma 4.3, which converts the linear queueing recursion into a quadratic one that the drift condition directly controls). A second trap is conditioning: the drift bound is conditioned on the current backlog vector , not on the full history — a weaker, memoryless form of conditioning that is exactly what makes the lemma apply uniformly to i.i.d., Markov-modulated, and adversarial channel processes alike, provided the algorithm itself is memoryless in the state.
The Lyapunov-drift hypothesis conditions on the σ-algebra generated by the current backlog vector,
MeasurableSpace.comap (U t) inferInstance, via Mathlib's condExp; explicit Measurable/
Integrable guards on U t and on the drift term prevent condExp/∫ from silently defaulting
to 0 for a non-measurable or non-integrable process (a trivializing formalization this mission
rules out: without those guards, an arbitrary non-integrable backlog process would satisfy the
drift hypothesis vacuously and "prove" the theorem for a process that manifestly is not stable).
The limsup ≤ B/ε conclusion is stated as ∀ t, (Cesàro average at t) ≤ B/ε rather than via
Mathlib's Filter.limsup, matching the standard telescoping proof (which bounds the average for
every t, not merely eventually) and avoiding Filter.limsup's junk value on an unbounded
sequence in the non-complete lattice ℝ. Out of scope for this mission: the algorithm-specific
Theorem 4.5 (dynamic backpressure throughput optimality) and Lemma 4.4 (the single-queue corollary
via admissible processes) — the former needs the book's named algorithm plus Chapter 3's capacity
region restated as a local hypothesis and the explicit constant B of Eq. (4.12); the latter needs
this chunk's own restatement of Chapter 3's admissibility structures. Both are left for a future
mission with a larger time budget rather than approximated.
Every wireless network control algorithm — routing, scheduling, power control, admission control — is ultimately judged against one question: which traffic loads can it keep stable? Answering that question requires a precise, algorithm-independent notion of queueing stability under random arrivals and a randomly time-varying, possibly non-ergodic-looking channel. Tassiulas & Ephremides (1992) and Neely, Modiano & Rohrs (2005) developed the framework used throughout Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006): "strong stability" of a queue backlog process, defined purely through the time-averaged expected backlog, with no assumption that the arrival or service process is stationary, Markov, or even has a well-defined long-run average. The present mission formalizes the chapter's foundational single-queue results — the two structural facts every later network-wide capacity and control result in the book is built from.
A queue is described by three processes on slots : an arrival process (new bits admitted at the end of slot ), a service process (the transmission rate offered during slot ), and the backlog , evolving by the queueing law
The queue is strongly stable if its expected backlog has a bounded time average, . An arrival process is admissible with rate if (i) its time-average expected rate is , (ii) its second moment conditioned on the history is uniformly bounded, and (iii) for every there is an averaging window over which the conditional average rate exceeds by at most , uniformly in the starting time — a robust substitute for "the rate is exactly " that holds for i.i.d., Markov-modulated, and burstiness-constrained arrivals alike. A service process is admissible with rate analogously, with a deterministic pointwise upper bound in place of the second-moment condition. Both notions are formalized here on a filtered probability space , with the history of slots exactly as the book's own .
This is the chapter's central single-queue result: it converts the purely structural notion of strong stability into the one comparison — arrival rate versus service rate — that every later capacity-region and control-algorithm argument in the book reduces to.
This is the elementary real-analysis fact — no admissibility, no probability beyond an already-given expectation sequence — that underlies the necessity half of Lemma 3.6's proof.
Strong stability and the admissibility framework are the load-bearing definitions of the entire book: every later chapter's algorithm-performance theorem (Chapter 4's backpressure throughput optimality, Chapter 5's utility-optimal Lyapunov drift bound, Chapter 6's energy-constrained control) is a theorem about when its induced queues are strongly stable, and every one of those proofs cites Lemma 3.6 (or its network generalization, Theorem 3.8's capacity region) as the final step converting a drift bound into a stability conclusion. Formalizing it fixes, once for the whole series, the precise real-analysis and conditional-expectation content of "arrival rate below service rate implies stability" that a Prove2Me solver would otherwise have to reconstruct from scratch for each downstream chapter.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for strong stability, admissible arrival process, Lyapunov drift, network capacity region — the one hit, a Foster–Lyapunov hitting-time bound for a finite-state MDP, is a scalar drift-to-a-target-state object, not a queue-backlog vector with no absorbing state, and is not reused). This mission is the first formalization of either result.
The obvious first idea for the sufficiency half (b) is to try to bound directly by unrolling the queueing recursion and taking expectations termwise. This fails immediately: expectation does not commute with , so in general — the whole reason admissibility's second-moment and -slot averaging clauses exist is to control exactly this gap between the pathwise recursion and its expectation, via a genuine (non-elementary) drift argument. The necessity half (a) has the opposite trap: it is tempting to prove from a single-slot expectation inequality, but a queue can be strongly stable while oscillates on any finite window, so the argument has to go through the time-averaged (Lemma 3.3) quantity, not a slot-by-slot one.
Admissibility's conditional-expectation clauses are stated with Mathlib's Filtration ℕ and
condExp (P[f | 𝓕 t]), following this platform's established idiom for martingale-difference
hypotheses. Every conditional or plain expectation in a defining clause carries an explicit
Integrable guard, because Mathlib's Bochner integral and condExp both silently default to 0
on a non-integrable function — without the guard, a process with an undefined or infinite second
moment would satisfy admissibility vacuously, which is not the book's assumption (the book assumes
these moments are finite; it never derives it). Lemma 3.3 is formalized directly on the real
sequences representing , , —
exactly the content the book's own statement and proof use, with no further probabilistic
structure, since the lemma's hypotheses and conclusion never mention anything but these
expectations. Out of scope for this mission: the network-wide capacity region (Definition 3.7,
Theorem 3.8, Corollaries 3.9-3.10) and the graph-family construction /
of §3.2-3.3. Faithfully formalizing " is stably supportable by the network" requires
embedding admissible-process realizations into a full multi-queue routing model, which is
substantially heavier than either result formalized here and was left out entirely — per this
series' faithfulness-over-coverage rule — rather than approximated by, e.g., dropping the
second-moment or -slot clauses of admissibility, which would silently change what "admissible"
means. A trivializing formalization to rule out: defining AdmissibleArrival/AdmissibleService
without the Integrable guards above would make Lemma 3.6 provable by choosing a non-integrable
process, which is not the book's theorem.
Independent sums are a basic model for accumulated random fluctuation. A central limit theorem describes their distribution at one large time, and a functional limit theorem describes weak convergence of a rescaled path. Strong approximation asks for substantially more: construct the sums and a Brownian motion on one probability space so that their paths remain close, with an explicit error bound that holds simultaneously over all earlier integer times. Such a coupling turns Brownian path estimates into quantitative information about random walks and independent sums.
Chapter 7, Section 5 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986) states this strong approximation result as Theorem 5.1. Its estimate has logarithmic deterministic error and a strictly exponential tail. The theorem is known as a Komlós–Major–Tusnády type approximation, but the mission follows the exact formulation and hypotheses printed by Ethier and Kurtz.
Let be a probability measure on . The hypothesis requires an such that
Thus the moment-generating integral is finite on a neighborhood of zero. No centering, symmetry, bounded-support, or positive-variance assumption is made.
The conclusion constructs one probability space carrying an iid sequence with common law and a Brownian motion . The Brownian motion has drift and variance chosen to match one summand:
Writing , both and are evaluated on this same space. The theorem does not require the iid sequence to be independent of the Brownian coordinate; their dependence is precisely what permits a close coupling.
There are positive constants , , and , depending only on , such that for every integer and every real ,
Both inequalities are strict: the discrepancy event uses and its probability is . The constants and the entire coupling are chosen before and . The logarithmic term is retained at , where .
The Lean statement uses sequence coordinates indexed from zero, so coordinate represents the source variable and Finset.range k is exactly the sum of the first variables. An existential index with expresses the finite maximum event without replacing either strict inequality.
Weak convergence compares distributions after rescaling and does not place a prelimit sum and its limiting process on the same sample point. This theorem instead supplies a simultaneous pathwise comparison through a common-space construction. The exponential tail quantifies the chance that the uniform error up to time exceeds the logarithmic scale by an additional amount .
The formal statement records the complete coupling rather than only its consequence for normalized terminal sums. It exposes the iid coordinate laws, mutual independence of those coordinates, the Brownian law, the moment-matched affine scaling, the positivity and quantifier order of the constants, and the exact maximal-error event. This is a statement-only formalization: the theorem remains an open Lean goal, and no proof claim is made.
Matching a single sum to a Gaussian random variable is not enough. The construction must coordinate every partial sum with one Brownian path, uniformly over all , while keeping the error logarithmic and the excess probability exponentially small. Independent coupling at each time would destroy consistency across times, while an ordinary invariance principle gives convergence in distribution without the stated finite- tail. The difficulty is therefore the joint construction with all of these quantitative requirements at once.
The common carrier is the product of a real sequence space with the subtype of continuous functions from nonnegative real time to . A probability measure on that carrier is the joint law. iIndepFun asserts mutual independence of all sequence coordinates, and HasLaw gives each coordinate the law . IsBrownianReal specifies the standard Brownian second coordinate.
The Brownian motion appearing in the estimate is defined from that standard coordinate by
This representation covers the zero-variance case: then the scaled Brownian fluctuation vanishes and is deterministic, while the auxiliary standard Brownian coordinate may still be present on the common carrier. The exponential-moment hypothesis supplies the intended finite first and second moments. Probabilities use extended nonnegative reals, and the finite positive real bound is embedded with ENNReal.ofReal.
No local auxiliary definition is expression-essential: all objects in the theorem are provided by Mathlib. The mission intentionally excludes the section's rescaling observations and Poisson corollaries, which do not form separate capstone goals in the accepted grouping. Useful future contributions include the proof of this exact common-space theorem and reusable coupling infrastructure that preserves strict tail estimates.
The group Steiner tree problem generalizes the ordinary Steiner tree problem: given a rooted tree and several groups of vertices, find a minimum-cost subtree that connects at least one vertex of each group to the root. It is a canonical instance of the generalized-connectivity family this survey studies in Chapter 11 — a family that also contains the online set-cover problem (Chapter 5 of this series) as a special case. Buchbinder and Naor's chapter shows how to convert the celebrated offline randomized-rounding algorithm of Garg, Konjevod and Ravi [56] into an online one, by imitating its per-edge coupling structure one iteration at a time as the online fractional solution (obtained from this survey's own Chapter 4 framework) evolves. This mission formalizes that online rounding scheme's three defining probabilistic guarantees and the resulting competitive-ratio theorem.
Fix a rooted tree T = (V, E, r) with non-negative edge costs c : E → ℝ, and k groups
g₁, …, g_k ⊆ V, each request (r, gᵢ) arriving online. An online covering algorithm (from
Chapter 4's framework, applied to the LP relaxation of this connectivity problem) maintains a
monotonically increasing fractional weight w : E → ℝ on the edges, reinterpreted so that wₑ
is the maximum flow that can be routed through e to any vertex of its subtree — a technical
substitution needed so weights are monotone non-increasing along any root-to-leaf path, the
property the rounding algorithm requires. At the end of each iteration in which some weights are
augmented from w to w' = w + δ, the rounding algorithm processes every edge e with
δₑ > 0, in topological order starting from the root, and randomly decides whether to add it to
a growing random edge-cover C ⊆ E: deterministically, if w'ₑ > 1; via a single coin flip, if
e is incident to the root or its parent edge's inclusion in C is already certain; via a coin
flip conditional on the parent edge already being in C, otherwise. Because a coin is only ever
flipped for a child once its parent is (or is already known to be) in C, C always induces a
connected subtree containing the root.
Theorem 11.4 (the goal, p. 231): there is a randomized online algorithm for the group Steiner
problem in trees with competitive ratio O(log²n log k), where n is the number of leaves. It
is built by running T independent trials of the rounding scheme in parallel and taking the
union of the resulting covers, for T chosen (this mission's own explicit derivation — the book
gives only the narrative "we run O(log k log N) independent trials... using simple
probabilistic analysis") so that every group fails to be covered with probability at most
1/(2k), while the union's expected cost stays at T · log(n) · OPT.
Three milestones, in attack order, each stated exactly as the book states it (p. 230-231), with
the book's own caveat "we state the main lemmas and omit the proofs" preserved — no in-source
proof exists for any of the three beyond the algorithm's own description, so each is left sorry
with no invented proof strategy:
ℙ[e ∈ C] = w'ₑ for every edge, and ℙ[e ∈ C] = 1
whenever wₑ > 1 already.C is at most ∑_{e∈T} cₑ w'ₑ (linearity of expectation
applied to Lemma 11.1).g of size at most N with total routable flow wg ≥ 1, the
probability some vertex of g is covered is Ω(1/log N).This is the survey's most involved application of the primal-dual framework: unlike Chapters 5, 9, 10 and 13, which round a single scalar decision per online step, the group Steiner algorithm must couple an entire iteration's worth of edge decisions so that the resulting random set stays a connected subtree — the coin-flip probabilities in the Algorithm box are exactly the minimal adjustment needed to keep marginal probabilities matching the fractional solution while preserving this connectivity invariant online. No formal development of the group Steiner problem (online or offline) was found on the platform as of 2026-09-20; this mission is the first.
Two distinct obstacles. First, faithfully representing "the probability that e ∈ C" for an
online, coupled random process without assuming its proof: the mission represents the
algorithm's random cover as an abstract finite probability distribution RandomCover E and
states each lemma as an implication from the Algorithm box's three coupling rules (transcribed as
hypotheses on marginal and conditional probabilities) to the claimed marginal or expected-value
conclusion — capturing exactly what the book asserts without proof, rather than either assuming
the conclusion trivially or constructing a full multi-iteration coupled process (which the
source's own "we omit the proofs" indicates is genuinely nontrivial, citing [56]). Second,
Theorem 11.4's own competitive ratio is stated in the book only asymptotically, with a purely
narrative derivation ("we run O(log k log N) independent trials... we get a competitive ratio
of O(log n log k log N)... probability at least 1 − 1/k") and no displayed formula anywhere
in the chapter. Per this series' explicit-constants rule, this mission supplies its own explicit
closed form for the number of trials T and the resulting bounds via a standard
Chernoff/union-bound argument applied to Lemma 11.3's constant α; this derivation is the
mission's own (documented below), not a transcription, since none exists in the source to
transcribe.
RandomCover E is a finite pmf p : Finset E → ℝ (Finset E itself finite since E is
Fintype), with marg, condProb and expectedCost/probHits derived from it by ordinary
Finset sums — no measure theory, since the sample space is always finite. RoundedTree E bundles
parent : E → Option E (e(p)) and a non-negative cost. Lemma 11.3's wg (the flow routable to
a group's vertices simultaneously) is left as hypothesis-supplied data rather than defined via an
explicit max-flow formalization, which this mission's scope does not require (welcome
contribution). Theorem 11.4's number of trials is the explicit closed form
T = ⌈(log N · log(2k)) / α⌉, α the (existentially quantified, uniform) constant from Lemma
11.3; its coverage guarantee is 1 − 1/(2k) per group (this mission's own union-bound
derivation), not the book's stated 1 − 1/k — the book reaches the stronger bound via an
additional shortest-path fallback mechanism for any group the trials miss, which is out of scope
here (welcome contribution, along with completing any of the four sorrys and formalizing
Theorem 11.5's extension to general graphs via HST embedding, out of scope since it depends on an
external embedding result not proved in this book).
Search-engine ad-auctions sell items (ad slots) to buyers who arrive with per-item bids and a fixed daily budget, online: each item must be allocated the moment it appears, with no ability to revisit past allocations, and no buyer may ever be charged more than its budget. Buchbinder and Naor's survey [1] models this as a generalization of online bipartite matching and derives an allocation algorithm through the same online primal-dual recipe formalized elsewhere in this series (Chapter 4's framework), applied to a genuinely different LP shape — a maximization (revenue) problem whose "packing" role and "covering" role are the reverse of Chapters 4, 5 and 7 — and to a different constraint structure (budget caps on a per-buyer accumulated sum, not a per-constraint 0/1 covering requirement). This mission covers Section 10.1, "The Basic Algorithm": the single-slot allocation algorithm and its -competitive analysis (Theorem 10.1). Sections 10.2-10.3 (multiple ad-slots via strong duality; stochastic per-buyer spending guarantees) are out of scope — see Formalization scope.
Fix a finite set of buyers, each with budget , and a finite set of items; buyer bids for item , revealed one item at a time in the order enumerated by . Let , carried as an explicit positive parameter. The Allocation algorithm (p. 212), upon each item 's arrival, allocates it to the buyer maximizing (where is buyer 's current primal value); if already, nothing happens (the buyer is "full"). Otherwise it charges buyer the minimum of and its remaining budget, sets the dual allocation variable , sets , and updates for a constant fixed by the analysis. The revenue actually collected from buyer is — the buyer is never charged more than its budget. Unlike Chapters 4/7, this LP's dual (the ad-auctions revenue objective, Fig. 10.1) is the maximization problem being solved online; the "primal" covering LP (, variables) exists only as a duality certificate.
Theorem 10.1 (the goal, p. 212), given the milestone's dual near-feasibility bound and the fact that each buyer's total accrued bids exceed its budget by at most a factor of (Claim (3)'s consequence):
with taken verbatim from the theorem's own statement — the exact formula, not an instantiation. Inequality (10.1) (p. 213), the milestone, is the book's own induction-proved lower bound on a buyer's primal value in terms of its accrued bids: .
Theorem 10.1 is the entry point to a short but influential sub-line of the online primal-dual method — Section 10.2 extends it to multiple ad-slots via strong duality for maximum-weight matching (rather than the weak duality this framework otherwise relies on throughout), and Section 10.3 incorporates stochastic per-buyer spending guarantees, both reusing this section's constant and its limit as (recovering the classic -competitive ratio for the unweighted, unbudgeted case). It is also the first mission in this series to apply the online primal-dual method to a genuine revenue-maximization problem rather than a covering/packing pair with matching roles. No formal development of ad-auctions, budgeted online matching, or this constant was found on the platform as of 2026-09-20 (searches below); this mission is the first.
As with 04-framework's Algorithm 3 and 07-generalized-caching's Fractional Caching algorithm,
the central obstacle is characterizing an online process by its own final output. Unlike those
two chapters, however, step (3)'s update increment varies per allocation (bd, the specific bid
of the item just won), so no closed-form solution of the recurrence exists in general; buyerX is
instead defined as an explicit List.foldl realizing the exact per-step update, over the
(temporally ordered) list of bids a buyer actually won — a faithful, if less immediately readable,
transcription of "the algorithm's output as a function of its own trajectory," in the same spirit
as this series' other closed-form definitions. A second difficulty specific to this chapter: the
book's derivation of inequality (10.1) is itself an induction on iterations (not a single algebraic
step, unlike Eq. (7.2) in 07-generalized-caching), and the theorem's final bound further combines
it with a separate "at most one undercharged iteration" argument (Claim (3)'s conclusion,
p. 214-215) turning the raw accrued-bid bound into one about the actually collected (budget-capped)
revenue — both are stated here as explicit hypotheses (the milestone, and
h_at_most_one_undercharge) rather than derived, since the goal is a faithful statement, not a
proof; both sorrys are documented, not silently discharged.
AdAuctionsInstance I M bundles b : I → M → ℝ, B : I → ℝ (hB_pos), and Rmax : ℝ with
hRmax_pos : 0 < Rmax and hRmax_bound : ∀ i j, b i j ≤ Rmax * B i — the last two as explicit
hypotheses, never derived via Finset.sup, matching 04-framework's d and
07-generalized-caching's k. cParam inst := (1+Rmax)^(1/Rmax) uses Real.rpow (ℝ^ℝ).
buyerX inst i bids folds step (3)'s update over a list of won bids; revenue/actualCharge
realize and its budget-capped charge. Reals throughout. Explicitly out of
scope: Section 10.2's multiple-slot generalization (Theorem 10.2), which requires strong duality
for maximum-weight bipartite matching as an explicit premise (the book: "our analysis... crucially
relies on strong duality") — a substantially different LP structure (an integral matching LP, not
this section's per-buyer budget LP) that this mission's AdAuctionsInstance does not model, and
whose applicability of PrimalDualOnline.LP.strong_duality_adapter (this book's own Theorem 2.2)
was not verified in the time available. Section 10.3's stochastic guarantee (Theorem 10.3) is
likewise out of scope, and its own BRIEF.md-flagged ambiguity (whether its scalar g is
or another aggregate of the per-buyer vector ) was not resolved. Both are natural
follow-on missions, not attempted here. Welcome contributions: completing the two sorrys, and the
Section 10.2-10.3 follow-on mission(s).
Section 4 of this survey derives a simple randomized -competitive algorithm for the online set-cover problem, by rounding the fractional solution the online packing-covering framework produces. An intriguing question the survey poses next: can the same guarantee be achieved deterministically? The standard tool for removing randomness, the method of conditional expectations, requires finding a pessimistic estimator — a potential function whose value the algorithm can track and whose behavior certifies the randomized algorithm's guarantee step by step. Chapter 5 constructs exactly this potential function for the weighted online set-cover problem, and shows that greedily minimizing it online reproduces the randomized algorithm's competitive ratio with no randomness at all. This mission formalizes that construction: the potential function itself (Lemma 5.1) and the correctness guarantee it buys (Theorem 5.2).
Fix a finite universe of elements and a finite family of sets with positive costs , both known to the algorithm in advance (only which elements will actually need covering, and in what order, is unknown). A monotonically increasing assignment of fractional weights to sets is produced online by a fractional subroutine (any - competitive online fractional algorithm — the survey's own Section 4.2 supplies one). An element's weight is . Given a target (a guessed upper bound on the optimal integral cover's cost — the survey handles an unknown optimum by doubling this guess across phases, outside this chapter's own scope), the algorithm maintains a chosen cover and the potential
where and is 's characteristic function. Whenever a set 's weight increases, the algorithm computes both with and without adding to and chooses whichever keeps from exceeding its value before the step (failing only if neither does, which Lemma 5.1 shows cannot happen when ).
Theorem 5.2 (goal, p. 139): given the invariant that Lemma 5.1 maintains throughout a run, (i) every element of weight is covered, and (ii) the chosen cover costs at most .
Lemma 5.1 (milestone, p. 137): the potential function never increases in expectation across a weight-augmenting step, under the algorithm's own randomized choice of whether to add the augmented set to the cover (the internal argument — via the method of conditional expectations — that certifies the deterministic algorithm's choice rule never fails).
This chapter answers, for the online set-cover problem specifically, a question that recurs
throughout online algorithm design: when can a randomized guarantee be derandomized online? The
potential-function technique here is the survey's own template for the answer (it recurs,
per the chapter's Notes section, in the routing algorithm of Chapter 9 and the ad-auctions
algorithm of Chapter 10, both formalized as separate missions in this series) — a self-contained,
reusable instance of "derandomization via an explicit pessimistic estimator" in the online
setting, distinct from the offline set-cover primal-dual and dual-fitting algorithms of this
book's own Chapter 2, already on the platform (PrimalDualOnline.SetCover.*, checked below: a
static instance with no arrival order and no potential function, a genuinely different model).
The central formalization challenge is that Lemma 5.1's own statement, "", denotes the potential's value in expectation under the algorithm's randomized choice — not a single deterministic before/after pair — since the lemma is proved via a probabilistic argument (adding to the cover with probability ) whose role is purely internal to justifying the deterministic algorithm's rule (choose whichever of the two options controls ). Stating the lemma as a bare inequality between two potential values, without the mixture, would either be false (the "add " branch alone can increase ) or would silently smuggle in the derandomized choice as a hypothesis rather than proving it is always available. This mission states the expectation explicitly as a probability-weighted average of the two branch potentials, matching the actual analytic content of the book's proof (equations 5.1-5.6) rather than its final one-line restatement.
SetCoverInstance E T bundles elemSets : E → Finset T (the sets containing an element) and
positive costs c. elementWeight and coveredBy are literal transcriptions of and
"". potential transcribes 's displayed formula verbatim, with n cast from
Fintype.card E. potential_nonincreasing (Lemma 5.1) is the expectation inequality described
above. algorithm_correctness (Theorem 5.2) takes the potential invariant Φ < n² as a
hypothesis (the state Lemma 5.1, applied repeatedly from the initial value , is
what the book's own proof shows every reachable state satisfies) together with an explicit ratio
β standing for "the fractional solution is O(log m)-competitive" (∑ wₛcₛ ≤ βα) — the
book imports this fact from Section 4 as a black-box subroutine rather than re-deriving a
specific numeric constant in this chapter, and this mission does the same rather than re-deriving
Chapter 4's own constant under the (different) substitution the book's prose glosses
over. The conclusion is then the fully explicit α · log n · (3β + 2), matching the book's own
derivation (displayed inequality, p. 139-140) with O(log m) replaced by the parameter β.
This correctly rules out the trivializing formalization in which the O(log m log n) bound is
left as an unquantified existential constant, or in which Φ's invariant is assumed directly as
an unmotivated free hypothesis rather than the fact Lemma 5.1 is what actually establishes.
Reals throughout; Real.log, Real.exp, Real.rpow (via the ^ notation on reals) for the
book's own log, exp and n^{2w_e}. Nothing here is reused from 04-framework
(concurrent draft; per this series' own rule, drafts do not import drafts) even though this
chapter's fractional subroutine is conceptually the same online covering framework — restated
here only as the abstract ratio β, not as a Lean dependency. Welcome contributions: completing
the two sorrys, and formalizing the doubling-across-phases wrapper (Section 5.1's "Obtaining a
Deterministic Algorithm" discussion) that removes the need to know α ≥ c(C_OPT) in advance.
Many online problems — renting vs. buying equipment, routing traffic without knowing future
demand, allocating advertising budget as bids arrive — share a common linear-programming shape:
a covering (minimization) problem whose constraints appear one at a time, or its dual packing
(maximization) problem whose variables appear one at a time, with no ability to revisit past
decisions. Buchbinder and Naor's survey [1] recasts the online primal-dual method, originally
developed for offline approximation in Section 2 of the same survey (already covered on this
platform via the PrimalDualOnline namespace, citing Buchbinder's thesis [2]), as a general
recipe for such online problems, unifying earlier ad hoc analyses of the ski-rental problem
(Chapter 3) and paving the way for the online set-cover, routing, caching, and ad-auction
algorithms formalized elsewhere in this series. This mission covers Chapter 4, "The Basic
Approach": the framework itself and its three founding algorithms.
Fix a finite index set of primal variables with non-negative cost coefficients , and a finite index set of covering constraints, revealed one at a time in the order enumerated by . Each constraint is given by a set (the book's simplified setting, in which every non-zero coefficient equals and every right-hand side equals ; Chapter 14 removes this restriction) and asserts . An online covering algorithm may only increase the , never decrease them, and upon a constraint's arrival must eventually make it hold. The online covering problem is to minimize subject to every revealed constraint, online. Its Lagrangian dual is the online packing problem: a dual variable arrives together with constraint , may only be increased while is being processed, and the objective is to maximize subject to for every — the packing constraint on becomes fully known only once every with has arrived, so it, too, is revealed gradually. , the largest constraint size, is carried as an explicit parameter throughout.
Section 4.2 gives three algorithms solving both problems simultaneously — the same run produces a covering solution and a packing solution — with the same worst-case guarantee but different flavors: Algorithm 1 is a discrete process (each processing round performs a whole number of identical multiplicative-plus-additive updates until its constraint is satisfied); Algorithm 2 is the continuous limit of Algorithm 1 (dual variables increase continuously and follows an explicit exponential of the accumulated dual sum); Algorithm 3 replaces the continuous update with one triggered by an approximate complementary-slackness condition, at the cost of a mild dual infeasibility. All three make essential use of the online order: an algorithm that saw the whole instance up front would trivially solve the offline LP.
Theorem 4.3 (Algorithm 3 — the goal, p. 124):
Theorem 4.1 (Algorithm 1) and Theorem 4.2 (Algorithm 2, p. 118 and p. 121) are the same three-part guarantee for the other two algorithms, with in place of for Algorithm 1 (and its packing solution genuinely integral), and with in place of both and for Algorithm 2 (whose packing solution is exactly feasible, not merely approximately so). The competitive ratios are stated against an arbitrary offline-feasible comparison solution on each side (covering and packing) rather than against an unconstructed LP optimum — the standard weak-duality reformulation of "-competitive", and the one the book's own proofs (which invoke weak duality directly, never LP optimality) actually establish.
The framework converts three qualitatively different design intuitions — the ski-rental-style discrete doubling, the continuous primal-dual differential equation, and complementary slackness — into three algorithms with an identical asymptotic guarantee, , matching the (packing) and (covering) lower bounds the book proves in Section 4.3 (Lemmas 4.5-4.6, not part of this mission). This is the load-bearing substrate for the rest of the survey: Chapter 5's online set-cover algorithm, Chapter 13's bounded-allocation problem, and Chapter 14's general packing-covering constraints all restate this chapter's framework locally rather than re-deriving it, and are formalized as separate missions in this series. Formalizing it here, once, with the exact constants each proof establishes, is what lets those missions cite a single faithful statement instead of three independently-drifting restatements. No formal development of this framework was found on the platform as of 2026-09-20 (searches below); this mission is the first.
The central obstacle is not the algebra of any single algorithm's proof — each is a short, self-contained argument — but stating the guarantee for an online process using only its final output. An algorithm is characterized here by the closed-form relation its update rule establishes between the accumulated dual sum and the primal value (e.g., Algorithm 3's once activated, before), together with primal feasibility as the hypothesis that a run has completed; a formalization that instead handed the algorithm the whole instance in advance, or dropped primal feasibility as a hypothesis, would either trivialize the online promise or make the stated bound simply false. A second difficulty specific to this formalization: Theorem 4.3's own proof bounds the primal cost by splitting it into a piece controlled by the final-state complementary-slackness conditions (immediate from the closed form and the -bound) and a piece controlled by a derivative/telescoping argument over the continuous accumulation process itself — the latter is a genuinely dynamic fact about the trajectory, not just its endpoint, and is recorded as a documented simplification below rather than folded into the hypotheses, since the goal is a faithful statement, not a proof.
CoveringInstance I J bundles S : J → Finset I, c : I → ℝ, and d : ℝ with 0 < d and
∀ j, (S j).card ≤ d as explicit hypotheses (never derived as d := ⨆ j, (S j).card, matching
the book's own presentation and avoiding a vacuous formalization in which d is chosen after
the fact to make the bound trivial). dualSum inst y i := ∑_{j \mid i \in S(j)} y_j. Each
algorithm's output is a noncomputable def from the accumulated dual data to ℝ (alg1X,
alg2X, alg3X), so that "the algorithm's output" is genuinely a function of its dual
trajectory rather than an independently-constrained free variable — ruling out the trivializing
formalization in which and are unrelated variables merely required to satisfy the
conclusion's own inequalities. Reals throughout (ℝ, not ℝ≥0 or ENNReal); Finset.filter
realizes " such that "; Real.logb 2 and Real.log (natural log) match the
book's own log₂ and ln. Reusable beyond this mission: CoveringInstance, dualSum, and the
weak-duality-style "competitive against any feasible comparison solution" pattern, which
05-online-set-cover, 13-bounded-allocation, and 14-general-packing-covering are expected to
restate locally (per this series' own rule against cross-draft imports between concurrent
missions) rather than import directly. Welcome contributions: completing any of the three
sorrys, and formalizing the Section 4.3 lower bounds (Lemmas 4.5-4.6) as a follow-on mission.
Perturbative quantum field theory computes correlation functions of a field by expanding around a Gaussian (free) theory. Every term of that expansion is a Feynman diagram, and the rule that turns a diagram into a number is Wick's theorem: the expectation of a product of Gaussian field modes is the sum, over all ways of pairing the modes up, of the product of the two-point functions of the pairs. The same identity is known in probability and statistics as the Isserlis theorem (L. Isserlis, 1918) and is the standard tool for computing moments of Gaussian vectors; in random-matrix theory the counting of pairings it produces is the origin of the Catalan-number asymptotics of Wigner's semicircle law.
The uploaded source is the Wikipedia article Feynman diagram, which states Wick's theorem for the free scalar field and then, in the section Higher Gaussian moments — completing Wick's theorem, verifies the one-variable case by direct Gaussian integration. This mission formalizes that content: the combinatorics of pairings, the one-dimensional Gaussian moment formulas, and the multivariate identity itself.
Fix and work on with coordinates . Let be a centered Gaussian measure on : a Gaussian probability measure all of whose coordinate means vanish, for every . Its covariance (in the physics reading, the propagator) is
A pairing of the labels is a partition of these labels into unordered pairs; equivalently, a permutation of the labels with and for all (a fixed-point-free involution). The set of pairings is written . For a weight indexed by labels, the Wick sum is
the inner product ranging over the pairs of , each counted once through its smaller element.
In the article's field-theory notation the labels are momenta , the coordinates are the field modes , and the two-point function carries the momentum-conserving delta function, . This mission works with the finite-dimensional Gaussian vector rather than the field, so the delta functions are absorbed into the covariance matrix .
For a centered Gaussian measure on and any labels ,
No hypothesis is imposed on the covariance: it may be singular and the labels may repeat, which is exactly the situation the article's "completing Wick's theorem" section addresses.
Targets 1–3 are the article's displayed Gaussian integrals, target 4 is its pairing count, targets 5–6 are the two explicit consequences it records for the field correlators.
Wick's theorem is the computational content of every Feynman-diagram expansion: once it is available, a perturbative term is a finite sum over diagrams, and the symmetry factors of diagrams are bookkeeping on the pairing set . On the probabilistic side it gives all moments of a Gaussian vector in closed form, which is the entry point to Gaussian chaos expansions, Wiener–Itô integrals, and moment methods for random matrices.
Mathlib (revision 0df444a) has real Gaussian measures gaussianReal, the general class
IsGaussian of Gaussian measures on a topological vector space, the Gaussian integral
, and the double factorial Nat.doubleFactorial, but no
higher-moment formula for Gaussian measures and no Isserlis/Wick statement. The mission therefore
produces new library-level content, not a re-derivation of existing formal results; the result
itself has been classical since 1918 (Isserlis) and 1950 (Wick).
The obvious route — expand the characteristic function and differentiate times at — requires differentiating under an integral sign times and identifying the resulting combinatorial sum with a sum over pairings; both steps are where the formal work lies. Integrability is not automatic from the statement and has to be established (Gaussian measures have moments of all orders, but the product must be shown integrable before any manipulation). The naive attempt to reduce to the independent case by diagonalizing meets a second difficulty: the change of variables must be tracked through the pairing sum, and may be singular, so no invertible whitening transform exists in general. The one-variable case (milestone 3) is not a special case to be waved through either: it is the statement the article singles out, because a naive "each mode pairs with a distinct partner" argument fails when all labels coincide.
The ambient space is EuclideanSpace ℝ (Fin d); measures are Mathlib Measures and Gaussianity
is the Mathlib class IsGaussian, which is defined by every continuous linear functional pushing
forward to a real Gaussian law. Centering is stated as an explicit hypothesis on the coordinate
means, so the measure is not assumed standard and the covariance is unconstrained (in particular
degenerate covariances, and repeated labels , are included). Integrals are Bochner
integrals, which return for non-integrable functions; the statements are nonetheless
non-vacuous because Gaussian measures integrate all polynomials.
Pairings are formalized as fixed-point-free involutions of Fin (2 * n) and the pair product
ranges over , so each pair contributes once. The case is included:
the empty product is , the unique pairing of the empty label set is the identity, and both
sides of the goal equal . The double factorial is Mathlib's Nat.doubleFactorial, evaluated at
2 * n - 1 in truncated natural subtraction, so the value is .
Contributions welcome: the Gaussian moment lemmas (milestones 1–3) as standalone Mathlib-style results, the pairing count (milestone 4) as pure combinatorics independent of the analysis, and any reduction of the goal to the independent-coordinate case.
A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius by hand, and it is natural to ask what guarantee that choice actually buys: how large must be, as a function of the sample size and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.
Fix . Let be the unknown true distribution on with mean vector and covariance matrix , and suppose is light-tailed: there exist and with . Let be independent, identically distributed samples from ; write for their joint law (the -fold product measure) and for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution . Recall from the Gelbrich construction the mean-covariance uncertainty set , and the Gelbrich risk of a loss function over the Gelbrich hull .
Milestone (Theorem 21, concentration inequalities II). There is , depending on only through (not on any finer feature of ), such that for every ,
Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every and ,
With probability at least over the draw of the training sample, the Gelbrich risk
computed from that sample upper-bounds the true risk of every admissible loss function
simultaneously — not just of one fixed chosen in advance. (The paper's part (b), the
analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer of the Gelbrich risk minimization problem, is not
formalized in this mission — see Formalization scope.)
Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, , is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with . Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of and the precise sense in which is "distribution-free" given — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).
The central formalization difficulty is not proving the theorems (both are left as sorry in this
draft) but stating the existential constant correctly. The paper says "depends on only
through " — informally, a promise that is uniform across every
distribution sharing those five parameters, not merely that some exists for each
separately (a vacuously true, much weaker statement obtained by naively quantifying after ).
The correct encoding places before the universal quantifier over : for fixed
, one must work for every with that mean, covariance, and tail
bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee
into a triviality (FAITHFULNESS_TRAPS.md trap 8).
Distributions live on EuclideanSpace ℝ (Fin m); , the law of iid samples, is the
-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "" is that product measure's mass on the event set. All risk and uncertainty-set
definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull,
gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own
namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor
02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can
retire the duplication once those missions are live. The existential constant c is placed before
the universal quantifier over P in both theorems, exactly capturing "depends on P only through
µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class
L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk
minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an
optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent
optimization problem), which is additional infrastructure this mission's time budget did not
cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the
optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an
optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries
hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for
every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching
Assumption 1 (p. 9); both were added after moderation found the goal's original statement,
without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the
risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension-
dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its
downstream guarantees and the asymptotic-consistency results) are out of scope for this mission,
which targets the Gelbrich-risk branch (Theorems 21/22) specifically.
Linear systems are the inner loop of scientific computing: discretized differential equations, least-squares fitting, network flow balances and equilibrium models all end in . Direct elimination solves the system exactly in operations, but for the large sparse systems produced by discretization the cost and the round-off growth make iterative methods preferable: start from an arbitrary vector and apply a cheap update until the residual is small. The question such a method raises is when the iteration converges, and to that the chapter gives a clean sufficient answer: diagonal dominance.
This mission is the third in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers the iterative part of Chapter 5, Solução de Sistemas Lineares.
Let be a real matrix and . Assume for all .
The Jacobi method computes every coordinate of the new iterate from the old one:
The Gauss-Seidel method updates the coordinates in order and uses the values already updated in the same sweep:
Both are instances of an affine iteration associated with an equivalent rewriting .
The matrix is diagonally dominant when each diagonal entry dominates its row:
The goal theorem is Proposição 5.10.1: if is diagonally dominant and x^\\star solves Ax^\\star = b, then the Gauss-Seidel iterates converge to x^\\star from any starting vector.
The milestones are the general facts the source uses to get there: that the limit of a convergent affine iteration is a fixed point of it and hence a solution of the system (Proposição 5.5.1), that a contraction condition with forces convergence to the solution (Proposição 5.5.3), and that the Jacobi sweep has exactly the solutions of as its fixed points (Proposição 5.5.2).
Diagonal dominance is the hypothesis a practitioner can check by inspection, and it is satisfied by the matrices that come from standard finite-difference stencils, from strictly diagonally dominant collocation systems and from many equilibrium models. The theorem says that for those systems Gauss-Seidel needs no spectral analysis and no preconditioner to be safe: convergence holds from any starting vector. The supporting milestones isolate the two halves of the argument — a fixed-point identification and a contraction estimate — in a form reusable for other splittings (Jacobi, SOR, block variants).
Mathlib has Banach's fixed point theorem and the theory of matrix norms, but not the Gauss-Seidel sweep, the notion of diagonal dominance as used here, or the convergence statement, which is what this mission adds.
Gauss-Seidel is not a plain affine map applied coordinatewise: within one sweep the coordinates are updated sequentially, so the new value of coordinate depends on the new values of coordinates . Formalizing the sweep therefore requires a recursion over the coordinate index before the recursion over the iteration counter, and the contraction estimate has to be propagated along that inner recursion. The classical proof compares \\max_i |x_i^{(k+1)} - x_i^\\star| with \\max_i |x_i^{(k)} - x_i^\\star| and needs, for each , a bound that already uses the improved bounds for ; getting that induction right is the substance of the mission.
Vectors are functions from a finite index type with elements to , and convergence is convergence in that finite product space (equivalently, coordinatewise). The Gauss-Seidel sweep is defined through an auxiliary partial sweep: after inner steps the first coordinates carry their new values and the remaining ones their old values, and the full sweep is the partial sweep after steps. The Jacobi sweep is defined directly. Diagonal dominance is the strict inequality above, with the sum taken over the row with the diagonal index removed; for every statement is vacuous, and the goal theorem is then trivially true because the space has a single point. Division by the diagonal entry is total division, so the definitions make sense even when ; diagonal dominance rules that out, because the right-hand side of the dominance inequality is nonnegative. The goal theorem assumes a solution x^\\star is given rather than asserting its existence, and it asserts convergence for every starting vector, generalizing the source's choice . The contraction milestone states the consistency of the norms as the hypothesis in the supremum norm rather than fixing a particular matrix norm.
Most equations that arise in applications cannot be solved in closed form: the age of the Moon from a radioactive-decay balance, the deflection of a clamped beam, the equilibrium of a catenary, all reduce to solving for a function with no algebraic inverse. A first course in numerical methods therefore opens with root finding: constructive procedures that produce a sequence of approximations together with a theorem saying that the sequence converges to a root and how fast.
This mission is the first in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (Departamento de Computação e Estatística, UFMS, 2000). It covers Chapter 3, Zeros de Funções, whose capstone is the local convergence of Newton's method.
Let and let be a zero of , i.e. . The chapter studies three constructions.
Bisection. Starting from an interval with , put and keep the half of on whose endpoints still changes sign. The width of the bracketing interval is halved at every step.
Linear iteration (MIL). Rewrite as a fixed-point equation and iterate from an arbitrary .
Newton's method. Take the particular iteration function
obtained by truncating the Taylor expansion of at after the linear term.
A sequence has order of convergence when tends to a finite constant, where ; is linear and quadratic convergence.
The goal theorem is the local convergence of Newton's method at a simple zero. If is twice differentiable on an open interval containing , its second derivative is continuous there, and never vanishes on , then there is such that
where is the Newton sequence started at . This is the formal content of the chapter's statement that Newton's method converges provided the initial guess is chosen close enough to the root.
The milestones are the supporting results of the chapter: the error bound and convergence of bisection, the convergence of the linear iterative method under a derivative bound , the a posteriori estimate , and the quadratic order of Newton's method at a simple zero.
Bisection, fixed-point iteration and Newton's method are the three root finders every numerical-analysis course starts with, and the three convergence theorems above are what justifies using them. The a posteriori estimate is what turns the iteration into an algorithm with a stopping criterion: it bounds the distance to the root by a quantity the program can measure. The quadratic order statement explains the observed doubling of correct digits per step at a simple zero and its loss at a multiple zero.
On the formalization side, Mathlib already has a fixed-point theorem for contractions on complete spaces and the mean value theorem, but not the statements in the form used in numerical analysis: bisection with its explicit bracket, the a posteriori bound, or Newton's local convergence and quadratic rate stated for the concrete iteration sequence. This mission asks for those.
The delicate point in all three theorems is that the iterates must be known to stay in the region where the hypotheses hold; the informal proofs assume this silently. For the linear iterative method the mission therefore states the invariance hypothesis explicitly ( maps the closed interval into itself). For Newton's method, no such hypothesis is given: the existence of a neighbourhood of that the iteration preserves is part of what must be proved, and it comes from the continuity of together with . The quadratic-order milestone also has to handle the degenerate possibility , which would put a zero in the denominator; it is excluded by hypothesis.
Everything is over the real numbers. The iterations are given as explicit recursive sequences: the bisection construction returns the bracketing pair and its midpoint, and there are separate sequences for the fixed-point and Newton iterations. Newton's method takes the derivative as a separate function argument , tied to by a hypothesis of the form " has derivative at every of the interval"; this avoids relying on any junk value of a derivative operator where fails to be differentiable. Division is total, so a step at a point where vanishes would leave the iterate unchanged; the hypotheses exclude this inside the interval.
Two deliberate deviations from the source are worth flagging for the auditor. First, Proposição 3.5.1 assumes only for , but its proof divides by ; the formal statement assumes on the whole interval, so is a simple zero. Second, the convergence statement for the linear iterative method adds the hypothesis that maps the closed interval into itself, without which the iterates may leave the region where the derivative bound is assumed.
A table of values is all one has of many functions: measurements, tabulated physical constants, the output of an expensive simulation. Interpolation reconstructs a function between tabulated points by passing a polynomial through them, and it underlies much of the rest of numerical analysis — quadrature rules, finite-difference formulas and predictor-corrector schemes for differential equations are all obtained by integrating or differentiating an interpolating polynomial. What makes the reconstruction trustworthy is a formula for the error committed away from the nodes.
This mission is the fifth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 7, Interpolação.
Let be distinct nodes and the tabulated values of a function . The Lagrange form of the interpolating polynomial is
so that for every , and is the unique polynomial of degree at most with this property.
The interpolation error at a point that is not a node is the difference .
The goal theorem is Proposição 7.3.1: if is times differentiable on and all nodes lie in , then for every different from all nodes there exists with
The milestones are the other results of the chapter needed to make sense of it: the existence and uniqueness of the interpolating polynomial of degree at most through points with distinct abscissas (Proposição 7.2.1), the fact that the Lagrange formula does interpolate the data, and the practical error bound of Proposição 7.3.2, when .
The error formula is the reason interpolation is a numerical method and not just a curve-drawing device: it shows that the error is governed by two independent factors, the smoothness of through and the geometry of the nodes through the product . Everything downstream follows from it — the and error terms of the trapezoidal and Simpson rules in the next mission are obtained by integrating exactly this expression, and the choice of Chebyshev nodes is the attempt to make the product factor small.
The standard proof introduces the auxiliary function with chosen so that , and then applies Rolle's theorem times to conclude that vanishes somewhere. Formalizing the repeated application of Rolle's theorem, keeping track of the distinct zeros and the nested intervals they generate, is the substance of the work; it is an induction that has to be organized carefully rather than a computation.
The nodes are given as a strictly increasing family of reals lying in the open interval , and the interpolating polynomial is the explicit Lagrange sum rather than an abstract polynomial: at a node it is defined by the same formula, whose factors then include contributions unless the nodes are distinct, which is why the distinctness hypothesis appears in the interpolation milestone. Smoothness is expressed as continuous differentiability of order on the open interval , and the derivative appearing in the error term is the iterated derivative computed within that set; since the set is open this agrees with the ordinary -st derivative. The evaluation point is assumed to lie in and to differ from every node; the point is asserted to exist in , with no claim of uniqueness or of any relation to beyond membership in the interval. The uniqueness milestone is stated with Mathlib's polynomial type and the degree bound , which includes the zero polynomial.
Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).
A (finite) Markov decision process consists of a finite set of states , a finite set of actions , a transition kernel giving the distribution over the next state after taking action at state , and an expected reward for that transition. A (stationary) policy assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing turns the MDP into an ordinary Markov chain on : at each step the agent is at some state , draws , receives (expected) reward , and moves to a state drawn from . For a discount factor , the value of at is the expected discounted sum of future rewards starting from ,
and the state-action value function is the analogous quantity for taking at and then following . Marginalizing the raw kernel and reward over the mixed action gives the induced transition matrix and induced reward vector — the objects that turn 's value into a genuinely linear-algebraic quantity. A policy is optimal if for every policy and every state ; write for its value function.
Theorem 17.10 (goal). For a finite MDP and a fixed policy , the matrix (with the policy-induced transition matrix) is invertible, and 's value function is the unique solution of the Bellman equations, given in closed form by
Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:
Theorem 17.7 (milestone). A policy is optimal if and only if it places probability only on -maximizing actions: for every with , .
Theorem 17.11 (milestone). The Bellman optimality operator , , is a -contraction for ; consequently, for any starting vector , the value-iteration sequence converges to a fixed point of .
Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ( iterations for -accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor , not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).
The obvious shortcut for Theorem 17.10 is to assert is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that , being row-stochastic (every row of sums to exactly , since and are both proper distributions), has operator norm exactly, so strictly; this rules out as an eigenvalue of , which is exactly what invertibility of requires. The same fact, applied differently, drives Theorem 17.11: showing is -Lipschitz requires bounding by comparing the maximizing action for against the same action's value under (not 's own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.
States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and
reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel
asserting the required distribution property explicitly rather than assuming it silently. A
policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every
s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own
quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine
mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit
state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition
17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a
unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather
than one being definitionally true of the other. The trivializing formalization this rules out
is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and
calling the resulting identity a theorem; both would erase the mission's actual content.
Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model
with a termination-probability deficit rather than exact row-stochasticity, and
FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither
specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted
convention, so every definition here is drafted fresh rather than imported. This chunk covers
§17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration);
§17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning
algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a
stochastic-approximation convergence substrate this mission does not build.
Operations research and applied probability are full of questions of the shape "is X riskier, larger, or later than Y?" when X and Y are random: two queueing disciplines' waiting times, two inventory policies' shortfall, two insurance portfolios' claim size. Comparing their means answers a weaker question than the modeler usually wants, since two distributions can share a mean while one is uniformly the "worse" one to face. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) is the standard reference for the family of orders built to make "X is stochastically no larger than Y" precise, and this mission formalizes the foundational member of that family: the usual stochastic order, together with its central structural theorem.
Let be a real-valued random variable on a probability space , and let be a real-valued random variable on a (possibly different) probability space . is smaller than in the usual stochastic order, written , if
Equivalently, for every : 's cumulative distribution function never exceeds 's. Two features of the definition matter for everything that follows. First, it is a comparison of distributions, not of jointly defined variables — and need not live on the same probability space, and the order depends only on their laws. Second, the inequality must hold for every threshold simultaneously; it is not a comparison of two summary statistics such as means or medians, and a distribution can fail even while .
A closely related order compares residual lifetimes rather than raw tail probabilities. is smaller than in the hazard rate order, written , if the survival functions , satisfy for all — the general, density-free form of the condition that for absolutely continuous distributions reduces to a pointwise comparison of hazard rates . It is one of several stronger orders (alongside the likelihood ratio order) that the book shows all imply , and it is the mission's second definition.
This is the order's Strassen-type coupling theorem: holds exactly when copies of and can be realized on one common probability space so that, almost surely, the copy of never exceeds the copy of . It is the weakest possible statement with this shape (existence of some coupling on some space, not a canonical one), and it is the archetype every later chapter's own coupling theorem — for the hazard rate order, the convex order (via a martingale coupling), the multivariate orders — restates for its own comparison.
The usual stochastic order is the weakest and most widely used of the book's orders, and the coupling theorem is the tool that makes it tractable: comparing tail probabilities for every threshold is an infinite family of inequalities, while exhibiting one coupling on one space settles the comparison in a single stroke. This is the technique behind, among many applications in the book and the wider literature, comparing waiting times across queueing disciplines, bounding the effect of parameter uncertainty on a risk measure, and proving monotonicity results for Markov chains by coupling their sample paths. The closure properties (Theorem 1.A.3) are what let such comparisons survive composition with a monotone payoff function or a sum of independent components — exactly the operations a queueing or inventory model performs on its primitives.
Formalizing this theorem establishes, in one place, both the statement and the exact shape of its
existential witness (a genuine ∃ over a probability space and two identically distributed
random variables, not merely two abstractly-known-to-exist objects), which is the piece every
later chapter's own coupling theorem in this series needs to get right independently. No proof is
attempted in this mission; the book's own three-line construction (, for a uniform ) is a natural target for a future proof-bearing pass.
The definitional trap is the "for all " in : it is tempting to shortcut it into a comparison of one summary statistic (a mean, an essential supremum, a specific quantile), which is uniformly weaker and would make Theorem 1.A.1 either false or a different, easier theorem. The coupling theorem itself has a second trap in its existential structure: the common probability space must be genuinely quantified — fixed neither to nor in advance — and "" is equality of the two random variables' laws, not almost-sure equality of and themselves (they typically do not share a domain before the construction). Theorem 1.A.3(b)'s general statement, for an arbitrary increasing on independent families, is easy to understate as only its convolution corollary; the book gives both, and the general statement is the one with the actual content (the sum is recovered by taking to be the coordinate sum, itself increasing).
Random variables are represented as measurable functions into from arbitrary
measurable spaces, and "equality in law" is Mathlib's native ProbabilityTheory.IdentDistrib,
which is defined for two (possibly different) probability spaces and requires almost-everywhere
measurability rather than fixing an ambient space in advance — matching the book's own treatment
of as a comparison between distributions. UsualOrder μ ν X Y and HazardRateOrder μ ν X Y both take on and on a
separate , so no theorem here can be trivialized by silently forcing and
onto one shared space. HazardRateOrder is stated via the survival-function cross-product
inequality (Eq. 1.B.4), the form that needs no absolute-continuity hypothesis, rather than via a
derivative-based hazard rate, so it applies to the same general random variables as UsualOrder
without an extra regularity hypothesis the book itself does not require at this level of
generality. Independence in Theorem 1.A.3(b) is Mathlib's ProbabilityTheory.iIndepFun; the
random variable of Theorem 1.A.2 is left valued in an arbitrary measurable space, matching
the book's unrestricted statement, rather than narrowed to -valued for convenience. A
trivializing formalization is ruled out explicitly: is not formalized as a comparison
of means, medians, or any single moment, and the coupling theorems' ∃ is a genuine existential
over a probability space, not a hypothesis smuggling in the witness's existence.
This mission draws on no platform prior art (repeated searches for "stochastic order", "coupling",
"Strassen" and "identically distributed" turned up nothing on-topic as of 2026-09-18); it is the
first mission in a nine-chapter series covering the whole book, and its own definitions are not
imported by later chapters — each restates locally what it needs, per the series' own convention
that draft items cannot import another draft's definitions. Reusable beyond this mission: the
UsualOrder/HazardRateOrder shape (parametrizing over two separate probability spaces) is the
pattern every later chapter's own order definition follows.
Estimating a covariance matrix from samples is a canonical high-dimensional problem: the natural estimator, the sample covariance , is consistent in operator norm only when , which fails outright in the regime common to modern applications. When is additionally known to be sparse — few nonzero entries per row — a simple fix restores consistency even when : threshold every entry of below a data-dependent level to zero. This mission formalizes the matrix concentration machinery behind that fix and the resulting guarantee, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 6.
For a random matrix , the matrix variance is , and the Loewner order on symmetric matrices means is positive semidefinite. A zero-mean symmetric random matrix satisfies Bernstein's condition (Definition 6.10) with parameter if for — the matrix analogue of the scalar Bernstein condition of Chapter 2. The operator (spectral) norm is 's largest singular value.
Given a threshold , the hard-thresholding operator is , extended entrywise to matrices (Eq. (6.52)). A covariance matrix 's sparsity pattern is captured by its adjacency matrix (p. 181); always, with equality only when has no zero entries, and whenever has at most nonzero entries per row.
Let be i.i.d. zero-mean random vectors with covariance , each coordinate sub-Gaussian with parameter at most . If , then for any , the thresholded sample covariance with satisfies
The error scales with the graph sparsity , not with directly — the whole point of thresholding when the ambient dimension is much larger than the sample size.
For independent, zero-mean, symmetric random matrices satisfying Bernstein's condition with parameter ,
This is the general matrix concentration tool the whole chapter builds toward; Theorem 6.23 is one of its corollaries.
For any with , — a purely deterministic fact, with no probability involved, that reduces Theorem 6.23's proof to a single probabilistic input: controlling .
Theorem 6.17 is the workhorse of the whole chapter: besides Theorem 6.23, it also underlies Corollary 6.20's operator-norm bound for the unstructured sample covariance matrix (used in turn for the two example ensembles in Section 6.4.5), by taking . Theorem 6.23 itself is the standard justification for thresholding-based covariance estimators used throughout high-dimensional statistics whenever the sparsity pattern of , though unknown, is believed to be structured.
Formalizing it. No faithful prior art exists on the platform for the matrix Bernstein bound
or covariance thresholding (a fresh search for "matrix Bernstein," "Bernstein condition
matrix," "thresholding covariance," and "sparse covariance" returned no hits). The existing
RademacherWigner.* items formalize spectral-edge and empirical-spectral-distribution bounds
for the Wigner ensemble specifically (a symmetric matrix with i.i.d. entries) — a narrower,
different random-matrix model from the general Bernstein-condition matrices this chapter treats,
and not reused here. All three theorems are drafted as open goals (:= by sorry).
The naive approach to a matrix tail bound — apply the scalar Chernoff/Bernstein technique directly to the operator norm — fails because the operator norm is not a linear functional of , so the scalar moment generating function bound does not translate directly. The resolution (Lemma 6.13, not itself part of this mission) instead bounds the trace of the matrix exponential of the sum, which is linear-algebraically tractable via the Golden–Thompson-type inequality and the union bound over the (at most ) nonzero eigenvalue directions of the aggregate variance — this is exactly why the bound's prefactor is , not the ambient dimension : a low-rank aggregate variance (e.g. from a highly structured collection of matrices) yields a much tighter bound than a naive union bound over all eigen-directions would. Theorem 6.23's own difficulty is entirely in the reduction to Theorem 6.17 plus Eq. (6.54): checking that satisfies the Bernstein condition with the stated parameters, and that concentrates at the stated rate via a union bound over the matrix entries.
"Symmetric" is realized via Mathlib's Matrix.IsSymm; the Loewner order via
(B-A).PosSemidef. The matrix moment generating function itself (ΨQ(λ):=E[e^{λQ}]) is not
formalized, since none of this mission's three theorem statements need it directly — Bernstein's
condition (Definition 6.10) is stated purely in terms of polynomial moments ,
avoiding the substantial extra machinery (Mathlib's NormedSpace.exp for matrices) that a
faithful matrix-exponential definition would require, at no cost to faithfulness for the three
statements actually drafted.
Independence of / is realized via Mathlib's iIndepFun; this required adding
a local MeasurableSpace (Matrix (Fin d) (Fin d) ℝ) instance in the workspace, since Matrix is
a def, not an abbrev, over the underlying Pi type, so Lean's instance search does not
automatically find the Pi-type MeasurableSpace instance for it. "Identically distributed" is
realized via Mathlib's IdentDistrib against a fixed reference index. "Each component
sub-Gaussian" is restated locally as an explicit MGF bound at the reference index, per this
book's cross-chapter rule against importing another chapter's draft definitions.
If a statement admits a trivializing formalization: the rank(...) prefactor of Theorem 6.17
is kept exactly, not replaced by the ambient dimension (which would be a strictly weaker,
non-trivializing but unfaithful simplification, since the bound's whole point is that
rank(...) ≤ d can be much smaller). ‖·‖_max and opNorm at d=0 return Mathlib's junk
value 0 (harmless: no matrix entries or singular values exist at that degenerate size either).
Out of scope for this mission: Theorem 6.15 (the sub-Gaussian-tail matrix concentration result
that precedes Theorem 6.17 in the same section) and Corollary 6.20 (the unstructured
covariance-estimation corollary) — both natural follow-on work, cut for this chunk's time
budget; see STATUS.md.
Ranking is the learning problem behind search engines, recommendation systems and fraud-alert
triage: what matters is not a single classification decision but the relative order the system
assigns to a set of items, because a user or analyst can only act on the very top of a ranked
list. Chapter 10 develops margin-based generalization theory for the score-based ranking
setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a
genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of
two positions, and the chapter's bound must therefore control two marginal complexities rather
than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style
empirical-error guarantee proved by the same normalization-factor telescoping argument as
chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.
A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a
preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a
scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The
empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk
05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a
pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and
R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem
10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population
form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's
Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}.
Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces
RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^-
(Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds
RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma
7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a
standing fact of the boosting series) to give RankBoost's own margin-based guarantee.
Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0,
with probability at least 1-δ, for all h∈H:
Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x),
feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).
Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.
Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).
Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's
Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x'
alone and a term on x alone, each bounded by the Rademacher complexity under its own
marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a
single-sample bound would either be false or silently assume D1=D2 (which only holds for a
symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct
theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk
07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping
product of normalization factors Z_t), but with genuinely different per-round quantities
(ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per
BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not
convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of
boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on
the platform: GET /theorems?q=ranking%20loss returns zero hits.
Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s
Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and
σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating
a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery
applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md
names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity
4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same
telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t,
ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own
recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost
Lean.
MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/
RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates
chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull
definition — all duplicated rather than imported since a draft item cannot import another
chunk's draft module, and none is listed as reusable in missions/README.md's "Published
definitions" table at the time of this session. D1, D2 are computed directly as
Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal
hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of
the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit
upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's
pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in
r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned
function f are modeled as their own recursively-defined algorithm state (mirroring chunk
07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from
RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per
BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to
RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis
connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No
numerical constant is altered from the book in any of the four theorems.
Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived
from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate
descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite
ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20,
explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria),
out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's
and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is
not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.
In the Standard Model the scalar sector consists of a single complex doublet. The general Two-Higgs-Doublet Model (THDM) replaces it by two complex doublets of the same weak hypercharge . This is the minimal extension of the scalar sector that is still renormalisable and gauge invariant, and it is forced on any supersymmetric completion: the Minimal Supersymmetric Standard Model has exactly two Higgs doublets. Before any phenomenology can be done with such a model, two questions have to be answered for the given parameter point: is the scalar potential stable, i.e. bounded from below, and does its global minimum break down to the electromagnetic ?
The general THDM potential has real parameters, and answering these questions directly in field space — eight real scalar degrees of freedom, of which three are gauge — is unwieldy. Maniatis, von Manteuffel, Nachtmann and Nagel (2006) proposed a reformulation in terms of gauge-invariant bilinears, in which the gauge orbits of the Higgs fields are parametrised by a Minkowski-type four-vector confined to the closed forward light cone, and the potential becomes a quadratic polynomial on that cone. In these variables the stability question reduces to a one-variable problem: the sign of an explicit rational function on a finite set of at most ten real numbers. This mission formalizes that analysis: the gauge-orbit parametrisation (their Theorem 4), the classification of the stationary points of the potential (their Theorem 2), and the stability criterion itself (their Theorem 1).
Write the two doublets as rows of a complex matrix,
and form the hermitian matrix of gauge-invariant scalar products , i.e. . Decomposing in the Pauli basis gives four real functions
Positive semi-definiteness of is equivalent to and : the four-vector lies on or inside the forward light cone. A gauge transformation acts as with , and leaves invariant.
The most general gauge-invariant renormalisable potential is
with real parameters , and a real symmetric matrix . For one sets , so that , and
Stationary points of on the ball are governed by the functions
where is a Lagrange multiplier for the constraint . The finite set collects: every regular with ; the point when ; and every eigenvalue of at which stays finite and . It has at most ten elements, and is exactly the set of stationary values of .
For the stationary points of the full potential one uses four-vector notation , , and the metric , so that on the domain , , with .
For the potential is stable for , marginal for and unstable for . For ,
and if on with equality somewhere, the sign of — replaced by when is an eigenvalue of — decides between stability in the weak sense and instability.
Theorem 4 (gauge orbits); the four stability cases (a), (b.2), (b.3), (b.4) of Section 4 including the criterion for the marginal case; equation (4.39) identifying the stationary values of with ; equations (4.42)–(4.44) giving at those stationary points; and Theorem 2, the classification of the stationary points of .
The criterion is a decision procedure: given the parameters of a THDM, stability is settled by evaluating one rational function at the roots of another, without any search in field space. The authors use it to re-derive the known stability conditions for the MSSM potential and to settle the stability and symmetry-breaking properties of the THDM potential of Gunion et al., for which , and come out as the strong-stability conditions. Theorem 4 is what makes the whole approach legitimate: it says that nothing is lost in passing from fields to the invariants , because the fibres of that map are exactly the gauge orbits.
The results are established in the published literature; what this mission adds is machine-checked proofs. The statements are not present in Mathlib in any form, and the note added in version 3 of the paper — a condition for the marginal case that was missing in the original version — is a concrete reminder that the case analysis here is easy to get subtly wrong.
The obvious route to stability is to minimise directly; it fails because the domain is a cone with a boundary, and the minimisation over the boundary introduces a Lagrange multiplier whose admissible values are the roots of , including the degenerate "exceptional" solutions where is singular. Those exceptional solutions are not a technicality: they are where the eigenvalue clauses of , the correction in (4.43), and the junk-value behaviour of matrix inverses all live. The marginal case ( and vanishing simultaneously somewhere) is not decided by the signs alone and needs the quantitative bound .
Vectors in are plain functions Fin 3 → ℝ with an explicitly defined dot product; is a Matrix (Fin 3) (Fin 3) ℝ and its symmetry is carried as a hypothesis. Four-vectors are indexed by Unit ⊕ Fin 3 so that and are block matrices, with the first component being . Higgs configurations are complex matrices and ; a gauge transformation is with .
Stability is formalized as the honest statement that is bounded from below on the physical domain , — not as any of the sign conditions that the theorem derives — so none of the implications is true by definition. Matrix inversion in Lean returns the zero matrix at a singular argument; every occurrence of is therefore guarded by a regularity hypothesis, and the values of at an eigenvalue of are defined as limits, with the existence of those limits part of the membership condition for . The projection is characterised by its defining property (it lies in the eigenspace and is orthogonal to it) rather than by a choice of eigenbasis.
A complete development needs linear algebra over (resolvents, symmetric matrices, eigenspaces), and the spectral decomposition of positive semi-definite complex matrices for Theorem 4, and elementary real analysis (compactness of the ball, limits of rational functions) for Section 4. The gauge-orbit statement and the light-cone parametrisation are reusable for any multi-doublet scalar sector; contributions of the -doublet generalisation (Appendix B, Theorem 5) are welcome as follow-ups.
Every convergence-rate result in the preceding chapters is an upper bound: some specific estimator (the Lasso, PCA, kernel ridge regression) achieves a given error rate. A natural and much harder question is the complementary one: is that rate actually the best any procedure could achieve, no matter its computational cost? Answering this requires a theory of lower bounds that holds simultaneously for every conceivable estimator — a fundamentally different kind of argument from constructing and analyzing one particular algorithm. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 15, develops this theory, unifying classical techniques (Le Cam, Assouad, Fano) under one reduction: converting continuous estimation into discrete hypothesis testing.
Let be a sample space and a class of probability distributions on . A functional assigns each distribution a parameter of interest. An estimator is a measurable map . Fix a semi-metric — symmetric, triangle-inequality-satisfying, , but possibly for — and an increasing . The minimax risk is
the smallest worst-case expected loss achievable by any measurable estimator (Eq. (15.2)).
Given a 2δ-separated set
(every pair satisfies ) with representative distributions
, Wainwright constructs a testing problem: sample
uniformly from , then ; write for the resulting joint law of
. A test function attempts to recover from ; its
error probability is .
For any increasing and any 2δ-separated set with its induced joint testing measure
,
This mission formalizes Proposition 15.1 alone (see Formalization scope below for why, and what a follow-up mission would add to reach Fano's method proper, Proposition 15.12).
Proposition 15.1 is the single reduction every subsequent technique in the chapter specializes: Le Cam's two-point method (Lemma 15.9, , bounding the testing error via total variation distance), Fano's method (Proposition 15.12, bounding it via mutual information and Fano's inequality), and Assouad's method (a different, hypercube-based packing). Formalizing it in full generality — general , general semi-metric, general -ary packing set — gives a single reusable lemma that a future mission proving any of these specific bounds can build on directly, rather than re-deriving the reduction each time.
The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the reduction, in a form composing with any future formalization of the chapter's testing-error bounds (total variation, Fano, or otherwise).
The proof combines two ingredients that must each be kept in their sharpest form: Markov's inequality applied to (which only needs increasing, not convex or any specific shape — a premature specialization to would silently prove a weaker, less reusable statement), and the reduction of any estimator to a test via nearest- packing-point assignment (Eq. (15.4)), which uses the triangle inequality on in a specific direction (bounding from below via and ) to show that a small estimation error forces the induced test to be correct. Getting the direction and strictness of every inequality right — non-strict separation, but strict distance in the "test is correct" event — is where a naive restatement goes wrong.
, are arbitrary measurable spaces; the distribution class is
realized as an indexed family measure : Idx → Measure 𝒳 rather than a bare set of measures,
composing directly with θ : Idx → Ω. The semi-metric is a bare function with explicit
nonnegativity/reflexivity/symmetry/triangle-inequality hypotheses, matching the book's own
footnote definition, rather than Mathlib's PseudoMetricSpace typeclass (kept self-contained,
no extra instance machinery). The minimax risk is valued in ENNReal via the lower Lebesgue
integral ∫⁻, not the Bochner integral, specifically to avoid the non-integrable-loss junk
value 0 that a Bochner-integral formalization would silently introduce — a trivializing
formalization would use ∫ (Bochner) here, letting a non-integrable loss vanish and making the
inequality easier to satisfy than the book's actual claim; this mission does not do that. The
joint testing measure is characterized by its slice-measure equations directly on the
product space , avoiding Mathlib's general conditional/disintegration
machinery while remaining exactly equivalent to " uniform, ".
Disclosed major scope decision. BRIEF.md recommended Proposition 15.12 (the Fano bound
itself, Φ(δ)(1 - (I(Z;J)+\log 2)/\log M)) as this mission's goal. That statement requires, in
addition to everything above, a formalized notion of mutual information between a
finite-valued and a general (possibly continuous) random variable, and its use of a Fano-type
inequality (Eq. (15.31), itself deferred by the book to "Section 15.4" and not fully quoted in
the brief). Building a faithful mutual-information formalization general enough for this
setting (finite , arbitrary measurable ) — matching Mathlib's or this repo's existing,
narrower information-theoretic developments (SourceCoding.*, built for a different,
channel-coding purpose per BRIEF.md's own prior-art note) or building one from scratch — is
substantially more than this session's remaining budget after building and self-reviewing
08-pca and 07-sparse-linear. This mission instead formalizes Proposition 15.1, the
foundational reduction Proposition 15.12 itself specializes (via a particular bound on
), so that a follow-up mission can add the mutual-information/Fano
step on top of HighDimStat.Minimax.estimation_to_testing without redoing this reduction.
This mission's name, fixed from missions/README.md, still names "Fano's Method" as the
series slot this chunk occupies; its actual content is the reduction step every method in that
family (including Fano's) shares — recorded explicitly here and in STATUS.md, not left
implicit.
Regression is usually taught with a fixed parametric model: linear regression fits a -dimensional coefficient vector, and the estimation error is controlled by . Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size ? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.
Fix design points in an arbitrary covariate space (fixed, not random — this is the fixed-design setting) and observe
where is the unknown regression function, is a known noise level, and are i.i.d. standard Gaussian. Given a class of candidate functions, the nonparametric least-squares estimate is any minimizer
Error is measured in the empirical (design-dependent) seminorm . A class of functions is star-shaped if and together imply — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class and radius , the local Gaussian complexity
measures how much a mean-zero Gaussian process can be made to look like a member of restricted to the ball of radius . A critical radius is any positive solution of ; by Lemma 13.6, is non-increasing on star-shaped, so this inequality always has a smallest positive solution.
Lemma 13.6. For any star-shaped , is non-increasing on , and consequently has a smallest positive solution for every .
Theorem 13.5 (special case, ).
Theorem 13.13 (goal — general oracle inequality, not assumed in ). With solving the critical inequality for , there are universal constants such that for all ,
with probability at least . The goal is deliberately the statement with unresolved universal constants and an infimum over , rather than any single instantiated bound, so the target survives sharper constant tracking.
Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding for a particular and reading off . Its value is that it isolates exactly the one place where the geometry of enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.
The naive route to Theorem 13.13 is to bound pointwise via the basic inequality and then bound the right side by for — but is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius is what makes the per-annulus bound tight enough for the final sum to converge.
Design points are an arbitrary type X (no topology or metric structure is needed for the
statements themselves); the least-squares estimate is represented as a Prop
(IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching
the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian
complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector
on an abstract probability space, with the inner supremum taken over the subtype of the
radius-restricted slice of the class — this is well-defined (not the junk value 0 of an
unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any
nonempty star-shaped class (taking exhibits in the class). Since neither X nor
H carries a topology, separability or countability constraint, SatisfiesCriticalInequality
adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding
against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable
integrand — a value that would otherwise trivially satisfy the critical inequality for every
positive δ, regardless of the function class's actual local complexity. The trivializing
formalization to rule out here is stating Theorem 13.13's universal constants after the
quantification over the function class and sample size, which would let
secretly depend on the instance and make the "universal" claim vacuous; this mission places
the constant quantifiers first, before the class, design and noise data they must not depend
on. A complete downstream development would add: the concentration-of-Gaussian-complexity step
(Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy /
Dudley-integral machinery of Section 13.2.1 for bounding explicitly on concrete classes
(Sobolev balls, RKHS balls) — none of which is attempted here.
Every convex optimization algorithm in machine learning — from projected gradient descent to support vector machines to the mirror-descent methods of later chapters of this book — is justified by a small set of optimality certificates: a checkable condition on a candidate solution that guarantees it actually solves the problem, without searching the whole feasible set. The most widely used such certificate is the Karush–Kuhn–Tucker (KKT) system: a set of gradient and complementary-slackness equations that a solution of a convex program with differentiable data must satisfy, and that (under a mild constraint qualification) is also sufficient. It is the tool a practitioner reaches for to check optimality of a numerical solver's output, and the tool a theorist reaches for to derive an algorithm (dual ascent, augmented Lagrangian, interior point methods) in the first place. Every convex machine learning model introduced in Chapter 1 of this book — regularized least squares, support vector machines, logistic regression with constraints — is an instance of the general convex program these milestones analyze.
The result traces back to Kuhn and Tucker's 1951 paper Nonlinear Programming, with Karush's 1939 unpublished thesis establishing the same conditions independently and earlier; Slater's 1950 unpublished note is the source of the constraint qualification that bears his name and that makes the necessity direction possible. Lan's Chapter 2 gives a compact, modern, purely finite-dimensional derivation of the whole chain — separation, duality, saddle points, KKT — from first principles, self-contained in about twenty pages, aimed squarely at the convex programs that appear in machine learning.
Fix and work in with its standard inner product . A convex program (2.3.16) is
where is a nonempty closed convex set, are convex, and are affine. A point is feasible if it satisfies every and ; is optimal if it is feasible and for every feasible .
The normal cone of at is — the set of directions that make an obtuse angle with every direction into from ; it is when , recovering unconstrained first-order optimality. The Lagrangian is for multipliers , ; the Lagrange dual value is , and the Lagrange dual problem is . Weak duality, , holds unconditionally by construction. Slater's condition asks for with , ; the restricted Slater condition weakens the interior requirement to the relative interior while keeping strict inequality for every (here: every) nonlinear constraint.
Each of these five is stated the way the book states it — no constant is hard-coded, no O(·) is involved, and every hypothesis (closedness, convexity, Slater/restricted-Slater) is exactly the one the corresponding proof uses.
The KKT system is the interface between convex optimization theory and every algorithm that
exploits it: primal-dual methods track approximate KKT residuals as a stopping criterion, and the
derivation of the Lagrange dual (used throughout the book's later treatment of composite and
constrained problems) rests on strong duality, milestone strong_duality here. The saddle-point
characterization (saddle_point_sufficient/saddle_point_necessary) is the standard route to
designing an algorithm: a method that provably drives a pair to a saddle point
of is provably convergent to an optimal , without ever needing to verify optimality
directly against the primal problem.
None of the six substantive results here has a machine-checked proof on Prove2Me. The platform
holds a genuinely weaker unconstrained-in- condition (OnlineConvexOpt.ConvexBasics. kkt_optimality, Hazan's Theorem 2.2: for ,
with no inequality/equality constraints or multipliers at all) and a structurally different,
strictly more general cone-based Lagrange-duality development (VectorSpaceOpt.lagrange_duality
and VectorSpaceOpt.lagrangian_saddle_sufficient_pointed, from Luenberger, which bundle all
constraints into a single map into a convex cone in a general normed space, rather than Lan's
explicit inequality / equality split). Formalizing this mission
produces the finite-dimensional convex-program version of KKT in exactly the shape it is used and
taught: separate multiplier vectors for inequality and equality constraints, an explicit normal
cone rather than a cone-map abstraction, and both directions of the necessity/sufficiency split.
The separation theorem (Theorem 2.1) itself is routine once the projection onto a closed convex set is available. The real difficulty is entirely in the direction of the Convex Theorem on Alternative that Proposition 2.9 states: the naive idea — "insolvability of (I) should give a separating hyperplane between and directly" — fails, because these are sets in and separating them there does not produce a sign-definite multiplier vector. Lan's proof instead lifts to and separates the epigraph-like set from the open orthant-like set ; only in this lifted space does the separating normal's sign constraint (forced by 's unboundedness in the positive directions) translate into . Getting the sign of the -th coordinate strictly positive — needed to normalize and divide — is itself a small separate argument using the Slater subsystem's solution. The KKT necessity direction (the goal) then chains three of these already-nontrivial results (separation → CTA → strong duality → saddle necessity) before translating the saddle-point condition on into the gradient/normal-cone form via differentiability of at .
All milestones are stated over EuclideanSpace ℝ (Fin n) with Convex/ConvexOn from Mathlib.
Affine equality constraints are represented by explicit witnesses with , so that is
available without a separate affine-differentiability lemma. The normal cone is Lan's
own primal-space object (normalCone); the restricted Slater condition uses Mathlib's
intrinsicInterior ℝ X for , distinct from the plain interior X used by
the un-restricted Slater condition of Theorems 2.6/2.7(b). Primal optimal values and Lagrange dual
values are stated via IsGLB/pointwise-inequality forms rather than raw sInf, so that no
hypothesis is silently made true by an empty or unbounded set defaulting sInf to a junk value —
in every milestone here the relevant set is guaranteed nonempty by the Slater-point hypothesis
already present.
A trivializing formalization this mission rules out: stating kkt_necessary/kkt_sufficient
with (no set constraint) and empty (no functional constraints) would
collapse the normal-cone condition to and make the whole KKT apparatus vacuous
of any duality content; the milestones here keep , and as genuine free parameters (the
theorems are stated for arbitrary m, p : ℕ, including but not restricted to the degenerate case)
so that the constrained content of Lan's theorem is what gets proved.
Reusable beyond this mission: normalCone and lagrangian are generic enough that any later
chapter of this book needing Lagrangian duality or normal-cone stationarity (none of the current
first-wave chapters 03/06 needs them directly) could import them once published rather than
redeclaring. Contributions most welcome on the two hardest milestones,
cta_solvable_of_insolvable and kkt_necessary, since they carry the mission's real difficulty;
separation_point_closed can likely be discharged quickly via Mathlib's
geometric_hahn_banach_point_closed.
Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.
A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission
uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for
this notion throughout. A linear functional is bounded if
for some and all ; the Riesz representation theorem
(Theorem 12.5) says every such functional is for a unique .
A bivariate function is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set , with no topological structure on required. A reproducing kernel Hilbert space (RKHS) for a kernel is a Hilbert space of functions on such that, for every , the function belongs to and
— the reproducing property. Equivalently (Definition 12.12), is an RKHS exactly when every evaluation functional is bounded on .
Given any PSD kernel function on any set , there is a Hilbert space (embedded into functions on ) in which satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same are linearly isometric via an isometry intertwining their embeddings into functions on .
Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with " is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions give an explicit feature map into realizing , and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in -coordinates.
The formalization difficulty is concentrated in getting the type of the existence-and-
uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a
subtype of a fixed ambient space in Lean, so "the Hilbert space " of Theorem 12.11 is
formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on " via an injective
linear embedding into — and uniqueness must then be stated as an isometric
equivalence between any two witnessing Hilbert spaces that respects this embedding, the
faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces
are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses
(a bare PSD kernel, no topology on ) cleanly separated from Mercer's theorem's additional
compactness, continuity and measure-theoretic apparatus — the two theorems are frequently
conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's
structure.
is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the
book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its
own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that
scope. The integral operator of Eq. (12.11a) is presented as an abstract linear map on
Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than
constructed as a def, since constructing it as a genuine well-defined operator (needing
integrability and a.e.-measurability arguments) is proof content, not definitional content,
and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis
index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X
(Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence
conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is
finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization
of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly
warned against by this chapter's own brief), or state Mercer's convergence merely pointwise
or in rather than absolutely and uniformly; this mission avoids both. Out of scope: the
constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof
content, not part of the statement), the chapter's worked kernel examples (linear, polynomial,
Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem
(Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural
follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13,
mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather
than importing this mission's draft, per this book's series-wide convention.
Chapters 2 through 8 of Wainwright's High-Dimensional Statistics build up sharp error bounds for a sequence of specific high-dimensional models — sparse linear regression via the Lasso (Chapter 7), sparse principal components (Chapter 8) — each proved from scratch with techniques tailored to that model's own penalty and loss. Chapter 9 steps back and asks what made all of those arguments work, and isolates the answer into two structural ingredients: a decomposable regularizer, whose triangle inequality is tight across a well-chosen subspace pair, and a restricted curvature condition on the loss, holding only on the cone that decomposability forces the estimation error into. Once these two ingredients are checked for a particular model, a single, already-proved oracle inequality hands back the error bound — no further optimization-theoretic argument is needed. This mission formalizes that oracle inequality itself, together with its two supporting theorems, as the reusable core the book's later chapters (nuclear-norm matrix regression in Chapter 10, graphical model selection in Chapter 11, group-sparse and overlap-group Lassos) each specialize.
Let be a finite-dimensional real inner product space (e.g. , or a matrix space with the Frobenius inner product), and consider the regularized M-estimator
where is a convex empirical cost function, is a norm-based regularizer, and is a user-chosen regularization weight. Write for the true parameter and for the estimation error.
A pair of subspaces of — the model subspace and its (possibly larger) closure — has an associated perturbation subspace , the orthogonal complement of . The regularizer is decomposable with respect to if the triangle inequality is an equality whenever and — the regularizer penalizes deviations away from the model subspace exactly as much as it possibly could. The canonical example is the -norm with the subspace of vectors supported on a fixed index set .
Writing for the dual norm, the good event says the regularization weight dominates the dual norm of the score function at the truth — the non-probabilistic conditioning hypothesis every result in this chapter is stated under. The subspace Lipschitz constant measures the worst-case price of converting between the regularizer and the error norm on a subspace .
Under (A1) convex, satisfying restricted strong convexity (RSC) with curvature , radius and tolerance — for — and (A2) decomposable with respect to : conditioned on , any optimal satisfies
and, whenever and ,
Theorem 9.19 is the book's own claimed unifying result: as it remarks explicitly, the theorem
is a deterministic implication, and every later probabilistic corollary in Parts II and III of
the book is obtained by (i) checking that a specific loss/regularizer pair is decomposable with
respect to a natural subspace pair for the problem at hand, (ii) certifying the RSC condition
with high probability for that loss (via concentration arguments from Chapters 2–6), and (iii)
choosing large enough that the good event holds with high probability — then reading
off the rate directly from . Chapter 7's Lasso
bound (Theorem 7.13, mission 07-sparse-linear) is exactly Corollary 9.20 specialized to
and the subspace of -sparse vectors — but Chapter 9 proves it
once, in a form that Chapter 10's nuclear-norm-regularized low-rank matrix regression (mission
10-matrix-rank), Chapter 11's graphical model selection, and the chapter's own group-Lasso and
overlap-group-Lasso examples all instantiate without re-deriving the optimization argument.
The formalization difficulty here is almost entirely conceptual rather than syntactic: getting
the two-subspace apparatus exactly right. The book explicitly
allows to be a strict superset of (needed for the nuclear norm
in Chapter 10, where the naive choice fails to be decomposable at
all), so every definition and theorem in this mission is parameterized by the pair, not by a
single subspace — and three genuinely different projections appear across the statements: the
error vector's projection onto and onto (both keep
the bar), versus the true parameter's projection onto (the complement of the
small, unbarred subspace). A further subtlety specific to this printed source: several of the
book's own displayed equations for in Theorem 9.19 and Corollary 9.20 lose the
overbar on in PDF text extraction (a rendering artifact, not a mathematical
ambiguity); resolving which subspace is meant required reading the surrounding proof text line
by line, since only — not — is mathematically
consistent with how the constant is derived and used (see MODERATION_NOTES.md).
is [NormedAddCommGroup Ω] [InnerProductSpace ℝ Ω] [FiniteDimensional ℝ Ω], matching
the book's implicit assumption of a finite-dimensional inner-product parameter space throughout
this part of the book. The regularizer's norm axioms (IsRegularizerNorm), the dual norm, and
the subspace Lipschitz constant are all defined via sSup/sInf-free explicit formulas or
sSup over an explicitly-described set (never an unconstrained supremum over all of ),
so no faithfulness trap from an unbounded or empty supremum arises (see
MODERATION_NOTES.md's trap table). κ > 0 and λ_n > 0 are made explicit hypotheses of every
theorem, matching Definition 9.15's own stated positivity of and the chapter's
running convention that is a positive regularization weight — never a narrowing
of the theorem's actual scope. A trivializing formalization of this chapter would either collapse
the two-subspace machinery to a single subspace (which is faithful
only for the /group-Lasso examples, not the general theorem, and not what Chapter 10
needs) or silently drop the second conjunct of Theorem 9.19's conclusion (part (b), the actual
quantitative rate) in favor of only the qualitative part (a); this mission formalizes the full
two-subspace statement and both conjuncts of the goal theorem. Out of scope: the chapter's
worked examples (sparse GLMs, Corollary 9.26; group Lasso; nuclear-norm matrix regression) that
specialize the goal to concrete models — Chapter 10's own mission (10-matrix-rank) restates
the needed instance of this framework locally rather than importing this mission's draft, per
this book's series-wide convention that no draft imports another chunk's draft. Also out of
scope: the RSC-implies-restricted-eigenvalue correspondence (Example 9.16) and the
-based general RSC certification (Theorem 9.36, Section 9.8), both purely
probabilistic results that lie outside this chapter's own deterministic core.
The first eight chapters of Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) compare single random variables — location, variability, convexity. Chapter IX turns to a different question: given two coordinates of a random vector, how strongly do they tend to move together? "Large values of go with large values of " is a qualitative property (positive dependence); comparing how much two bivariate distributions exhibit it, holding their individual marginals fixed, is what this chapter's positive dependence orders make precise. This mission formalizes the two central ones — the PQD order and the supermodular order — and the supermodular order's closure properties, the chapter's own capstone result.
Let and be two random vectors, with joint survival function and joint distribution function (similarly for ). is smaller than in the PQD order, written , if
(It follows, though it need not be assumed, that and then share the same univariate marginals — the two inequalities together pin the marginals down, unlike a single one alone.) This is Lehmann's positive-quadrant-dependence order in its general multivariate form: 's coordinates cluster together, in both the upper and lower "quadrants," at least as strongly as 's.
A function is supermodular if for the coordinatewise meet/join — the function-level notion the platform's Topkis/Supermodularity series already formalizes for games and lattices, reused here directly. is smaller than in the supermodular order, written , if for every supermodular for which the two expectations exist. Because the indicator of any upper or lower orthant is itself supermodular, (Eq. 9.A.17): the supermodular order is strictly finer than the PQD order, and for the two coincide.
whenever every is increasing, or every is decreasing (part a); and
(part c, closure under marginalization). These are two of Theorem 9.A.9's five closure properties — the theorem the brief for this mission recommends as its goal — chosen as the ones that need no further definitional machinery beyond the orders themselves (composition and a coordinate projection, both plain pushforwards of the vector's law).
Positive dependence orders formalize a comparison operations research and risk management need constantly but rarely state precisely: two portfolios, insurance lines, or queueing networks with identical individual risk profiles can still differ sharply in how their components co-move, and that co-movement — not the marginals — is often what drives tail risk, correlated failures, or aggregate variability. The supermodular order is the standard tool for comparing this directly: Theorem 9.A.9's closure properties are what let a comparison established for primitive components survive the operations a model actually performs on them — relabeling by a monotone transform (part a), reading off a subset of coordinates (part c), combining independent sub-vectors (part b), conditioning on a covariate (part d), or passing to a distributional limit (part e). Chapter VI's multivariate stochastic order and Chapter VII's multivariate convex order are the two other multivariate orders in the book; the supermodular order is the one built specifically to compare dependence structure rather than location or spread, and it connects directly to the platform's existing Topkis/Supermodularity series, whose function-level predicate this mission reuses rather than restates.
Formalizing Theorem 9.A.9 fixes the exact shape a supermodular-order closure claim takes when built as a pushforward of the vector's law — the natural Mathlib-idiomatic rendering once the order is stated on laws rather than on variables tied to a fixed ambient space — for any future mission in this series or elsewhere that needs to state a closure property of a vector-valued stochastic order. No proof is attempted; both drafted parts of Theorem 9.A.9 have short book proofs (part (a) from the fact that composing a supermodular function with all-increasing or all-decreasing coordinate maps is again supermodular; part (c) the book calls "easy to prove"), making them plausible future proof targets.
The chapter's central definitional trap is that the PQD order's defining condition — even in its general multivariate form — determines the marginals as a consequence of the two joint inequalities holding together, not as a separate hypothesis to add; adding same-marginals as an extra explicit condition on top of Eqs. (9.A.13)-(9.A.14) would not be false, but it would present as a hypothesis something the theorem's own two conditions already force. A second trap is specific to Theorem 9.A.9(a): the must be uniformly increasing or uniformly decreasing across all coordinates, not an arbitrary per-coordinate mix — a mixed-monotonicity version is a materially different, unproven claim, since it is exactly the all-same-direction condition that keeps a composition with a supermodular function supermodular. A third, more basic trap common to every function-class order in this book: "for every supermodular " must be a genuine universal quantifier with the two expectations' existence stated as an explicit hypothesis, not a global assumption or a specific test function standing in for the whole class.
Unlike the univariate orders formalized elsewhere in this series (which take random variables
, on two possibly-different probability spaces),
PQDOrder and SupermodularOrder here are stated directly on the two vectors' laws — measures
on for a finite index type — since the book's own comparisons
never reference a joint law of and together, only their separate distributions. This is
also what lets Theorem 9.A.9(a)'s coordinatewise composition and (c)'s marginalization be stated
as plain pushforwards (Measure.map) of one law, without carrying an ambient sample space through
the statement. The index type is left an arbitrary finite type (Fintype ι, not fixed to Fin n)
so the same two declarations serve both a full -vector and any marginal sub-vector obtained by
restricting to a subset of coordinates — the shape Theorem 9.A.9(c) itself needs. Supermodularity
reuses the platform's own Supermodularity.Monotonicity.SupermodularOn (from the Topkis series,
via a kind: reference item) with its relativizing set argument fixed to Set.univ, its plain
unrelativized form — checked to match the book's φ(x)+φ(y)≤φ(x∧y)+φ(x∨y) on ι → ℝ's own
coordinatewise lattice structure exactly, not a games- or player-scoped variant. Independence in
Theorem 9.A.4 is formalized by taking the joint law of the two independent vectors to be the
product measure of their marginals — the standard way to construct an independent coupling
with prescribed marginals — rather than adding a separate independence hypothesis about
pre-existing random variables. Measurable hypotheses are added on every map a Measure.map is
taken along, guarding against the pushforward's junk-zero-measure convention for a non-measurable
map; none narrows what the book's own theorems claim, since every map used (a monotone/antitone
composition, a coordinate projection) is genuinely measurable. A trivializing formalization is
ruled out explicitly: the supermodular quantifier ranges over the reused, already-audited Topkis
predicate rather than a hand-rolled or restricted one, and the "for all increasing "
of Theorem 9.A.4 is a genuine universal over jointly-monotone functions of two arguments, not a
fixed example.
This mission draws on the platform's own Topkis/Supermodularity series for its supermodular
function-level building block (Supermodularity.Monotonicity.SupermodularOn, reused as a
reference item — the strongest prior-art connection of the whole nine-chapter series, per the
series plan) but on no prior art for the orders themselves (repeated searches for "PQD",
"positive dependence", "Fréchet bound" and "supermodular" returned nothing on-topic beyond the
Topkis series as of 2026-09-18). Reusable beyond this mission: the laws-only, arbitrary-Fintype-
index formalization pattern is available to any later mission in this series needing a
multivariate order (Chapter VI's multivariate stochastic order, Chapter VII's multivariate convex
order) that wants marginalization or coordinatewise composition stated as plain pushforwards.
Principal component analysis (PCA) is one of the oldest and most widely used tools in multivariate statistics: given data with covariance matrix , project onto the top eigenvector(s) of to find the directions of maximal variance. In practice one never observes itself, only a perturbed version — a sample covariance matrix , with the (random) estimation error. The natural question, asked since at least Davis and Kahan (1970) and Wedin (1972), is: how close is the top eigenvector of to that of ? Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 8, gives a self-contained, sharp, non-asymptotic answer, phrased entirely in terms of two deterministic quantities: the eigengap of , and a single scalar summarizing how the perturbation couples to the top eigendirection.
Unlike most of the results in this book series, this one is a statement of pure linear algebra: no probability, no concentration inequality, no sample size is needed to state or prove it. Randomness enters only afterward, when is instantiated as an actual sampling error and bounded using the machinery of earlier chapters (Corollary 8.7, out of this mission's scope).
Let be a symmetric positive semidefinite matrix. Say is a maximal unit eigenvector of if and maximizes the Rayleigh quotient over the whole unit sphere — the variational characterization of the top eigenvector/eigenvalue pair, matching Eq. (8.14) of the book. Write for the corresponding top eigenvalue. Say has eigengap at if every unit vector orthogonal to satisfies — the Courant-Fischer variational form of the book's .
For a symmetric perturbation matrix , write for its -operator norm, and
for the component of orthogonal to — the piece of the perturbation that actually couples the top eigendirection to the rest of the space (Eq. (8.11)). Note can be far smaller than : a perturbation can be large in every direction yet barely move the top eigenvector, if its interaction with specifically is small.
Let be symmetric positive semidefinite with maximal unit eigenvector and eigengap . For any symmetric with , and any maximal unit eigenvector of with ,
Under the same eigengap hypothesis, with $\Psi(\Delta;P) := \langle\Delta,P\Delta\rangle
The bound isolates exactly what drives eigenvector instability: not the raw size of the perturbation but its projection onto the top eigendirection, rescaled by the inverse eigengap. This explains, in one inequality, the qualitative phenomenon Example 8.4 illustrates numerically (a tiny perturbation can move the eigenvector far when the eigengap is small) and quantifies exactly how far. It is the deterministic engine behind every consistency result for PCA in the rest of the chapter: Corollary 8.7 (rates for the spiked covariance model) and the sparse-PCA guarantee (Theorem 8.10) both specialize this same bound, after bounding and using concentration for a specific random design. It is also a sharp instance of the general Davis-Kahan-type perturbation theory for symmetric matrices, phrased with an explicit, non-asymptotic constant rather than an .
The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the bound and its supporting basic inequality, composing with any future formalization of the chapter's probabilistic corollaries.
The proof is genuinely variational, not spectral: it never diagonalizes or , only uses that and are optimal for their respective Rayleigh-quotient maximizations. The one place a naive argument fails is in bounding itself (the proof of Lemma 8.6): a direct Cauchy-Schwarz bound on using alone would produce a bound in terms of throughout, not the sharper the theorem actually delivers; getting the sharper dependence requires decomposing along and its orthogonal complement and tracking the two pieces separately (the , decomposition on p. 244). The sharpness of the threshold is also not a proof artifact: the book's own example (, ) shows the perturbed matrix can lose a unique maximal eigenvector exactly at .
, , are Matrix (Fin d) (Fin d) ℝ; "symmetric" is
M.transpose = M; "positive semidefinite" is the quadratic-form condition
for all , stated directly rather than via a
Mathlib PosSemidef typeclass. "Maximal unit eigenvector" and "eigengap" are both
given their variational (Rayleigh-quotient) characterizations rather than defined
through Mathlib's enumerated matrix-eigenvalue API — mathematically equivalent to the
book's spectral definitions by the Courant-Fischer theorem, and the same
characterization the book's own proof works with throughout (Eq. (8.14)). The operator
norm is likewise realized variationally, valid because this
mission only ever applies it to symmetric matrices, exactly as the book does in this
chapter. is realized as a basis-independent vector in (the
component of orthogonal to ) rather than the book's
basis-dependent representative; its -norm — the only quantity
the theorem's conclusion uses — is identical either way.
Deliberate scope decision, disclosed here rather than silently: the book's own
Theorem 8.5 concludes that "has a unique maximal eigenvector
" satisfying the bound — asserting both existence and uniqueness as part
of the theorem, on top of the quantitative bound. This mission formalizes only the
quantitative bound, for an arbitrary maximal unit eigenvector of
satisfying the sign condition —
exactly what the book's own proof establishes (the proof never separately argues
existence or uniqueness; both are consequences that could be derived from the bound
together with a compactness argument for existence, left to a future extension) and
exactly what every downstream use in the chapter (Examples, Corollary 8.7) actually
invokes. A trivializing formalization would instead drop the sharp threshold
to ≤, or conflate the general operator norm with the
symmetric-matrix Rayleigh-quotient characterization for a non-symmetric ; this
mission does neither. Corollary 8.7 (spiked covariance rates) and Theorem 8.10
(sparse PCA, needing the uniform deviation condition of Eq. (8.26)) are out of this
mission's scope; a companion mission formalizing them on top of this one's
pca_eigenvector_perturbation_bound is natural future work, together with a proof
of existence of a maximal unit eigenvector via compactness of the sphere.
Chapter III's convex order compares two real-valued random variables by "how spread out" they are, holding the mean fixed. Chapter VII lifts the same idea to random vectors: is smaller than in the multivariate convex order if every convex function of has smaller expectation than the same function of . This mission formalizes that order, its increasing-convex companion, and their martingale-coupling characterizations — the direct -dimensional generalizations of Chunk 03's and Chunk 04's own goal theorems — plus a cheap mean-equality corollary and a simple standalone scaling result.
Let be a random vector taking values in on , and a random vector taking values in on . is smaller than in the multivariate convex order, , if
and smaller than in the increasing convex order, , if the same holds for every that is both increasing (coordinatewise) and convex. Since each coordinate projection and its negation are both convex, forces componentwise (Eq. 7.A.5) — unlike , which only forces .
The direct -dimensional generalization of Theorem 3.A.4 (Strassen's martingale coupling, Chunk 03's own goal theorem): a joint law on a common probability space realizing as a genuine martingale pairing between copies of and . The book states no further "Furthermore" strengthening here, unlike the univariate and increasing-convex cases.
iff there exist on a common space with ,
, and a submartingale, a.s. —
the direct generalization of Theorem 4.A.5's increasing-convex case (Chunk 04's own goal
theorem), proved by the book's own cross-reference "by essentially the same method" as the goal.
The book's bracketed increasing-concave companion is a genuinely separate statement (swapped
conditioning) and is not drafted here for budget (see STATUS.md).
ConvexOrder's own defining
quantifier applied to each coordinate projection.The multivariate convex order is the natural tool for comparing the variability of random vectors — portfolios of returns, multi-resource cost vectors, correlated component lifetimes — in a way that respects every direction of the space simultaneously rather than coordinate by coordinate. Its martingale-coupling characterization is the same tool that makes Strassen's theorem useful in the univariate case: it turns the intractable "for every convex " quantifier into a single explicit joint construction, and because it generalizes directly (the book's own proof of Theorem 7.A.4, not drafted here, applies the univariate Theorem 3.A.4 coordinate by coordinate to build the multivariate coupling), it is the natural second data point — after Chunk 03's univariate case and Chunk 06's usual-order case — for what a "coupling-characterization" mission in this book's series looks like once both the order and the dimension vary. Theorem 7.A.9's scaling result is a compact, self-contained illustration of how the order behaves under a common operation (randomized scaling) that appears throughout the book's later risk and insurance examples.
No platform prior art exists: GET /theorems?q=convex+order and q=martingale return only false
positives (checked at this book's triage time, re-confirmed this session). This mission restates
the multivariate convex and increasing convex orders and their coupling characterizations as a
self-contained pair, parallel in structure to Chunks 03 and 04's univariate missions but
independently drafted, since drafts cannot import each other's Lean.
The chief formalization risk this chapter's own brief flags is confusing "convex" for
(ordinary convexity, Mathlib's ConvexOn) with a
coordinatewise or lattice-based notion — in particular, with Chunk 09's supermodular functions,
a different and weaker condition. A second risk is the "increasing" half of IcxOrder: unlike
convexity, "increasing" genuinely is the coordinatewise order (matching Chunk 06's convention),
so IcxOrder mixes two different kinds of predicate on the same φ (Monotone in the
coordinatewise sense, ConvexOn in the ordinary sense) and getting either one wrong silently
changes which order is being stated. A third risk, specific to Theorem 7.A.2, is the bracketed
icx/icv alternative: as in Chunk 04, the two cases are not symmetric rewrites of each other (the
conditioning variable swaps), so a Lean statement conflating them with Or would misstate one
case — this mission avoids the risk by drafting only the increasing-convex case and recording the
omission explicitly rather than attempting an unsound unification.
Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces.
ConvexOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with ConvexOn ℝ Set.univ φ (ordinary
convexity) and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν inside the ∀; IcxOrder adds
Monotone φ in Mathlib's default coordinatewise (Pi) order on Fin n → ℝ — the same order
Chunk 06's MultivariateOrder uses — as a genuinely separate definition from ConvexOrder, not
one derived from the other, since Theorem 7.A.12 (not drafted here) relates the two nontrivially
and conflating them would trivialize such a relationship. Equality in law is
ProbabilityTheory.IdentDistrib; the martingale/submartingale conditions use Mathlib's
conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ (resp. X̂ ≤ᵐ[ρ] ρ[Ŷ | m]) with m generated
by X̂, here genuinely Fin n → ℝ-valued (well-defined since Fin n → ℝ is a finite-dimensional,
hence complete, normed space over ℝ) — restated locally rather than imported from Chunks 03/06,
since drafts cannot import another mission's definitions. Theorem 7.A.9's scaling U·X is
Mathlib's scalar multiplication on the ℝ-module Fin n → ℝ.
Two deliberate scope restrictions, recorded rather than silently applied: (1) Theorem 7.A.2 is drafted only for the increasing-convex case, per this chapter's own pitfall 3 (the icv companion's swapped conditioning structure is a genuinely different predicate, not a sign-flipped rewrite, and budget did not justify a fourth definition/theorem pair to draft it separately, unlike Chunk 04 which had budget for both cases of its analogous theorem); (2) Theorem 7.A.5 through 7.A.8's closure properties (mixtures, convolutions, weak limits, the random-sum generalization) are left out entirely — each needs conditional-distribution or convergence-in-distribution machinery this mission's four items do not otherwise require, and none is on the goal's own attack chain.
A trivializing formalization this mission rules out: drafting IcxOrder by deriving it from
ConvexOrder and a separate monotonicity wrapper in a way that makes their relationship (Theorem
7.A.12: , not drafted here) provable by
unfolding rather than by genuine content — the two are kept as independently-quantified
predicates for this reason. This mission draws on no platform prior art (searches for "convex
order" and "martingale" as of 2026-09-18 return only false positives). Reusable beyond this
mission: the ConvexOrder/IcxOrder pattern and their martingale/submartingale coupling shape
parallel Chunks 03/04's univariate pair and Chunk 06's multivariate usual-order pair closely
enough that a future pass drafting the icv companion, or Chapter VII's later dispersion and
transform orders, could restate the same shape with minimal adaptation.
StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex),
for the univariate convex and increasing convex orders and their martingale/submartingale
couplings this chapter directly generalizes; Chunk 06 (StochasticOrders.Multivariate), for the
multivariate usual stochastic order and its own coupling characterization.