proposition: Theorem concats_entropy ss : \sum_(s <- ss) nHs s <= nHs (flatten ss).
proof: Proof. rewrite exchange_big /nHs /=. apply leR_sumR => a _. rewrite (bigID (fun s => N(a|s) == O)) /=. rewrite big1; last by move=> i ->. rewrite num_occ_flatten add0R. rewrite [in X in _ <= X](bigID (fun s => N(a|s) == O)). rewrite [in X in _ <= X]big1 //= ?add0n; last by move=> i /eqP. rewrite (eq_bigr (fun i => N(a|i) * log (size i / N(a|i)))); last by move=> i /negbTE ->. rewrite -big_filter -[in X in _ <= X]big_filter. set ss' := [seq s <- ss | N(a|s) != O]. case/boolP: (ss' == [::]) => Hss'. by rewrite (eqP Hss') !big_nil eqxx. have Hnum s : s \in ss' -> (N(a|s) > 0)%nat. by rewrite /ss' mem_filter lt0n => /andP [->]. have Hnum': 0 < N(a|flatten ss'). apply /ltR0n; destruct ss' => //=. rewrite /num_occ count_cat ltn_addr //. by rewrite Hnum // in_cons eqxx. have Hsz: 0 < size (flatten ss'). apply (ltR_leR_trans Hnum'). by apply /le_INR /leP /count_size. apply (@leR_trans ((\sum_(i <- ss') N(a|i))%:R * log (size (flatten ss') / (\sum_(i <- ss') N(a|i))%nat))); last first. case: ifP => Hsum. by rewrite (eqP Hsum) mul0R. apply leR_wpmul2l => //. apply Log_increasing_le => //. apply/mulR_gt0 => //. apply/invR_gt0/ltR0n. by rewrite lt0n Hsum. apply leR_wpmul2r. apply /Rlt_le /invR_gt0 /ltR0n. by rewrite lt0n Hsum. apply /le_INR /leP. rewrite !size_flatten !sumn_big_addn. rewrite !big_map big_filter. rewrite [in X in (_ <= X)%nat] (bigID (fun s => N(a|s) == O)) /=. by apply leq_addl. have Htotal := esym (num_occ_flatten a ss'). rewrite big_tnth in Htotal. have Hnum2 : N(a|flatten ss') != O. rewrite -lt0n; exact/ltR0n. set d := seq_nat_fdist Htotal Hnum2. set r := fun i => (size (tnth (in_tuple ss') i)) / N(a|tnth (in_tuple ss') i). have Hr: forall i, r i \in Rpos_interval. rewrite /r /= => i. rewrite classical_sets.in_setE; apply Rlt_mult_inv_pos; apply /ltR0n. apply (@leq_trans N(a|tnth (in_tuple ss') i)). by rewrite Hnum // mem_tnth. by apply count_size. by apply /Hnum /mem_tnth. move: (jensen_dist_concave log_concave d Hr). rewrite /d /r /=. under eq_bigr do rewrite ffunE /=. under [X in _ <= log X -> _]eq_bigr do rewrite ffunE /=. rewrite -(big_tnth _ _ _ xpredT (fun s => (N(a|s) / N(a|flatten ss')) * log ((size s) / N(a|s)))). rewrite -(big_tnth _ _ _ xpredT (fun s => (N(a|s) / N(a|flatten ss')) * (size s / N(a|s)))). move/(@leR_wpmul2r N(a|flatten ss') _ _ (leR0n _)). rewrite !big_distrl /=. rewrite (eq_bigr (fun i => N(a|i) * log (size i / N(a|i)))); last first. by move=> i _; rewrite mulRAC -!mulRA (mulRA (/ _)) mulVR ?mul1R // gtR_eqF. move/leR_trans; apply. rewrite mulRC -num_occ_flatten big_filter. rewrite (eq_bigr (fun i => size i / N(a|flatten ss'))); last first. move=> i Hi; rewrite mulRCA {1}/Rdiv mulRAC. by rewrite mulRV ?mul1R // INR_eq0'. rewrite -big_filter -/ss' -big_distrl. rewrite -big_morph_natRD /=. by rewrite size_flatten sumn_big_addn big_map. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb fdist entropy convex ln_facts jensen num_occ