proposition: Lemma multinomial_ineq (l : seq nat) (p := \prod_(j <- l) j ^ j) (s := \sum_(j <- l) j) : 'C[l] * p <= s ^ s.
proof: Proof. rewrite -lez_nat -!natz natrX natrM natr_sum. pose lz : seq int := [seq i%:R | i <- l]. have -> : (\sum_(i <- l) i%:R = \sum_(i <- lz) i)%R by rewrite big_map. pose m := s; pose n := s. have /generalizedNewton -> : n <= m by []. have paux (i : 'I_(size l)) : nth 0 l i < m.+1. rewrite ltnS /m /s. have /(big_rem _) -> /= : (nth 0 l i) \in l by rewrite mem_nth. exact: leq_addr. pose aux (i : 'I_(size l)) := Ordinal (paux i). pose tl := mktuple aux. have Heq : tmap_val tl = l. suff Heq1 (i : 'I_(size l)) : nth 0 (tmap_val tl) i = nth 0 l i. apply: (@eq_from_nth nat 0 _ _); rewrite size_map size_tuple // . move => i Hisize. suff -> : nth 0 (tmap_val tl) (Ordinal Hisize) = nth 0 l (Ordinal Hisize) by []. exact: Heq1. by rewrite (nth_map ord0 0) /tl ?size_tuple ?(nth_mktuple aux ord0 i). rewrite /lz size_map; set P := BIG_P. have /(bigD1 _) -> /= : P tl. rewrite /P /n /s big_tuple big_tnth /=; apply/eqP/eq_bigr => i _. by rewrite tnth_mktuple /aux /= (tnth_nth 0) in_tupleE. suff {P} -> : (('C[l])%:R * p%:R = ('C[tmap_val tl])%:R * monomial [seq i%:R | i <- l] (tmap_val tl) :> int)%R. rewrite cprD; apply: sumr_ge0 => i _; apply: mulr_ge0. - by rewrite ler0n. - rewrite /monomial big_seq_cond. apply: prodr_ge0 => j; rewrite andbT => /nth_index hj. rewrite -(hj (1 : int, 0%N)) nth_zip /=; last first. by rewrite !size_map size_tuple. rewrite exprn_ge0 //. set ll := (X in (0 <= nth _ X _)%R); set k := index _ _. case: (ltnP k (size ll)) => [/mem_nth |] hk. suff ll_pos x : x \in ll -> (0 <= x)%R by apply: ll_pos. rewrite /ll; case/mapP => u _ ->; exact: ler0n. by rewrite nth_default. congr (_ * _)%R. - apply/eqP; rewrite eqr_nat. by rewrite Heq. - rewrite /monomial /p Heq natr_prod. suff -> : zip [seq i%:R | i <- l] l = map (fun i => (Posz i,i)) l. rewrite big_map. by apply: eq_bigr => i _ /=; first by rewrite natrX -exprnP -natz. apply: (@eq_from_nth _ (0%:R,0));rewrite size_zip !size_map minnn// => i Hi. rewrite nth_zip ?size_map // ; rewrite (nth_map 0 (Posz 0)) // . by rewrite (nth_map 0 (Posz 0,0)) // natz. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp