proposition: Lemma wolfowitz a b A B : 0 < A -> 0 < B -> a <= \sum_(x in s) P `^ k x <= b -> (forall x : 'rV_k, x \in s -> A <= P `^ k x <= B) -> a / B <= (#| s |)%:R <= b / A.
proof: Proof. move=> A0 B0 /andP [Ha Hb] H. have eq_le_ : forall x y, (x = y) -> (x <= y)%O. by move=> ? ? ? ? ->. have HB : \sum_(x in s) P `^ _ x <= #|s|%:R * B. apply (@le_trans _ _ (\sum_(x in s) [fun _ => B] x)). by apply: ler_sum => /= i iA; move: (H i iA) => /andP []. rewrite -big_filter /= big_const_seq /= iter_addr /=. rewrite addr0 -(mulr_natl B (count _ _)). apply: ler_wpM2r; first by rewrite ltW. apply eq_le_. have [/= l el [ul ls] [pl sl]] := big_enumP _. by rewrite count_predT sl; congr (_%:R)%R. have HA : (#|s|)%:R * A <= \sum_(x in s) P `^ _ x. apply (@le_trans _ _ (\sum_(x in s) [fun _ => A] x)); last first. by apply: ler_sum => i Hi /=; case/andP: (H i Hi). rewrite -big_filter /= big_const_seq /= iter_addr /=. rewrite addr0 -(mulr_natl A (count _ _)). apply: ler_wpM2r; first by rewrite ltW. apply eq_le_. have [/= l el [ul ls] [pl sl]] := big_enumP _. by rewrite count_predT sl; congr (_%:R)%R. apply/andP. split. - by rewrite ler_pdivrMr //; move/le_trans : Ha; exact. - by rewrite ler_pdivlMr //; exact: (le_trans HA). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext