Mathlib Map

Map · 60

probability

MSC 60 · Probability theory and stochastic processes

4,345 declarations (3,939 theorems, 406 definitions) across 132 files. 9 of the 45 famous theorems listed for this area are in Mathlib (20%), 10 in some Lean library. 9 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas7

  • 60A Foundations of probability theory 1,902
  • 60G Stochastic processes 1,209
  • 60E Distribution theory 870
  • 60B Probability theory on algebraic and topological structures 190
  • 60J Markov processes 101
  • 60F Limit theorems in probability theory 64
  • 60C Combinatorial probability 9

Famous theorems9 of 45

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 36

In Mathlib · 9

From the 100 theorems list3

Open conjectures stated in Lean9

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing9 of 38

From Mathlib's own undergraduate checklist.

Probability Theory · 9 of 38

  • Definitions of a probability space › law of total probability
  • Random variables and their laws › absolute continuity of probability laws
  • Random variables and their laws › law of joint probability
  • Random variables and their laws › transfer theorem
  • Random variables and their laws › uniform law
  • Random variables and their laws › probability generating functions
  • Random variables and their laws › applications of probability generating functions to sums of independent random variables
  • Convergence of a sequence of random variables › Lévy's theorem
  • Convergence of a sequence of random variables › weak law of large numbers

Structures defined here14

Typeclasses defined in this area's files, most assumed first.

Files132

Largest first. The code after each file is its assigned subarea.