proposition: Lemma joint_entropy_dist_ub : `| `H(P , V) - `H(P , W) | <= / ln 2 * #|A|%:R * #|B|%:R * - xlnx (sqrt (2 * D(V || W | P))).
proof: Proof. rewrite 2!xlnx_entropy. rewrite -addR_opp -mulRN -mulRDr normRM gtR0_norm; last exact/invR_gt0/ln2_gt0. rewrite -2!mulRA; apply leR_pmul2l; first exact/invR_gt0/ln2_gt0. rewrite oppRK big_morph_oppR -big_split /=. apply: leR_trans; first exact: leR_sumR_Rabs. rewrite -2!iter_addR -2!big_const pair_bigA /=. apply: leR_sumR; case => a b _; rewrite addRC /=. apply Rabs_xlnx => //. apply (@leR_trans (d(P `X V, P `X W))). - rewrite /var_dist /R_dist (bigD1 (a, b)) //= distRC. rewrite -[X in X <= _]addR0. by apply/leR_add2l/RleP/sumr_ge0 => ? _; exact/RleP/normR_ge0. - rewrite cdiv_is_div_joint_dist => //. exact/Pinsker_inequality_weak/joint_dominates. Qed.
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