proposition: Lemma le_sum_all_cond (T : finType) (P : pred T) (r1 r2 : K) F G : 0 < r1 -> 0 < r2 -> \sum_(i in P) G i > 0 -> (forall i, P i -> 0 <= F i) -> (forall i, P i -> 0 <= G i) -> (r1 * \sum_(i in P) G i) <= \sum_(i in P | r2 <= F i / G i) G i -> r1 * r2 <= (\sum_(i in P) F i) / \sum_(i in P) G i.
proof: Proof. move=> Hr1p Hr2p HGp HF HG Hr1. have HGneq0 : forall i, i \in P -> r2 <= F i / G i -> G i != 0. move=> i Hi Hir2. have : 0 < F i / G i by apply (Order.POrderTheory.lt_le_trans Hr2p). move: (HF i Hi) (HG i Hi). rewrite le0r. move/orP => [|] HFi HGi. by rewrite (eqP HFi) mul0r ltxx. rewrite pmulr_rgt0 // => /lt0r_neq0 HGi1. by rewrite -(invrK (G i)) invr_neq0. apply (@Order.POrderTheory.le_trans _ K ((\sum_(i in P | r2 <= F i / G i) G i / \sum_(i in P) G i) * (\sum_(i in P | r2 <= F i / G i) F i / \sum_(i in P | r2 <= F i / G i) G i))). apply ler_pM; try by assumption || apply ltW. rewrite -big_distrl -(mulr1 r1) -(mulfV (lt0r_neq0 HGp)) mulrA /=. apply ler_pM => //. by rewrite mulr_ge0 // ltW. by rewrite invr_ge0 ltW. rewrite -big_distrl /=. rewrite (_ : \sum_(i in P | r2 <= F i / G i) F i = \sum_(i in P | r2 <= F i / G i) (F i / G i) * G i); first last. apply eq_bigr => i /andP [Hi Hir2]. rewrite -mulrA (mulrC _ (G i)) mulfV ?mulr1 //. by apply HGneq0. have HGp' : \sum_(i in P | r2 <= F i / G i) G i > 0. apply (@Order.POrderTheory.lt_le_trans _ K (r1 * (\sum_(i in P) G i))) => //. by apply mulr_gt0. rewrite -{1}(mulr1 r2) -(mulfV (lt0r_neq0 HGp')). rewrite mulrA big_distrr /=. apply ler_pM => //. apply sumr_ge0 => i /andP [Hi Hir2]. rewrite mulr_ge0 //; try by apply ltW. by apply HG. by rewrite ltW // invr_gt0. apply ler_sum => i /andP [Hi Hir2]. apply ler_pM => //; try by apply ltW. exact: HG. apply (@Order.POrderTheory.le_trans _ K (\sum_(i in P | r2 <= F i / G i) F i / \sum_(i in P) G i)). rewrite -!big_distrl /= mulrC -mulrA (mulrA _ _ (\sum_(i in P) G i)^-1). rewrite mulVf ?mul1r //. apply lt0r_neq0. apply: @Order.POrderTheory.lt_le_trans; try apply Hr1. by apply mulr_gt0. rewrite -big_distrl /=. apply: ler_pM => //. apply sumr_ge0 => i /andP [Hi Hir2]. exact: HF. by rewrite ltW // invr_gt0. rewrite [\sum_(i in P) F i](bigID (fun i => r2 <= F i / G i)) /=. rewrite ler_wpDr// sumr_ge0// => i /andP[Hi Hir2]. exact: HF. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner