Theorem InformationTheory.integral_llr_add_sub_measure_univ_nonneg

Modification history

2025-03-03 11:12
Mathlib/InformationTheory/KullbackLeibler/Basic.lean
feat(InformationTheory): define the Kullback-Leibler divergence between two finite measures (#21053) …
Added InformationTheory.integral_llr_add_sub_measure_univ_nonnegView on Github →