fact: Hypothesis set_of_I_has_ubound : classical_sets.has_ubound (fun y => exists P, `I(P, W) = y).
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals Lra mathcomp(Rstruct reals) ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts fdist entropy channel_code channel divergence conditional_divergence variation_dist pinsker