proposition: Lemma convex_relative_entropy (p1 p2 q1 q2 : {fdist A}) (r : {prob R}) : p1 `<< q1 -> p2 `<< q2 -> D(p1 <| r |> p2 || q1 <| r |> q2) <= D(p1 || q1) <| r |> D(p2 || q2).
proof: Proof. move=> pq1 pq2. exact: (convex_div (exist _ (p1, q1) pq1) (exist _ (p2, q2) pq2)). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(mathcomp_extra Rstruct reals) Reals Ranalysis_ext Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist jfdist_cond entropy convex binary_entropy_function log_sum divergence