proposition: Theorem v_scode_converse' : n%:R * `H P <= @E_leng_cw _ _ P f.
proof: Proof. case: (Req_dec 0 (INR n))=>[<-|nnon0]. by rewrite mul0R; apply/ltRW/(EX_gt0 (P `^ n) f_uniq). have npos : 0 < n%:R by rewrite (_ : 0 = INR 0) // ltR_neqAle leR_nat leq0n. rewrite -(@leR_pmul2r (/ n%:R)); last exact/invR_gt0. rewrite (mulRC (INR n)) -mulRA mulRV ?mulR1; last exact/gtR_eqF. apply: le_epsilon => eps eps0. pose fm (x : 'rV['rV[A]_n]_((m eps))) := extension f (tuple_of_row x). case: (Rle_or_lt ((m eps)%:R * (log #| 'rV[A]_n |%:R)) (@E_leng_cw _ _ (P `^ n) fm)). move/(@converse_case2 _ _ fm (P `^ n)). rewrite !entropy_TupleFDist ELC_TupleFDist. rewrite (leR_pmul2l (mpos eps nnon0)) => H. apply: (@leR_trans (@E_leng_cw _ _ P f / n%:R)) => //. by rewrite leR_pdivl_mulr // mulRC. by rewrite leR_addl; exact/ltRW. have mnon0 : (m eps)%:R <> 0 by exact/eqP/gtR_eqF/mpos. move => case2. move: (@converse_case1 _ _ _ (P `^ n) (fm_uniq f_uniq (Rlt_not_eq _ _ (mpos eps nnon0))) case2). rewrite !entropy_TupleFDist ELC_TupleFDist -!mulRA mulRA. move/(Rmult_le_compat_r _ _ _ (Rlt_le _ _ (Rinv_0_lt_compat _ (mpos eps nnon0)))). rewrite -mulRA -mulRA mulRC mulRA -mulRA mulVR ?mulR1; last exact/eqP. rewrite mulRDl (mulRC (m eps)%:R) -mulRA ?mulRV ?mulR1; last exact/eqP. move/(Rmult_le_compat_r _ _ _ (Rlt_le _ _ (Rinv_0_lt_compat _ npos))). rewrite (mulRC (INR n)) -mulRA mulRV ?mulR1; last exact/gtR_eqF. rewrite mulRDl. move/leR_trans; apply. rewrite leR_add2l. rewrite mulRA (mulRC (exp 1)) -(mulRA (m eps)%:R). apply le_eps => //. move: case2. rewrite ELC_TupleFDist mulRC (mulRC (m eps)%:R) card_mx mul1n -natRexp log_pow; last first. by rewrite (_ : 0 = INR 0) //; apply/lt_INR/ltP/fdist_card_neq0; exact: P. move/(ltR_pmul2r (mpos eps nnon0)) => /ltRW. by apply: leR_trans; exact/le_1_EX. 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