Theorem InformationTheory.klDiv_of_not_integrable

Modification history

2026-10-28 01:05
Mathlib/InformationTheory/KullbackLeibler/Basic.lean
chore: replace `irreducible_def` with `no_expose` (#45063) …
Modified InformationTheory.klDiv_of_not_integrableView on Github →
2025-03-03 11:12
Mathlib/InformationTheory/KullbackLeibler/Basic.lean
feat(InformationTheory): define the Kullback-Leibler divergence between two finite measures (#21053) …
Added InformationTheory.klDiv_of_not_integrableView on Github →