Map · 94
information theory
MSC 94 · Information and communication theory, circuits
204 declarations (174 theorems, 30 definitions) across 8 files. 0 of the 4 famous theorems listed for this area are in Mathlib (0%). 29 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
- 94A Communication, information 123
- 94B Theory of error-correcting codes and error-detecting codes 81
Famous theorems0 of 4
From the 1000+ theorems project, which classifies each theorem by MSC area.
Open conjectures stated in Lean29
Statements without proofs, collected by the Formal Conjectures project.
- Green40.green_40Green's Open Problems
- Green40.green_40.f_eq_one_for_allGreen's Open Problems
- Green40.green_40.f_two_eq_oneGreen's Open Problems
- Green40.green_40.variants.all_nGreen's Open Problems
- Green40.green_40.variants.arbitrary_subsetsGreen's Open Problems
- OpenQuantumProblem13.mutuallyUnbiasedBasesOpenQuantumProblems
- OpenQuantumProblem13.mutuallyUnbiasedBases_dim10OpenQuantumProblems
- OpenQuantumProblem13.mutuallyUnbiasedBases_dim12OpenQuantumProblems
- OpenQuantumProblem13.mutuallyUnbiasedBases_dim14OpenQuantumProblems
- OpenQuantumProblem13.mutuallyUnbiasedBases_dim15OpenQuantumProblems
- OpenQuantumProblem13.mutuallyUnbiasedBases_dim6OpenQuantumProblems
Files8
Largest first. The code after each file is its assigned subarea.
- Mathlib.InformationTheory.Hamming
Hamming spaces
94B · 81
- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Properties of Shannon q-ary entropy and binary entropy functions
94A · 45
- Mathlib.InformationTheory.KullbackLeibler.Basic
Kullback-Leibler divergence
94A · 29
- Mathlib.InformationTheory.KullbackLeibler.KLFun
The real function `fun x ↦ x * log x + 1 - x`
94A · 26
- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
Data processing inequality for the Kullback-Leibler divergence
94A · 13
- Mathlib.InformationTheory.KullbackLeibler.ChainRule
Chain rule for the Kullback-Leibler divergence
94A · 6
- Mathlib.InformationTheory.Coding.UniquelyDecodable
Uniquely Decodable Codes
94A · 3
- Mathlib.InformationTheory.Coding.KraftMcMillan
Kraft-McMillan Inequality
94A · 1