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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
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?
Machine learning's canonical training objective — minimize an expected or empirical risk over a data distribution — is almost never observed exactly: at each step an algorithm sees only a noisy gradient sample (a minibatch gradient, a single-example gradient, a simulation draw). Stochastic mirror descent (Nemirovski, Juditsky, Lan & Shapiro 2009) is the modern, general-norm answer to "what happens to first-order convergence guarantees when the gradient itself is a random variable": it takes the deterministic mirror-descent scheme of the previous chapter and replaces the exact subgradient with an unbiased stochastic estimate, and asks for both an expected convergence rate and, when the noise is well-behaved, an explicit probability-of-large-deviation guarantee. This is the theoretical backbone of stochastic gradient descent as used in practice.
Fix a nonempty closed convex set in a real normed space , and a convex with and an arbitrary minimizer, exactly as in Chapter 3. A stochastic oracle , queried at a point with a fresh random sample , returns an estimate of a subgradient : (unbiasedness), (a dual-norm Lipschitz bound, Eq. (4.1.7)), and (a second-moment/variance bound). The stochastic mirror-descent update is exactly Chapter 3's mirror-descent update with in place of the deterministic : (Eq. (4.1.6)), where is the Bregman divergence of a fixed distance-generating function .
Every constant is exactly the book's; (not a generic ) is the goal's own noise-dependent constant, taken verbatim.
This is the first mission in the series to leave the purely deterministic, real-analytic setting of Chapters 2-3 and formalize a genuinely probabilistic convergence guarantee: an expectation taken over an entire random algorithm trajectory , not merely over a single random variable. Getting the goal theorem's statement right requires being explicit about exactly which quantities are random (the iterates , hence and ) and which are deterministic constants fixed in advance (), and about the precise mathematical content of "the stochastic gradient's bias vanishes after conditioning on the past" — Lemma 4.1 is included specifically because it is the general machine that makes that vanishing rigorous, independent of the optimization application.
No result matching stochastic mirror descent, Assumption 4's sub-Gaussian/light-tail condition, or
this martingale-difference concentration lemma exists on the platform as of 2026-09-18 (q= stochastic gradient, q=stochastic mirror descent, q=martingale, q=sub-Gaussian — see
Prior art below for what these queries actually returned).
The central difficulty is disentangling which facts in the chapter's proof genuinely need
measure theory and which do not. The per-step algorithmic relations — 's minimality,
's subgradient inequality at , the dual-norm bound on — hold for every sample path
individually and are formalized pointwise in , exactly as chunk 03-deterministic
formalizes its deterministic analogues; only the second-moment bound and the final expectation
inequality are genuine integrals. The one place this pointwise treatment cannot simply mirror the
deterministic case is the noise cross-term :
in the book's proof this vanishes because is conditionally mean-zero given
the past and is a function of the past (the martingale-difference property, via the tower
property of conditional expectation) — a genuinely non-pointwise fact. Rather than thread an
explicit filtration through the goal theorem's own statement (which Lemma 4.1 already does, as
the chapter's dedicated home for that machinery), the goal theorem takes this post-tower-property
consequence directly as a named hypothesis (hcross); see Formalization scope.
stochastic_mirror_iterate_three_point and stochastic_mirror_descent_bound are stated over a
general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching chunk
03-deterministic's general-norm milestones (mirror_iterate_three_point/mirror_descent_bound)
rather than the Euclidean/inner-product specialization of that chunk's §3.1 items — Chapter 4's
own stochastic mirror descent is presented directly in the general-norm framework of §3.2, with no
Euclidean-only warm-up. is left a free two-point function (never hard-coded to a squared
Euclidean distance), and the stochastic gradient and the subgradient selector are
continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm
with no separate definition needed — the same trivializing formalization chunk
03-deterministic rules out (specializing to the Euclidean case) applies here and is ruled
out the same way.
martingale_difference_deviation_bound (Lemma 4.1) is a standalone probabilistic result,
formalized with Mathlib's MeasureTheory.Filtration and condExp machinery: the sequence
's generated filtration, 's -measurability, and the two
conditional-expectation hypotheses (conditional mean zero, conditional sub-Gaussian tail) are all
literal translations of the book's own E|ξ[t-1] notation.
Left out of scope, for time: Assumption 4 (the light-tail/sub-Gaussian oracle assumption),
Proposition 4.1 (the large-deviation bound under Assumption 4, which chains Lemma 4.1's
concentration bound with the constant stepsize policy (4.1.11) and a second Markov-inequality
argument on ), Lemma 4.2 and Theorem 4.2 (the smooth- case,
§4.1.2, requiring a separate recursion and averaging convention ). All four are natural
continuations reusing this mission's stochastic_mirror_iterate_three_point and/or
martingale_difference_deviation_bound; a later mission or an amendment to this one could add
them without touching what is here. Per Hard Rule 7 (faithfulness over coverage), a genuinely
faithful formalization of Proposition 4.1 in particular — which needs Assumption 4's own
conditional-MGF hypothesis threaded consistently with Lemma 4.1's, plus the constant-stepsize
substitution and a second concentration argument — was judged to need more time than this
session's budget allowed to do without shortcuts; it is named here rather than approximated.
Chapter XI boosted a weak learner into a strong one for a single offline fit to a fixed sample. Chapter 12 asks the analogous question online: when the pool of experts is too large to run Hedge over directly (the contextual-learning setting, where "experts" are policies mapping contexts to actions and their number is exponential), can black-box access to a cheap approximate — "weak" — online learner be boosted into an algorithm with vanishing regret against the whole hypothesis class, without ever touching it directly? Chapter 12 answers yes, by cascading weak learners through a Frank–Wolfe-style online construction whose running time is independent of the hypothesis class's size.
A -weak OCO learner (WOCL, Definition 12.1) for hypothesis class guarantees, against any linear loss sequence with bounded range, — competitive with only a -fraction of the best fixed hypothesis's performance, plus a sublinear additive term. Because a -multiple guarantee is not shift-invariant, this is stated (Eq. 12.2) after normalizing losses so at the decision set's center of mass.
The weak learner's predictions must be scaled by to be useful, which pushes them outside the decision set — so Algorithm 36 needs a way to evaluate a proxy loss at points outside and project back without paying much. Section 12.3's extension operator (a smoothed, distance-penalized version of ) solves this: Lemma 12.3 shows it agrees with on up to , and that projecting onto costs at most another .
Algorithm 36 cascades copies of a -WOCL: starting from , each stage takes a -weighted step toward the -th weak learner's scaled prediction, and each weak learner is fed the gradient of the extended loss at the previous stage's iterate as its own linear loss — a genuinely projection-free, Frank–Wolfe-style construction (as in Chapter VII), applied here to a cascade of learners rather than a single gradient-descent sequence.
for ; for .
For -smooth and -Lipschitz, .
With , , Algorithm 36's predictions satisfy
Theorem 12.4's comparator is the convex hull of , not the best single hypothesis — strictly
stronger, and (as the book notes) still a meaningful guarantee even at (a weak learner
that already matches 's best hypothesis), since the boosting algorithm's payoff is purely the
upgrade from to . Combined with §12.1.1's binary-classification instantiation and the
-vs--style efficiency argument, this is the
chapter's answer to whether contextual-learning-scale expert classes (exponential in context
count) can be handled with per-round cost independent of — a genuinely new computational
regime relative to Hedge's -dependence. No prior art was found on the platform for
online boosting or the extension operator (planning search: q=online+boosting,
q=extension+operator — 0 hits); this mission drafts all three results fresh, building
internally on a Frank–Wolfe-style construction restated locally (Chunk 07 is not yet published).
Lemma 12.3's proof combines the smoothing operator's own approximation guarantee (part 1, "since for , this follows immediately from Lemma 2.8") with a Cauchy–Schwarz argument balancing the gradient-norm bound against the penalty coefficient exactly at (part 2) — a delicate one-parameter tuning, not a generic estimate. Lemma 12.5's proof (not fully excerpted here, continuing past PDF p. 223 with an inductive argument on across the cascade stages) is structurally the Chapter VII Theorem 7.1/Lemma 7.4 argument applied once per stage, compounding the -WOCL guarantee's slack across all stages simultaneously — a genuinely two-dimensional induction (over both rounds and stages ) that the offline or single-stage online analyses do not need. Theorem 12.4's own proof (PDF p. 224 onward, not fully excerpted) combines both lemmas with the specific parameter substitutions , , and to reach the stated closed-form bound.
Extension/SmoothedFunction redeclare Chapter II's smoothing operator (matching
BanditConvex.SmoothedFunction, Chunk 06, in content — neither is yet published) rather than
importing it, per Addendum 2 rule 5. IsGammaWOCL is drafted at the shifted-form Eq. (12.2) the
rest of the chapter actually works with (not Definition 12.1's own unshifted form with the
center-of-mass term ), matching the book's own explicit simplification. IsOnlineBoostingRun
mechanizes Algorithm 36's full five-line cascade (stage-by-stage iterate, weak-learner scaling,
final projection, and the per-stage linear-loss construction from the extended loss's gradient) —
the fullest mechanization in this mission's items, since Theorem 12.4's own hypotheses (hWOCL,
one γ-WOCL guarantee per stage) need the run's internal structure to connect xplay to the weak
learners' regret guarantees at all. Lemma 12.5 is drafted at a more abstract level (x^N,
x^\star, Regret_T(W) as direct inputs, matching how the book's own proof of that lemma
proceeds before Theorem 12.4's own parameter substitution), consistent with the "no more
mechanization than the statement needs" principle used throughout this series (e.g. Chunk 10's
Lemma 7.4-style scoping). CH(H) is Mathlib's own convexHull ℝ H, applied to H viewed as a
subset of the function space — a faithful match to the book's {∑_{h∈H}p_hh \mid p\in\Delta_H}
that also correctly handles infinite H, which the book's own sum notation does not
literally cover.
Not formalized: §12.1's motivating discussion and its binary-classification/personalized-article
examples (illustrative, not numbered theorems); the running-time-independent-of-|H| claim
(prose, not part of Theorem 12.4's own mathematical content, per BRIEF.md); Remarks 1-2
following Theorem 12.4 (commentary, no further claim).
Every algorithm in Chapters I–VIII minimizes regret, an online, adversarial performance measure with no reference to a data-generating distribution. Chapter 9 asks what regret minimization buys in the classical statistical learning setting, where examples are drawn i.i.d. from a fixed distribution and the goal is a hypothesis that generalizes well to unseen data. The chapter's answer is a black-box reduction: run any OCO algorithm on the sequence of losses induced by i.i.d. training examples, average its iterates, and the sublinear-regret guarantee converts directly into a PAC generalization bound — with no algorithm-specific analysis required.
A hypothesis predicts labels from examples ; its generalization error against a distribution over labeled pairs is for a loss function . Section 9.1's Theorem 9.1 (No Free Lunch) shows this goal is hopeless without restricting to a hypothesis class : for any learning algorithm and any sample size , there is a domain, a zero-error concept, and a distribution against which the algorithm's learned hypothesis is wrong at least of the time with probability at least . Definitions 9.2–9.3 (PAC and agnostic PAC learnability) and Theorem 9.4 (finite classes are agnostically PAC learnable) set up the target the chapter's reduction achieves for a much broader class of hypothesis sets.
Section 9.2's reduction (Algorithm 29) takes any OCO algorithm and a convex hypothesis class : draw i.i.d. labeled examples, feed the loss function at each round, and output the running average of 's iterates.
For any domain with and any algorithm , there is a concept and a distribution with and .
For any , with probability at least ,
Theorem 9.5 is a genuine reduction theorem, in the strongest sense the book uses that phrase in
this manuscript: it needs no property of beyond a regret bound, so every sublinear-regret
algorithm in Chapters III–VIII (online gradient descent, RFTL, the bandit and projection-free
algorithms) is, via this one theorem, automatically also an agnostic PAC learning algorithm for
its hypothesis class — with an explicit, finite-sample generalization bound, not merely an
asymptotic guarantee. This is also the book's only chapter connecting OCO to classical statistical
learning theory, making Theorem 9.5 the bridge result the rest of the manuscript's machinery feeds
into. No prior art was found on the platform for PAC learning, no-free-lunch, or generalization
bounds in this sense (planning search: q=PAC, q=no+free+lunch, q=generalization — the one
"no free lunch" hit found, PRNGCompression.prng_no_free_lunch, is an unrelated
Kolmogorov-complexity result, not a substitute); this mission drafts both results fresh.
Theorem 9.1's proof (the probabilistic method) computes an expectation over a uniformly random concept and a uniformly random sample simultaneously, shows this joint expectation of the learned hypothesis's error is at least , and only then extracts (i) the existence of a single bad concept via linearity of expectation, and (ii) a probability bound via Markov's inequality on the error as a random variable over samples for that fixed concept — a genuinely two-stage probabilistic argument, not a direct combinatorial construction. Theorem 9.5's proof (not included in the excerpted milestone pages, continuing past PDF p. 180 into §9.2.1's Azuma's inequality machinery) builds a martingale from the sequence of per-round loss deviations and applies a concentration inequality to convert the algorithm's regret bound (a statement about the sum of realized losses) into a high-probability statement about 's expected loss under — the gap between "regret is small" and "generalization error is small" is exactly what the martingale/concentration argument closes.
GeneralizationError/GeneralizationErrorZeroOne give the two loss regimes the chapter uses:
a general parametrized real-valued hypothesis (matching the linear-hypothesis convention of §9.1.3, generalized via an explicit pred evaluation map since the book's own
notation "" for implicitly identifies a parameter vector with
its induced predictor) and the zero-one loss for Bool-labeled concepts (Theorem 9.1's own
setting). IsAgnosticReductionRun formalizes Algorithm 29's construction directly, including its
round-0 convention (h_1 ← A(∅), matching the series' standing convention for an empty history)
and the i.i.d. sampling assumption made explicit via ProbabilityTheory.iIndepFun and identical
marginal law D. Theorem 9.5's own regret hypothesis (hA) states "an OCO algorithm whose regret
is guaranteed to be bounded by RegretT(A)" as a genuine property of A — holding for every cost
sequence and horizon — matching the book's phrasing exactly, not a one-off fact about the single
realized (random) cost sequence this particular run produces. The loss ℓ is assumed bounded in
[0,1], the chapter's implicit standing assumption (matching the zero-one loss and bounded
hinge-loss examples of §9.1.3) needed for the concentration argument behind the
√(8log(2/δ)/T) term; see MODERATION_NOTES.md.
Not formalized: Definitions 9.2–9.3 (PAC/agnostic-PAC learnability) and Theorem 9.4 (finite-class
PAC learnability), per BRIEF.md's explicit guidance that Theorem 9.4's proof is not
self-contained on these pages but spread across the whole chapter, culminating in Theorem 9.5
itself — treating it as background context rather than a separate formalization target avoids
either reconstructing that proof or drafting a numbered result whose "proof" would just be a
forward reference to this mission's own goal. Theorem 9.5's optional corollary form (the sample
complexity bound T = O((1/ε²)log(1/δ) + T_ε(A))) is likewise not drafted, per BRIEF.md's
"otherwise keep the milestone to the displayed inequality." §9.2.1's Azuma's inequality survey
(background probability theory, available in Mathlib's Probability/Martingale/) is not itself a
formalization target.
Every algorithm through Chapter VI updates its iterate by a Euclidean projection onto the decision set . For many decision sets that arise in practice — bounded-nuclear-norm matrices (matrix completion / recommendation systems), the flow polytope (network routing), the Birkhoff–von Neumann polytope (ranking/permutations), matroid polytopes — a projection requires an expensive operation (an SVD, a quadratic program) while a linear minimization over the same set is comparatively cheap (an eigenvector computation via the power method, a shortest-path or minimum-weight-matching computation, a greedy matroid algorithm). Chapter 7 develops an OCO algorithm that replaces every projection with a call to a linear-minimization oracle, at the cost of a worse regret rate.
The conditional gradient (CG) / Frank–Wolfe method (Algorithm 25) minimizes a -smooth function over a convex set (diameter ) without ever projecting: at each round it calls the oracle and steps , staying inside automatically since it is a convex combination of two points of . Theorem 7.1 gives its convergence rate; §7.3.1's matrix completion example and §7.4's routing/ranking/matroid examples motivate why the oracle call is often much cheaper than a projection.
The online conditional gradient (OCG) algorithm (Algorithm 27) lifts this to the OCO setting. Applying CG naively to each separately fails (the method only sees gradient direction, and a single round's direction is not enough information); instead, the algorithm builds the aggregate regularized function from all past gradients, calls the linear oracle on , and takes a -weighted step toward the oracle's answer.
Online conditional gradient (Algorithm 27) with , attains
This is the chapter's central trade: Algorithm 27's regret is worse than Chapter
III's full-information rate and Chapter V's RFTL rate, but its per-round cost is a
single linear-minimization oracle call, not a projection — exactly the trade that makes it the
practical choice for the recommendation-system, routing, and ranking applications the chapter
develops in detail. Theorem 7.1's offline rate is independently significant as the field's
standard Frank–Wolfe convergence guarantee, reused as the analytical engine (via Eq. (7.2)) for
both Lemma 7.4's online bound and, historically, for a large family of projection-free methods
outside OCO entirely. No prior art was found on the platform for Frank–Wolfe, conditional
gradient, or projection-free methods (q=Frank-Wolfe returned 0 hits during planning); this
mission drafts the standard textbook account fresh.
Theorem 7.1's proof is a one-step smoothness-plus-convexity inequality (Eq. (7.2)) combined with
an induction lemma (Lemma 7.2, not separately drafted — it is a purely algebraic recursion
h_{t+1} ≤ h_t(1-η_t) + η_t²c ⟹ h_t ≤ 4c/t, reused verbatim by Lemma 7.4's own induction and not
independently central to the chapter's content). Lemma 7.4's proof is the chapter's most delicate
step: it applies Theorem 7.1's offline analysis technique to the online aggregate function
— not to any single , and not even to a fixed function across rounds, since
itself changes every round as more gradients accumulate — then combines it with a second
inequality (comparing to via strong convexity and
Cauchy–Schwarz) and a careful algebraic balancing of the , , parameters
(Eq. (7.6)) to close the induction. Theorem 7.3's own proof is a second reduction: it relates the
algorithm's regret against the true cost sequence to Lemma 7.4's bound on , via an
intermediate comparison to (playing the role of Chapter V's RFTL iterates applied to a
shifted cost sequence ).
IsLinearMinimizer makes the "projection-free" linear-oracle call (Eq. (7.4)) an explicit,
first-class object, reused by both Algorithm 25 and Algorithm 27's definitions, rather than
silently replaced by a projection anywhere. SmoothOn is redeclared under this chapter's own
sub-namespace (not imported from Chapter II, which is not yet a published series definition);
see MODERATION_NOTES.md. AggregateFunction/AggregateGradient give and its closed-form
gradient explicitly, matching Algorithm 27 line 4's formula exactly (the book computes directly rather than leaving it abstract, so this mission does too). This chunk indexes
rounds from 1 throughout (not the 0-indexed Finset.range shift used elsewhere in the series),
since Algorithm 27's own line 4 sums to and every theorem in this chapter states a
per-round or Finset.Icc 1 T-summed bound directly in the book's own round numbers — a
deliberate, chunk-local convention choice, not an inconsistency with earlier chapters'
definitions (this chunk does not import them). Lemma 7.4 keeps Theorem 7.3's specific parameters
and a -Lipschitz hypothesis as explicit premises, since the book's own proof of the lemma uses
them, rather than presenting it as a fully parameter-free general fact.
Not formalized: Lemma 7.2 (a routine algebraic recursion, not independently central, and reused identically inside Lemma 7.4's own proof rather than cited as a numbered result on its own); Algorithm 26 and §7.3.1's matrix-completion specialization, §7.4's routing/ranking/matroid examples, and Corollary-level results (illustrative applications, not further formalizable theorems); §7.1's linear-algebra review (singular values, nuclear norm — background, not a formalization target for this mission).
Every RL guarantee proved earlier in this series — UCB-VI's regret bound, the contextual bandit oracle reductions — scales with the size of the state space , because the algorithms maintain a separate statistic per state. Real environments (images, sensor readouts, natural language) have combinatorially or infinitely many states, so a tabular guarantee is vacuous there: the only hope is to generalize across states via a class of value functions, the way supervised learning generalizes across inputs via a hypothesis class. The chapter develops two algorithms along this line: LSVI-UCB, the linear-function-approximation analogue of UCB-VI whose regret is independent of (a low-rank MDP result originating with Jin, Yang, Wang, and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020, arXiv:1907.05388), and BiLinUCB, which attains an analogous sample-complexity guarantee under the strictly more general structural condition of low Bellman rank (Jiang, Krishnamurthy, Agarwal, Langford, and Schapire, Contextual Decision Processes with Low Bellman Rank are PAC-Learnable, ICML 2017, arXiv:1610.09512; the Q-type variant formalized here follows Du, Kakade, Wang, and Yang, Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning?, ICLR 2020, arXiv:1910.03016). This mission formalizes the second, strictly more general track: BiLinUCB and its Bellman-rank guarantee; LSVI-UCB is left out of scope (see Formalization scope).
Both algorithms act on the finite-horizon episodic MDP of the earlier chapters of this series (RLBasics.Core), with
value . For a state-action value
function (with the convention ), the Bellman
residual of under policy at layer is
which vanishes identically when , the optimal value function (Bellman optimality). Given a class of candidate value functions, has Bellman rank relative to (Definition 8) if is the least integer such that, at every layer , there exist embeddings with for every policy and — equivalently, the least rank of the matrix of Bellman residuals, at any layer. A linear MDP (the setting of LSVI-UCB, §7.2) is the special case where the transition kernel and reward themselves factor through a known feature map ; every linear MDP has Bellman rank at most relative to the linear value-function class, but Bellman rank captures far more (kernel/neural function classes, and low-rank MDPs whose feature map is unknown).
The chapter presents two algorithms. LSVI-UCB (§7.2.1) runs episodes of ridge regression per layer against the linear feature map, forming a confidence ellipsoid of radius around each layer's estimated parameter and acting greedily with respect to an upper-confidence bonus built from that ellipsoid — the same optimism-under-uncertainty template as UCB-VI, now regularized rather than tabular; it motivates Bellman rank but is not itself formalized by this mission (see Formalization scope). BiLinUCB (§7.3.1), the algorithm this mission formalizes, instead proceeds in iterations of episodes: each iteration plays the greedy policy for the current optimistic-on-average value function , collects fresh episodes, and shrinks the confidence set by discarding value functions whose empirical Bellman residual along the played policy is large; after iterations it outputs the policy with the best empirical return observed at any iteration.
for of Bellman rank relative to , where is BiLinUCB's output policy after iterations of episodes. This is the weakest stable form: it fixes the shape of the sample complexity (polynomial in , logarithmic in , independent of ) and leaves the leading constants — which the book itself introduces only as "a sufficiently large numerical constant" — outside the formal claim. Unlike every other goal in this series, this is a PAC (sample-complexity) guarantee on the algorithm's final output policy, not a bound on cumulative regret accrued while learning: BiLinUCB commits to only after the training phase ends, and its suboptimality is measured post-training.
Reaching it rests on two structural facts about BiLinUCB's confidence sets, each formalized as a milestone in attack order:
Proposition 47 shows that a single structural parameter — Bellman rank — is sufficient for sample-efficient RL with function approximation, with a sample complexity that depends only on the horizon, the rank, and the value-function class's log-cardinality, never on . This subsumes the linear-MDP guarantee of Proposition 46 (LSVI-UCB, §7.2.1; not itself a target of this mission, see Formalization scope) as a special case — every linear MDP has Bellman rank — while covering strictly more models (kernelized and neural value-function classes with a low-dimensional Bellman-residual factorization that need not come from a known linear feature map). The result is proved in the source and this mission formalizes its statement and the two structural lemmas its proof rests on, as stated; no new mathematics is contributed. Formalizing it commits, for the first time on this platform, to machine-checkable statements of the Bellman rank abstraction, the elliptic-norm confidence-set machinery it drives, and a PAC- (rather than regret-) style learning guarantee, none of which appear in the platform's existing bandit or tabular-RL missions.
The obvious first attempt is to formalize Bellman rank as an unconstrained integer
parameter attached to the MDP, sidestepping the actual rank condition on the
Bellman-residual matrix; this is a trivializing formalization; Bellman rank must be
the least dimension admitting the stated bilinear factorization; see Formalization
scope. A second obstacle is that BiLinUCB's optimism is only "on average" with
respect to the initial state distribution (initValue), unlike LSVI-UCB's pointwise
optimism over every state and action — conflating the two confidence-set
constructions collapses the chapter's main conceptual contrast. Finally, the two
technical lemmas (29 and 30) separate a purely probabilistic statement (validity of
the empirical confidence set, via Hoeffding and a union bound) from a purely
deterministic consequence (the elliptic-norm bound and optimism, which hold on any
sample path where the probabilistic event occurred); keeping this separation is what
lets Proposition 47's proof combine them cleanly, and collapsing it into one
monolithic high-probability statement would misrepresent the book's proof structure.
The MDP, policy, and trajectory/history machinery (EpisodicMDP, Policy,
IsPolicy, Trajectory, Learner, probEvent) are reused unchanged from the
series' published RLBasics.Core/RLBasics.UCBVI definitions. The value-function
class is realized as an abstract finite, nonempty type Qc together
with an evaluation map qeval : Qc → ℕ → S → A → ℝ, kept fully abstract rather than
specialized to any concrete function class — specializing it to, e.g., linear
functions would collapse Proposition 47 back into a restatement of Proposition 46,
which is exactly the trivializing formalization this mission avoids. Bellman rank
(IsBellmanRank) is defined as the least natural number admitting the bilinear
factorization (an IsLeast over the coercion to HasBellmanRankLE), never as a free
parameter. Every realized per-step reward is taken equal to its conditional mean
throughout (exact, by the tower property, and not a restriction to
deterministic rewards). The elliptic norm of Lemma 30 is expressed via the direct
sum-of-squared-inner-products identity rather than introducing Matrix/matrix-inverse machinery, since no
milestone here needs an explicit matrix inverse. Every place the book writes
≲/∝/"a sufficiently large numerical constant" is formalized as an existentially
quantified universal constant, fixed ahead of every MDP, value-function class, and
instance — never depending on the instance itself. This
mission scopes entirely to the Bellman-rank track (Definition 8, BiLinUCB, Lemmas
29-30, Proposition 47); Proposition 46 (LSVI-UCB) and its supporting Lemmas 27-28 are
the chapter's motivating linear special case (Section 7.2) but are left out of this
mission's scope for time and are not claimed as proved by it — LSVI-UCB's
confidence-ellipsoid construction is materially different from BiLinUCB's
empirical-Bellman-residual confidence set (see Difficulty) and would need its own
milestone chain. A complete development needs no
infrastructure beyond what is already published in RLBasics.Core/RLBasics.UCBVI;
contributions completing the sorrys in the two technical lemmas and the goal are
welcome.
Every regret guarantee through Chapter IX compares the algorithm to the single best fixed decision in hindsight. That comparison is meaningless when the environment itself changes: a commuter's best route differs on weekdays versus weekends, an investor's best portfolio differs in a bull versus a bear market. A standard sublinear-regret algorithm, competing against one static comparator, will converge to some average compromise between regimes — exactly the wrong behavior when the regimes are genuinely different. Chapter 10 develops adaptive regret, a strictly stronger performance metric that demands low regret on every contiguous sub-interval of time simultaneously, and an efficient algorithm (Simple-FLH) that attains it for any base OCO algorithm at only a logarithmic additive cost.
For a comparator sequence with path length , the dynamic regret measures performance against a moving target (§10.1). The chapter's central object, adaptive regret (Definition 10.2), instead takes the supremum of ordinary regret over every contiguous sub-interval :
An algorithm is strongly adaptive if its adaptive regret matches its ordinary regret up to logarithmic factors in (§10.2.1).
The chapter builds toward this via the Fixed-Share algorithm (§10.3, Algorithm 30) — a variant of Hedge for the discrete expert-tracking problem, adding a uniform exploration term to each round's multiplicative update so that no expert's weight can vanish entirely — and then lifts it (§10.4) to the continuous OCO setting via Simple-FLH (Algorithm 32): run one fresh copy of a base OCO algorithm per starting time , and apply Fixed-Share to this set of "experts."
Online gradient descent with constant step size satisfies, for every comparator sequence ,
Given -exp-concave losses, Fixed-Share with guarantees, for every interval and every expert ,
Simple-FLH guarantees
Theorem 10.6 answers §10.2.1's own question — are there algorithms simultaneously optimal in
ordinary regret and adaptive regret? — affirmatively and constructively: Simple-FLH pays only an
additive over whatever regret its base algorithm already achieves, for
any -exp-concave-loss algorithm (in particular, taking to be the Online Newton
Step algorithm of Chapter IV gives an adaptive-regret algorithm with no asymptotic cost at all).
This is the chapter's capstone reduction, structurally similar to Chapter IX's OCO-to-PAC
reduction: a generic wrapper around any algorithm in a broad class, converting one guarantee into
a strictly stronger one. No prior art was found on the platform for adaptive regret, dynamic
regret, or Fixed-Share (planning search: q=adaptive+regret, q=dynamic+regret,
q=tracking+regret — no hits); this mission drafts all three results fresh.
Theorem 10.1's proof adapts Theorem 3.1's telescoping-sum argument to a moving comparator, picking up an extra term that Cauchy–Schwarz and the diameter bound convert into the path length — a genuinely different quantity from regret, not a trivial corollary. Theorem 10.3's proof (Lemma 10.4, an exp-concavity-driven potential argument structurally parallel to Hedge's own analysis in Chapter I) tracks how the fixed-share exploration term prevents any expert's weight from decaying below a usable floor, so that even an expert active only over a short sub-interval still has enough accumulated weight at time for the argument to close — the sup-over-all-intervals form of the guarantee is exactly what this floor buys. Theorem 10.6's own proof is comparatively short (a direct application of Theorem 10.3 to Simple-FLH's experts, instantiated at the expert matching the interval's own start point), but depends on both of the preceding results' analyses for its correctness.
AdaptiveRegretT is stated as a genuine supremum over a finite index set (subintervals of
[0,T-1]), so it is a maximum, never a real-suprema-of-an-unbounded-set junk value — the chapter
brief's own flagged pitfall (do not state it as a sum or average). ExpConcave is redeclared
locally (Chapter IV's own exp-concavity is not yet a published series definition; see
MODERATION_NOTES.md). IsFixedShareRun gives expert decisions xi as external data (matching
the book's own treatment, where "an expert i suggests decision x^i_t" is not itself part of
Fixed-Share's specification) — Theorem 10.3 is drafted at this level of generality, applying to
Fixed-Share on any experts, matching how the book itself proves it once and reuses it for
Simple-FLH. The goal (Theorem 10.6) connects Simple-FLH's experts to the base algorithm A via
the one property the book's own proof actually uses — each expert's interval-regret bound
inherited from A — rather than mechanizing Algorithm 32's exact re-indexing formula for
starting a fresh copy of A at each round, which never enters the numerical bound; see
MODERATION_NOTES.md. Three of this chapter's headline results (Theorems 10.1, 10.3, 10.6) are
stated in the book with a bare O(·); per CAPTAIN_BRIEF.md rule 7 and BRIEF.md's explicit
guidance, this mission uses the explicit constant each proof actually derives instead (Theorem
10.1's own η-parametrized inequality before the unstated optimal choice of η; Theorems 10.3
and 10.6's own final displayed bounds before they are folded into O(·) notation).
Not formalized: Definition 10.2's own generalization to -shifting comparators (a remark, not a
numbered theorem), §10.2.1's tightness/lower-bound claims (left as exercises in the book, no
proof given), Lemma 10.4 (an intermediate step whose content is folded directly into Theorem
10.3's own explicit bound), and §10.5's starred FLH2 (Theorem 10.7, poly-logarithmic running
time) — an advanced, optional stretch goal per BRIEF.md, not attempted given the chapter's
non-starred primary goal (Theorem 10.6) was reachable within budget.
The magic-square programme already on this platform works at fixed small orders: MacMahon's enumeration of the squares, both the magic count and the semi-magic count ; the classification of the normal squares; and the counts of the panmagic and symmetric order-three classes. Each of those is a statement about a single order. This mission changes the axis: it asks what the counting function does when the order itself is allowed to vary.
Timeline.
That split is the point of the mission, so it is worth naming before anything is proved. A quasi-polynomial of degree and period agrees with a degree- polynomial on each residue class modulo , the polynomials differing between classes; a polynomial is the case . For the magic squares the values do depend on modulo a period — at order three vanishes unless — and the same is true of every other class. For it never happens.
An semi-magic square of line sum is an array of nonnegative integers in which every row and every column sums to . Entries may repeat, and no condition is placed on the diagonals. Write for the number of such arrays.
In Lean the array is a Square n ℕ, that is, a Matrix (Fin n) (Fin n) ℕ; the condition is IsSemiMagic M t, which asks every rowSum and every colSum to equal t; and the counting function is semiMagicCount n t, the cardinality of the finset of all arrays over Fin (t + 1) satisfying IsSemiMagic. Restricting the entries to Fin (t + 1) loses nothing, since an entry of a square of line sum is at most .
Dividing by turns such an array into a doubly stochastic matrix, a nonnegative real matrix whose every row and column sums to . So is equally the number of lattice points in the -fold dilation of the Birkhoff polytope . Two geometric facts about are what the mission is about. Its dimension is : the entries satisfy line equations, exactly one of which is dependent. Its vertices are the permutation matrices, by the Birkhoff–von Neumann theorem, hence integral. The mission states that both facts are visible in the arithmetic of .
This is Theorem 1 of [BCCG 2003], stated there for . It is the shape of the truth, not a closed form, so no later improvement of the explicit formulas can invalidate it. The three parts are not independent: the degree is the dimension of , and the two identities are the reciprocity law for lattice-point counting, applied to .
The goal is far from the easy cases, and the mission is laid out so that each rung is an independently provable statement.
MagicSquares.semi_magic_count_two () and MagicSquares.semi_magic_count_three (MacMahon's ). Included as references, not as targets.Its leading coefficient is and its normalised volume is .
The result itself. The theorem makes the semi-magic squares countable in closed form at every order, and it is why the semi-magic count can be tabulated as a polynomial while the magic, symmetric and pandiagonal counts cannot: a polynomial is determined by finitely many values, a quasi-polynomial is not without knowing its period. The reciprocity identities are the same statement seen from the interior of , which is why they are what pins an explicit polynomial down once its degree is known. The order-four polynomial above was verified against direct enumeration on seventeen values of ; that verification is evidence, not proof, and is recorded because the general statement is what has to be proved.
Formalizing it. The theorem has been known since 1973 and has had an elementary proof since 1980; what does not exist anywhere is a machine-checked proof. Mathlib contains no Ehrhart theory, no quasi-polynomial machinery and no rational-generating-function toolbox — the string "Ehrhart" does not occur in it — so a formalization must construct its own lattice-point-counting argument for this family of polytopes, or find an elementary route that avoids polytopes altogether. Either outcome is reusable: the same absence blocks the quasi-polynomial counts , and of BCCG's Theorem 2, which the earlier missions approach only at order three.
The first idea anyone has is to interpolate: compute for enough values of and fit a polynomial. That works, and it is how the order-four rung was produced, but it cannot prove the general statement: the degree is what is being asserted, so the number of values needed is not known in advance, and with itself a variable no finite computation settles it. Interpolation is legitimate as a target at order four; it must not be mistaken for a route to the goal.
The second idea is to import the geometry as a black box: a rational polytope dilated by has a counting function that is a quasi-polynomial of degree equal to its dimension, with period dividing the least common multiple of the vertex denominators. That is Ehrhart's theorem, and it is the textbook route. It is not available here, and reconstructing it in general is a larger project than this mission; the statements the mission asks for are the ones that survive without it.
The part of the goal with no counting interpretation at all is the second line. is defined on ; the assertion that a polynomial agreeing with it there vanishes at and satisfies is a statement about the interior of the polytope, and it cannot be read off from the combinatorial definition. A solver who proves only the polynomiality and the degree has not finished the goal.
The formalization commits to the following conventions.
semiMagicCount n t, the Finset.card of the arrays over Square n (Fin (t+1)) satisfying IsSemiMagic. Entries are natural numbers, not integers or reals.ℚ and is quantified existentially. Negative arguments are handled by casting the integer into ℚ and evaluating there; Polynomial.eval₂ is unusable for the reciprocity, since it would need a ring homomorphism , which does not exist.p.natDegree = (n - 1) ^ 2, with natural-number subtraction, which makes the case harmless rather than degenerate.1 ≤ n is carried explicitly although the statement is meaningful at ; it matches the source.∀ t by a finite range of values, or replacing semiMagicCount by a smooth surrogate, would make the statement easy and empty. The universal quantifier over and the exact value of natDegree are what give the goal its content.Reusable beyond this mission: any development of lattice-point counting in the Birkhoff polytope, of dilations of rational polytopes, or of quasi-polynomials. The vocabulary of the programme (MagicSquares, MagicSquaresPandiagonal, MagicSquaresMostPerfect, MagicSquaresTransforms, MagicSquaresNormal3) is shared with the earlier missions and is included as reference items rather than redefined.
The real Clifford algebra is the smallest Euclidean Clifford algebra whose full structure carries a nontrivial multiplicity-eight representation-theoretic decomposition, and it has become a recurring object in programs that build internal gauge and family structure from Clifford generators rather than imposing it by hand. Within such programs, the single most basic representation-theoretic question one can ask about the algebra is: how does a distinguished subalgebra, acting by the adjoint action, decompose the odd part of the algebra as a representation?
This mission answers that question exactly, for the specific triple of bivectors built on the index set . The computation was carried out structurally (by splitting active indices from spectator indices) in the LeanProofs research program in 2026 and recorded with exact multiplicities; no machine-checked proof exists yet. The purpose here is to close that gap: the result is finite-dimensional linear algebra, completely within reach of a Lean 4 + Mathlib development, and every constant in it is explicit.
Fix with its standard inner product and the associated quadratic form , and let be the real Clifford algebra generated by symbols with
The algebra is -graded in the usual sense: it is the direct sum of its grade- subspaces, spanned by products of distinct generators, of dimension . The odd sector is the linear span of the odd grades,
On it, register three bivectors and their halved adjoint actions:
where . The triple satisfies the relations and cyclic permutations, so the generate a copy of with cyclically. The associated quadratic Casimir is the endomorphism
Because each is even, every preserves the odd sector, and so does .
the two eigenspaces spanning the whole odd sector. Equivalently, as a representation of the generated ,
eight copies of the spin-1 module and eight copies of the trivial module. The goal deliberately asserts only the eigenspace dimensions and their spanning property — the decomposition shape — not any particular basis or pairing.
the three weight spaces spanning the sector. This refines the goal: each copy contributes weights and each copy contributes weight .
The result itself. The spectrum pins down exactly how an acting from inside the algebra sees the odd sector: not irreducibly, but as a clean multiplicity split between spin-1 and spin-0. In the LeanProofs program this decomposition is load-bearing for everything downstream that distinguishes "active" indices from "spectator" indices — the multiplicity is the number of spectator degrees of freedom, and its appearance in the spectrum is what makes the split structural rather than coincidental. The weight decomposition further identifies the Cartan grading and is the natural first test case for any technology that must eventually handle larger Clifford algebras or other subalgebras.
Formalizing it. The computation is proved (structurally, by hand, in the research record) but not machine-checked. Everything needed lives in Mathlib: CliffordAlgebra, its grading CliffordAlgebra.evenOdd, Submodule, LinearMap, Module.finrank. What the mission produces is a fully verified finite spectral computation inside Clifford algebra — a reusable certificate that the platform's Clifford and grading infrastructure supports exact representation-theoretic bookkeeping, not just algebraic identities.
The obstruction is bookkeeping, not ideas. The natural attack — split indices into active and spectator , decompose as a tensor product of graded pieces, and read off the multiplicity from the spectator sector — requires transferring the action across such a tensor decomposition, which Mathlib does not provide ready-made for Clifford algebras. A purely computational route (fix the 64-element blade basis, build the matrices of the explicitly, compute kernels) is straightforwardly correct but laborious; making it readable is the real work. The statement is stated through arbitrary endomorphisms bound pointwise to the halved adjoint actions precisely so that solvers may choose either route.
The mission commits to: the quadratic form Q60 as QuadraticMap.weightedSumSquares ℝ (fun _ : Fin 6 => 1); generators e6 i = CliffordAlgebra.ι Q60 (Pi.single i 1); the odd sector as the Mathlib-native CliffordAlgebra.evenOdd Q60 1; and the registered triple as products of two generators. All theorems quantify over endomorphism witnesses bound pointwise to , so no particular matrix realization is privileged. Spectra are stated as eigenspace decompositions with exact Module.finrank multiplicities — never as pointwise eigenvalue claims, which would be false for mixed vectors. No trivializing formalization exists: the multiplicities are hard constants, and the dimension gate (32) rules out statements about degenerate sector choices. The definition file is reusable for any future mission on ; the su(2) relations and dimension gate are self-contained milestones. Contributions of either a structural (active/spectator split) or computational (explicit blade basis) proof are equally welcome.
Mathlib.LinearAlgebra.CliffordAlgebra.Grading (the evenOdd grading used as the odd sector).Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.
The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.
The links are , link carrying circuits. A route belongs to a set of routes, and the link-route incidence matrix records how much of each link a route needs: a call on route requires circuits from link and is lost if any link has fewer than free. (The classical case is a – matrix and exactly when ; from section 3.3 the book allows any non-negative integers.)
Calls requesting route arrive as a Poisson process of rate , independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing for the number of calls in progress on route , the process is Markov on
and is called a loss network with fixed routing.
Write for Erlang's formula, , published in mission I of this series. The Erlang fixed point equations are
The factor removes link 's own thinning from the product, so in the – case the argument is , the reduced load offered to link .
The goal fixes no formula for and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube ; uniqueness is the substance.
The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution on ; and the acceptance probability . Then the optimization side: that and the utilization are strictly increasing in , which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on , equation (3.6).
The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by . That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector coming from the maximum-probability problem.
Formalizing it. Nothing here is open. What the mission produces is the loss network model in
Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked
statement of the object the reduced-load approximation computes. It is also where this series'
earlier missions pay off: the uncapacitated network is literally the open migration process of
mission II with , , , and the exact distribution
(3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of
mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I
published.
Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization is strictly increasing in , which is itself a milestone here.
A second, formal difficulty: the equations involve , so a solution with would be meaningless. It is worth checking before starting that no such solution exists for , rather than assuming it.
Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only –), capacities are natural numbers, and arrival rates are positive reals. The feasible set is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.
Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route is and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; is the reciprocal of the sum in the book's notation. Capacities are assumed at least in the goal: a link with no circuits blocks everything, identically, and the factor would then be undefined rather than merely large.
The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.
Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the – equations (3.1) of section 3.2; the utilization function and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.
Existence of equilibrium is the first question any model of strategic interaction must answer, and the classical answer — Nash's theorem via Kakutani's fixed point theorem — asks for a convex, compact strategy space and continuous payoffs. Many of the models economists actually use do not have that: a firm's technology set can be discrete or irregular, and a payoff need only be upper semicontinuous, not continuous. Topkis [1979] showed that when a game's structure is instead order-theoretic — each player's strategies form a lattice, and the players' incentives reinforce each other in a precise sense — an equilibrium exists without any convexity or continuity assumption at all, and the proof method delivers something Kakutani's theorem cannot: a greatest and a least equilibrium point, with the whole equilibrium set forming a complete lattice. Zhou [1994] later showed the completeness of the equilibrium lattice in full generality; this mission formalizes the resulting theorem (Topkis's Theorem 4.2.1) together with its parametric extension (Theorem 4.2.2, established independently by Milgrom and Roberts [1990a] and Sobel [1988]), which shows how the greatest and least equilibria move as a parameter of the game — its technology, its cost structure — changes. This machinery underlies monotone comparative statics for games throughout economics: oligopoly models with strategic complements, coordination games, and search and matching models with increasing returns.
A noncooperative game consists of a finite player set , a set of feasible joint strategies (allowing the set of strategies feasible for one player to depend on the others' choices, so need not be a product set), and a payoff function for each player . Write for the strategies of every player but , for the section of at — player 's feasible strategies given the others' choice — and for player 's best-response set. The best joint response correspondence is . A feasible is an equilibrium point if for every player and every feasible deviation — no player can unilaterally improve.
A lattice is a partially ordered set in which every pair of elements has a join
and a meet . A function is supermodular on a subset if for all in it, and has increasing
differences in two of its arguments if is
monotone whenever . A game is a supermodular game
if is a sublattice, is supermodular in for every fixed
and every , and has increasing differences in for every — jointly, the conditions under which each player's own
strategy components are complements and complementary to the other players' strategies
(Theorem 2.6.1 of chunk 01-lattices/02-monotonicity's book).
If is a supermodular game, is nonempty and compact, and each is upper semicontinuous in on for every and every , then
is nonempty, has a greatest and a least element, and, under the order it inherits from , is itself a nonempty complete lattice.
Let be a partially ordered set and, for each , a supermodular game with nonempty, compact, and increasing in ; suppose each is upper semicontinuous in and has increasing differences in . Then for every there exist a greatest and a least equilibrium point of game , and both are increasing functions of on — the equilibrium set moves monotonically as the parameter increases.
Two supporting results are formalized as milestones because Theorem 4.2.1's own proof uses them directly: Lemma 4.2.1 (equilibrium points are exactly the fixed points of the best joint response correspondence) and Lemma 4.2.2, parts (b) and (f) (the best joint response set is a nonempty compact sublattice for every feasible , and the correspondence is increasing in ).
The result itself. Theorem 4.2.1 is the lattice-theoretic alternative to
Nash/Kakutani existence: it needs no convexity of and no continuity of
(upper semicontinuity suffices), and in exchange it delivers a greatest and a least
equilibrium — with an explicit order-theoretic characterization via Theorem 2.5.1 of
chunk 01-lattices — and the guarantee that the entire equilibrium set is a complete
lattice, not merely nonempty. Theorem 4.2.2 gives this existence result teeth for
applied comparative statics: it says that if a firm's cost structure, a market's demand
parameter, or any other feature of the game increases (in the sense of the induced set
order on and increasing differences in the payoffs), the extremal equilibria
increase too — the qualitative content behind results such as "more competition leads
to lower prices" in supermodular oligopoly models.
Formalizing it. The platform's existing Nash-equilibrium theorem
(AGT.nash_existence, Theorem 1.8 of Algorithmic Game Theory) is a Brouwer/Kakutani
argument for finite games with mixed strategies: it needs finiteness of every player's
strategy set (so that mixed strategies form a compact convex simplex) and gives no
lattice structure on the equilibrium set at all. Theorem 4.2.1 is a different
technique entirely — it needs no finiteness, no mixing, and no convexity, and its
conclusion (a complete lattice of equilibria) is exactly the content Brouwer/Kakutani
cannot give. This mission is therefore not a restatement of Nash's theorem in different
notation, but a second, independent existence technique with a strictly different
structural payoff, formalized here for the first time on the platform. It builds
directly on chunk 01-lattices's Theorem 2.5.1 (Zhou's fixed point theorem for
increasing correspondences) and chunk 02-monotonicity's supermodularity/increasing
differences definitions, both formalized earlier in this series.
The natural first idea for existence — "the best joint response correspondence has a fixed point by some general fixed-point theorem for correspondences" — needs the correspondence to be convex-valued and upper hemicontinuous for a Kakutani argument, neither of which supermodularity or upper semicontinuity alone supply: a best-response set under only upper semicontinuity can be a disconnected, non-convex set (e.g. the maximizers of a supermodular but non-quasiconcave function). The actual route goes through order instead of topology: Lemma 4.2.2 shows the best joint response set is a compact sublattice (hence subcomplete, by Theorem 2.3.1) and that the correspondence is increasing under the induced set order, which is exactly the hypothesis Theorem 2.5.1's non-constructive supremum/infimum construction needs — no convexity anywhere. A second subtlety, which the mission is careful not to elide: the equilibrium set of a supermodular game need be neither compact nor a sublattice of when there are more than one player (Topkis's Examples 4.2.1 and 4.2.2 exhibit both failures); only the weaker claim — a complete lattice under the inherited order — is true in general, and that is what Theorem 2.5.1(b) supplies.
A joint strategy is represented as a dependent function ∀ i, Fin (m i) → ℝ over a
finite player type ι, with a player's own strategy accessed and overwritten via
Function.update, so that is never reified as a separate object — every
statement about or membership in substitutes y for
x's own i-th coordinate directly. IsSupermodularGame reuses chunk
02-monotonicity's SupermodularOn and IncreasingDifferencesOn verbatim, applied to
each player's own payoff, rather than restating the supermodularity/increasing-
differences conditions from scratch — a formalization that inlined a weaker,
ad hoc notion here (e.g. supermodularity of the joint payoff vector rather than each
player's own payoff in their own strategy) would trivialize the connection to chunk
02-monotonicity's theorems that the book's own proof relies on. Theorem 4.2.1's
"nonempty complete lattice" conclusion is formalized, as in chunk 01-lattices, via
IsLUB/IsGLB on the subtype of equilibrium points — never as membership of the
ambient supremum/infimum in the equilibrium set, which the book's own
Examples 4.2.1–4.2.2 refute; a solution that instead proved the equilibrium set compact
or a sublattice of would be proving a strictly stronger and false claim.
Only parts (b) and (f) of Lemma 4.2.2 are formalized, since those are the only two of
its eight parts the proof of Theorem 4.2.1 uses; a complete development still needs
chunk 01-lattices's Theorem 2.3.1 (subcomplete iff compact) and Theorem 2.5.1/2.5.2,
and chunk 02-monotonicity's Theorem 2.8.1 and Corollary 2.7.1, none of which are
restated here.
Two-player zero-sum games and linear programming are, on their surface, unrelated pieces of 20th-century mathematics: von Neumann's minimax theorem for games (1928) was proved with tools from topology, and linear programming duality (Dantzig, 1940s) with convexity and geometry. Yet the two are formally equivalent — Dantzig recounts von Neumann conjecturing the equivalence outright, on first hearing a description of linear programming, because he had "just recently completed a book with Oscar Morgenstern on the theory of games" [Albers, Alexanderson, and Reid, More Mathematical People, 1990]. Freund and Schapire (1999) later showed that both concepts reduce, in one uniform way, to online regret minimization: a decades-old topological existence proof and a decades-old LP-duality argument both become corollaries of a single fact about no-regret learning. This mission formalizes the algorithmic content of that reduction — Hazan's Lemma 8.4, which is not merely an existence statement but a concrete, efficient algorithm with an explicit convergence rate.
A two-player zero-sum game in normal form is a real matrix (Hazan restricts entries to for interpretability as losses/rewards, a convention this mission's theorems drop as inessential — the argument is invariant to scaling and shifting). The row player picks a mixed strategy in the probability simplex ; the column player picks . The row player's expected loss, and simultaneously the column player's expected reward, is the bilinear form .
The row player's guaranteed loss is : the smallest loss she can secure no matter what the column player does.
Symmetrically, the column player's guaranteed reward is . Always ("weak duality" — an
elementary max-min/min-max inequality, Direction 1 of Section 8.3). Von Neumann's minimax
theorem (Theorem 8.3) is the nontrivial converse: , a common value
called the value of the game, whose optimal strategies form a Nash
equilibrium — already on the platform as AGT.zero_sum_minimax.
Algorithm 28 ("Simple LP", p. 147) computes an approximate equilibrium constructively. The row player runs a multiplicative-weights / Exponentiated Gradient update against the sequence of best-response losses the column player generates in a repeated -round play of the game: starting from the uniform strategy , at each round the column player best-responds with , and the row player updates . The algorithm returns the time-averaged strategy .
for the vector returned by Algorithm 28 after rounds with learning rate . The book calls a "-approximate solution" to the zero-sum game — and, via Section 8.2.1's equivalence, to the linear program the game encodes — in exactly this sense. The goal is stated against , the quantity the algorithm's own analysis produces; Theorem 8.3 identifies it with and with the book's , so nothing about the bound is lost by this choice of rendering.
the external-regret bound the row player's multiplicative-weights update achieves against the adaptively-chosen linear loss sequence — the single analytical fact the goal's proof needs.
The result itself. Lemma 8.4 gives a genuinely efficient algorithm: rounds of a trivial multiplicative update to reach an -approximate value and equilibrium of an zero-sum game, and — through the equivalence with LP duality — an approximation algorithm for a broad class of linear programs, predating and prefiguring the multiplicative-weights-based approximation schemes surveyed by Arora, Hazan, and Kale (2012). It is also the constructive engine behind Theorem 8.3: unlike the classical topological proof of the minimax theorem, this one produces the equilibrium, not just its existence.
Formalizing it. The equilibrium-existence half of this story, Theorem 8.3, is already a
published, proved-format Prove2Me theorem (AGT.zero_sum_minimax, from the Algorithmic Game
Theory series) and is reused here as a reference item rather than redrafted. What that theorem
does not capture — and what makes this mission non-trivial rather than a restatement — is the
quantitative, algorithmic content: that one specific, simple, Hedge-type update, run for a
specific number of rounds, provably gets within a specific, explicit distance of the value,
using only the existence of some sublinear-regret online algorithm as a black box.
The tempting shortcut is to formalize only "no-regret learning dynamics converge to an
equilibrium" as a qualitative statement, discharging it by citing AGT.zero_sum_minimax
(equilibria exist) plus a generic regret bound. That collapses Lemma 8.4 into a restatement of
Theorem 8.3 and drops exactly what is new here: the explicit rate , tied
to one concrete update rule (Algorithm 28) rather than an arbitrary sublinear-regret black box.
The real content is in chaining three quantitative facts — Eq. (8.1)'s specific regret bound for
the multiplicative-weights update, the column player's best-response equality (Eq. (8.2)), and
the definitional unfolding of — with none of the slack that a purely qualitative
"an algorithm with sublinear regret exists" argument would tolerate.
Matrices are Matrix (Fin n) (Fin m) ℝ with n, m ≥ 1 (empty strategy sets are excluded
throughout, matching this mission's reference item AGT.zero_sum_minimax); mixed strategies use
Mathlib's stdSimplex ℝ (Fin n). lambdaR/lambdaC are rendered with iInf/iSup over simplex
membership, the same convention Introduction to Online Convex Optimization III fixed for
RegretT earlier in this series. Algorithm 28's run is packaged as a Prop-valued structure
(IsSimpleLPRun) rather than a computable function, in the style of this series' other
algorithm-run definitions (IsHedgeRun, IsOnlineGradientDescent): initial uniform strategy,
a best-response condition on the column player at every round, and the multiplicative-weights
recursion on the row player, with the learning rate η left free and fixed to
√(2 log n / T) only at the point the theorems need the book's specific constant.
The trivializing risk here is stating only that some sublinear-regret algorithm secures the
bound (already implied, vacuously, by AGT.zero_sum_minimax plus any regret bound); this
mission rules that out by fixing the exact update rule of Algorithm 28 in IsSimpleLPRun and
proving the bound for that rule specifically, with the book's exact constant √(2 log n)/√T, not
an unspecified O(·).
Chapter 5's Corollary 5.7 (the general RFTL/Exponentiated-Gradient regret bound) belongs to a
different mission of this series and is not imported; eg_regret_bound restates, locally and
self-containedly, exactly the instance of it this chapter's proof needs. A later mission for
Chapter 5, once published, could supersede this local restatement by specializing its general
bound — a natural contribution for a solver with that mission's Lean available.
Online convex optimization (OCO) models a repeated decision process: at each round a learner picks a point in a convex set, an adversary (or the world) reveals a convex cost function, the learner pays that cost at its own point, and the process repeats. No statistical assumption on the sequence of costs is made. This model, introduced by Zinkevich [Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003], underlies most of modern online learning: portfolio selection, online routing, and — through its special case of stochastic optimization — the training of essentially every large machine-learning model in current use, since stochastic gradient descent (the subject of §3.4 of this chapter) is exactly an application of the regret bounds proved here.
The algorithm this chapter introduces, online gradient descent (OGD), is the field's default answer: take a gradient step against the most recently observed cost, project back onto the feasible set. It predates OCO itself as a heuristic, but Zinkevich's contribution — and this chapter's — is the regret analysis: a guarantee that holds against every sequence of costs, adversarially chosen, with an explicit, small constant. Precursors for less general settings appear in Kivinen and Warmuth [1997]; logarithmic-regret algorithms for OCO, the subject of §3.3 here, are due to Hazan, Agarwal and Kale [2007].
Fix a convex set in a real inner product space, playing the role of the decision (or "action") space, and a sequence of cost functions , each convex. At round , the learner (not knowing ) plays a point , then observes and pays . Regret after rounds compares the learner's cumulative cost to that of the single best fixed decision made with hindsight of the whole sequence:
A learner with regret is, on average, eventually as good as the best fixed point in , even though it never knew the cost sequence in advance.
Two chapter-wide parameters bound how hard an instance can be: , the diameter of ( for all ), and , a common bound on the gradient norm of every over ( for all ), which implies but is strictly stronger than -Lipschitzness on . Online gradient descent (Algorithm 8) plays arbitrarily, then at every round sets and projects, , for a sequence of step sizes chosen in advance.
using step sizes . This is the chapter's — and arguably the book's — central result: the simplest algorithm for the fully general OCO protocol already attains regret, with an explicit small constant, against convex Lipschitz costs with no further structure.
Any algorithm for OCO incurs regret in the worst case: no algorithm, however clever, can improve asymptotically on Theorem 3.1's rate. This is the weaker, worst-case-existence half of the theorem (see Formalization scope).
If every is additionally -strongly convex, the same algorithm — with only the step sizes changed to — achieves
Strong convexity is a strictly stronger hypothesis than convexity, so this target does not subsume the goal; it sits alongside it as the chapter's second, sharper regime.
Theorem 3.1 is the reference point against which every later algorithm and every later chapter's improvement (Online Newton Step, RFTL, adaptive-regret methods) is measured: any new algorithm for OCO is judged first by whether it matches this rate, then by what extra structure lets it do better. Theorem 3.2 closes the question for the general convex-Lipschitz class: is not an artifact of a loose analysis, it is information-theoretically necessary. Theorem 3.3 identifies the one extra hypothesis (strong convexity) that buys an exponential improvement in the horizon dependence, from to , without any other change to the algorithm — the same phenomenon that in the book's Chapter 2 separated well-conditioned from general convex offline optimization, now transplanted to the online, adversarial setting.
None of these three statements has a machine-checked proof on the platform prior to this mission (see Formalization scope below for what was checked). Formalizing them establishes the regret protocol and the OGD algorithm as reusable definitions for the rest of this thirteen-chapter series, several chapters of which (Online Newton Step, RFTL, bandit convex optimization) build directly on Algorithm 8 or its regret guarantee.
The regret bound's proof (Theorem 3.1) is short but not naive: bounding by convexity alone gives no telescoping structure, so the argument instead bounds it using the projection step — the Pythagorean inequality for — applied to the specific point . This turns the per-round convexity bound into a telescoping sum in , and only the resulting sum, evaluated with the specific step-size schedule , produces the rate; a constant or linearly growing step size does not. The same projection argument is reused for Theorem 3.3, where the strong-convexity inequality is engineered to make the terms cancel exactly against the projection telescoping, leaving a harmonic sum. Theorem 3.2's difficulty is of a different kind: it is a lower bound over every algorithm, proved by exhibiting a randomized hard instance (the hypercube with sign-vector linear costs) on which no algorithm can do better than random guessing in expectation.
is formalized as a subset of an arbitrary real, complete inner product space (not
fixed to ), since the chapter's argument uses only Hilbert-space structure.
Rounds are 0-indexed (Finset.range T) rather than the book's 1-indexed rounds, so a step
size stated here at round is the book's step size at round . D and G are
carried as shared section hypotheses (the chapter-wide diameter and gradient-norm bounds),
not re-derived or re-stated per theorem; G is formalized exactly as the book defines it
(p. 20: a bound on over , via Mathlib's HasGradientAt), not as the
weaker two-point Lipschitz condition it implies — an earlier draft used the weaker
Lipschitz hypothesis and was corrected during moderation, since it made the drafted
theorems strictly stronger than the book's own (true by an added argument the book does not
give, but not faithful to the stated proof). The projection step is formalized relationally
(IsMetricProjection, an arbitrary closest point) rather than as a canonical function,
since a general convex set need not come with one built into Mathlib.
For Theorem 3.2, this mission formalizes the theorem's main sentence — the worst-case existence claim — quantifying over "any algorithm" as a non-anticipating map from the full cost sequence to the play sequence, with the hard cost sequence existentially quantified after the algorithm and the horizon: for every algorithm and every horizon there is a cost sequence forcing regret against it. (An earlier draft quantified the cost sequence first — one fixed sequence defeating every algorithm — which is false: a constant algorithm playing a minimizer of that one sequence has zero regret against it; this was corrected during moderation.) It does not formalize the theorem's parenthetical strengthening, that the same bound holds even when costs are drawn from a fixed stationary distribution; that claim is about expected regret of a deterministic algorithm against a random cost sequence, and would need a probability-space formalization of the OCO protocol that this mission's definitions do not build. A formalization limited to the deterministic worst case does not trivialize the theorem: it is exactly the inequality " cannot be improved," stated without the randomization machinery of its proof.
Theorem 3.4 (the stochastic gradient descent corollary, via a noisy gradient oracle with bounded second moment) is not included: it needs an expectation over a random oracle applied at a random, round-dependent point, which is a substantially heavier probabilistic object than the deterministic protocol built here, and is left for a future mission or an extension of this one.
Consider a decision maker who must choose, at each of rounds, between two actions on the advice of "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.
At each round , a decision maker chooses one of two actions, or . After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. experts also each commit to a prediction every round, and the decision maker may consult their record.
The Weighted Majority (WM) algorithm maintains a weight for each expert , initialized to . It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by for a fixed parameter , leaving correct experts' weights unchanged. denotes the algorithm's own mistake count through round , and expert 's.
The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, , and follows that expert's prediction; is its expected mistake count.
Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses suffered by expert at round . It samples expert with probability from weights updated multiplicatively in the loss, . Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round is .
where . This is the chapter's most general result and the one the book reuses later on; it leaves free (no asymptotic tuning), so it survives whatever later chapters do with .
Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two
maximally simple experts, any deterministic strategy is beaten by a factor of by an
adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable —
first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic
penalty from to ), then Theorem 1.5 removes the
binary-mistake restriction altogether, replacing it with an explicit second-moment correction
term that vanishes as losses shrink. Together they trace
the chapter's own narrative arc from "no algorithm beats " to "an explicit, parameter-free
family of algorithms gets within of the best expert for any ."
All four results are proved by the book via the same device — a potential function
— one of the first instances of the potential-function method that
recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and
throughout online learning generally. None of these four statements, in this exact form, has a
formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest
existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope
below), proves an asymptotically similar bound by an entirely different route and under a
different loss model.
The natural first attempt at any of these bounds is to track (or , or ) directly and induct on ; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round says nothing about round 's outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using , or, for Hedge, for ) and a lower bound via the single best expert's weight, — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing .
Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight
sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own
output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun
fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and
x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote
prediction rule explicitly (per the triage rubric, the algorithm is part of the audited
statement here, not a black box the proof is free to instantiate). Randomization in RWM and
Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the
inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as
a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification
explicit ("denote in vector notation the expected loss of the algorithm by
"), so no probability space is introduced. Theorem
1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction
(prediction at round depends only on outcomes before ), instantiated at the book's own
two-expert construction (one expert always predicts , the other always ) rather than a
fully general -expert adversary argument — a strictly weaker instance of the general claim,
but the exact one the book's proof establishes, so no scope is lost relative to what is proved.
is kept as an explicit free parameter throughout, per the book's own presentation
(no substitution of the corollary's optimized
into the milestone statements).
A trivializing formalization to rule out: fixing (a single expert) would make Lemmas 1.3–1.5 hold vacuously with regardless of the potential-function argument; every formal statement here quantifies over an unconstrained with , not a hard-coded small case.
The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the
book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's
proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves
for exponential weights on the simplex against -valued losses,
via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a
different proof technique, a different (bounded, not merely non-negative) loss assumption, and
stated for simplex-comparator regret rather than the per-expert loss comparator here; it is
listed as a reference/comparison point, not reused.
Reinforcement learning (RL) formalizes sequential decision-making under uncertainty: an agent repeatedly observes a state, takes an action, receives a reward, and transitions to a new state, with the goal of maximizing cumulative reward over an unknown environment. It underlies applications from game-playing agents to robotics and adaptive medical treatment. What separates RL from the bandit and contextual bandit problems of earlier chapters in this series is state: the environment carries information forward across time steps, so a good action now can pay off many steps later, and a poor exploration strategy can take exponentially long to discover it. This mission formalizes the foundational results of finite-horizon episodic RL — the Markov Decision Process (MDP) model, the Bellman-optimality principle that makes dynamic programming possible, and the analytical toolkit (the performance-difference and Bellman-residual-decomposition lemmas) used throughout the field's regret analyses — culminating in a polynomial regret guarantee for UCB-VI, the canonical optimism-based algorithm for tabular RL introduced by Azar, Osband, and Munos (Minimax Regret Bounds for Reinforcement Learning, ICML 2017, arXiv:1703.05449).
A finite-horizon episodic Markov Decision Process consists of a finite state space , a finite action space , a horizon , per-layer transition kernels and reward distributions , and an initial state distribution . An episode unrolls for : the learner selects an action under a randomized non-stationary policy (each ), receives reward , and transitions to . The value of is , and the state-action and state value functions , are the analogous reward-to-go quantities from layer onward. In the online RL problem, is unknown, the learner interacts with it for episodes, and the goal is to minimize the regret against the best policy .
for the UCB-VI algorithm run with the explicit bonus , under Assumption 6 (deterministic, known, -bounded rewards). This is the weakest stable form of the guarantee: it fixes only the shape of the bound (polynomial in , logarithmic in ), leaving the exact leading constant — which the book itself does not pin down on this page — outside the formal claim.
Reaching it rests on three structural facts, each formalized as a milestone in attack order:
The result itself. Theorem 1 is the chapter's headline result: the first guarantee, in this development, that a learning algorithm — one that does not know the environment's transitions in advance — can achieve regret growing only polynomially in the size of the state space, the action space, and the horizon, and only as in the number of episodes. The chapter's own "combination lock" example (Figure 8) shows this is not automatic: naive exploration strategies (such as -greedy, which suffices for ordinary bandits) incur regret exponential in the horizon on some MDPs with as few as states. UCB-VI's guarantee is the sample-complexity foundation on which essentially every subsequent result on tabular, linear, and general function-approximation RL in the book is built.
Formalizing it. No part of this chapter's mathematical content already has a
faithful counterpart on the platform (see Difficulty, below, and Formalization
scope). This mission contributes: (i) a from-scratch Lean formalization of the
finite-horizon episodic MDP model and its value functions, faithful to the book's
/-indexing and reward-distribution conventions; (ii) faithful statements
(drafted with sorry, not yet proved) of Proposition 25 and Lemmas 13–15; and (iii) a
faithful statement of Theorem 1 itself, including a from-scratch construction of the
finite -episode adaptive interaction process needed to make sense of a
high-probability regret guarantee. Proving these — Proposition 25 by backward
induction, Lemmas 13–15 by telescoping, and Theorem 1 by combining Lemma 15's
optimism bound with a concentration argument bounding the estimation-error and
martingale terms of Eqs. (5.30)–(5.33) (omitted here; see Difficulty) — is open work
for solvers.
The obvious approach to Theorem 1 — bound the regret episode-by-episode using only the fact that is close to in some fixed sense — fails because 's error is itself random (it depends on the transitions observed so far) and compounds across layers of dynamic programming. Lemma 15 defuses the compounding: it shows the sub-optimality gap is additive in the per-layer Bellman residuals rather than multiplicative, provided is optimistic. Making optimistic with high probability, in turn, requires a concentration argument for the empirical transition estimates (an application of Freedman's or the Azuma–Hoeffding inequality, not included among this mission's milestones) and a union bound over all — accounting for the inside the bonus's logarithm. The final regret sum further requires bounding by a pigeonhole/potential-function argument over the visitation counts, which is where the scaling — rather than a naive — originates. None of this concentration or counting machinery is included in the current milestones; a solver attempting Theorem 1 needs it as prerequisite lemmas.
MDP and value functions. States and actions are finite types (Fintype); layers
are represented -indexed throughout the Lean development (the book's layer is
h - 1), with the terminal convention V _ _ H _ = 0 matching .
Since every value/expectation formula in this chapter uses the reward distribution
only through its mean, EpisodicMDP.R records that
mean directly — equivalent, by linearity of expectation, to carrying the full
distribution, and changing no theorem's content. Transition kernels and policies are
represented as plain real-valued functions (S → A → ℝ-style) rather than as
Mathlib's PMF, with IsPolicy/the EpisodicMDP structure's own proof fields
asserting the probability-distribution properties (nonnegativity, summing to )
where the book requires membership in or a well-formed kernel;
this keeps every expectation a finite Finset.sum, needing no measure theory. The
optimal value functions Qstar/Vstar are defined as literal suprema over the
entire (uncountable, since ) policy type — not via a recursive
shortcut — which is what rules out the trivializing formalization of Proposition 25:
defining Vstar by the very recursion the proposition asserts would make the
proposition a tautology, whereas here it is a genuine claim about a supremum over an
enormous space of competitor policies.
UCB-VI and Theorem 1. Because , , , and are all finite, the -episode
adaptive interaction (in which round 's policy is a function of the realized
history of the first episodes) is modeled as a finite probability space: the
outcome type Fin T → Trajectory S A H is a Fintype, "probability" is a finite sum
over it, and "with probability " is a plain inequality between two real
numbers — no MeasureTheory is used anywhere in this mission. The universal constant
in Theorem 1 is existentially quantified (∃ C > 0, …) rather than given as a
literal numeral, since its value is not pinned down by the book on this page and this
mission does not carry out the (non-milestoned) concentration argument that would
derive it; this is the convention adopted throughout for the book's own ""
notation. The empirical-transition estimator inside is defined to be when
(no data yet collected for that pair) — a boundary case Eq. (5.25)
does not address, resolved here by convention rather than proof.
Prior art. The platform's existing BanditAlgorithm.UCRL2Algorithm mission
formalizes UCRL2 for the average-reward, infinite-horizon MDP setting with a
diameter parameter, and its Bellman-optimality statement is the average-cost
optimality equation — genuinely different from this chapter's finite-horizon
episodic Bellman recursion, even though both go by the name "Bellman optimality."
No reference item was reused; every definition and theorem in this mission is
drafted from scratch. Both missions bound regret via optimism over a confidence set
of models, but for different objectives (average reward vs. finite-horizon
cumulative reward) and different MDP classes.
Reusable infrastructure and open contributions. EpisodicMDP, Policy,
V/Q/Qstar/Vstar, and stateDist/stateExp are reusable by any future mission
on finite-horizon episodic RL in this book's later chapters. Contributions welcome:
proofs of the four milestone lemmas (by backward induction and telescoping,
respectively); the concentration lemmas underlying Theorem 1's optimism guarantee
(Eqs. (5.30)–(5.33) of the source, not milestoned here); and the final regret proof
combining them.
Let be an odd squarefree positive integer and let be a set of units modulo with . Then : every residue class, unit or not, is a sum of three elements of .
This is Corollary 1.5 of Xuancheng Shao, A density version of the Vinogradov three primes theorem, Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2. It is the local input to Shao's density version of the three primes theorem, and it is a clean finite statement in its own right.
At the set has five elements, so exactly, and is not a sum of three of its elements. The hypothesis therefore fails by nothing at all and the conclusion already fails. If is weakened to , the statement is false.
The corollary cannot be proved by induction on sets. Passing from to a prime factor splits into fibers of different densities, and a set is the wrong object to carry through that split. The induction has to run on functions , and the corollary is the case of a weighted statement, Proposition 1.4. That is the one step from which the rest follows.
The weighted statement then splits at the primes 3 and 5. For coprime to 30 the induction runs on the prime factors, using Cauchy-Davenport-Chowla for three sets modulo a prime, and it produces the stronger bilinear conclusion . The modulus 15 is handled separately by a linear program over the eight units. Two averaging inequalities, one symmetric and one asymmetric, are what turn a density above into a single good triple in both halves.
The nine milestones follow Shao's own numbering: the two averaging inequalities of Section 2 (Lemmas 2.1 and 2.2), the finite check at (Lemma 2.3), the three-set Cauchy-Davenport-Chowla bound, the divisor reduction that lets the proof assume , the induction away from 3 and 5 (Proposition 3.1), the modulus-15 case (Proposition 3.2), the weighted local result (Proposition 1.4), and the counting bridge that the units modulo number .
Every item is stated in Mathlib primitives alone, so the mission needs no definition items: IsUnit, Nat.totient, Odd, Squarefree, Finset, and Antitone. The set of units modulo is written Finset.univ.filter (fun x => IsUnit x) at each use rather than through a defined abbreviation, so a reader auditing a statement has to trust only Mathlib. That is also why open scoped Classical appears in the preamble.
The density hypothesis is written 5 * Nat.totient m < 8 * A.card, which is cleared of division so the whole statement stays in with no rounding.
Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors and , the primal is within of optimal.
The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.
Fix finite index types (primal variables) and (primal constraints), a matrix , a cost vector and a right-hand side . The covering primal and packing dual are
Note the index convention: carries the primal-variable index first, so the primal constraint indexed by sums over and the dual constraint indexed by sums over .
Given , the pair satisfies approximate complementary slackness when
For a primal-feasible , a dual-feasible , and satisfying the two conditions above,
Taking recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.
with no nonnegativity assumption on , or beyond feasibility itself.
Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of , produce a dual optimum of of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.
The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.
This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.
It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.
The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on versus and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.
Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.
Mirror symmetry began as an empirical observation in string theory: certain pairs of Calabi–Yau threefolds, with no evident geometric relation, give rise to the same physical theory, and invariants that are hard to compute on (counts of holomorphic curves) turn into easy computations on (variations of complex structure). The paper Mirror symmetry is T-duality by A. Strominger, S.-T. Yau and E. Zaslow, Nucl. Phys. B 479 (1996) 243–259, proposed the first structural explanation: should carry a fibration by special Lagrangian 3-tori, the mirror should be obtained by replacing each fibre with its dual torus, and the mirror map should be fibrewise T-duality. This proposal is now called the SYZ conjecture, and it organises most later geometric work on mirror symmetry.
The string-theoretic argument of Sections 1–2 of the paper is heuristic and is not formalizable as stated. Section 3 is different: it is a self-contained piece of differential geometry about the moduli space of a special Lagrangian submanifold together with a flat connection on it. This mission formalizes Section 3.
A short timeline of the mathematics the section rests on:
Fix . The ambient Calabi–Yau manifold is modelled by , carrying
Here is the standard Hermitian product of , conjugate-linear in its first argument.
The brane is an -torus. It is presented by its universal cover: a map that is periodic up to translation,
for a fixed family of periods . Such an is exactly a map of the torus into the complex torus , and integration over is integration over the unit cube .
Write for the partial derivatives of . The map is Lagrangian at if for all , i.e. ; it is special Lagrangian if in addition , i.e. . This is the supersymmetry condition of the paper (Section 2, conditions (ii) and (iii)). The induced metric is , the volume density is , and the second fundamental form of a Lagrangian immersion is the totally symmetric tensor
Given a family of such maps, its deformation -form is
the -form obtained by contracting the velocity into the Kähler form. For an -parameter family , , one gets such forms , , one per moduli direction.
The moduli data of Section 3 is a smooth -parameter family of special Lagrangian tori, all with the same periods, subject to two normalizations taken from the paper: each is harmonic for the induced metric (closed and co-closed), and the cohomology class of each is constant along the family. The (McLean) metric on the moduli parameters is
The full moduli space of the paper also records the flat connection; its moduli form a torus of the same dimension, with coordinates . On , modelled by with coordinates , the paper puts the block-diagonal metric and the constant almost complex structure , , with fundamental -form .
The goal theorem is the conclusion of Section 3: for every such family, the fundamental -form of the moduli space is closed,
and since is constant in these coordinates it is integrable, so is Kähler.
The milestones are the numbered intermediate results of the paper, in the paper's own order:
$$\textbf{ closed:}\quad \partial_c \int_L \theta^{a_1}\wedge\cdots\wedge\theta^{a_n} = 0 .
\textbf{Hessian} \Rightarrow \textbf{Kähler:}\quad \partial_a g_{bc} = \partial_b g_{ac} ;\Longrightarrow; d,\omega_{\mathcal M} = 0 .$$
Together, Propositions 1 and 2 are the statement that the tangent space to the moduli space consists of harmonic -forms — McLean's theorem in the form the paper uses it. Eq. (3.4) is the technical heart, and the last milestone is the step from it to the goal.
The result. Section 3 supplies the only rigorous mathematics in the paper. It says that the object the physics predicts to be a Calabi–Yau manifold — the moduli space of a supersymmetric brane — does carry the first piece of that structure, a Kähler metric, and that it carries a natural -form which, for toroidal branes, is a holomorphic -form and hence a candidate for the Calabi–Yau form of the mirror. Eq. (3.4) says the McLean metric is locally the Hessian of a potential; this affine-Hessian structure of the SYZ base is the starting point of the later large-complex-structure-limit programme.
Formalizing it. The Section 3 results have rigorous published proofs (McLean for the tangent space, Hitchin for the Hessian property), but no machine-checked proof exists for any of them, and Mathlib currently has no special Lagrangian geometry, no Hodge theory, and no differential forms on manifolds. The mission therefore also produces reusable infrastructure: a workable coordinate model of calibrated submanifold geometry, the variation formulas for the induced metric and for the pullbacks of and , and the Hessian-metric criterion for a Kähler structure, which is independent of the rest and reusable wherever affine-Kähler geometry appears.
The obvious approach to the goal — "the metric is Hessian, so take the potential and write down the Kähler form" — is not available: the potential is not part of the data, and producing it requires the symmetry first. That symmetry is the hard step, and it is hard for a specific reason: differentiating in the direction produces four terms — from , from , from the inverse metric , and from the volume density — and only their sum is symmetric in . Two of them are killed by an integration by parts that needs both harmonicity of and compactness of (this is where the torus, and not a coordinate patch, is essential); one is killed because a special Lagrangian submanifold is minimal, so the mean curvature term in vanishes; what survives is , which is symmetric because is a symmetric -tensor. Every one of those four cancellations has to be carried out.
Proposition 2 carries a separate difficulty: it is an identity between the variation of a determinant and a divergence, and it is false without the hypothesis that is special Lagrangian at the point in question — for a merely Lagrangian there is a further term proportional to the Lagrangian angle.
The formalization commits to the following, all of which are visible in the definition item and none of which are silent:
fderiv returns at a point of non-differentiability, so a statement about derivatives of a non-smooth map is a statement about zeros; every item therefore carries an explicit smoothness hypothesis, and the moduli-level items carry it inside the family structure.A complete development needs, beyond the definition item: the chain and product rules for fderiv on , symmetry of second derivatives, differentiation under the integral sign on a compact box, integration by parts for periodic functions on , and the derivative of and of matrix inversion. The last two, and the Hessian-implies-Kähler milestone, are reusable outside this mission. Contributions that replace the flat ambient by a general Kähler ambient chart, or that lift the model to Mathlib manifolds once differential forms exist there, are welcome and would supersede parts of this development.
The local theory of curves describes what happens near one point; the global theory asks what a curve must satisfy because it closes up. Two classical statements make the difference visible. The isoperimetric inequality says that among all simple closed plane curves of a given length, the circle encloses the largest area — a question already settled in intent by the Greeks, but given a satisfactory proof only in the nineteenth century, and the short proof reproduced by do Carmo is E. Schmidt's from 1939. The four-vertex theorem says that the curvature of a simple closed convex curve has at least four critical points, so no convex oval has the curvature profile of a curve that just rises and falls once.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §1-7, "Global Properties of Plane Curves" (pp. 31–46): the area formula, equation (1) on p. 33; the isoperimetric inequality, Theorem 1 on p. 34; the theorem of turning tangents on p. 37; the lemma, equation (5) on p. 38; and the four-vertex theorem, Theorem 2 on p. 37.
This is the third mission of a series formalizing do Carmo's book, and shares the namespace
DoCarmoDG with the earlier ones.
A closed plane curve of length is a regular map whose derivatives of all orders agree at the two endpoints; equivalently, and as used here, a smooth -periodic map . It is parametrized by arc length when for all , in which case is its length. It is simple when it has no self-intersection: for distinct .
Write for rotation by , . For a curve parametrized by arc length the signed curvature is
which is do Carmo's convention of §1-5, Remark 1: the normal is chosen so that has the orientation of the natural basis, and then . A vertex is a parameter with . The curve is convex when, for every parameter , the whole trace lies in one of the two closed half-planes bounded by the tangent line at .
An angle function for is a smooth with ; the rotation index is . The area bounded by a positively oriented simple closed curve is given by do Carmo's equation (1),
The three equivalent forms of the area formula (1); the existence of a smooth angle function; the identity ; the theorem of turning tangents (the rotation index of a simple closed curve is ); the isoperimetric inequality with equality exactly for circles; and do Carmo's lemma (5), , which drives the proof of the goal.
The isoperimetric inequality is the ancestor of a large family of geometric inequalities, and its sharp case characterizes the circle — the first instance of the pattern "extremal configuration is the round one" that recurs throughout geometry. The four-vertex theorem is a genuinely global statement with no local counterpart: locally, the curvature of a convex arc may be strictly monotone, and it is only the requirement that the curve close up convexly that forces four critical points. Its converse, for strictly positive curvature, was proved by H. Gluck in 1971; do Carmo notes that the theorem also holds for simple closed curves that are not convex, by a harder argument.
Mathlib contains integration, the winding number of a loop in the complex plane and the Jordan curve theorem, but it does not contain the signed curvature of a plane curve, the theorem of turning tangents in this form, the isoperimetric inequality for curves with its equality case, or the four-vertex theorem. What this mission adds is that vocabulary and machine-checked proofs of the four classical statements.
Each target fails for a different reason under the naive approach.
For the area formula, the identification of with the area of the interior is exactly the Jordan-curve input that do Carmo declares he is assuming; the formalization avoids that dependency by defining the bounded area through the integral, so a solver has to prove only the integration-by-parts identities among the three forms of (1).
For the theorem of turning tangents, the difficulty is that a smooth lift of the tangent indicatrix must be produced and then shown to increase by exactly over one period — a degree-theoretic statement about a loop in the circle, where simplicity of the curve is what excludes the values .
For the isoperimetric inequality, Schmidt's proof compares the curve with a circle tangent to two parallel supporting lines and uses the arithmetic–geometric mean inequality; the equality discussion, which is where the characterization of the circle lives, is the delicate part.
For the four-vertex theorem, the obvious argument — "curvature on a compact interval attains a maximum and a minimum, so there are two vertices" — gives only two, and the whole content is the step from two to four. The lemma (5) supplies the contradiction: if changed sign only at the maximum and the minimum, a suitable line through those two points would make the integrand of (5) of one sign and not identically zero.
Curves are smooth maps ℝ → EuclideanSpace ℝ (Fin 2), closedness being -periodicity with
, which is do Carmo's condition that the curve and all its derivatives agree at the
endpoints. Unit speed is imposed globally, so the parameter is arc length and is the length.
Simplicity is injectivity on the half-open period . Convexity is stated per parameter: for
each the trace lies in one closed half-plane of the tangent line at , the choice of side
being allowed to depend on , as in the book's phrasing.
The area is defined by do Carmo's integral (1) rather than as the measure of the interior of the curve, so no Jordan curve theorem is presupposed; consequently the isoperimetric statement is formulated with the absolute value , which makes it independent of the curve's orientation and equal to the enclosed area for a positively oriented simple curve. The equality case asserts that the trace lies on a circle of positive radius.
"At least four vertices" is formalized as the existence of four pairwise distinct parameters in at which vanishes, which rules out the degenerate reading in which one vertex is counted several times.
The Grothendieck-Teichmüller group organises a family of symmetries that act on braided monoidal categories, on quantised universal enveloping algebras, on the little-discs operad, and on the ring of periods of the projective line minus three points. Three versions exist: a profinite one , introduced by Grothendieck and Drinfeld and containing the absolute Galois group ; a pro- one; and a pro-unipotent one , together with its graded companion . This mission is about the graded, pro-unipotent side, which is the version that governs the homological-algebra and deformation-quantisation applications, and which is closest to a concrete, computable object: a Lie algebra of Lie polynomials in two variables, cut out by three explicit equations.
Its Lie algebra carries a distinguished family of elements , one in each odd degree at least , produced from the Knizhnik-Zamolodchikov associator. Deligne, Drinfeld and Ihara conjectured that is the free Lie algebra on such a family. A timeline of what is actually known:
Let be the free Lie algebra over on two generators and , graded by total word length. For a Lie algebra over and , write for the image of under the unique Lie algebra morphism sending and .
For , the Drinfeld-Kohno Lie algebra is generated over by symbols , , subject to
the third relation for pairwise distinct and the fourth for pairwise distinct. It is the Lie algebra of infinitesimal braid relations: the associated graded of the pure braid Lie algebra, and the coefficient algebra of the Knizhnik-Zamolodchikov connection.
The graded Grothendieck-Teichmüller Lie algebra is the set of satisfying three equations:
All three are linear in and degree preserving, so is a graded -subspace.
is not closed under the bracket of ; it is closed under the Ihara (Poisson) bracket
where is the derivation of determined by and . Writing for the Lie algebra of derivations of under the commutator, the assignment satisfies , and it is injective on ; this is the form in which the Lie structure of is expressed in the formal statements below.
Finally, for and the multiple zeta value is
These numbers are the coefficients of the Knizhnik-Zamolodchikov associator, which is why they enter a mission about ; they satisfy the stuffle and shuffle relations, whose common refinement (the double shuffle relations) is the arithmetic side of the same story.
Concretely: the Lie algebra morphism from the free Lie algebra on countably many generators to sending the -th generator to is injective, and its image is exactly . The statement fixes the degrees of the generators but not the generators themselves, which is the weakest form that still carries the content of the conjecture.
The same family exists with the morphism merely injective: the generate a free Lie subalgebra. This is a theorem (Brown 2012); the open part of the goal is surjectivity.
The Ihara bracket is a Lie bracket; is closed under it; the degree- element lies in ; every odd degree contains a non-zero element of ; multiple zeta values satisfy the stuffle and shuffle relations; and .
A positive answer would determine completely and, through the --associator torsor, describe the pro-unipotent Grothendieck-Teichmüller group by generators without relations. Downstream it would pin down the homotopy automorphisms of the rationalised little-discs operad and the Lie algebra of the motivic Galois group of mixed Tate motives over up to the same freeness statement. Without it, even the dimension of in a given degree is only known to be bounded above by the Broadhurst-Kreimer style count, with equality unproved.
Formalizing this mission produces a machine-checked definition of , and the Ihara bracket - objects that have no Mathlib counterpart at present - and machine-checked proofs of the Lie-theoretic facts around them. Brown's theorem itself is proved in the literature but not formalized; the goal statement is genuinely open, and no part of this mission is closed by an existing Lean development known to the proposal.
The obvious approach to the goal - exhibit the generators and count dimensions degree by degree - fails in both directions. Upwards, no closed formula for is known: they are extracted from the Knizhnik-Zamolodchikov associator, whose coefficients are regularised iterated integrals, and only their leading coefficients are controlled. Downwards, freeness of the subalgebra they generate is not an algebraic manipulation of the three defining equations: Brown derives it from the motivic theory of multiple zeta values, where the missing input is a basis theorem for a period algebra, not an identity in . Even the milestone " is closed under the Ihara bracket" is not a formality: the pentagon equation lives in and must be transported through substitutions into a quotient Lie algebra.
The formalization commits to the following conventions, all visible in the definition files.
FreeLieAlgebra ℚ (Fin 2),
i.e. by Lie polynomials, not the completed Lie algebra of the
source. The three defining equations are homogeneous, so the graded object determines the
completed one; solvers should be aware that no topology or completion appears anywhere.Fin n by the Lie ideal generated by the four relation families above, so dkGen i j is
under the shift Fin 4 = {0,1,2,3} versus indices .LieDerivation ℚ (FreeLieAlgebra ℚ (Fin 2)) (FreeLieAlgebra ℚ (Fin 2)), so that freeness can
be stated as injectivity of a morphism out of a free Lie algebra without first installing a
new Lie algebra structure. Note is injective on but not on
all of , where ; a supporting item records the injectivity actually
used.tsum; for non-admissible words
the series diverges and the definition returns Mathlib's junk value. Every statement about
them therefore carries an admissibility hypothesis: all letters and first letter
. The stuffle and shuffle products are multisets of words, so no free module on words
is needed.Contributions welcome: the Lie-theoretic milestones (Lemma 7.2, Corollary 7.1, closure of , the degree- element) are self-contained and need no motivic input; the multiple zeta milestones need summability infrastructure for iterated series; Brown's theorem and the goal need a substantial development that does not yet exist in Lean.
Waldspurger's non-standard fundamental lemma is an identity between stable orbital integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even isogenous as algebraic groups, but whose root data become identified after tensoring with . The basic example is the pair , whose root systems and are exchanged by Langlands duality; the identity is what allows the twisted fundamental lemma to be deduced from the ordinary one. Waldspurger formulated the conjecture in L'endoscopie tordue n'est pas si tordue (2008); it is Theorem 1.12.7 of Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), proved there in equal characteristic by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.
Before any of that geometry can start, the two sides have to be compared: one needs a single Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving both groups at once. Producing that comparison is a self-contained piece of linear algebra over the root data, carried out in Ngo's §1.12, and it is what this mission asks for.
Let and be split reductive groups over a field, pinned, with maximal tori and . Each is determined by its root datum , where is the set of roots, the set of coroots and the set of simple roots singled out by the pinning.
An isogeny of root data between and (Ngo, Definition 1.12.1) is a pair of isomorphisms of -vector spaces
which are transposes of one another, such that carries the set of lines () bijectively onto the set of lines (), matching lines of simple roots with lines of simple roots, and such that has the same property for the lines spanned by coroots. Two semisimple groups with the same adjoint group are isogenous in this sense; so are a group and its Langlands dual, the interesting cases being , and , where a short root is sent to and a long root to with . Groups obtained by twisting a pair of isogenous pinned groups by a common torsor are called paired.
A prime is good with respect to when it divides neither of the indices
the two lattices being compared inside the single -vector space identified by .
i.e. conjugation by carries the Weyl group acting on onto the Weyl group acting on . Ngo's reason is that the reflection attached to a root depends only on the line through that root, so the bijection of root lines transports reflections to reflections. This equivariance is what makes the induced isomorphism descend to an isomorphism of the spaces of characteristic polynomials, which is Lemme 1.12.6 and which is what allows two points and with to be compared at all.
Two steps lead there: the reflection computation that makes a matched pair of root lines give a matched pair of reflections, and the integral statement behind Ngo's good-characteristic hypothesis — that when the two indices above are invertible in the base ring, the two lattices become identified after base change.
Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over with residue characteristic exceeding twice the Coxeter numbers, and for points and corresponding under , the stable orbital integrals of the characteristic functions of and agree. Waldspurger showed that this identity, together with the ordinary fundamental lemma, implies the twisted fundamental lemma. None of the objects in that statement — reductive group schemes over a discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the isomorphism the two sides of Theorem 1.12.7 cannot even be matched up.
Beyond this paper, the notion of an isogeny of root data and the good-characteristic base change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands duality for split groups, and neither is currently available.
The reflection step looks like a one-line computation and is one — but only once the two proportionality constants are known to agree. If and , the conjugate of is exactly when , and that is forced by transposition together with . The genuine difficulty in the goal is different: the definition only says that and permute lines, so one has to show that the bijection induced on root lines and the bijection induced on coroot lines are the same bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.
The lattice milestone has its own trap: the quotient must be shown to have vanishing after base change, not merely to vanish, or the inclusion becomes only surjective.
Root data are modelled by Mathlib's RootPairing ι ℚ M N, with the character space,
the cocharacter space, and rational coefficients throughout, so that "tensoring with
" is built into the ambient objects rather than performed explicitly. A choice of
simple roots is recorded as a subset of the index type rather than as a RootPairing.Base;
nothing in the statements depends on that subset beyond its role in the definition of an
isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space
generated by the coreflections, which is the form in which it acts on the Cartan.
The goal is stated as a two-sided intertwining property rather than as an equality of subgroups: every element of is intertwined by with some element of and conversely. This avoids introducing a conjugation homomorphism, and it is the form in which the statement is used. Both root pairings in the goal are required to be finite, reduced root systems, matching Ngo's hypothesis that and are reductive groups.
The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility in the base ring of the two indices, each expressed as the cardinality of an explicit quotient group; the conclusion is the bijectivity of the map induced on the tensor product by the inclusion of the intersection. If a quotient were infinite its cardinality is reported as , and invertibility of then forces the base ring to be trivial, so no false statement hides in that corner.
No statement here is vacuous: any pair consisting of a root system and itself, with and the identity, satisfies every hypothesis, and the pair gives the intended non-trivial instances.
A stochastic partial differential equation is driven by noise that lives on an infinite-dimensional function space, and the first object one has to control is the law of that noise: a Gaussian measure on a separable Banach space. Martin Hairer's lecture notes An Introduction to Stochastic PDEs (arXiv:0907.4178) devote their first technical chapter (Section 4) to exactly this, because every later construction — stochastic convolutions, invariant measures for semilinear equations, the ergodic theory of the stochastic Navier–Stokes equations — is phrased against it.
The single structural fact that chapter produces is the Cameron–Martin theorem (Theorem 4.44, p. 31). It answers the question: in which directions may one translate an infinite-dimensional Gaussian measure without destroying its null sets? In finite dimensions the answer is "all of them", because Lebesgue measure is translation invariant. In infinite dimensions the admissible directions form a proper, and typically much smaller, Hilbert subspace — the Cameron–Martin space — and the translated measure is either equivalent to or mutually singular with it, with nothing in between. This dichotomy is the reason Girsanov-type changes of measure, Schilder-type large deviation rate functions, support theorems and Malliavin calculus all take the form they do.
Throughout, is a separable Banach space, its topological dual, and a Borel probability measure on .
is Gaussian (Definition 4.4, p. 19) if for every continuous linear functional the push-forward is a Gaussian measure on in the sense of Definition 4.1, i.e. has characteristic function ; the degenerate case , a Dirac mass, is included. It is centred if all these one-dimensional laws have mean zero, which is expressed here as .
For a centred Gaussian the covariance form (4.2, p. 20) is
It is well defined because is -integrable, and it is a bounded bilinear form (Corollary 4.14, p. 22).
The Cameron–Martin space (Definition 4.26, p. 27) is classically built as the completion of
under . This mission uses the equivalent intrinsic description of Exercise 4.38 (p. 29), which avoids the completion:
The supremum is taken in ; since is admissible whenever is, it equals over the same set. For write , .
For a centred Gaussian measure on a separable Banach space and ,
Both implications are asserted: translation along a Cameron–Martin direction produces an absolutely continuous measure, and translation along any other direction does not (in fact it produces a mutually singular measure).
The milestone list follows the route of Section 4.2:
The Cameron–Martin theorem is what makes the Cameron–Martin space a canonical object rather than a formal construction: is simultaneously the set of admissible shifts, the intersection of all full-measure linear subspaces (Proposition 4.45), and the space whose unit ball governs Gaussian isoperimetry (Theorem 4.53, Borell–Sudakov–Cirel'son). Downstream in the notes it is used to identify invariant measures of linear SPDEs and to compare them; outside the notes it is the starting point of Malliavin calculus and of large deviation theory for Gaussian measures.
Status, precisely. The Mathlib library pinned by this mission already contains a substantial part of Section 4: the predicate IsGaussian (Definition 4.4), uniqueness of measures with equal characteristic functionals on a separable Banach space (Propositions 4.8 and 4.11), invariance of under rotations (Proposition 4.12), Fernique's theorem (Theorem 4.13), and the covariance form of (4.2) together with its boundedness (Corollary 4.14) as a continuous bilinear form on the dual. Those results are therefore not milestones here; they are the assumed foundation. What is absent, and what this mission asks for, is everything from the Cameron–Martin space onwards: its definition, its elementary properties, and Theorem 4.44 itself. No machine-checked proof of the infinite-dimensional Cameron–Martin theorem is known to the captain in any Lean library.
The naive route — write down the two densities and take their ratio — is unavailable: there is no translation-invariant reference measure on an infinite-dimensional Banach space, so "the density of " does not exist and the Radon–Nikodym derivative of with respect to must be produced directly, as the exponential of a random variable.
That random variable is the obstruction. For the functional is continuous and the computation is a characteristic-function identity. But is in general strictly smaller than : a general has an associated that exists only as an -limit of continuous functionals, defined -almost everywhere and linear only on a measurable subspace of full measure (Propositions 4.34 and 4.39). Establishing that these limits are Gaussian with the expected variance (Proposition 4.40) is the technical bridge, and it is why milestone 3 is stated as a statement about -limits rather than about elements of .
The converse half has a different shape. One must produce, for , a single one-dimensional projection that separates from arbitrarily well; unboundedness of over the covariance unit ball supplies with and as large as desired, and the quantitative Gaussian total-variation bound of milestone 5 converts this into total variation distance , i.e. mutual singularity.
The development is in Lean 4 with Mathlib, in the namespace HairerSPDE, shared by the whole series drawn from these notes. The conventions it commits to:
NormedAddCommGroup, NormedSpace ℝ, its Borel σ-algebra, CompleteSpace and SecondCountableTopology — the last two encode "separable Banach space".IsGaussian, which is Definition 4.4 verbatim; centredness is the extra hypothesis , needed because IsGaussian permits a non-zero mean.covarianceBilinDual, which equals (4.2) for centred measures with finite second moment and is set to zero otherwise; Fernique's theorem rules the degenerate branch out for Gaussian measures.fun x ↦ x + h, absolute continuity is Mathlib's ≪, and "measurable linear subspace" is a Submodule ℝ B whose carrier is a measurable set.The goal is an equivalence, so neither half can be discharged vacuously: the direction is non-trivial already for in finite dimensions, and the converse has content precisely when . Note that always, and that for a Dirac mass the covariance form vanishes and ; both degenerate cases are inside the statement rather than excluded by hypothesis.
Contributions welcome beyond the milestones: the reproducing kernel space and the isomorphism of Proposition 4.34, measurable linear extensions (Proposition 4.39), the dilation singularity of Proposition 4.43, and in the infinite-dimensional case (second half of Proposition 4.45). All of these are reusable outside this mission.
Chapter 11 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) replaces the Riemann integral of Chapter 6 with the Lebesgue integral, and the reward is a theory of integration whose limit theorems have no superfluous hypotheses and whose space of square-integrable functions is complete. The chapter runs from set functions and outer measures, through the Carathéodory construction of Lebesgue measure, measurable functions and the integral, to the convergence theorems (monotone convergence, Fatou, dominated convergence) and finally to the space and the Riesz–Fischer theorem (Theorem 11.42):
That completeness is what makes a Hilbert space, and it is the reason the Fourier series of Chapter 8 converge in the mean to the functions they represent.
This mission is the eleventh and last in a series formalizing Rudin Chapters 1–11. It uses the Riemann–Stieltjes integral of Mission VI (for Theorem 11.33, comparing the two integrals) and the trigonometric Fourier series of Mission VIII (for the reading of Parseval's theorem).
A set function on a ring of sets is countably additive if it takes the value on a countable disjoint union. Rudin constructs an outer measure from such a by covering with elementary sets and taking an infimum, calls a set measurable when it is approximable by elementary sets in the metric , and proves that the measurable sets form a -algebra on which is countably additive (Theorem 11.10). A real function is measurable when is measurable for every , and the integral is defined first for simple functions, then for nonnegative measurable functions as a supremum, and then for general by .
The space consists of the measurable with , normed by ; a sequence converges in the mean to if .
Mathlib's measure theory is used wherever it is mathematically the same object:
MeasureTheory.OuterMeasure and its Carathéodory -algebra, MeasurableSet,
Measurable, the lower Lebesgue integral ∫⁻ for nonnegative extended-real functions, the
Bochner integral ∫ and Integrable for the general case. What is set up freshly is Rudin's
of functions — Rudin.MemL2, Rudin.L2Norm, Rudin.CauchyL2,
Rudin.TendstoL2 — rather than Mathlib's quotient space Lp, because the Riesz–Fischer theorem
as Rudin states it produces an honest limit function, and the ε-N phrasing of Cauchyness and
of mean convergence is part of the statement.
If is a Cauchy sequence in , then there exists with : the space is complete.
Rudin's proof extracts a subsequence with , sums the telescoping series, uses the monotone convergence theorem and the Schwarz inequality to show that the sum converges almost everywhere, and identifies the pointwise limit as the mean limit of the whole sequence. Every ingredient is a milestone of this mission.
The Lebesgue theory is the point at which analysis acquires limit theorems that do not require uniform convergence. Monotone convergence, Fatou's lemma and dominated convergence are the three statements that make the integral usable in probability, in Fourier analysis and in the theory of partial differential equations, and the Riesz–Fischer theorem is what makes a Hilbert space and therefore the natural home of Fourier expansions: Parseval's identity (11.45) is the assertion that the Fourier coefficient map is an isometry onto .
Theorem 11.33 is the bridge back to the earlier chapters — every Riemann-integrable function is Lebesgue-integrable with the same integral, and a bounded function on is Riemann-integrable exactly when it is continuous almost everywhere — so the two halves of the book agree wherever both apply.
Mathlib has an extensive measure theory and proves many of these results in considerable generality. This mission's contribution is to state them in Rudin's formulation, for Rudin's of functions and with his explicit ε-N definitions, so that the chapter is available as a coherent, self-contained unit that matches the textbook line by line and links back to the Riemann–Stieltjes integral of Mission VI.
Individually, most milestones will reduce to Mathlib results after the correct dictionary is in
place, and the interesting work is exactly in that translation: Rudin's measurability
({x : f(x) > a} measurable) versus Mathlib's Measurable, Rudin's integral of a nonnegative
function versus ∫⁻ with values in ℝ≥0∞, Rudin's of genuine functions versus
Lp as a quotient by almost-everywhere equality. The last of these is what makes the goal
theorem nontrivial to derive: Mathlib's completeness of Lp gives a limit class, and one must
choose a measurable representative and verify Rudin's mean convergence with the concrete norm
Rudin.L2Norm, which is Real.sqrt (∫ f²) and not an ENNReal quantity.
Theorem 11.33 (Riemann implies Lebesgue) and Theorem 11.38 (density of continuous functions)
are the two other places where real work is required: the first has to connect the Chapter 6
definition of the Riemann integral with intervalIntegral, and the second is an approximation
argument.
Conventions fixed by this mission:
MeasureTheory.Measure, MeasurableSet,
Measurable, Integrable, ∫⁻ x, f x ∂μ for nonnegative ℝ≥0∞-valued integrands and
∫ x, f x ∂μ for the general real case. Rudin's Carathéodory construction is
MeasureTheory.OuterMeasure.caratheodory.ℝ≥0∞-valued
functions, matching Rudin's use of extended real values there.Rudin.MemL2 μ f is "f is measurable and f² is integrable"; Rudin.L2Norm μ f is
Real.sqrt (∫ x, (f x)^2 ∂μ); Rudin.CauchyL2 and Rudin.TendstoL2 are Rudin's ε-N Cauchy
condition and mean convergence. No quotient is taken, so the goal theorem produces a function.Rudin.RiemannIntegrable and Rudin.RiemannIntegral from
Mission VI, so the two integrals are literally compared.Contributions of the convergence theorems (11.28, 11.31, 11.32) and of the Schwarz inequality (11.35) are especially useful, since the goal theorem consumes them directly.
Chapter 8 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) puts the general theory of the preceding chapters to work on concrete functions. Power series are differentiated term by term; the exponential function is defined by its series and the trigonometric functions and the number are extracted from it; the fundamental theorem of algebra is proved; Fourier series are introduced through general orthonormal systems; and the Gamma function is characterized by log-convexity.
The chapter's capstone is Parseval's theorem (Theorem 8.16): for Riemann-integrable -periodic functions, the Fourier series converges in the mean square sense and the inner product is computed by the (absolutely convergent) sum of products of Fourier coefficients. It is the statement that the trigonometric system is not merely orthonormal but complete, and it is the finite-dimensional Pythagorean theorem carried to infinite dimensions.
This mission is the eighth in a series formalizing Rudin Chapters 1–11; it uses the convergence tests of Mission III and the uniform-convergence and approximation theorems of Mission VII, and it is the analytic counterpart of the abstract theory of Mission XI.
A power series is ; by Chapter 3 it converges on an interval . A sequence of complex functions on is an orthonormal system if for and ; the Fourier coefficients of relative to it are , and the Fourier series is . For the trigonometric system on one writes
A trigonometric polynomial is a finite sum . The Gamma function is for .
For Riemann-integrable -periodic and with Fourier coefficients and :
Parseval's theorem is the completeness statement for the trigonometric system: Bessel's inequality (8.12) holds for every orthonormal system, and equality for all is exactly what distinguishes a complete system. The proof shows how the pieces of the book fit together: it uses the approximation theorem 8.15 (itself a corollary of Stone–Weierstrass from Chapter 7), the minimizing property 8.11, and the Schwarz inequality of Chapter 1. Chapter 11 generalizes the conclusion to arbitrary complete orthonormal systems in , where the Riemann-integrable hypothesis can be dropped.
The other milestones are where the elementary functions acquire their properties: the -periodicity of the complex exponential, the definition of as twice the first positive zero of the cosine, and the log-convexity characterization of the Gamma function are all established here rather than assumed.
Mathlib has the exponential and trigonometric functions, , the fundamental theorem of algebra, the Gamma function with the Bohr–Mollerup theorem, and a Fourier theory on the additive circle. The work in this mission is to state Rudin's versions — -periodic functions on , generic orthonormal systems on an interval, Riemann-integrable rather than square-integrable hypotheses — and connect them to that library.
Parseval's theorem is where an approximation argument in the uniform norm has to be converted into one in the mean square norm. The chain is: approximate in by a continuous periodic (a nontrivial step for a merely Riemann-integrable , and the place where the hypothesis is really used), approximate uniformly by a trigonometric polynomial , and then use the minimizing property of the partial sums to conclude is small. The first step has no analogue in the uniform theory and is the main obstacle; the third depends on being an orthogonal projection, which is Theorem 8.11.
Conventions fixed by this mission:
∫ x in a..b, f x, not the real-valued Riemann–Stieltjes integral built in Mission VI; for
the Riemann-integrable integrands of this chapter the two agree. Integrability hypotheses are
stated as IntervalIntegrable.Rudin.fourierCoeff, Rudin.fourierPartialSum, Rudin.L2Norm,
Rudin.IsTrigPolynomial, Rudin.HasPeriodTwoPi, and, for general systems,
Rudin.IsOrthonormalSystem and Rudin.genFourierCoeff, all following Rudin's normalizations
(in particular the in and in ).Rudin.SeriesConvergesTo from Mission III, so that conditional
convergence is expressible; the two-sided sums of Parseval are
stated as limits of the symmetric partial sums , as in Rudin.Chapter 10 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) builds the calculus of differential forms in and proves the theorem that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the Green, divergence and classical Stokes theorems all say the same thing — that integrating a derivative over a region is the same as integrating the original object over the boundary of that region — and Stokes' theorem (Theorem 10.33),
is that statement, once "region" is made precise as a chain of parametrized surfaces and "derivative" as the exterior derivative.
This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse function theorem and the several-variable calculus of Mission IX.
For an open , a -surface in is a -mapping from a parameter domain — a -cell or the standard simplex — into ; surfaces are maps, not point sets. A -form in is a formal sum
with continuous coefficients, whose meaning is the rule assigning to each -surface the number
The exterior derivative of is the -form with coefficients ; the pullback along a differentiable substitutes into the coefficients and the differentials. A -chain is a formal integer combination of -surfaces with parameter domain , its integral is the corresponding combination of integrals, and its boundary is obtained from the alternating sum of the faces of .
If is a -chain of class in an open and is a -form of class in , then
For this is the fundamental theorem of calculus, for Green's theorem, for the divergence theorem, and for , the theorem of Stokes.
Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that and are adjoint, which is also the starting point of de Rham cohomology. Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form being exact disappears, so the failure of exactness measures the shape of the domain. The change of variables theorem (10.9) is what makes integrals independent of the parametrization and is used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for passing from local to global statements.
Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their boundaries, nor a version of Stokes' theorem for such chains. This mission builds that apparatus and states the chapter's theorems for it; the definitions are reusable for any development that wants a hands-on, coordinate-based treatment of forms.
This is the most demanding mission of the series, for two reasons. First, the objects have to be set up before anything can be said: forms as coefficient families, their integrals as Jacobian integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved by reducing to a single oriented simplex, transporting along the parametrization by Theorem 10.25, and then computing the integral over by an iterated integral in which all but two terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the face maps right, and it is where a formalization will spend its time.
A further subtlety: with forms presented by coefficients indexed by all index tuples, the identity is false coefficient-wise and true as an identity of forms. Since Rudin defines a form to be its integration functional, statements of the shape "this form vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20, 10.22(c) and 10.39 are stated here.
Conventions fixed by this mission:
Fin n → ℝ. A -form is Rudin.KForm k n, a coefficient
function indexed by all tuples Fin k → Fin n, following Rudin's equation (34).Rudin.integralOverCell and Rudin.integralOverSimplex are Rudin's equation (35) for the two
admissible parameter domains, with Rudin.jacobian the determinant of the matrix of partial
derivatives. The integral over the parameter domain is the Lebesgue integral for the volume
measure, which agrees with Rudin's Riemann integral for continuous integrands.Rudin.extDeriv and Rudin.pullback are the exterior derivative and the pullback;
Rudin.Chain, Rudin.Chain.integral and Rudin.Chain.boundary are chains with integer
multiplicities, their integrals, and the boundary built from the faces of the standard simplex
with Rudin's signs .ContDiff ℝ 1 and ContDiff ℝ 2 for Rudin's and .Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are especially welcome, since they are exactly the lemmas the goal theorem consumes.
Chapter 5 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is the differential calculus of one real variable, developed from the definition of the derivative as a limit of difference quotients. Its organizing result is the mean value theorem and the family of consequences that follow from it: monotonicity criteria, L'Hospital's rule, and — the chapter's capstone — Taylor's theorem (Theorem 5.15), which approximates a function by a polynomial of degree and expresses the error exactly as a single -th derivative evaluated at an unspecified intermediate point.
Taylor's theorem is what makes differentiability quantitatively useful. It is the tool that turns local smoothness into explicit error bounds, and the estimates of Chapter 8 for the exponential, trigonometric and Gamma functions all rest on it.
This mission is the fifth in a series formalizing Rudin Chapters 1–11; it uses the continuity and compactness results of Mission IV.
Let be real-valued on . For the derivative is
whenever the limit exists. Higher derivatives are defined by iteration; exists on a set only if exists in a neighbourhood of each of its points. has a local maximum at if for all near .
Given a positive integer and a point , the Taylor polynomial of at of degree is
Let be continuous on , let exist for , and let be points of . Then there is a point strictly between and such that
For this is exactly the mean value theorem.
The mean value theorem converts a hypothesis about derivatives into a statement about increments, and everything in the chapter is an application of that conversion. Monotonicity criteria (5.11) are the basis of every "the function is increasing, hence injective" argument, including the change of variable in Chapter 6. Darboux's theorem (5.12) shows that derivatives, though not necessarily continuous, cannot have simple discontinuities — a fact that is easy to state and impossible to guess from the definition. Theorem 5.19 is the form of the mean value theorem that survives for vector-valued functions: the equality is lost (there need be no single point where the vector increment is proportional to the derivative), and only the inequality remains; the same phenomenon dictates the statements of Chapter 9.
Mathlib contains the mean value theorem, L'Hospital's rule, and a Taylor theorem with various remainder forms. The value of this mission is a statement of Taylor's theorem in Rudin's exact formulation — arbitrary distinct endpoints in , hypotheses only on and , an intermediate point strictly between them — and the derivation of the chapter's other results in a form the later missions can quote.
Taylor's theorem is proved by choosing the constant so that and applying Rolle's theorem times to ; the bookkeeping is in tracking that for and that each application produces a new intermediate point strictly inside the previous interval. In a proof assistant the iteration is the awkward part: the induction is on with the interval shrinking, and the statement must be general enough in and (either order) for the inductive step to apply. The hypothesis that exists only on the open interval, while is merely continuous on the closed one, must be preserved — strengthening it to on would make the statement weaker than Rudin's.
Conventions fixed by this mission:
deriv and iteratedDeriv, which are total functions returning
0 where the function is not differentiable; every statement therefore carries explicit
differentiability hypotheses exactly where Rudin states them.Set.Icc a b and Set.Ioo a b, and "for some between and
" is stated as an explicit disjunction, since the goal does not assume
.EuclideanSpace ℝ (Fin k), and the conclusion
is the inequality, not an equality — the equality version is false, as Rudin notes.