HighDimProb

High-dimensional probability and finite-dimensional random matrices in Lean 4

English | 简体中文

HighDimProb is a Mathlib-based Lean 4 library for concentration inequalities, metric entropy, random processes, and finite-dimensional random matrices. It provides focused imports, compiled examples, API tests, and an append-only Judge suite so that formalized results can be used and audited downstream.

API overview · Examples · Documentation · Interactive roadmap · Contributing

TL;DR

HighDimProb provides composable Lean APIs for high-dimensional probability, random processes, and random-matrix theory, so users can quickly build end-to-end formal proofs with explicit assumptions and inspectable intermediate steps, keeping mathematical black boxes to a minimum. It is not limited to machine learning: any field that relies on this mathematics can use it.

Library overview

Area	Recommended import	Includes
Scalar probability	HighDimProb	Objects, expectation, tails, moments, variance, Orlicz vocabulary, and typed statements.
Scalar concentration	HighDimProb.Concentration	Markov, Chebyshev, MGF routes, Orlicz–tail–moment implications, Rademacher, Hoeffding, and Bernstein.
Metric entropy and processes	HighDimProb.SubGaussianProcess and focused concentration imports	Nets, covering and packing, parent maps, finite chaining, finite suprema, and entropy-integral bounds.
Random matrices	HighDimProb.RandomMatrix	Finite matrices, Loewner order, spectral tools, trace exponential, sums, and variance proxies.
Matrix concentration	HighDimProb.RandomMatrix.Concentration	Trace-MGF, Matrix Bernstein, operator norm, centered rank-one, and sample covariance routes.
Development aggregate	HighDimProb.Experimental	Broad opt-in import for modules under active development.

Representative results

Lean API	Result	Reference or usage
HighDimProb.hoeffding_sum_bounded	Classical two-sided Hoeffding inequality for finite independent bounded sums.	Hoeffding's inequality · Judge case
HighDimProb.bernstein_sum_subExponential	Two-sided Bernstein min-form bound for independent centered sub-exponential sums.	Source · Judge case
HighDimProb.packingCoveringInequality	The standard comparison between packing and covering numbers at related scales.	Nets example
HighDimProb.expect_abs_sub_dyadic_path_le_truncatedEntropyIntegral	Finite dyadic chaining controlled by a truncated covering-number entropy integral.	Empirical-process example
HighDimProb.MatrixBernstein.operatorNormTail_of_primitives	A self-adjoint Matrix Bernstein operator-norm tail bound from explicit primitives.	RandomMatrix API
HighDimProb.MatrixBernstein.sampleCovarianceExactRow	A centered sample-covariance route with an exact row-variance identity.	Sample-covariance example

Exact theorem names and hypotheses are indexed in the theorem atlas and the generated API documentation.

Getting started

The repository currently tracks Lean and Mathlib v4.29.1.

Build the library

git clone https://github.com/dududuguo/HighDimProb.git
cd HighDimProb
lake exe cache get
lake build
lake test

Use HighDimProb as a dependency

Add the package to your lakefile.toml:

[[require]]
name = "HighDimProb"
git = "https://github.com/dududuguo/HighDimProb"
rev = "main"

Then import the smallest surface needed by your proof:

import HighDimProb.Concentration
import HighDimProb.RandomMatrix.Concentration

The root import HighDimProb intentionally contains only Init, Scalar, and Statements; larger theorem families use focused imports.

Proof routes

flowchart LR
  Root["HighDimProb"] --> Scalar["Scalar probability"]
  Scalar --> Conc["Concentration"]
  Conc --> H["Hoeffding · Bernstein · Orlicz"]

  Root --> Proc["Random processes"]
  Proc --> Nets["Nets and metric entropy"]
  Nets --> Chain["Finite chaining · entropy integral"]

  Root --> RM["Random matrices"]
  RM --> MB["Matrix Bernstein"]
  MB --> Apps["Operator norm · rank one · sample covariance"]

Loading

The interactive roadmap expands these routes into their dependencies and source modules. More proof diagrams and the Lean import graph are collected in docs/visualizations/.

Examples and documentation

The examples compile with the library and are written as downstream code:

• Basic usage
• Orlicz feature extraction
• Epsilon nets and metric entropy
• Empirical-process nets and finite chaining
• Random-matrix statement routes
• Sample-covariance tail bounds

Start with the documentation index for guided reading, or open the RandomMatrix API for the supported matrix surface and its exact assumptions.

Contributing

Search Mathlib before adding infrastructure, keep imports narrow, and add a compiled test for each public API. Contributions must not use sorry, admit, new axioms, or placeholder theorem bodies.

python .github/scripts/check_text_quality.py
python scripts/judge_policy_check.py
lake build HighDimProbJudge
lake test

Judge files registered in .github/judge-lock.json are immutable; new public coverage is added as a new leaf. See CONTRIBUTING.md for the complete workflow.

License and acknowledgements

HighDimProb is available under the Apache License 2.0. Thanks to @freezed-corpse-143 for contributions to the project.