Mathlib Map

Map · 42

harmonic analysis

MSC 42 · Harmonic analysis on Euclidean spaces

354 declarations (316 theorems, 38 definitions) across 14 files. 2 of the 5 famous theorems listed for this area are in Mathlib (40%). 13 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.

Subareas2

  • 42A Harmonic analysis in one variable 316
  • 42B Harmonic analysis in several variables 38

Famous theorems2 of 5

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

Not yet in Mathlib · 3

In Mathlib · 2

From the 100 theorems list1

Open conjectures stated in Lean13

Statements without proofs, collected by the Formal Conjectures project.

Files14

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