We apologize for the delay in posting this overview. In June 2022 there were 460 PRs merged into mathlib. We list some of the highlights below.
- PR #14135 proves compactness of the character space of a normed algebra. This is a key step in developing the continuous functional calculus.
- PR #8112 proves the Krein-Milman theorem for real normed spaces: any compact convex set is the closure of the convex hull of its extreme points.
- PR #14677 proves Stone's separation theorem: in a vector space over a linearly ordered field, for any pair of disjoint convex subsets, one can partition the whole space into two convex subsets containing the given sets. This is a generalization of the geometric Hahn-Banach theorem where the partition is made of half-spaces.
Measure theory and probability
- PR #14578 characterizes weak convergence of finite measures in terms of integrals of bounded continuous real-valued functions.
- PR #14755 introduces moments and moment generating function of a real random variable.
- PR #13592 solves the Ballot problem: if in an election, candidate A receives $p$ votes whereas candidate B receives $q$ votes where $p > q$ then the probability that candidate A is strictly ahead throughout the count is $(p - q) / (p + q)$.
- PR #14758 proves the Łoś–Vaught Test.
Number theory and group theory
- PR #14231 reformulates the spectral theorem in terms of matrices.
linear_combinationtactic became more powerful in PR #14229 by allowing combinations of arbitrary proofs.