proposition: Lemma entroPN_0 : `E X = 1 -> `H PN = 0.
proof: Proof. move => EX_1. have eq_0_P : forall a, X a <> 1 -> 0 = P a. move: EX_1. rewrite (_ : 1 = 1%mcR)// -{1}(FDist.f1 P) => EX1 a Xnon1. have /leR_sumR_eq H : forall i : A, i \in A -> P i <= (size (f i))%:R * P i. move=> i _; rewrite -{1}(mul1R ( P i)). apply/leR_wpmul2r; first exact/RleP/FDist.ge0. by move: (Xpos i); rewrite (_ : 1 = 1%:R) //= (_ : 0 = 0%:R) // ltR_nat leR_nat. case: (Req_dec (P a) 0) => //. have : (size (f a))%:R * P a = P a by rewrite (H EX1 a). rewrite -{2}(mul1R (P a)). by move/Rmult_eq_reg_r => tmp /tmp. rewrite /entropy Ropp_eq_0_compat //. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addR ?mulR0 //= => i _. rewrite /pr_eq; unlock. rewrite /Pr ffunE. rewrite -INRE. case: (Req_dec i%:R 1)=>[->| neq0]. rewrite [X in _ * log X = _](_ : _ = 1); first by rewrite /log Log_1 mulR0. rewrite (_ : 1 = 1%mcR)//. rewrite -{2}(FDist.f1 P). rewrite [in RHS](bigID (fun a => a \in [set x | (size (f x))%:R == 1])) /=. rewrite [X in _ = _ + X](_ : _ = 0); first by rewrite addR0. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addR ?mulR0 // => j. by rewrite inE; move/eqP/eq_0_P. rewrite [X in X * _ = _](_ : _ = 0); first by rewrite mul0R. rewrite big1 // => j. rewrite inE; move/eqP => eq_Xj_i. by move: neq0; rewrite -eq_Xj_i => /eq_0_P. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code