Mathlib Map

Map · 28

measure theory

MSC 28 · Measure and integration

12,070 declarations (10,875 theorems, 1,195 definitions) across 288 files. 12 of the 27 famous theorems listed for this area are in Mathlib (44%), 13 in some Lean library. 7 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.

Subareas4

  • 28A Classical measure theory 11,205
  • 28C Set functions and measures on spaces with additional structure 515
  • 28B Set functions, measures and integrals with values in abstract spaces 247
  • 28D Measure-theoretic ergodic theory 103

Famous theorems12 of 27

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

Not yet in Mathlib · 15

In Mathlib · 12

From the 100 theorems list1

Open conjectures stated in Lean7

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing4 of 38

From Mathlib's own undergraduate checklist.

Measures and integral calculus · 4 of 38

  • Integration › change of variables to spherical co-ordinates
  • Fourier analysis › convolution product of periodic functions
  • Fourier analysis › Dirichlet theorem
  • Fourier analysis › Fejer theorem

Structures defined here24

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

Files288

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