fact: Definition pinsker_fun p c := fun q => p * log (div_fct (fun _ => p) id q) + (1 - p) * log (div_fct (fun _ => 1 - p) (fun q => 1 - q) q) - 4 * c * comp (fun x => x ^2) (fun q => p - q) q.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext logb ln_facts bigop_ext convex fdist divergence variation_dist partition_inequality