Mathlib

Mathlib-shaped helper lemmas staged for upstreaming: conditional distributions, conditional independence, and integration gaps.

Analysis 891 core · 1111 supporting · 46 submodules Analytic tools for approximation, convexity, smoothness, matrix perturbation, interval certification, complex root analysis, and Hilbert-space geometry. Measure­Theory 2 to review 85 core · 90 supporting · 33 submodules Measure-theoretic tools for conditional expectation, densities, partitions, integration, measurable selection, finite supports, and moment restrictions. Algebra 7 core · 7 supporting · 1 submodule Algebraic infrastructure for finite sums and products, count-vector combinatorics, and reusable ring identities. Algebraic­Geometry 54 core · 64 supporting · 4 submodules Polynomial and rational maps, rational derivatives, and affine-algebraic dimension tools. Algorithms 76 core · 69 supporting · 1 submodule Finite algorithms centered on monotone-deque sliding-window calculations, with correctness, mutation-count, and storage guarantees for rolling extrema in discrete data. Combinatorics 19 core · 32 supporting · 2 submodules Boolean-cube Möbius identities and the Johnson scheme with its harmonic and Kneser-graph structure. Data 3 core · 0 supporting · 2 submodules Small additions to Mathlib's basic data structures, kept here until they are upstreamed. Geometry 25 core · 49 supporting · 1 submodule Geometry infrastructure extending Mathlib: tangent and normal spaces, normal bundles, and shape operators of smooth embedded submanifolds of Euclidean space. Information­Theory 36 core · 70 supporting · 11 submodules Entropy, conditional entropy, finite KL and mutual-information identities, Fano bounds, Gaussian and product calculations, density tilts, and finite chain rules. Linear­Algebra 81 core · 88 supporting · 9 submodules Linear-algebra tools including Cholesky and Vandermonde constructions, normal equations, monomial matrices, positive-matrix spectra, and tensor recovery. Optimization 60 core · 59 supporting · 6 submodules Finite-dimensional optimization: sign cells of an affine system and their closure, Karush-Kuhn-Tucker conditions for constrained problems, and linear programs over the rationals. Probability 456 core · 625 supporting · 32 submodules General probabilistic infrastructure for independence, kernels, Gaussian and Poisson laws, distributional convergence, Stein approximations, and certified calculations. Topology 42 core · 25 supporting · 4 submodules Compact-set exclusion, subsequential limits, and affine uniform convergence.