proposition: Lemma cdiv_is_div_joint_dist : D(V || W | P) = D((P `X V) || (P `X W)).
proof: Proof. rewrite (_ : D(V || W | P) = \sum_(a in A) (\sum_(b in B) V a b * (log (V a b / W a b)) * P a)); last first. apply eq_bigr => a _. by rewrite -(big_morph _ (morph_mulRDl _) (mul0R _)) mulRC. rewrite pair_bigA big_mkcond /=. apply eq_bigr => -[a b] /= _. rewrite fdist_prodE /= -RmultE (mulRC (P a)) [in RHS]mulRAC. case/boolP : (P a == 0) => [/eqP -> | Pa0]; first by rewrite !mulR0. congr (_ * _). case/boolP : (V a b == 0) => [/eqP -> | Vab0]; first by rewrite !mul0R. congr (_ * _). have Wab0 : W a b != 0 := dominatesEN (V_dom_by_W Pa0) Vab0. rewrite fdist_prodE /= {2}/Rdiv -RmultE (mulRC _ (W a b)) (invRM (W a b)) //. by rewrite -mulRA (mulRCA (P a)) mulRV // mulR1. Qed.
imports: mathcomp(all_ssreflect ssralg finset matrix) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb ln_facts num_occ fdist entropy channel divergence types jtypes proba jfdist_cond