proposition: Lemma lee_sum_fset_nat (R : realDomainType) (f : (\bar R)^nat) (F : {fset nat}) n (P : pred nat) : (forall i, P i -> 0%E <= f i) -> [set` F] `<=` `I_n -> \sum_(i <- F | P i) f i <= \sum_(0 <= i < n | P i) f i.
proof: Proof. move=> f0 Fn; rewrite [leRHS](bigID (mem F))/=. suff -> : \sum_(0 <= i < n | P i && (i \in F)) f i = \sum_(i <- F | P i) f i. by rewrite leeDl ?sume_ge0// => i /andP[/f0]. rewrite -big_filter -[RHS]big_filter; apply: perm_big. rewrite uniq_perm ?filter_uniq ?index_iota ?iota_uniq ?fset_uniq//. move=> i; rewrite ?mem_filter. case: (boolP (P i)) => //= Pi; case: (boolP (i \in F)) => //= Fi. by rewrite mem_iota leq0n add0n subn0/=; apply: Fn. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun