candidate lemma for a PR (bounded, lee_sum, nneseries) #1530
Description
They are coming from the PR on the sampling lemma PR #1240 @t6s
Lemma bounded_image (T : Type) (K : numFieldType)
(V : pseudoMetricNormedZmodType K) (E : T -> V) (A : set T) :
[bounded y | y in E @` A] = [bounded E x | x in A].
Proof.
rewrite /bounded_near !nearE.
congr (+oo _); apply: funext=> M.
apply: propext; split => /=.
by move=> + x Ax => /(_ (E x)); apply; exists x.
by move=> H x [] y Ay <-; exact: H.
Qed.
Lemma finite_bounded (K : realFieldType) (V : pseudoMetricNormedZmodType K)
(A : set V) : finite_set A -> bounded_set A.
Proof.
move=> fA.
exists (\big[Order.max/0]_(y <- fset_set A) normr y).
split=> //.
apply: (big_ind (fun x => x \is Num.real))=> //.
by move=> *; exact: max_real.
move=> x ltx v Av /=.
apply/ltW/(le_lt_trans _ ltx)/le_bigmax_seq=> //.
by rewrite in_fset_set// inE.
Qed.
Arguments card_le_finite [T U].
(* naming inconsistency: there is also `sub_finite_set`:
sub_finite_set :
forall [T : Type] [A B : set T], A `<=` B -> finite_set B -> finite_set A *)
Lemma finite_range_comp (T0 T1 T2 : Type) (f : T0 -> T1) (g : T1 -> T2) :
finite_set (range f) \/ finite_set (range g) -> finite_set (range (g \o f)).
Proof.
rewrite -(image_comp f g).
case.
move=> cf; apply: (card_le_finite _ (range f))=> //.
exact: card_image_le.
move=> cg; apply: (card_le_finite _ (range g))=> //.
exact/subset_card_le/image_subset.
Qed.
Arguments finite_range_comp [T0 T1 T2].
(* generalizations with an additional predicate (m <= i)%N as in big_geq_mkord *)
Lemma lee_sum_fset_nat_geq (R : realDomainType) (f : sequence \bar R)
(F : {fset nat}) (m n : nat) (P : pred nat) :
(forall i : nat, P i -> (0%R <= f i)%E) ->
[set` F] `<=` `I_n ->
((\sum_(i <- F | P i && (m <= i)%N) f i)%R
<= (\sum_(m <= i < n | P i) f i)%R)%E.
Proof.
move=> f0 Fn.
rewrite big_geq_mkord/= -(big_mkord (fun i => P i && (m <= i)%N)).
apply: lee_sum_fset_nat=> //.
by move=> ? /andP [] *; exact: f0.
Qed.
Arguments lee_sum_fset_nat_geq {R f} F m n P.
Lemma lee_sum_fset_lim_geq (R : realType) (f : sequence \bar R)
(F : {fset nat}) m (P : pred nat) :
(forall i : nat, P i -> (0%R <= f i)%E) ->
((\sum_(i <- F | P i && (m <= i)%N) f i)%R
<= \big[+%R/0%R]_(m <= i <oo | P i) f i)%E.
Proof.
move=> f0; pose n := (\max_(k <- F) k).+1.
rewrite (le_trans (lee_sum_fset_nat_geq F m n _ _ _))//; last first.
by apply: nneseries_lim_ge => // k _; exact: f0.
move=> k /= kF; rewrite /n big_seq_fsetE/=.
by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax.
Qed.
Arguments lee_sum_fset_lim_geq {R f} F m P.
Lemma nneseries_esum_geq (R : realType) (a : nat -> \bar R) m (P : pred nat) :
(forall n : nat, P n -> (0%R <= a n)%E) ->
\big[+%R/0]_(m <= i <oo | P i) a i = \esum_(i in [set x | P x && (m <= x)%N]) a i.
Proof.
move=> a0; apply/eqP; rewrite eq_le; apply/andP; split.
apply: lime_le.
by apply: is_cvg_nneseries_cond => n _; exact: a0.
apply: nearW=> n.
apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i && (m <= i)%N]%fset].
split; first exact: finite_fset.
by move=> /= k /imfsetP[/= i]; rewrite inE => + ->.
rewrite fsbig_finite//= set_fsetK big_imfset/=; last first.
by move=> ? ? ? ? /val_inj.
by rewrite big_filter big_enum_cond/= big_geq_mkord.
apply: ub_ereal_sup => _ [/= F [finF PF] <-].
rewrite fsbig_finite//= -(big_rmcond_in (fun i=> P i && (m <= i)%N))/=.
exact: lee_sum_fset_lim_geq.
by move=> k; rewrite in_fset_set// inE => /PF ->.
Qed.
Lemma nneseriesID (R : realType) m (a P : pred nat) (f : nat -> \bar R):
(forall k : nat, P k -> (0%R <= f k)%E) ->
\big[+%R/0]_(m <= k <oo | P k) f k =
(\big[+%R/0%R]_(m <= k <oo | P k && a k) f k)%E
+ (\big[+%R/0%R]_(m <= k <oo | P k && ~~ a k) f k)%E.
Proof.
move=> nn.
rewrite nneseries_esum_geq//.
rewrite (esumID a)/=; last by move=> ? /andP [] *; exact: nn.
have->: [set x | P x && (m <= x)%N] `&` (fun x : nat => a x) =
[set x | (P x && a x) && (m <= x)%N].
by apply: funext=> x /=; rewrite (propext (rwP andP)) andbAC.
have->: [set x | P x && (m <= x)%N] `&` ~` (fun x : nat => a x) =
[set x | (P x && ~~ a x) && (m <= x)%N].
apply: funext=> x /=.
by rewrite (propext (rwP negP)) (propext (rwP andP)) andbAC.
by rewrite -!nneseries_esum_geq//; move=> ? /andP [] *; exact: nn.
Qed.