Missing undergraduate mathematics in mathlib

This gives pointers to undergraduate maths topics that are currently missing in mathlib. The list is gathered from the French curriculum. There is also a page listing undergraduate maths topics that are already in mathlib.

If you want to work on an item from this list then you should first check the pull requests list to see whether it is already coming, then the issues list to see whether it is discussed there, and finally talk about this idea on Zulip.

To update this list, please submit a PR modifying docs/undergrad.yaml in the mathlib repository.

Linear algebra

Duality: orthogonality.

Finite-dimensional vector spaces: rank of a system of linear equations.

Multilinearity: special linear group.

Matrices: elementary row operations, elementary column operations, Gaussian elimination, row-reduced matrices.

Structure theory of endomorphisms: diagonalization, triangularization, invariant subspaces of an endomorphism, kernels lemma, Jordan-Chevalley-Dunford decomposition, Jordan normal form.

Linear representations: irreducible representation, examples.

Exponential: endomorphism exponential.

Group Theory

Classical automorphism groups: special orthogonal group, special unitary group.

Representation theory of finite groups: representations of abelian groups, dual groups, Fourier transform for finite abelian groups, convolution, class function over a group, orthonormal basis of irreducible characters, examples of groups with small cardinality.

Ring Theory

Algebra: algebra over a commutative ring.

Polynomial rings: Newton's identities.

Field Theory: $\R(X)$-partial fraction decomposition, $\C(X)$-partial fraction decomposition.

Bilinear and Quadratic Forms Over a Vector Space

Bilinear forms: rank of a bilinear form.

Orthogonality: Sylvester's law of inertia, real classification, complex classification.

Endomorphisms: special orthogonal group, special unitary group, normal endomorphism, diagonalization of normal endomorphisms, simultaneous diagonalization of two real quadratic forms, with one positive-definite, polar decompositions in $\mathrm{GL}(n, \R)$, polar decompositions in $\mathrm{GL}(n, \C)$.

Low dimensions: classification of elements of $\mathrm{O}(2, \R)$, classification of elements of $\mathrm{O}(3, \R)$.

Affine and Euclidean Geometry

General definitions: equations of affine subspace, affine property, group generated by homotheties and translations, transformations fixing a basis of directions.

Euclidean affine spaces: isometries that do and do not preserve orientation, direct and opposite similarities of the plane, classification of isometries in two and three dimensions, angles between planes, inscribed angle theorem, group of isometries stabilizing a subset of the plane or of space, regular polygons, metric relations in the triangle, using complex numbers in plane geometry.

Application of quadratic forms to study proper conic sections of the affine euclidean plane: focus, eccentricity, quadric surfaces in 3-dimensional Euclidean affine spaces.

Single Variable Real Analysis

Numerical series: Convergence of real valued-series, summation of comparison relations, comparison of a series and an integral, error estimation, absolute convergence, products of series.

Differentiability: piecewise $C^k$ functions.

Taylor-like theorems: Taylor's theorem with little-o remainder, Taylor's theorem with integral form for remainder, Taylor series expansions.

Integration: integral over a segment of piecewise continuous functions, improper integrals, absolute vs conditional convergence of improper integrals, comparison test for improper integrals.

Sequences and series of functions: normal convergence.

Convexity: continuity and differentiability of convex functions.

Single Variable Complex Analysis

Complex Valued series: antiderivative, power series expansion of elementary functions(log).

Functions on one complex variable: Cauchy-Riemann conditions, contour integrals of continuous functions in $\C$, antiderivatives of a holomorphic function, representations of the $\log$ function on $\C$, theorem of holomorphic functions under integral domains, winding number of a closed curve in $\C$ with respect to a point, isolated singularities, Laurent series, meromorphic functions, residue theorem, sequences and series of holomorphic functions.

Topology

Normed vector spaces on $\R$ and $\C$: equivalent norms.

Hilbert spaces: example, classical Hilbert bases of orthogonal polynomials, $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem.

Multivariable calculus

Differential calculus: directional derivative, partial derivatives, Jacobian matrix, gradient vector, Hessian matrix, $k$-th order partial derivatives, Taylor's theorem with little-o remainder, Taylor's theorem with integral form for remainder.

Differential equations: maximal solutions, exit theorem of a compact subspace, autonomous differential equations, phase portraits, qualitative behavior, stability of equilibrium points (linearisation theorem), linear differential systems, method of constant variation (Duhamel’s formula), constant coefficient case, solving systems of differential equations of order $> 1$.

Submanifolds of $\R^n$: local graphs, local parameterization, local equation, tangent space, position with respect to the tangent plane, gradient, line integral, curve length, Lagrange multipliers.

Measures and integral calculus

Integration: differentiability of integrals with respect to parameters, change of variables to spherical co-ordinates.

Fourier analysis: convolution product of periodic functions, Dirichlet theorem, Fejer theorem, Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(\R^d)$, Plancherel’s theorem.

Probability Theory

Definitions of a probability space: law of total probability.

Random variables and their laws: absolute continuity of probability laws, law of joint probability, transfer theorem, binomial law, geometric law, Poisson law, uniform law, exponential law, Gaussian law, characteristic function, probability generating functions, applications of probability generating functions to sums of independent random variables.

Convergence of a sequence of random variables: Levy's theorem, weak law of large numbers, central limit theorem.

Distribution calculus

Spaces $\mathcal{D}(\R^d)$: smooth functions with compact support on $\R^d$, stability by derivation, stability by multiplication by a smooth function, partitions of unity, constructing approximations of probability density functions in spaces of common functions (trig, exp, rational, log, etc).

Distributions on $\R^d$: definition of distributions, locally integrable functions as distributions, derivative of a distribution, Dirac measures, derivatives of Dirac measures, derivative of the Heaviside function, Cauchy principal values, multiplication by a smooth function, convergence of sequences of distributions, support of a distribution.

Spaces $\mathcal{S}(\R^d)$: stability by multiplication by a slowly growing smooth function, gaussian functions, Fourier transforms on $\mathcal{S}(\R^d)$, convolution of two functions of $\mathcal{S}(\R^d)$.

Tempered distributions: definition, derivation of tempered distributions, multiplication by a function $C^\infty$ of slow growth, $L^2$ functions and Riesz representation, $L^p$ functions, periodic functions, Dirac comb, Fourier transforms, inverse Fourier transform, Fourier transform and derivation, Fourier transform and convolution product.

Applications: Poisson’s formula, using convolution and Fourier-Laplace transform to solve one dimensional linear differential equations, weak solution of partial derivative equation, fundamental solution of the Laplacian, solving the Laplace equations, heat equations, wave equations.

Numerical Analysis

Solving systems of linear inequalities: conditioning, Gershgorin-Hadamard theorem, Gauss’s pivot, LU decomposition.

Iterative methods: Jacobian, Gauss-Seidel, convergence analysis, spectral ray, singular value decomposition, example of discretisation matrix by finite differences of the laplacian in one dimension.

Iterative methods of solving systems of real and vector valued equations: linear systems case, proper element search, brute force method, optimization of convex function in finite dimension, gradient descent square root, nonlinear problems with real and vector values, bisection method, Picard method, Newton’s method, rate of convergence and estimation of error.

Numerical integration: Rectangle method, error estimation, Monte-Carlo method, rate of convergence, application to the calculation of multiple integrals.

Approximation of numerical functions: estimation of the error.

Ordinary differential equations: numerical aspects of Cauchy's problem, explicit Euler method, consistency, stability, convergence, order.

Fourier transform: discrete Fourier transform on a finite abelian group, fast Fourier transform.