proposition: Lemma pinsker_function_spec_pos c q : 0 <= c <= / (2 * ln 2) -> 0 <= q < 1 -> 0 <= pinsker_function_spec c q.
proof: Proof. move=> Hc [q0 q1]. rewrite (_ : 0 = pinsker_function_spec c 0); last first. by rewrite /pinsker_function_spec /= subR0 /log Log_1; field. apply pinsker_fun_increasing_on_0_to_1 => //. by case: Hc. Qed.
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