proposition: Lemma out_entropy_dist_ub : `| `H(P `o V) - `H(P `o W) | <= / ln 2 * #|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 -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 -iter_addR -big_const; apply leR_sumR => b _; rewrite addRC. apply: Rabs_xlnx => //. rewrite 2!fdist_outE -addR_opp big_morph_oppR -big_split /=. apply: leR_trans; first exact: leR_sumR_Rabs. apply: (@leR_trans (d((P `X V), (P `X W)))). - rewrite /var_dist /=. apply (@leR_trans (\sum_a \sum_b `| ((P `X V)) (a, b) - ((P `X W)) (a, b) | )); last first. by apply Req_le; rewrite pair_bigA /=; apply eq_bigr => -[]. apply: leR_sumR => a _. rewrite (bigD1 b) //= distRC -[X in X <= _]addR0. rewrite 2!fdist_prodE /= !(mulrC (P a)) addR_opp. 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