diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a14df7346..1ed83e6d9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,10 +58,25 @@ ### Generalized +- in `sequences.v`, + + generalized indexing from zero-based ones (`0 <= k < n` and `k \oo]--> nu Aoo. exact: charge_semi_sigma_additive. have nuAoo : 0 <= nu Aoo. - move/cvg_lim : cvg_nuA => <-//=; apply: nneseries_ge0 => n _. + move/cvg_lim : cvg_nuA => <-//=; apply: nneseries_ge0 => n _ _. exact: nuA_ge0. have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0. rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first. @@ -853,7 +853,7 @@ move=> /cvg_ex[[l| |]]; first last. by rewrite leNgt => /negP; apply; rewrite ltNye_eq fin_num_measure. - move/cvg_lim => limoo. have := @npeseries_le0 _ (fun n => maxe (z_ (v n) * 2^-1%:E) (- 1%E)) xpredT 0. - by rewrite limoo// leNgt => /(_ (fun n _ => max_le0 n))/negP; apply. + by rewrite limoo// leNgt => /(_ (fun n _ _ => max_le0 n))/negP; exact. move/fine_cvgP => [Hfin cvgl]. have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n --> \oo]). apply/cvg_ex; exists l; move: cvgl. diff --git a/theories/esum.v b/theories/esum.v index 7549ecad0..8696387ac 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -300,7 +300,8 @@ Lemma lee_sum_fset_lim (R : realType) (f : (\bar R)^nat) (F : {fset nat}) \sum_(i <- F | P i) f i <= \sum_(i f0; pose n := (\max_(k <- F) k).+1. -rewrite (le_trans (lee_sum_fset_nat F n _ _ _))//; last exact: nneseries_lim_ge. +rewrite (le_trans (lee_sum_fset_nat F n _ _ _))//; last first. + by apply: nneseries_lim_ge => i _; exact: f0. move=> k /= kF; rewrite /n big_seq_fsetE/=. by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax. Qed. @@ -311,7 +312,7 @@ Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) : \sum_(i a0; apply/eqP; rewrite eq_le; apply/andP; split. - apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n. + apply: (lime_le (is_cvg_nneseries_cond (fun n _ => a0 n))); apply: nearW => n. apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i]%fset]. split; first exact: finite_fset. by move=> /= k /imfsetP[/= i]; rewrite inE => + ->. @@ -536,7 +537,7 @@ Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) : cvg ((fun n => \sum_(0 <= k < n | P k) fine (f k))%R @ \oo). Proof. move=> f0 Pf; apply: nondecreasing_is_cvgn. - by apply: nondecreasing_series => n Pn; exact/fine_ge0/f0. + by apply: nondecreasing_series => n _ Pn; exact/fine_ge0/f0. exists (fine (\sum_(i x /= [n _ <-]. rewrite summable_fine_sum// -lee_fin fineK//; last first. by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (summable_pinfty Pf). @@ -627,7 +628,8 @@ Lemma esumB D f g : summable D f -> summable D g -> \esum_(i in D) f i - \esum_(i in D) g i. Proof. move=> Df Dg f0 g0. -have /eqP : esum D (f \- g)^\+ + esum_posneg D g = esum D (f \- g)^\- + esum_posneg D f. +have /eqP : esum D (f \- g)^\+ + esum_posneg D g = + esum D (f \- g)^\- + esum_posneg D f. rewrite !ge0_esum_posneg// -!esumD//. apply eq_esum => i Di; rewrite funeposE funenegE. have [fg|fg] := leP 0 (f i - g i). @@ -648,7 +650,8 @@ rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first. rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq; last 2 first. - - rewrite ge0_esum_posneg// (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. + - rewrite ge0_esum_posneg//. + rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. - rewrite fin_num_adde_defl// ge0_esum_posneg//. rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di. diff --git a/theories/kernel.v b/theories/kernel.v index 31d8ba818..872dab165 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -823,7 +823,7 @@ move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ = apply: eq_integral => V _. by apply/esym/cvg_lim => //; exact/measure_semi_sigma_additive. apply/cvg_closeP; split. - by apply: is_cvg_nneseries => n _; exact: integral_ge0. + by apply: is_cvg_nneseries => n _ _; exact: integral_ge0. rewrite closeE// integral_nneseries// => n. exact: measurableT_comp (measurable_kernel k _ (mU n)) _. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 284f18536..8a966ebcb 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1966,7 +1966,7 @@ rewrite [X in measurable_fun _ X](_ : _ = rewrite [X in measurable_fun _ X](_ : _ = (fun x => limn_esup (fun n => \sum_(0 <= i < n | P i) (h i) \_ D x))); last first. apply/funext=> x; rewrite is_cvg_limn_esupE//. - apply: is_cvg_nneseries_cond => n Pn; rewrite patchE. + apply: is_cvg_nneseries_cond => n _ Pn; rewrite patchE. by case: ifPn => // xD; rewrite h0//; exact/set_mem. apply: measurable_fun_limn_esup => k. under eq_fun do rewrite big_mkcond. @@ -2926,7 +2926,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first. by apply: leeDl; exact: integral_ge0. rewrite ge0_integralE//=; apply: ub_ereal_sup => /= _ [g /= gf] <-. rewrite -integralT_nnsfun (integral_measure_series_nnsfun _ mD). -apply: lee_nneseries => n _. +apply: lee_nneseries => [n _ _|n _]. by apply: integral_ge0 => // x _; rewrite lee_fin. rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //. - by move=> x _; rewrite lee_fin. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 2a1e1993c..108042b88 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2920,7 +2920,7 @@ have [N F5e] : exists N, \sum_(N <= n //; first by move=> i _; exact: esum_ge0. + apply: lee_nneseries => //; first by move=> i *; exact: esum_ge0. move=> n Nn; rewrite measure_bigcup//=. - by rewrite nneseries_esum// set_mem_set. - by move=> i _; exact: measurable_closure. diff --git a/theories/measure.v b/theories/measure.v index cc1637134..013b1a804 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3021,7 +3021,7 @@ apply: (@le_trans _ _ move=> XD; have Xm := decomp_measurable Dm XD. by apply: muS => // [i|]; [exact: mfD|exact: DXsub]. apply: lee_lim => /=; do ?apply: is_cvg_nneseries=> //. - by move=> n _; exact: sume_ge0. + by move=> n _ _; exact: sume_ge0. near=> n; rewrite [n in _ <= n]big_mkcond; apply: lee_sum => i _. rewrite ifT ?inE//. under eq_big_seq. @@ -4230,7 +4230,7 @@ have := outer_measure_sigma_subadditive mu (fun n => if n \in ~` `I_N then F n else set0). move/le_trans; apply. rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries. -- by move=> k _; exact: outer_measure_ge0. +- by move=> k _ _; exact: outer_measure_ge0. - move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk. by rewrite mem_not_I (negbTE Nk) outer_measure0. Qed. @@ -4510,7 +4510,8 @@ suff : forall X, mu X = \sum_(k _) = fun n => \sum_(k < n) mu (A k)); last first. rewrite funeqE => n; rewrite big_mkord; apply: eq_bigr => i _; congr (mu _). by rewrite setIC; apply/setIidPl; exact: bigcup_sup. - move=> ->; have := fun n (_ : xpredT n) => outer_measure_ge0 mu (A n). + move=> ->. + have := fun n (_ : xpredT n) (_ : xpredT n) => outer_measure_ge0 mu (A n). move/(@is_cvg_nneseries _ _ _ 0) => /cvg_ex[l] hl. under [in X in _ --> X]eq_fun do rewrite -(big_mkord xpredT (mu \o A)). by move/cvg_lim : (hl) => ->. @@ -4687,9 +4688,9 @@ rewrite (_ : esum _ _ = \sum_(i ? ? _ _; exact: (@can_inj _ _ _ snd). by congr esum; rewrite predeqE => -[a b]; split; move=> [i _ <-]; exists i. apply: lee_lim. -- apply: is_cvg_nneseries => n _. - by apply: nneseries_ge0 => m _; exact: (muG_ge0 (n, m)). -- by apply: is_cvg_nneseries => n _; apply: adde_ge0 => //; exact: mu_ext_ge0. +- apply: is_cvg_nneseries => n *. + by apply: nneseries_ge0 => m *; exact: (muG_ge0 (n, m)). +- by apply: is_cvg_nneseries => n *; apply: adde_ge0 => //; exact: mu_ext_ge0. - by near=> n; apply: lee_sum => i _; exact: (PG i).2. Unshelve. all: by end_near. Qed. @@ -4923,7 +4924,7 @@ rewrite -(limeD cBA cBNA) // (_ : (fun _ => _) = eseries (fun k => Rmu (B k `&` A) + Rmu (B k `&` ~` A))); last first. by rewrite funeqE => n; rewrite -big_split /=; exact: eq_bigr. apply/lee_lim => //. - by apply/is_cvg_nneseries => // n _; exact: adde_ge0. + by apply/is_cvg_nneseries => // n *; exact: adde_ge0. near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2. - apply: le_measure; rewrite /mkset ?inE//; [|by rewrite -setIUr setUCr setIT]. by apply: measurableU; [exact:measurableI|rewrite -setDE; exact:measurableD]. diff --git a/theories/sequences.v b/theories/sequences.v index 285fb6255..e520f2c9a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -951,13 +951,15 @@ rewrite -(subrr (limn (series u_))). by apply: cvgB => //; rewrite ?cvg_shiftS. Qed. -Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) : - (forall n, P n -> 0 <= u_ n)%R -> - nondecreasing_seq (fun n=> \sum_(0 <= k < n | P k) u_ k)%R. +Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) m : + (forall n, (m <= n)%N -> P n -> 0 <= u_ n)%R -> + nondecreasing_seq (fun n=> \sum_(m <= k < n | P k) u_ k)%R. Proof. move=> u_ge0; apply/nondecreasing_seqP => n. -rewrite [in leRHS]big_mkcond [in leRHS]big_nat_recr//=. -by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. +have [mn|nm] := leqP m n. + rewrite [leRHS]big_mkcond/= [leRHS]big_nat_recr//=. + by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. +by rewrite (big_geq (ltnW _)) // big_geq. Qed. Lemma increasing_series (R : numFieldType) (u_ : R ^nat) : @@ -1546,9 +1548,9 @@ Proof. by move=> ?; apply/cvg_ex; eexists; apply: ereal_nonincreasing_cvgn. Qed. (* NB: see also nondecreasing_series *) Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat) - (P : pred nat) : (forall n, P n -> 0 <= u_ n) -> - nondecreasing_seq (fun n => \sum_(0 <= i < n | P i) u_ i). -Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. + (P : pred nat) N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> + nondecreasing_seq (fun n => \sum_(N <= i < n | P i) u_ i). +Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr. Qed. Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) : f = g -> limn f = limn g. @@ -1558,12 +1560,14 @@ Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N : \sum_(N <= i n /=; apply: big_nat_widenl. Qed. -Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q : - \sum_(i n; rewrite big_mkcondl. Qed. -Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q : - \sum_(i n; rewrite big_mkcondr. Qed. Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : @@ -1571,8 +1575,8 @@ Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : \sum_(N <= i efg; apply/congr_lim/funext => n; exact: eq_bigr. Qed. -Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) : - P =1 Q -> \sum_(i \sum_(N <= i efg; apply/congr_lim/funext => n; apply: eq_bigl. Qed. Arguments eq_eseriesl {R P} Q. @@ -1617,9 +1621,9 @@ Qed. End ereal_series. -Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : - (forall n, P n -> 0 <= u_ n) -> - \sum_(0 <= i < k | P i) u_ i <= \sum_(i P n -> 0 <= u_ n) -> + \sum_(m <= i < k | P i) u_ i <= \sum_(m <= i -> //. by apply: ereal_sup_ubound; exists k. @@ -1663,36 +1667,36 @@ Lemma is_cvg_ereal_npos_natsum m : (forall n, (m <= n)%N -> u_ n <= 0) -> cvgn (fun n => \sum_(m <= i < n) u_ i). Proof. by move=> u_le0; apply: is_cvg_ereal_npos_natsum_cond => n /u_le0. Qed. -Lemma is_cvg_nneseries_cond P N : (forall n, P n -> 0 <= u_ n) -> +Lemma is_cvg_nneseries_cond P N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). Proof. -by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n _; exact: u_ge0. +by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n Nn; exact: u_ge0. Qed. -Lemma is_cvg_npeseries_cond P N : (forall n, P n -> u_ n <= 0) -> +Lemma is_cvg_npeseries_cond P N : (forall n, (N <= n)%N -> P n -> u_ n <= 0) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). -Proof. by move=> u_le0; apply: is_cvg_ereal_npos_natsum_cond => n _ /u_le0. Qed. +Proof. by move=> u_le0; exact: is_cvg_ereal_npos_natsum_cond. Qed. -Lemma is_cvg_nneseries P N : (forall n, P n -> 0 <= u_ n) -> +Lemma is_cvg_nneseries P N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). Proof. by move=> ?; exact: is_cvg_nneseries_cond. Qed. -Lemma is_cvg_npeseries P N : (forall n, P n -> u_ n <= 0) -> +Lemma is_cvg_npeseries P N : (forall n, (N <= n)%N -> P n -> u_ n <= 0) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). Proof. by move=> ?; exact: is_cvg_npeseries_cond. Qed. -Lemma nneseries_ge0 P N : (forall n, P n -> 0 <= u_ n) -> +Lemma nneseries_ge0 P N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> 0 <= \sum_(N <= i u0; apply: (lime_ge (is_cvg_nneseries u0)). -by apply: nearW => k; rewrite sume_ge0. +move=> u0; apply: (lime_ge (is_cvg_nneseries u0)); apply: nearW => k. +by rewrite big_nat_cond sume_ge0// => n /andP[/andP[+ _]]; exact: u0. Qed. -Lemma npeseries_le0 P N : (forall n : nat, P n -> u_ n <= 0) -> +Lemma npeseries_le0 P N : (forall n : nat, (N <= n)%N -> P n -> u_ n <= 0) -> \sum_(N <= i u0; apply: (lime_le (is_cvg_npeseries u0)). -by apply: nearW => k; rewrite sume_le0. +move=> u0; apply: (lime_le (is_cvg_npeseries u0)); apply: nearW => k. +by rewrite big_nat_cond sume_le0// => n /andP[/andP[+ _]]; exact: u0. Qed. End cvg_eseries. @@ -1718,32 +1722,21 @@ Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N : (forall i, P i -> 0 <= f i) -> (\sum_(N <= i f0; rewrite -limeMl//; last exact: is_cvg_nneseries. +move=> f0; rewrite -limeMl//; last by apply: is_cvg_nneseries => n _; exact: f0. by apply/congr_lim/funext => /= n; rewrite ge0_sume_distrr. Qed. Lemma adde_def_nneseries (R : realType) (f g : (\bar R)^nat) - (P Q : pred nat) : - (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) -> - (\sum_(i P n -> 0 <= f n) -> + (forall n, (m <= n)%N -> Q n -> 0 <= g n) -> + (\sum_(m <= i f0 g0; rewrite /adde_def !negb_and; apply/andP; split; apply/orP. -- by right; apply/eqP => Qg; have := nneseries_ge0 0 g0; rewrite Qg. -- by left; apply/eqP => Pf; have := nneseries_ge0 0 f0; rewrite Pf. +- by right; apply/eqP => Qg; have := nneseries_ge0 m g0; rewrite Qg. +- by left; apply/eqP => Pf; have := nneseries_ge0 m f0; rewrite Pf. Qed. -Lemma __deprecated__ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R)^nat) : - u_ @ \oo --> +oo <-> (forall A, (0 < A)%R -> \forall n \near \oo, A%:E <= u_ n). -Proof. -by split=> [/cvgeyPge//|u_ge]; apply/cvgeyPgey; near=> x; apply: u_ge. -Unshelve. all: by end_near. Qed. - -Lemma __deprecated__ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R)^nat) : - u_ @ \oo --> -oo <-> (forall A, (A < 0)%R -> \forall n \near \oo, u_ n <= A%:E). -Proof. -by split=> [/cvgeNyPle//|u_ge]; apply/cvgeNyPleNy; near=> x; apply: u_ge. -Unshelve. all: by end_near. Qed. - Lemma __deprecated__ereal_squeeze (R : realType) (f g h : (\bar R)^nat) : (\forall x \near \oo, f x <= g x <= h x) -> forall (l : \bar R), f @ \oo --> l -> h @ \oo --> l -> g @ \oo --> l. @@ -1758,13 +1751,13 @@ by rewrite gt_eqF// (lt_le_trans _ (u_ge0 _ Pn)). Qed. Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) N : - (forall i, P i -> 0 <= u i) -> + (forall i, (N <= i)%N -> P i -> 0 <= u i) -> (forall n, P n -> u n <= v n) -> \sum_(N <= i u0 Puv; apply: lee_lim. -- by apply: is_cvg_ereal_nneg_natsum_cond => n ? /u0; exact. -- apply: is_cvg_ereal_nneg_natsum_cond => n _ Pn. +- by apply: is_cvg_ereal_nneg_natsum_cond => n Nn /u0; exact. +- apply: is_cvg_ereal_nneg_natsum_cond => n Nn Pn. by rewrite (le_trans _ (Puv _ Pn))// u0. - by near=> n; apply: lee_sum => k; exact: Puv. Unshelve. all: by end_near. Qed. @@ -1777,9 +1770,9 @@ Lemma subset_lee_nneseries (R : realType) (u : (\bar R)^nat) (P Q : pred nat) Proof. move=> Pu PQ; apply: lee_lim. - apply: ereal_nondecreasing_is_cvgn => a b ab. - by apply: lee_sum_nneg_natr => // n Mn /PQ; exact: Pu. + by apply: lee_sum_nneg_natr => // n Mn Pn; apply: Pu => //; exact: PQ. - apply: ereal_nondecreasing_is_cvgn => a b ab. - by apply: lee_sum_nneg_natr => // n Mn; exact: Pu. + by apply: lee_sum_nneg_natr => // n Mn Pn; apply: Pu => //; exact: PQ. - near=> n; apply: lee_sum_nneg_subset => //. by move=> i; rewrite inE => /andP[iP iQ]; exact: Pu. Unshelve. all: by end_near. Qed. @@ -1951,7 +1944,8 @@ have : cvg (\sum_(0 <= k < n | P k) f k @[n --> \oo]). by apply: lee_sum_nneg_natr => n _; exact: f0. move/cvg_ex => [[l fl||/cvg_lim fnoo]] /=; last 2 first. - by move/cvg_lim => fpoo; rewrite fpoo// in foo. - - have : 0 <= \sum_(k n _; exact: f0. by rewrite fnoo. rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). apply/cvgeNP; rewrite oppe0. @@ -1959,38 +1953,42 @@ rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). exact/cvge_sub0. apply/funext => N; apply/esym/eqP; rewrite sube_eq//. by rewrite addeC -nneseries_split_cond//; exact/eqP/esym/cvg_lim. -by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. +rewrite ge0_adde_def//= ?inE; last exact: sume_ge0. +by apply: nneseries_ge0 => n Nn; exact: f0. Qed. -Lemma nneseriesD (R : realType) (f g : nat -> \bar R) (P : pred nat) : - (forall i, P i -> 0 <= f i) -> (forall i, P i -> 0 <= g i) -> - \sum_(i \bar R) (P : pred nat) N : + (forall i, (N <= i)%N -> P i -> 0 <= f i) -> + (forall i, (N <= i)%N -> P i -> 0 <= g i) -> + \sum_(N <= i f_eq0 g_eq0. -transitivity (limn (fun n => \sum_(0 <= i < n | P i) f i + - \sum_(0 <= i < n | P i) g i)). +transitivity (limn (fun n => \sum_(N <= i < n | P i) f i + + \sum_(N <= i < n | P i) g i)). by apply/congr_lim/funext => n; rewrite big_split. rewrite limeD /adde_def //=; do ? exact: is_cvg_nneseries. by rewrite ![_ == -oo]gt_eqF ?andbF// (@lt_le_trans _ _ 0) ?[_ < _]real0// nneseries_ge0. Qed. -Lemma nneseries_sum_nat (R : realType) n (f : nat -> nat -> \bar R) : +Lemma nneseries_sum_nat (R : realType) m n (f : nat -> nat -> \bar R) N : (forall i j, 0 <= f i j) -> - \sum_(j f0; elim: n => [|n IHn]. +move=> f0; elim: n => [|n ih]. by rewrite big_geq// eseries0// => i; rewrite big_geq. -rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0. -by apply/congr_lim/funext => m; apply: eq_bigr => i _; rewrite big_nat_recr. +have [mn|nm] := leqP m n. + rewrite big_nat_recr// -ih/= -nneseriesD//; last by move=> i; rewrite sume_ge0. + by apply/congr_lim/funext => ?; apply: eq_bigr => i _; rewrite big_nat_recr. +by rewrite big_geq// eseries0// => i; rewrite big_geq. Qed. Lemma nneseries_sum I (r : seq I) (P : {pred I}) [R : realType] - [f : I -> nat -> \bar R] : (forall i j, P i -> 0 <= f i j) -> - \sum_(j nat -> \bar R] N : (forall i j, P i -> 0 <= f i j) -> + \sum_(N <= j f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr. by rewrite big_nil eseries0// => i; rewrite big_nil. @@ -2026,12 +2024,6 @@ by move/(lt_le_trans Ml); rewrite ltxx. Unshelve. all: by end_near. Qed. End sequences_ereal. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgeyPge` or a variant instead")] -Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgeNyPle` or a variant instead")] -Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty (only parsing). #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `squeeze_cvge` and generalized")] Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing). @@ -2099,12 +2091,6 @@ Notation ereal_nonincreasing_cvg := ereal_nonincreasing_cvgn (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `ereal_nonincreasing_is_cvgn`")] Notation ereal_nonincreasing_is_cvg := ereal_nonincreasing_is_cvgn (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eseries0 instead.")] -Notation nneseries0 := eseries0 (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eq_eseriesr instead.")] -Notation eq_nneseries := eq_eseriesr (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eseries_pred0 instead.")] -Notation nneseries_pred0 := eseries_pred0 (only parsing). Arguments nneseries_split {R f} _ _.