From 1f6f6303f6f59f581838ba2d6448d0e4ee2a0e14 Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Wed, 29 Jul 2026 19:35:02 +0200 Subject: [PATCH 1/7] Add set of lemmas for esum --- theories/esum.v | 289 ++++++++++++++++++++- theories/measure_theory/measure_function.v | 3 +- 2 files changed, 280 insertions(+), 12 deletions(-) diff --git a/theories/esum.v b/theories/esum.v index dcedd52ddf..007e3e691d 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -155,13 +155,51 @@ Lemma pos_esum_ge (T1 : choiceType) (I : set T1) (a : T1 -> \bar R) x : x <= \esum_(i in I) a i. Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed. -Lemma le_pos_esum S f g : (forall i, S i -> f i <= g i) -> +Lemma pos_neq0_esum (I : set T) (a : T -> \bar R) : + \esum_(i in I) a i <> 0 -> exists i, a i <> 0. +Proof. +move=> ?. apply/existsp_asboolPn /asboolPn => h. +have // : (\esum_(i in I) a i = 0); by apply pos_esum1. +Qed. + +Lemma pos_esum_ge1 (I : set T) (f : T -> \bar R) : + (forall x, I x -> f x <= \esum_(i in (I : set T)) f i)%E. +Proof. +move=> x Ix. +apply: pos_esum_ge. +exists ([set` [::x]]%classic) => //=. ++ by split => // y /=; rewrite mem_seq1 => /eqP ->. +by rewrite -fsbig_seq //= big_seq1. +Qed. + +Lemma pos_sum_esum_ge J (f: T -> R) : + uniq J -> ((\sum_(j <- J) f j)%:E <= \esum_(i in [set: T]) (f i)%:E)%E. +Proof. +move => ?. +apply: pos_esum_ge. +exists [set` J]%classic => //. +rewrite fsumEFin // lee_fin -fsbig_seq //=. +Qed. + +Lemma le_pos_esum {U : choiceType} (S: set U) (f g: U -> \bar R) : + (forall i, S i -> f i <= g i) -> \esum_(i in S) f i <= \esum_(i in S) g i. Proof. move=> fg; rewrite ge_ereal_sup => //= _ [X [finX XS]] <-. by rewrite pos_esum_ge//; exists X => //; apply: lee_fsum => // t /XS /fg. Qed. +Lemma le_pos_esum_fine + {U : choiceType} (A : set U) (B : set T) (f : T -> U -> \bar R) : + (\esum_(i in A) (fine (\esum_(x in B) f x i))%:E <= + \esum_(i in A) (\esum_(x in B) f x i))%E. +Proof. +rewrite le_pos_esum // => i ?. +case h: (\esum_(x in B) _) => //=. ++ exact : leey. +by rewrite -h pos_esum_ge0. +Qed. + Lemma pos_esumZ S f (c : \bar R) : 0 <= c -> (forall t, S t -> 0 <= f t) -> \esum_(t in S) c * f t = c * \esum_(t in S) f t. Proof. @@ -385,18 +423,53 @@ Section esum_realType. Variables (R : realType) (T : choiceType). Implicit Types (S : set T) (f : T -> \bar R). -Lemma le_esum S f g : (forall x, S x -> 0 <= f x) -> +Lemma sum_esum_ge J (f: T -> R) : + (forall x, 0 <= f x)%R -> + uniq J -> ((\sum_(j <- J) f j)%:E <= \esum_(i in [set:T]) (f i)%:E)%E. +Proof. +move=> f0 uJ; rewrite ge0_esum. ++ by move=> x _; rewrite lee_fin; exact: f0. +exact: (PosEsum.pos_sum_esum_ge). +Qed. + +Lemma le_esum S f g : (forall x, S x -> f x <= g x) -> - \esum_(x in S) f x <= \esum_(x in S) g x. + \esum_(i in S) f i <= \esum_(i in S) g i. Proof. -move=> f0 leS; have g0 x : S x -> 0 <= g x. - by move=> /[dup] Ax /leS; apply: le_trans; exact: f0 Ax. -by rewrite !ge0_esum// PosEsum.le_pos_esum. +move=> leS. +have leS' : {in S, forall x, f x <= g x} by move=> x /set_mem; exact: leS. +rewrite /esum; apply: leeB. +- by apply: PosEsum.le_pos_esum => x /mem_set; exact: funepos_le. +- by apply: PosEsum.le_pos_esum => x /mem_set; exact: funeneg_le. Qed. Lemma esum_ge0 S f : (forall x, S x -> 0 <= f x) -> 0 <= \esum_(i in S) f i. Proof. by move=> f0; rewrite ge0_esum// PosEsum.pos_esum_ge0. Qed. +Lemma le_esum_fine {U : choiceType} (A : set U) (B : set T) (f : T -> U -> \bar R) : + (forall x y, 0 <= f x y)%E -> + (\esum_(i in A) (fine (\esum_(x in B) f x i))%:E <= + \esum_(i in A) (\esum_(x in B) f x i))%E. +Proof. +move=> hf. +rewrite [leLHS]ge0_esum. ++ by move=> i _; rewrite lee_fin; apply: fine_ge0; apply esum_ge0. +rewrite [leRHS]ge0_esum; first by move=> i _; apply esum_ge0. +under [leLHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum //. +under [leRHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum //. +exact: PosEsum.le_pos_esum_fine. +Qed. + +Lemma subset_esum (I J : set T) (a : T -> \bar R) : + (forall x, J x -> 0 <= a x) -> + I `<=` J -> (\esum_(i in I) a i <= \esum_(i in J) a i)%E. +Proof. +move=> a0 IJ. +have ?: forall x, I x -> 0 <= a x by move => x /IJ /a0. +rewrite ge0_esum // ge0_esum //. +by apply: PosEsum.subset_pos_esum. +Qed. + Lemma esum_fset S f : finite_set S -> (forall i, S i -> 0 <= f i) -> \esum_(i in S) f i = \sum_(i \in S) f i. Proof. by move=> finF f0; rewrite ge0_esum//; exact: PosEsum.pos_esum_fset. Qed. @@ -410,6 +483,13 @@ move=> Df0; rewrite ge0_esum; last exact: PosEsum.pos_esum1. by move=> i /Df0 ->. Qed. +Lemma esum0 {R : realFieldType} {I : choiceType} (D : set I) : + \esum_(i in D) (@cst I (\bar R) 0 i) = 0. +Proof. +by rewrite esum1 ?subee// => r _; + rewrite ?[LHS](funepos_cst0,funeneg_cst0). +Qed. + Section esum_cond. Context {R : realType} {T : choiceType}. Implicit Types (A B : set T) (f : T -> \bar R). @@ -483,6 +563,10 @@ Lemma esum_ge {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) x : x <= \esum_(i in I) f i. Proof. by move=> f0 If; rewrite ge0_esum// PosEsum.pos_esum_ge. Qed. +Lemma esum_unit {R : realType} {T : choiceType} (f : T -> \bar R) x : + \esum_(i in [set:T]) (if x == i then f i else 0) = f x. +Proof. by rewrite esum_if_eq_op esum_set1. Qed. + Lemma esum_eq0P {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R) : (forall i, A i -> 0 <= f i) -> \esum_(x in A) f x = 0 -> forall x, A x -> f x = 0. @@ -493,6 +577,18 @@ exists [set x]; first by split => // t ->. by rewrite -esum_set1 esum_fset// => i ->; exact: f0. Qed. +Lemma neq0_esum {R : realType} {T : choiceType} (I : set T) (a : T -> \bar R) : + \esum_(i in I) a i <> 0 -> exists i, a i <> 0. +Proof. +move=> ?. apply/existsp_asboolPn /asboolPn => h. +have // : (\esum_(i in I) a i = 0); by apply esum1. +Qed. + +Lemma esum_ge1 {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) : + (forall x, I x -> 0 <= f x) -> + (forall x, I x -> f x <= \esum_(i in (I : set T)) f i)%E. +Proof. by move=> f0 x Ix; rewrite ge0_esum//; exact: PosEsum.pos_esum_ge1. Qed. + Section esumZ. Context {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R). @@ -780,6 +876,22 @@ rewrite /summable fin_numElt; apply/idP/idP => [->|/andP[]//]. by rewrite andbT (lt_le_trans (ltNyr 0))//; exact: esum_ge0. Qed. +Lemma eq_summable D f g : f =1 g -> summable D f -> summable D g. +Proof. +move => eq_fg; rewrite /summable; apply: le_lt_trans. +by apply: le_esum => ?; rewrite eq_fg. +Qed. + +Lemma le_summable D f g : + (forall x, 0 <= f x <= g x) -> summable D g -> summable D f. +Proof. +move => eq_fg; rewrite /summable; apply: le_lt_trans. +apply: le_esum => i //. +have /andP := (eq_fg i). +move =>[ h1 h2]; rewrite !gee0_abs => //=. +by apply /le_trans;first apply h1. +Qed. + Lemma summableD D f g : summable D f -> summable D g -> summable D (f \+ g). Proof. move=> Df Dg; apply: le_lt_trans (lte_add_pinfty Df Dg). @@ -812,6 +924,50 @@ apply: PosEsum.le_pos_esum => t Dt. by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr. Qed. +Lemma summable_muleC D f1 f2 : + summable D (f2 \* f1) -> summable D (f1 \* f2). +Proof. +rewrite /summable => ?. +by under eq_esum do rewrite abseM muleC -abseM. +Qed. + +Lemma summableZ D f c : + c \is a fin_num -> summable D f -> summable D (fun x => c * f x). +Proof. +rewrite /summable => ??. +under eq_esum do rewrite abseM. +by rewrite esumZ // lte_mul_pinfty //= abse_fin_num. +Qed. + +Lemma summableZr D f c : +c \is a fin_num -> summable D f -> summable D (fun x => f x * c). +Proof. by move=> ??; apply/summable_muleC /summableZ. Qed. + +Lemma summableMl D f1 f2 : + (exists2 M, (forall x, D x -> `|f1 x| <= M) & M \is a fin_num) -> + summable D f2 -> summable D (f1 \* f2). +Proof. +move=> [M h1 Mfin] sf2. +rewrite /summable; apply: le_lt_trans (summableZ Mfin sf2). +apply: le_esum => x Dx; rewrite !abseM. +apply: lee_wpmul2r; first exact: abse_ge0. +by apply: le_trans (h1 x Dx) (lee_abs _). +Qed. + +Lemma summableMr D f1 f2 : + (exists2 M, (forall x, D x -> `|f2 x| <= M) & M \is a fin_num ) -> + summable D f1 -> + summable D (f1 \* f2). +Proof. by move => ??; apply/summable_muleC /summableMl. Qed. + +Lemma summableM D f1 f2 : + summable D f1 -> summable D f2 -> summable D (f1 \* f2). +Proof. +rewrite summableE => smS1 smS2; apply/summableMl => //. +exists (\esum_(x in D) `| f1 x|) => //. +by move => x; apply/esum_ge1. +Qed. + End summable_lemmas. Import numFieldNormedType.Exports. @@ -960,6 +1116,121 @@ Qed. End esumB. +Section esum_summable. +Context {R : realType} {T : choiceType}. +Implicit Types (S : T -> \bar R). + +Lemma summable_esum_funepos S : + summable [set: T] S -> \esum_(t in [set: T]) S^\+ t \is a fin_num. +Proof. +move => /summable_funepos. +rewrite summableE. +rewrite (@eq_esum _ _ _ (fun y : T => S^\+ y) (fun y : T => `|S^\+ y|)) //=. +by move => ??; rewrite gee0_abs. +Qed. + +Lemma summable_esum_fin_num S : + summable [set: T] S -> \esum_(i in [set:T]) S i \is a fin_num. +Proof. +move=> sm; rewrite /esum fin_numB; apply/andP; split. +- rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funepos_ge0. + exact: (summable_esum_funepos sm). +- have smN : summable [set: T] (\- S) by rewrite -summableN. + rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funeneg_ge0. + by rewrite -funeposN; exact: (summable_esum_funepos smN). +Qed. + +Lemma summable_esumN S : + summable [set : T] S -> \esum_(i in [set:T]) - S i = - \esum_(i in [set:T]) S i. +Proof. +move=> hs; rewrite /esum funeposN funenegN oppeB. +- apply: fin_num_adde_defr. + rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funepos_ge0. + exact: (summable_esum_funepos hs). +- by rewrite addeC. +Qed. + +Lemma summable_esumZ_pos S : + summable [set : T] S -> + forall d : \bar R, 0 <= d -> d \is a fin_num -> + \esum_(x in [set:T]) d * S x = d * \esum_(x in [set:T]) S x. +Proof. +move=> h d d0 dfin. +have -> : d = (fine d)%:E by rewrite fineK. +have ? : (0 <= fine d)%R by rewrite -lee_fin fineK. +have ? : (0 <= (fine d)%:E) by rewrite fineK. +have ? : (fine d)%:E \is a fin_num by []. +rewrite [in LHS]/esum ge0_funeposM// ge0_funenegM//. +rewrite (PosEsum.pos_esumZ _ (fun t _ => funepos_ge0 S t)) //. +rewrite (PosEsum.pos_esumZ _ (fun t _ => funeneg_ge0 S t)) //. +rewrite -muleBr //. +apply: fin_num_adde_defr. +rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funepos_ge0. +exact: (summable_esum_funepos h). +Qed. + +Lemma summable_esumZ S c : + `|c| \is a fin_num -> summable [set : T] S -> + \esum_(x in [set : T]) c * S x = c * \esum_(x in [set : T]) S x. +Proof. +move=> hf h. +have [c0|c0|->] := comparable_ltgtP (comparableT c 0). +- rewrite (eq_esum _ _ (fun x => - (`|c| * S x))). + + by move=> x _; rewrite lte0_abs// mulNe oppeK. + rewrite (summable_esumN (summableZ hf h)). + rewrite (summable_esumZ_pos h (abse_ge0 c) hf). + by rewrite lte0_abs// mulNe oppeK. +- apply: (summable_esumZ_pos h (ltW c0)). + by rewrite -abse_fin_num. +- rewrite [in RHS]mul0e; under eq_esum do rewrite mul0e. + by rewrite esum0. +Qed. + +Lemma esum_posneg (h : T -> \bar R) : + \esum_(x in [set:T]) h x = + \esum_(x in [set:T]) h^\+ x - \esum_(x in [set:T]) h^\- x. +Proof. +rewrite [in RHS]ge0_esum; first by move=> x _; exact: funepos_ge0. +rewrite [in RHS]ge0_esum; first by move=> x _; exact: funeneg_ge0. +by rewrite /esum. +Qed. + +Lemma summable_esumD S1 S2 : + summable [set: T] S1 -> summable [set: T] S2 -> + \esum_(x in [set : T]) (S1 x + S2 x) = + \esum_(x in [set : T]) S1 x + \esum_(x in [set : T]) S2 x. +Proof. +move=> sm1 sm2. +rewrite -(funeDB S1 S2). +rewrite (esum_posneg ((S1^\+ \+ S2^\+) \- (S1^\- \+ S2^\-))). +rewrite (@esumB _ _ [set:T] (S1^\+ \+ S2^\+) (S1^\- \+ S2^\-) + (summableD (summable_funepos sm1) (summable_funepos sm2)) + (summableD (summable_funeneg sm1) (summable_funeneg sm2)) + (fun i _ => adde_ge0 (funepos_ge0 S1 i) (funepos_ge0 S2 i)) + (fun i _ => adde_ge0 (funeneg_ge0 S1 i) (funeneg_ge0 S2 i))). +rewrite (@esumD _ _ [set:T] (S1^\+) (S2^\+) + (fun i _ => funepos_ge0 S1 i) (fun i _ => funepos_ge0 S2 i)). +rewrite (@esumD _ _ [set:T] (S1^\-) (S2^\-) + (fun i _ => funeneg_ge0 S1 i) (fun i _ => funeneg_ge0 S2 i)). +rewrite [in RHS](esum_posneg S1) [in RHS](esum_posneg S2). +rewrite oppeD. + apply: fin_num_adde_defl. + exact: (summable_esum_fin_num (summable_funeneg sm2)). +by rewrite addeACA. +Qed. + +Lemma summable_esumB {V : choiceType} S1 S2 : + summable [set: T] S1 -> summable [set: T] S2 -> + \esum_(x in [set : T]) (S1 x - S2 x) = + \esum_(x in [set : T]) S1 x - \esum_(x in [set : T]) S2 x. +Proof. +move=> sm1 sm2. +have nS2 : summable [set: T] (\- S2) by rewrite -summableN. +by rewrite (summable_esumD sm1 nS2) (summable_esumN sm2). +Qed. + +End esum_summable. + Section exchange_esum_ereal_sup. Context {R : realType} {T : choiceType} {f : T -> nat -> \bar R}. Hypothesis f_ge0 : forall t n, 0 <= f t n. @@ -970,10 +1241,8 @@ Lemma exchange_esum_ereal_sup (A : set T) : ereal_sup (range (fun n => \esum_(x in A) f x n)). Proof. rewrite ge0_esum. - by move=> x Ax; apply: le_ereal_sup_tmp; exists (f x 0). -under eq_imagel. - move=> B [fin BA]; rewrite fsbig_finite//= ereal_sup_sum//. - over. ++ by move=> x Ax; apply: le_ereal_sup_tmp; exists (f x 0). +under eq_imagel => B [fin BA] do rewrite fsbig_finite//= ereal_sup_sum//. rewrite exchange_ereal_sup; congr ereal_sup; apply: eq_imagel => n _. rewrite ge0_esum//; congr ereal_sup. by apply: eq_imagel => B [finB BA]; rewrite fsbig_finite. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 57526df8eb..e465a7b599 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1212,8 +1212,7 @@ rewrite esum_bigcup//. apply: (@trivIset_seqDU _ B) => //; exists y. by split => //; [exact: YBi|exact: YBj]. rewrite nneseries_esumT//. -apply: le_esum => /=; first by move=> i _; exact: esum_ge0. -move=> // i _. +apply: le_esum => /= i _. rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j). by rewrite esum_fset//; exact: decomp_finite_set. rewrite -SetRing.Rmu_fin_bigcup//=. From 51d76f91bce7246df6b1f6ad331a6795d66abdee Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 5 Aug 2026 12:49:10 +0900 Subject: [PATCH 2/7] review (wip) --- theories/esum.v | 153 ++++++++++++++++++++---------------------------- 1 file changed, 62 insertions(+), 91 deletions(-) diff --git a/theories/esum.v b/theories/esum.v index 007e3e691d..e59a4cf04e 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -123,7 +123,7 @@ Implicit Types (S : set T) (f g : T -> \bar R). Local Notation "\esum_ ( i 'in' P ) A" := (pos_esum P (fun i => A)). Lemma subset_pos_esum (I J : set T) (a : T -> \bar R) : - (I `<=` J)%classic -> (\esum_(i in I) a i <= \esum_(i in J) a i)%E. + I `<=` J -> (\esum_(i in I) a i <= \esum_(i in J) a i)%E. Proof. move=> IJ; apply: ereal_sup_le => _/= [A [finA AI]] <-. by exists A => //; split => //; exact: subset_trans IJ. @@ -155,33 +155,13 @@ Lemma pos_esum_ge (T1 : choiceType) (I : set T1) (a : T1 -> \bar R) x : x <= \esum_(i in I) a i. Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed. -Lemma pos_neq0_esum (I : set T) (a : T -> \bar R) : - \esum_(i in I) a i <> 0 -> exists i, a i <> 0. +Lemma pos_esum_ge1 S f x : S x -> f x <= \esum_(i in S) f i. Proof. -move=> ?. apply/existsp_asboolPn /asboolPn => h. -have // : (\esum_(i in I) a i = 0); by apply pos_esum1. +move=> Sx; apply: pos_esum_ge; exists [set x]; last by rewrite fsbig_set1. +by split => //; rewrite sub1set inE. Qed. -Lemma pos_esum_ge1 (I : set T) (f : T -> \bar R) : - (forall x, I x -> f x <= \esum_(i in (I : set T)) f i)%E. -Proof. -move=> x Ix. -apply: pos_esum_ge. -exists ([set` [::x]]%classic) => //=. -+ by split => // y /=; rewrite mem_seq1 => /eqP ->. -by rewrite -fsbig_seq //= big_seq1. -Qed. - -Lemma pos_sum_esum_ge J (f: T -> R) : - uniq J -> ((\sum_(j <- J) f j)%:E <= \esum_(i in [set: T]) (f i)%:E)%E. -Proof. -move => ?. -apply: pos_esum_ge. -exists [set` J]%classic => //. -rewrite fsumEFin // lee_fin -fsbig_seq //=. -Qed. - -Lemma le_pos_esum {U : choiceType} (S: set U) (f g: U -> \bar R) : +Lemma le_pos_esum {U : choiceType} (S : set U) (f g : U -> \bar R) : (forall i, S i -> f i <= g i) -> \esum_(i in S) f i <= \esum_(i in S) g i. Proof. @@ -189,15 +169,14 @@ move=> fg; rewrite ge_ereal_sup => //= _ [X [finX XS]] <-. by rewrite pos_esum_ge//; exists X => //; apply: lee_fsum => // t /XS /fg. Qed. -Lemma le_pos_esum_fine - {U : choiceType} (A : set U) (B : set T) (f : T -> U -> \bar R) : - (\esum_(i in A) (fine (\esum_(x in B) f x i))%:E <= - \esum_(i in A) (\esum_(x in B) f x i))%E. +Lemma le_pos_esum_fine {U : choiceType} (A : set U) (B : set T) + (h : T -> U -> \bar R) : + (\esum_(i in A) (fine (\esum_(x in B) h x i))%:E <= + \esum_(i in A) (\esum_(x in B) h x i))%E. Proof. -rewrite le_pos_esum // => i ?. -case h: (\esum_(x in B) _) => //=. -+ exact : leey. -by rewrite -h pos_esum_ge0. +rewrite le_pos_esum // => u Au. +have := pos_esum_ge0 B (h ^~ u). +by case: (\esum_(x in B) _). Qed. Lemma pos_esumZ S f (c : \bar R) : 0 <= c -> (forall t, S t -> 0 <= f t) -> @@ -420,20 +399,19 @@ Arguments eq_esum {R T} S f g. Notation "\esum_ ( i 'in' P ) F" := (esum P (fun i => F)) : ring_scope. Section esum_realType. -Variables (R : realType) (T : choiceType). +Context {R : realType} {T : choiceType}. Implicit Types (S : set T) (f : T -> \bar R). -Lemma sum_esum_ge J (f: T -> R) : - (forall x, 0 <= f x)%R -> - uniq J -> ((\sum_(j <- J) f j)%:E <= \esum_(i in [set:T]) (f i)%:E)%E. +Lemma sum_esum_ge s (h : T -> R) : uniq s -> + (forall x, 0 <= h x)%R -> + (\sum_(j <- s) h j)%:E <= \esum_(i in [set: T]) (h i)%:E. Proof. -move=> f0 uJ; rewrite ge0_esum. -+ by move=> x _; rewrite lee_fin; exact: f0. -exact: (PosEsum.pos_sum_esum_ge). +move=> us f0; rewrite ge0_esum; first by move=> t _; rewrite lee_fin f0. +apply: PosEsum.pos_esum_ge; exists [set` s] => //. +by rewrite fsumEFin// fsbig_seq. Qed. -Lemma le_esum S f g : - (forall x, S x -> f x <= g x) -> +Lemma le_esum S f g : (forall x, S x -> f x <= g x) -> \esum_(i in S) f i <= \esum_(i in S) g i. Proof. move=> leS. @@ -446,28 +424,26 @@ Qed. Lemma esum_ge0 S f : (forall x, S x -> 0 <= f x) -> 0 <= \esum_(i in S) f i. Proof. by move=> f0; rewrite ge0_esum// PosEsum.pos_esum_ge0. Qed. -Lemma le_esum_fine {U : choiceType} (A : set U) (B : set T) (f : T -> U -> \bar R) : - (forall x y, 0 <= f x y)%E -> - (\esum_(i in A) (fine (\esum_(x in B) f x i))%:E <= - \esum_(i in A) (\esum_(x in B) f x i))%E. +Lemma le_esum_fine {U : choiceType} (A : set U) (B : set T) + (f : T -> U -> \bar R) : (forall x y, 0 <= f x y) -> + \esum_(i in A) (fine (\esum_(x in B) f x i))%:E <= + \esum_(i in A) (\esum_(x in B) f x i). Proof. move=> hf. rewrite [leLHS]ge0_esum. -+ by move=> i _; rewrite lee_fin; apply: fine_ge0; apply esum_ge0. + by move=> i _; rewrite lee_fin; apply: fine_ge0; apply esum_ge0. rewrite [leRHS]ge0_esum; first by move=> i _; apply esum_ge0. -under [leLHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum //. -under [leRHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum //. +under [leLHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum//. +under [leRHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum//. exact: PosEsum.le_pos_esum_fine. Qed. -Lemma subset_esum (I J : set T) (a : T -> \bar R) : - (forall x, J x -> 0 <= a x) -> - I `<=` J -> (\esum_(i in I) a i <= \esum_(i in J) a i)%E. +Lemma subset_esum (I J : set T) f : (forall x, J x -> 0 <= f x) -> + I `<=` J -> \esum_(i in I) f i <= \esum_(i in J) f i. Proof. -move=> a0 IJ. -have ?: forall x, I x -> 0 <= a x by move => x /IJ /a0. -rewrite ge0_esum // ge0_esum //. -by apply: PosEsum.subset_pos_esum. +move=> f0 IJ. +have I0f : forall x, I x -> 0 <= f x by move => x /IJ /f0. +by rewrite !ge0_esum// PosEsum.subset_pos_esum. Qed. Lemma esum_fset S f : finite_set S -> (forall i, S i -> 0 <= f i) -> @@ -484,11 +460,8 @@ by move=> i /Df0 ->. Qed. Lemma esum0 {R : realFieldType} {I : choiceType} (D : set I) : - \esum_(i in D) (@cst I (\bar R) 0 i) = 0. -Proof. -by rewrite esum1 ?subee// => r _; - rewrite ?[LHS](funepos_cst0,funeneg_cst0). -Qed. + \esum_(i in D) @cst _ (\bar R) 0 i = 0. +Proof. by rewrite esum1. Qed. Section esum_cond. Context {R : realType} {T : choiceType}. @@ -564,7 +537,7 @@ Lemma esum_ge {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) x : Proof. by move=> f0 If; rewrite ge0_esum// PosEsum.pos_esum_ge. Qed. Lemma esum_unit {R : realType} {T : choiceType} (f : T -> \bar R) x : - \esum_(i in [set:T]) (if x == i then f i else 0) = f x. + \esum_(i in [set: T]) (if x == i then f i else 0) = f x. Proof. by rewrite esum_if_eq_op esum_set1. Qed. Lemma esum_eq0P {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R) : @@ -577,16 +550,16 @@ exists [set x]; first by split => // t ->. by rewrite -esum_set1 esum_fset// => i ->; exact: f0. Qed. -Lemma neq0_esum {R : realType} {T : choiceType} (I : set T) (a : T -> \bar R) : - \esum_(i in I) a i <> 0 -> exists i, a i <> 0. +Lemma esum_neq0 {R : realType} {T : choiceType} (I : set T) (a : T -> \bar R) : + \esum_(i in I) a i != 0 -> exists2 i, i \in I & a i != 0. Proof. -move=> ?. apply/existsp_asboolPn /asboolPn => h. -have // : (\esum_(i in I) a i = 0); by apply esum1. +apply: contra_neqP => /forall2NP a0; apply: esum1 => t /mem_set It. +by have [|/negP/negPn/eqP//] := a0 t; rewrite It. Qed. Lemma esum_ge1 {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) : (forall x, I x -> 0 <= f x) -> - (forall x, I x -> f x <= \esum_(i in (I : set T)) f i)%E. + forall x, I x -> f x <= \esum_(i in I) f i. Proof. by move=> f0 x Ix; rewrite ge0_esum//; exact: PosEsum.pos_esum_ge1. Qed. Section esumZ. @@ -879,17 +852,15 @@ Qed. Lemma eq_summable D f g : f =1 g -> summable D f -> summable D g. Proof. move => eq_fg; rewrite /summable; apply: le_lt_trans. -by apply: le_esum => ?; rewrite eq_fg. +by apply: le_esum => ?; rewrite eq_fg. Qed. Lemma le_summable D f g : (forall x, 0 <= f x <= g x) -> summable D g -> summable D f. Proof. -move => eq_fg; rewrite /summable; apply: le_lt_trans. -apply: le_esum => i //. -have /andP := (eq_fg i). -move =>[ h1 h2]; rewrite !gee0_abs => //=. -by apply /le_trans;first apply h1. +move=> fg; rewrite /summable; apply: le_lt_trans. +apply: le_esum => t Dt; have/andP[f0 {}fg] := fg t. +by rewrite !gee0_abs// (le_trans f0). Qed. Lemma summableD D f g : summable D f -> summable D g -> summable D (f \+ g). @@ -924,25 +895,21 @@ apply: PosEsum.le_pos_esum => t Dt. by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr. Qed. -Lemma summable_muleC D f1 f2 : - summable D (f2 \* f1) -> summable D (f1 \* f2). +Lemma summableZ D f c : c \is a fin_num -> + summable D f -> summable D (fun x => c * f x). Proof. -rewrite /summable => ?. -by under eq_esum do rewrite abseM muleC -abseM. +rewrite /summable => cfun fy. +under eq_esum do rewrite abseM. +by rewrite esumZ// lte_mul_pinfty// abse_fin_num. Qed. -Lemma summableZ D f c : - c \is a fin_num -> summable D f -> summable D (fun x => c * f x). +Lemma summableZr D f c : c \is a fin_num -> + summable D f -> summable D (fun x => f x * c). Proof. -rewrite /summable => ??. -under eq_esum do rewrite abseM. -by rewrite esumZ // lte_mul_pinfty //= abse_fin_num. +under eq_fun do rewrite muleC. +exact: summableZ. Qed. -Lemma summableZr D f c : -c \is a fin_num -> summable D f -> summable D (fun x => f x * c). -Proof. by move=> ??; apply/summable_muleC /summableZ. Qed. - Lemma summableMl D f1 f2 : (exists2 M, (forall x, D x -> `|f1 x| <= M) & M \is a fin_num) -> summable D f2 -> summable D (f1 \* f2). @@ -955,17 +922,21 @@ by apply: le_trans (h1 x Dx) (lee_abs _). Qed. Lemma summableMr D f1 f2 : - (exists2 M, (forall x, D x -> `|f2 x| <= M) & M \is a fin_num ) -> + (exists2 M, (forall x, D x -> `|f2 x| <= M) & M \is a fin_num) -> summable D f1 -> summable D (f1 \* f2). -Proof. by move => ??; apply/summable_muleC /summableMl. Qed. +Proof. +move=> Df2. +under eq_fun do rewrite muleC. +exact: summableMl. +Qed. Lemma summableM D f1 f2 : summable D f1 -> summable D f2 -> summable D (f1 \* f2). Proof. rewrite summableE => smS1 smS2; apply/summableMl => //. -exists (\esum_(x in D) `| f1 x|) => //. -by move => x; apply/esum_ge1. +exists (\esum_(x in D) `|f1 x|) => //. +exact: esum_ge1. Qed. End summable_lemmas. @@ -1118,7 +1089,7 @@ End esumB. Section esum_summable. Context {R : realType} {T : choiceType}. -Implicit Types (S : T -> \bar R). +Implicit Types (S : T -> \bar R). Lemma summable_esum_funepos S : summable [set: T] S -> \esum_(t in [set: T]) S^\+ t \is a fin_num. From 4a5ebddc1b4467826ad8a0b50f8963b527eff166 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 9 Aug 2026 18:12:16 +0900 Subject: [PATCH 3/7] esum/summable -> esummable, simplifications --- CHANGELOG_UNRELEASED.md | 31 ++ experimental_reals/distr.v | 9 +- experimental_reals/realsum.v | 141 +++--- theories/esum.v | 403 +++++++++--------- .../lebesgue_integrable.v | 42 +- .../lebesgue_integral_nonneg.v | 10 +- 6 files changed, 316 insertions(+), 320 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4ee12401e3..1215ecd979 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,6 +20,13 @@ - in `num_topology.v`: + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, `at_left_shift`, `at_right_shift` +- in `esum.v`: + + lemmas `eq_esummable`, `le_esummable`, `esummableZl`, `esummableZr`, + `esummableMl`, `esummableMr`, `esummableM` + + lemmas `esummable_esum_funepos`, `esummable_esum_funeneg`, + `esummable_esum_fin_num`, `esummable_esumN` + + lemma `esumE` + + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB` ### Changed @@ -31,8 +38,32 @@ ### Renamed +- in `esum.v`: + + `summable` -> `esummable` + + `summable_pinfty` -> `esummable_pinfty` + + `summableE` -> `esummableE` + + `summableD` -> `esummableD` + + `summableN` -> `esummableN` + + `summableB` -> `esummableB` + + `summable_funepos` -> `esummable_funepos` + + `summable_funeneg` -> `esummable_funeneg` + + `summable_fine_sum` -> `esummable_fine_sum` + + `summable_cvg` -> `esummable_cvg` + + `summable_nneseries_lim` -> `esummable_nneseries_lim` + + `summable_eseries` -> `esummable_eseries` + + `summable_eseries_esum` -> `esummable_eseries_esum` + +- in `lebesgue_integrable.v`: + + `integrable_summable` -> `integrable_esummable` + +- in `lebesgue_integral_nonneg.v`: + + `summable_integral_dirac` -> `esummable_integral_dirac` + ### Generalized +- in `esum.v`: + + lemmma `le_esum` + ### Deprecated ### Removed diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 7283768349..9a77ce3ac5 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -362,7 +362,7 @@ Lemma isd_mlet : isdistr mlet. Proof. split=> [x|J uqJ]; first by apply/ge0_psum. rewrite /mlet psum_bigop; first by move=> y x; rewrite mulr_ge0. - move=> u; apply/(le_summable (F2 := mu)) => //. + move=> u; apply/(le_summable (g := mu)) => //. by move=> x; rewrite mulr_ge0 //= ler_piMr ?le1_mu1. apply/(le_trans _ (le1_mu mu))/le_psum => //. move=> x; rewrite sumr_ge0 /= => [y _|]; first by rewrite mulr_ge0. @@ -495,10 +495,11 @@ Lemma eq0_dlet (mu : {distr T / R}) (F : T -> {distr U / R}) y : Proof. unlock dlet; rewrite /= /mlet => /eq0_psum h x /dinsuppP /eqP mu_x. have {}/h: summable (fun x => mu x * F x y). - apply/(le_summable (F2 := mu)) => // z. + apply/(le_summable (g := mu)) => // z. by rewrite mulr_ge0 //= ler_piMr // le1_mu1. by move/(_ x)/eqP; rewrite mulf_eq0 (negbTE mu_x) /= => /eqP. Qed. + End BindTheory. (* -------------------------------------------------------------------- *) @@ -515,7 +516,7 @@ rewrite (eq_psum (F2 := fun y => PosSum.psum (S^~ y))) => [x|]. by rewrite -psumZ //; apply/eq_psum => y /=. rewrite interchange_psum. + by move=> x; apply/summableZ/summable_mlet. -+ rewrite {}/S; apply/(le_summable (F2 := mu)) => //. ++ rewrite {}/S; apply/(le_summable (g := mu)) => //. move=> x; rewrite ge0_psum /= psumZ ?ler_piMr //. apply/(le_trans _ (le1_mu (f1 x)))/le_psum => //. by move=> y; rewrite mulr_ge0 //= ler_piMr ?le1_mu1. @@ -855,7 +856,7 @@ Implicit Types (mu : {distr T / R}) (A B E : pred T). Lemma summable_pr E mu : summable (fun x => (E x)%:R * mu x). Proof. -apply/(le_summable (F2 := mu)) => [x|]; last by apply/summable_mu. +apply/(le_summable (g := mu)) => [x|]; last by apply/summable_mu. by rewrite mulr_ge0 ?ler0n //= ler_piMl // lern1 leq_b1. Qed. diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v index 83ccb3421a..80b7b2e90c 100644 --- a/experimental_reals/realsum.v +++ b/experimental_reals/realsum.v @@ -29,7 +29,7 @@ Local Notation simpm := Monoid.simpm. (* -------------------------------------------------------------------- *) Section Summable. -Variables (T : choiceType) (R : realType) (f : T -> R). +Context {T : choiceType} {R : realType} (f : T -> R). Definition summable := exists (M : R), forall (J : {fset T}), \sum_(x : J) `|f (val x)| <= M. @@ -44,8 +44,8 @@ Qed. End Summable. -Lemma esum_summableP (T : choiceType) (R : realType) (f : T -> R) : - summable f <-> esum.summable [set: T] (EFin \o f). +Lemma esum_summableP {T : choiceType} {R : realType} (f : T -> R) : + summable f <-> esummable [set: T] (EFin \o f). Proof. have fsbigsum (B : {fset T}) : (\sum_(x \in [set` B]) `|f x|%:E)%R = (\sum_(x : B) `|f (\val x)|)%:E. @@ -53,15 +53,14 @@ have fsbigsum (B : {fset T}) : by rewrite sumEFin big_seq_fsetE/= (eq_bigl xpredT)// => x; apply/mem_set => /=. split. move=> [M fM]. - rewrite /esum.summable. - rewrite ge0_esum// (@le_lt_trans _ _ M%:E) ?ltey//. + rewrite /esummable ge0_esum// (@le_lt_trans _ _ M%:E) ?ltey//. apply/ereal_supP => _/= [A [/finite_fsetP[B AB] _] <-]. by rewrite AB fsbigsum; exact: fM. -rewrite /summable => H. +rewrite /summable => sf. exists (fine (\esum_(x in [set: T]) `|(EFin \o f) x|))%E => J/=. rewrite -lee_fin -fsbigsum fineK. by rewrite ge0_fin_numE// esum_ge0. -by rewrite -esum_fset// !ge0_esum//; apply: PosEsum.subset_pos_esum. +by rewrite -esum_fset// !ge0_esum//; exact: PosEsum.subset_pos_esum. Qed. Module PosSum. @@ -80,7 +79,7 @@ Definition sum {R : realType} {T : choiceType} (f : T -> R) : R := (* -------------------------------------------------------------------- *) Section SummableCountable. -Variable (T : choiceType) (R : realType) (f : T -> R). +Context {T : choiceType} {R : realType} (f : T -> R). Lemma summable_countn0 : summable f -> discrete.countable [pred x | f x != 0]. Proof. @@ -166,8 +165,7 @@ by move/ubP : (sup_upper_bound hs); apply; exists J. Qed. Lemma psum_sup_seq S : PosSum.psum S = - sup [set x | exists2 J : seq T, - uniq J & x = \sum_(x <- J) `|S x| ]%classic. + sup [set x | exists2 J : seq T, uniq J & x = \sum_(x <- J) `|S x| ]%classic. Proof. rewrite psum_sup; congr sup; rewrite predeqE => x; split. case=> J ->; exists (enum_fset J). @@ -177,12 +175,10 @@ case=> J uqJ ->; exists [fset x in J]. by rewrite (big_seq_fset \`|_|). Qed. -Lemma eq_summable (S1 S2 : T -> R) : - (S1 =1 S2) -> summable S1 -> summable S2. +Lemma eq_summable (f g : T -> R) : f =1 g -> summable f -> summable g. Proof. -move=> eq_12 [M h]; exists M => J; rewrite (le_trans _ (h J)) //. -rewrite le_eqVlt; apply/orP; left; apply/eqP/eq_bigr. -by move=> /= K _; rewrite eq_12. +move=> fg /esum_summableP sf; apply/esum_summableP. +by apply: eq_esummable sf => x _; rewrite /= fg. Qed. Lemma eq_summableb (S1 S2 : T -> R) : @@ -212,12 +208,11 @@ move=> eq_fg; rewrite /sum; congr (_ - _); apply/eq_psum. - exact/eq_funrneg. Qed. -Lemma le_summable (F1 F2 : T -> R) : - (forall x, 0 <= F1 x <= F2 x) -> summable F2 -> summable F1. +Lemma le_summable (f g : T -> R) : + (forall x, 0 <= f x <= g x) -> summable g -> summable f. Proof. -move=> le_F [M leM]; exists M => J; apply/(le_trans _ (leM J)). -apply/ler_sum => /= j _; case/andP: (le_F (val j)) => h1 h2. -by rewrite !ger0_norm // (le_trans h1 h2). +move=> fg /esum_summableP => sg; apply/esum_summableP. +by apply: le_esummable sg => t _; rewrite /= !lee_fin fg. Qed. Lemma le_psum (F1 F2 : T -> R) : @@ -355,9 +350,7 @@ End FinSumTh. (* -------------------------------------------------------------------- *) Section PSumGe. -Context {R : realType} (T : choiceType). - -Variable (S : T -> R). +Context {R : realType} (T : choiceType) (S : T -> R). Lemma ger_big_psum r : uniq r -> summable S -> \sum_(x <- r) `|S x| <= PosSum.psum S. @@ -386,9 +379,7 @@ End PSumGe. (* -------------------------------------------------------------------- *) Section PSumNatGe. -Context {R : realType}. - -Variable (S : nat -> R) (smS : summable S). +Context {R : realType} (S : nat -> R) (smS : summable S). Lemma ger_big_ord_psum n : \sum_(i < n) `|S i| <= PosSum.psum S. Proof. @@ -400,9 +391,7 @@ End PSumNatGe. (* -------------------------------------------------------------------- *) Section PSumCnv. -Context {R : realType}. - -Variable (S : nat -> R). +Context {R : realType} (S : nat -> R). Hypothesis ge0_S : (forall n, 0 <= S n). Hypothesis smS : summable S. @@ -453,16 +442,15 @@ End PSumCnv. (* -------------------------------------------------------------------- *) Section PSumAsLim. -Context {R : realType} {T : choiceType}. - -Variable (S : T -> R) (P : nat -> {fset T}). +Context {R : realType} {T : choiceType} (S : T -> R) (P : nat -> {fset T}). Hypothesis ge0_S : (forall x, 0 <= S x). Hypothesis smS : summable S. Hypothesis homo_P : forall n m, (n <= m)%N -> (P n `<=` P m). Hypothesis cover_P : forall x, S x != 0 -> exists n, x \in P n. -Lemma psum_as_lim : PosSum.psum S = fine (nlim (fun n => \sum_(j : P n) (S (val j)))). +Lemma psum_as_lim : + PosSum.psum S = fine (nlim (fun n => \sum_(j : P n) (S (val j)))). Proof. set v := fun n => _; have hm_v m n: (m <= n)%N -> v m <= v n. by move=> le_mn; apply/big_fset_subset/fsubsetP/homo_P. @@ -523,23 +511,18 @@ Qed. Lemma summable0 : summable (fun _ : T => 0 : R). Proof. by exists 0 => J; rewrite big1 ?normr0. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableD (S1 S2 : T -> R) : - summable S1 -> summable S2 -> summable (S1 \+ S2). +Lemma summableD (f g : T -> R) : summable f -> summable g -> summable (f \+ g). Proof. -case=> [M1 h1] [M2 h2]; exists (M1 + M2) => J /=. -pose M := \sum_(x : J) (`|S1 (val x)| + `|S2 (val x)|). -rewrite (@le_trans _ _ M) // ?ler_sum // => [K _|]. - by rewrite ler_normD. -by rewrite /M big_split lerD ?(h1, h2). +move=> sf sg; apply/esum_summableP. +rewrite [X in esummable _ X](_ : _ = (EFin \o f) \+ (EFin \o g))%E//. +by apply/esummableD; exact/esum_summableP. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableN (S : T -> R) : summable S -> summable (- S). +Lemma summableN (f : T -> R) : summable f -> summable (- f). Proof. -case=> [M h]; exists M => J; rewrite (le_trans _ (h J)) //. -rewrite le_eqVlt; apply/orP; left; apply/eqP/eq_bigr. -by move=> /= K _; rewrite normrN. +move=> sf; apply/esum_summableP. +rewrite [X in esummable _ X](_ : _ = \- (EFin \o f))%E//. +by rewrite -esummableN; exact/esum_summableP. Qed. (* -------------------------------------------------------------------- *) @@ -568,47 +551,40 @@ move=> sm1; rewrite (@eq_summableb _ _ (S2 \+ S1)) ?summablebDl //. by move=> x /=; rewrite addrC. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableZ (S : T -> R) c : summable S -> summable (c \*o S). +Lemma summableZ (f : T -> R) c : summable f -> summable (c \*o f). Proof. -case=> [M h]; exists (`|c| * M) => J; move/(_ J): h => /=. -move/(ler_wpM2l (normr_ge0 c)); rewrite mulr_sumr. -move/(le_trans _); apply; rewrite le_eqVlt; apply/orP. -by left; apply/eqP/eq_bigr=> j _; rewrite normrM. +move/esum_summableP => sf; apply/esum_summableP. +rewrite [X in esummable _ X](_ : _ = (fun x => c%:E * (f x)%:E)%E)//. +exact: esummableZl. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableZr (S : T -> R) (c : R) : - summable S -> summable (c \o* S). -Proof. by move=> smS; apply/summable_mulrC/summableZ. Qed. +Lemma summableZr (f : T -> R) (c : R) : summable f -> summable (c \o* f). +Proof. by move=> smS; exact/summable_mulrC/summableZ. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableMl (S1 S2 : T -> R) : - (exists M, forall x, `|S1 x| <= M) -> summable S2 -> summable (S1 \* S2). +Lemma summableMl (f g : T -> R) : + (exists M, forall x, `|f x| <= M) -> summable g -> summable (f \* g). Proof. -case=> M leM smS2; apply/summable_abs. -apply/(le_summable (F2 := M \*o \`|S2|)). -+ by move=> x /=; rewrite normr_ge0 /= normrM ler_wpM2r. -+ by apply/summableZ/summable_abs. +case=> M leM smg; apply/summable_abs. +apply/(le_summable (g := M \*o \`|g|)). +- by move=> x /=; rewrite normr_ge0 /= normrM ler_wpM2r. +- by apply/summableZ/summable_abs. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableMr (S1 S2 : T -> R) : - (exists M, forall x, `|S2 x| <= M) -> summable S1 -> summable (S1 \* S2). -Proof. by move=> bd sm; apply/summable_mulrC/summableMl. Qed. +Lemma summableMr (f g : T -> R) : + (exists M, forall x, `|g x| <= M) -> summable f -> summable (f \* g). +Proof. by move=> bd sm; exact/summable_mulrC/summableMl. Qed. -(* -------------------------------------------------------------------- *) -Lemma summableM (S1 S2 : T -> R) : - summable S1 -> summable S2 -> summable (S1 \* S2). +Lemma summableM (f g : T -> R) : summable f -> summable g -> summable (f \* g). Proof. -move=> smS1 smS2; apply/summableMl => //; exists (PosSum.psum S1). -by move=> x; apply/ger1_psum. +move=> sf sg; apply/esum_summableP. +rewrite [X in esummable _ X](_ : _ = (EFin \o f) \* (EFin \o g))%E//. +by apply/esummableM; exact/esum_summableP. Qed. Lemma summable_funrpos (f : T -> R) : summable f -> summable f^\+. Proof. -move/summable_abs; apply/le_summable => x. -by rewrite funrpos_ge0 le_funrpos_norm. +move=> sf; apply/esum_summableP; rewrite -funerpos. +exact/esummable_funepos/esum_summableP. Qed. Lemma summable_funrneg (f : T -> R) : summable f -> summable f^\-. @@ -650,13 +626,13 @@ Qed. (* -------------------------------------------------------------------- *) Lemma summable_sum (F : I -> T -> R) (P : pred I) r : - (forall i, P i -> summable (F i)) - -> summable (fun x => \sum_(i <- r | P i) F i x). + (forall i, P i -> summable (F i)) -> + summable (fun x => \sum_(i <- r | P i) F i x). Proof. move=> sm_F; elim: r => [|i r ih]. by apply/(eq_summable _ summable0) => x; rewrite big_nil. pose G x := (F i x) * (P i)%:R + \sum_(i <- r | P i) F i x. -apply/(eq_summable (S1 := G)) => [x|]. +apply/(eq_summable (f := G)) => [x|]. by rewrite {}/G big_cons; case: ifP=> Pi; rewrite !Monoid.simpm. apply/summableD => //; case/boolP: (P i) => [|_]. by move/sm_F; apply/eq_summable => x; rewrite mulr1. @@ -668,13 +644,10 @@ End SummableAlg. Lemma esum_sum {T : choiceType} {R : realType} (f : T -> R) : summable f -> \esum_(x in [set: T]) (f x)%:E = (sum f)%:E. Proof. -move=> hs; rewrite /esum; rewrite EFinB; congr (_ - _)%E. -- rewrite -esum_psum//; first exact: summable_funrpos. - rewrite ge0_esum/=; first by move=> x _; rewrite lee_fin. - by apply: PosEsum.eq_pos_esum => x _; rewrite funerpos. -- rewrite -esum_psum//; first exact: summable_funrneg. - rewrite ge0_esum/=; first by move=> x _; rewrite lee_fin. - by apply: PosEsum.eq_pos_esum => x _; rewrite funerneg. +move=> fs; rewrite esumE /sum EFinB. +rewrite -esum_psum//; first exact: summable_funrpos. +rewrite -esum_psum//; first exact: summable_funrneg. +by rewrite funerpos funerneg. Qed. (* -------------------------------------------------------------------- *) diff --git a/theories/esum.v b/theories/esum.v index e59a4cf04e..a393a2eed5 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -19,7 +19,7 @@ From mathcomp Require Import topology sequences normedtype numfun. (* function whose codomain is included in the extended *) (* reals; it is 0 if I = set0 and sup(\sum_A a) where A *) (* is a finite set included in I o.w. *) -(* summable D f := \esum_(x in D) `| f x | < +oo *) +(* esummable D f := \esum_(x in D) `| f x | < +oo *) (* ``` *) (* *) (******************************************************************************) @@ -38,7 +38,7 @@ Local Open Scope ring_scope. Local Open Scope ereal_scope. Section set_of_fset_in_a_set. -Variable (T : choiceType). +Context {T : choiceType}. Implicit Type S : set T. Definition fsets S : set_system T := [set F | finite_set F /\ F `<=` S]. @@ -64,7 +64,7 @@ End set_of_fset_in_a_set. define a generic `esum` below, which should be preferred *) Module PosEsum. Section posesum. -Variables (R : realFieldType) (T : choiceType). +Context {R : realFieldType} {T : choiceType}. Implicit Types (S : set T) (f g : T -> \bar R). Definition pos_esum S g := ereal_sup [set \sum_(x \in B) g x | B in fsets S]. @@ -117,7 +117,7 @@ End posesum. Arguments eq_pos_esum {R T} S f g. Section posesum_realType. -Variables (R : realType) (T : choiceType). +Context {R : realType} {T : choiceType}. Implicit Types (S : set T) (f g : T -> \bar R). Local Notation "\esum_ ( i 'in' P ) A" := (pos_esum P (fun i => A)). @@ -356,51 +356,57 @@ Arguments reindex_pos_esum {R T1 T2} P Q e a. End PosEsum. Section esum. -Variables (R : realFieldType) (T : choiceType). -Implicit Types (S : set T) (f g : T -> \bar R). +Context {R : realFieldType} {T : choiceType}. +Implicit Types (A : set T) (f g : T -> \bar R). -Definition esum S f := PosEsum.pos_esum S f^\+ - PosEsum.pos_esum S f^\-. +Definition esum A f := PosEsum.pos_esum A f^\+ - PosEsum.pos_esum A f^\-. Local Notation "\esum_ ( i 'in' P ) A" := (esum P (fun i => A)). -Lemma eq_esum S f g : (forall i, S i -> f i = g i) -> - \esum_(i in S) f i = \esum_(i in S) g i. +Lemma ge0_esum A f : (forall x, A x -> 0 <= f x) -> + \esum_(i in A) f i = ereal_sup [set \sum_(x \in B) f x | B in fsets A]. Proof. -by move=> e; congr (_ - _); apply: PosEsum.eq_pos_esum => i /set_mem/e fgi; - rewrite !(funeposE,funenegE) fgi. +move=> ?; rewrite /esum PosEsum.ge0_pos_esum_funepos//. +by rewrite PosEsum.ge0_pos_esum_funeneg// sube0. Qed. -Lemma ge0_esum S f : (forall x, S x -> 0 <= f x) -> - \esum_(i in S) f i = ereal_sup [set \sum_(x \in B) f x | B in fsets S]. +Lemma esumE A f : + \esum_(x in A) f x = \esum_(x in A) f^\+ x - \esum_(x in A) f^\- x. Proof. -move=> ?. -rewrite /esum PosEsum.ge0_pos_esum_funepos// PosEsum.ge0_pos_esum_funeneg//. -by rewrite sube0. +rewrite [in RHS]ge0_esum; first by move=> x _; exact: funepos_ge0. +by rewrite [in RHS]ge0_esum. +Qed. + +Lemma eq_esum A f g : (forall i, A i -> f i = g i) -> + \esum_(i in A) f i = \esum_(i in A) g i. +Proof. +by move=> e; congr (_ - _); apply: PosEsum.eq_pos_esum => i /set_mem/e fgi; + rewrite !(funeposE,funenegE) fgi. Qed. Lemma esum_set0 f : \esum_(i in set0) f i = 0. Proof. by rewrite /esum !PosEsum.pos_esum_set0 subee. Qed. -Lemma esumN S f : (forall x, S x -> 0 <= f x) -> - \esum_(x in S) - f x = - \esum_(i in S) f i. +Lemma esumN A f : (forall x, A x -> 0 <= f x) -> + \esum_(x in A) - f x = - \esum_(i in A) f i. Proof. move=> f0. rewrite [in RHS]ge0_esum// [LHS]/esum [X in X - _ = _]PosEsum.pos_esum1 ?add0r. - by move=> t /mem_set At; rewrite funeposN (@ge0_funenegE _ _ S). + by move=> t /mem_set At; rewrite funeposN (@ge0_funenegE _ _ A). rewrite /PosEsum.pos_esum; congr (- ereal_sup _). -apply: eq_imagel => B SB; apply: eq_fsbigr => x xB. +apply: eq_imagel => B AB; apply: eq_fsbigr => x xB. rewrite funenegN (@ge0_funeposE _ _ B)// => y By; apply: f0. -by case: SB => _; exact. +by case: AB => _; exact. Qed. End esum. -Arguments eq_esum {R T} S f g. +Arguments eq_esum {R T} A f g. Notation "\esum_ ( i 'in' P ) F" := (esum P (fun i => F)) : ring_scope. Section esum_realType. Context {R : realType} {T : choiceType}. -Implicit Types (S : set T) (f : T -> \bar R). +Implicit Types (D : set T) (f : T -> \bar R). Lemma sum_esum_ge s (h : T -> R) : uniq s -> (forall x, 0 <= h x)%R -> @@ -411,17 +417,17 @@ apply: PosEsum.pos_esum_ge; exists [set` s] => //. by rewrite fsumEFin// fsbig_seq. Qed. -Lemma le_esum S f g : (forall x, S x -> f x <= g x) -> - \esum_(i in S) f i <= \esum_(i in S) g i. +Lemma le_esum D f g : (forall x, D x -> f x <= g x) -> + \esum_(i in D) f i <= \esum_(i in D) g i. Proof. -move=> leS. -have leS' : {in S, forall x, f x <= g x} by move=> x /set_mem; exact: leS. -rewrite /esum; apply: leeB. +move=> leD. +have {}leD : {in D, forall x, f x <= g x} by move=> x /set_mem; exact: leD. +rewrite /esum leeB//. - by apply: PosEsum.le_pos_esum => x /mem_set; exact: funepos_le. - by apply: PosEsum.le_pos_esum => x /mem_set; exact: funeneg_le. Qed. -Lemma esum_ge0 S f : (forall x, S x -> 0 <= f x) -> 0 <= \esum_(i in S) f i. +Lemma esum_ge0 D f : (forall x, D x -> 0 <= f x) -> 0 <= \esum_(i in D) f i. Proof. by move=> f0; rewrite ge0_esum// PosEsum.pos_esum_ge0. Qed. Lemma le_esum_fine {U : choiceType} (A : set U) (B : set T) @@ -431,8 +437,8 @@ Lemma le_esum_fine {U : choiceType} (A : set U) (B : set T) Proof. move=> hf. rewrite [leLHS]ge0_esum. - by move=> i _; rewrite lee_fin; apply: fine_ge0; apply esum_ge0. -rewrite [leRHS]ge0_esum; first by move=> i _; apply esum_ge0. + by move=> i _; rewrite lee_fin; apply: fine_ge0; exact: esum_ge0. +rewrite [leRHS]ge0_esum; first by move=> i _; exact: esum_ge0. under [leLHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum//. under [leRHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum//. exact: PosEsum.le_pos_esum_fine. @@ -446,8 +452,8 @@ have I0f : forall x, I x -> 0 <= f x by move => x /IJ /f0. by rewrite !ge0_esum// PosEsum.subset_pos_esum. Qed. -Lemma esum_fset S f : finite_set S -> (forall i, S i -> 0 <= f i) -> - \esum_(i in S) f i = \sum_(i \in S) f i. +Lemma esum_fset D f : finite_set D -> (forall i, D i -> 0 <= f i) -> + \esum_(i in D) f i = \sum_(i \in D) f i. Proof. by move=> finF f0; rewrite ge0_esum//; exact: PosEsum.pos_esum_fset. Qed. End esum_realType. @@ -768,7 +774,7 @@ Qed. Arguments esum_set_image {R T} a e P. Section esum_bigcup. -Variables (R : realType) (T : choiceType) (K : set nat). +Context {R : realType} {T : choiceType} (K : set nat). Implicit Types (J : nat -> set T) (a : T -> \bar R). Lemma esum_bigcupT J a : trivIset setT J -> (forall x, 0 <= a x) -> @@ -828,42 +834,44 @@ move=> tF f0; rewrite esum_bigcupT// nneseries_esum//. by rewrite fun_true; apply: eq_esum => /= i _. Qed. -Definition summable (T : choiceType) (R : realType) (D : set T) +Definition esummable (T : choiceType) (R : realType) (D : set T) (f : T -> \bar R) := (\esum_(x in D) `| f x | < +oo)%E. +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable)] +Notation summable := esummable (only parsing). -Section summable_lemmas. +Section esummable_lemmas. Local Open Scope ereal_scope. -Variables (T : choiceType) (R : realType). +Context {T : choiceType} {R : realType}. Implicit Types (D : set T) (f : T -> \bar R). -Lemma summable_pinfty D f : summable D f -> forall x, D x -> `| f x | < +oo. +Lemma esummable_pinfty D f : esummable D f -> forall x, D x -> `| f x | < +oo. Proof. move=> Dfoo x Dx; apply: le_lt_trans Dfoo. rewrite (esumID [set x])// setI1 mem_set// esum_set1// leeDl//. exact: esum_ge0. Qed. -Lemma summableE D f : summable D f = (\esum_(x in D) `| f x | \is a fin_num). +Lemma esummableE D f : esummable D f = (\esum_(x in D) `| f x | \is a fin_num). Proof. -rewrite /summable fin_numElt; apply/idP/idP => [->|/andP[]//]. +rewrite /esummable fin_numElt; apply/idP/idP => [->|/andP[]//]. by rewrite andbT (lt_le_trans (ltNyr 0))//; exact: esum_ge0. Qed. -Lemma eq_summable D f g : f =1 g -> summable D f -> summable D g. +Lemma eq_esummable D f g : {in D, f =1 g} -> esummable D f -> esummable D g. Proof. -move => eq_fg; rewrite /summable; apply: le_lt_trans. -by apply: le_esum => ?; rewrite eq_fg. +move => eq_fg; apply: le_lt_trans. +by apply: le_esum => t Dt; rewrite eq_fg//; exact/mem_set. Qed. -Lemma le_summable D f g : - (forall x, 0 <= f x <= g x) -> summable D g -> summable D f. +Lemma le_esummable D f g : + (forall x, D x -> 0 <= f x <= g x) -> esummable D g -> esummable D f. Proof. -move=> fg; rewrite /summable; apply: le_lt_trans. -apply: le_esum => t Dt; have/andP[f0 {}fg] := fg t. +move=> fg; apply: le_lt_trans. +apply: le_esum => t Dt; have/andP[f0 {}fg] := fg _ Dt. by rewrite !gee0_abs// (le_trans f0). Qed. -Lemma summableD D f g : summable D f -> summable D g -> summable D (f \+ g). +Lemma esummableD D f g : esummable D f -> esummable D g -> esummable D (f \+ g). Proof. move=> Df Dg; apply: le_lt_trans (lte_add_pinfty Df Dg). rewrite -esumD//; do 2 rewrite ge0_esum//. @@ -871,15 +879,15 @@ rewrite -esumD//; do 2 rewrite ge0_esum//. by apply: PosEsum.le_pos_esum => t Dt; exact: lee_abs_add. Qed. -Lemma summableN D f : summable D f = summable D (\- f). +Lemma esummableN D f : esummable D f = esummable D (\- f). Proof. -by rewrite /summable; congr (_ < +oo); apply: eq_esum => t Dt; rewrite abseN. +by rewrite /esummable; congr (_ < +oo); apply: eq_esum => t Dt; rewrite abseN. Qed. -Lemma summableB D f g : summable D f -> summable D g -> summable D (f \- g). -Proof. by move=> Df; rewrite summableN; exact: summableD. Qed. +Lemma esummableB D f g : esummable D f -> esummable D g -> esummable D (f \- g). +Proof. by move=> Df; rewrite esummableN; exact: esummableD. Qed. -Lemma summable_funepos D f : summable D f -> summable D f^\+. +Lemma esummable_funepos D f : esummable D f -> esummable D f^\+. Proof. apply: le_lt_trans. do 2 rewrite ge0_esum//. @@ -887,7 +895,7 @@ apply: PosEsum.le_pos_esum => t Dt. by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl. Qed. -Lemma summable_funeneg D f : summable D f -> summable D f^\-. +Lemma esummable_funeneg D f : esummable D f -> esummable D f^\-. Proof. apply: le_lt_trans. do 2 rewrite ge0_esum//. @@ -895,78 +903,80 @@ apply: PosEsum.le_pos_esum => t Dt. by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr. Qed. -Lemma summableZ D f c : c \is a fin_num -> - summable D f -> summable D (fun x => c * f x). +Lemma esummableZl D f c : c \is a fin_num -> + esummable D f -> esummable D (fun x => c * f x). Proof. -rewrite /summable => cfun fy. -under eq_esum do rewrite abseM. +move=> cfin fy; rewrite /esummable; under eq_esum do rewrite abseM. by rewrite esumZ// lte_mul_pinfty// abse_fin_num. Qed. -Lemma summableZr D f c : c \is a fin_num -> - summable D f -> summable D (fun x => f x * c). -Proof. -under eq_fun do rewrite muleC. -exact: summableZ. -Qed. +Lemma esummableZr D f c : c \is a fin_num -> + esummable D f -> esummable D (fun x => f x * c). +Proof. by under eq_fun do rewrite muleC; exact: esummableZl. Qed. -Lemma summableMl D f1 f2 : - (exists2 M, (forall x, D x -> `|f1 x| <= M) & M \is a fin_num) -> - summable D f2 -> summable D (f1 \* f2). +Lemma esummableMl D f1 f2 : + (exists2 M, forall x, D x -> `|f1 x| <= M & M \is a fin_num) -> + esummable D f2 -> esummable D (f1 \* f2). Proof. -move=> [M h1 Mfin] sf2. -rewrite /summable; apply: le_lt_trans (summableZ Mfin sf2). +move=> [M Df1M Mfin] Df2; apply: le_lt_trans (esummableZl Mfin Df2). apply: le_esum => x Dx; rewrite !abseM. -apply: lee_wpmul2r; first exact: abse_ge0. -by apply: le_trans (h1 x Dx) (lee_abs _). +by rewrite lee_wpmul2r ?abse_ge0// (le_trans (Df1M x Dx) (lee_abs _)). Qed. -Lemma summableMr D f1 f2 : - (exists2 M, (forall x, D x -> `|f2 x| <= M) & M \is a fin_num) -> - summable D f1 -> - summable D (f1 \* f2). -Proof. -move=> Df2. -under eq_fun do rewrite muleC. -exact: summableMl. -Qed. +Lemma esummableMr D f1 f2 : + (exists2 M, forall x, D x -> `|f2 x| <= M & M \is a fin_num) -> + esummable D f1 -> esummable D (f1 \* f2). +Proof. by move=> Df2; under eq_fun do rewrite muleC; exact: esummableMl. Qed. -Lemma summableM D f1 f2 : - summable D f1 -> summable D f2 -> summable D (f1 \* f2). +Lemma esummableM D f1 f2 : + esummable D f1 -> esummable D f2 -> esummable D (f1 \* f2). Proof. -rewrite summableE => smS1 smS2; apply/summableMl => //. -exists (\esum_(x in D) `|f1 x|) => //. -exact: esum_ge1. +rewrite esummableE => smS1 smS2; apply/esummableMl => //. +by exists (\esum_(x in D) `|f1 x|) => //; exact: esum_ge1. Qed. -End summable_lemmas. +End esummable_lemmas. +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_pinfty)] +Notation summable_pinfty := esummable_pinfty (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableE)] +Notation summableE := esummableE (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableD)] +Notation summableD := esummableD (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableN)] +Notation summableN := esummableN (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableB)] +Notation summableB := esummableB (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_funepos)] +Notation summable_funepos := esummable_funepos (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_funeneg)] +Notation summable_funeneg := esummable_funeneg (only parsing). Import numFieldNormedType.Exports. -Section summable_nat. +Section esummable_nat. Local Open Scope ereal_scope. -Variable R : realType. +Context {R : realType}. -Lemma summable_fine_sum r (P : pred nat) (f : (\bar R)^nat) : summable P f -> +Lemma esummable_fine_sum r (P : pred nat) (f : (\bar R)^nat) : esummable P f -> (\sum_(0 <= k < r | P k) fine (f k))%R = fine (\sum_(0 <= k < r | P k) f k). Proof. move=> Pf; elim: r => [|r ih]; first by rewrite !big_nil. rewrite big_mkcond/= big_nat_recr// [in RHS]big_mkcond/= big_nat_recr//=. rewrite -!big_mkcond/= ih; case: ifPn => Pr => //; last by rewrite adde0 addr0. rewrite fineD//; last first. - by rewrite fin_num_abs (summable_pinfty Pf). -by apply/sum_fin_numP => i ir Pi; rewrite fin_num_abs (summable_pinfty Pf). + by rewrite fin_num_abs (esummable_pinfty Pf). +by apply/sum_fin_numP => i ir Pi; rewrite fin_num_abs (esummable_pinfty Pf). Qed. -Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) : - (forall i, P i -> 0 <= f i)%E -> summable P f -> +Lemma esummable_cvg (P : pred nat) (f : (\bar R)^nat) : + (forall i, P i -> 0 <= f i)%E -> esummable P f -> 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. exists (fine (\sum_(i x /= [n _ <-]. -rewrite summable_fine_sum// -lee_fin fineK//. - by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (summable_pinfty Pf). +rewrite esummable_fine_sum// -lee_fin fineK//. + by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (esummable_pinfty Pf). rewrite fineK//. rewrite nneseries_esum// fin_numElt; apply/andP; split. by rewrite (@lt_le_trans _ _ 0)// ?lte_ninfty//; exact: esum_ge0. @@ -976,8 +986,8 @@ apply: le_trans (nneseries_lim_ge n _) => //; apply: lee_sum => i _. by rewrite lee_abs. Qed. -Lemma summable_nneseries_lim (P : pred nat) (f : (\bar R)^nat) : - (forall i, P i -> 0 <= f i)%E -> summable P f -> +Lemma esummable_nneseries_lim (P : pred nat) (f : (\bar R)^nat) : + (forall i, P i -> 0 <= f i)%E -> esummable P f -> \sum_(i (\sum_(0 <= k < n | P k) fine (f k))%R) @ \oo))%:E. Proof. @@ -985,11 +995,11 @@ move=> f0 Pf; pose A_ n := (\sum_(0 <= k < n | P k) fine (f k))%R. transitivity (lim (EFin \o A_ @ \oo)). apply/congr_lim/funext => /= n; rewrite /A_ /= -sumEFin. apply eq_bigr => i Pi/=; rewrite fineK//. - by rewrite fin_num_abs (@summable_pinfty _ _ P). -by rewrite EFin_lim//; apply: summable_cvg. + by rewrite fin_num_abs (@esummable_pinfty _ _ P). +by rewrite EFin_lim//; exact: esummable_cvg. Qed. -Lemma summable_eseries (f : (\bar R)^nat) (P : pred nat) : summable P f -> +Lemma esummable_eseries (f : (\bar R)^nat) (P : pred nat) : esummable P f -> \sum_(i C_ n - (A - B)) @ \oo --> (0 : R^o))%R. move=> CAB. - rewrite [X in X - _]summable_nneseries_lim//; first exact/summable_funepos. - rewrite [X in _ - X]summable_nneseries_lim//; first exact/summable_funeneg. + rewrite [X in X - _]esummable_nneseries_lim//; first exact/esummable_funepos. + rewrite [X in _ - X]esummable_nneseries_lim//; first exact/esummable_funeneg. rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first. exact: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB). apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=. by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge. have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R. apply: cvgD. - - by apply: summable_cvg => //; exact/summable_funepos. - - by apply: cvgN; apply: summable_cvg => //; exact/summable_funeneg. + - by apply: esummable_cvg => //; exact/esummable_funepos. + - by apply: cvgN; apply: esummable_cvg => //; exact/esummable_funeneg. move=> /cvgrPdist_lt cvgAB; apply/cvgrPdist_lt => e e0. move: cvgAB => /(_ _ e0) [N _/= hN] /=. near=> n. rewrite distrC subr0. have -> : (C_ = A_ \- B_)%R. apply/funext => k. - rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//. + rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -esummable_fine_sum//. apply eq_bigr => i Pi; rewrite -fineB//. - - by rewrite fin_num_abs (@summable_pinfty _ _ P)// summable_funepos. - - by rewrite fin_num_abs (@summable_pinfty _ _ P)// summable_funeneg. + - by rewrite fin_num_abs (@esummable_pinfty _ _ P)// esummable_funepos. + - by rewrite fin_num_abs (@esummable_pinfty _ _ P)// esummable_funeneg. - by rewrite -[in LHS](funeposBneg f). by rewrite distrC; apply: hN; near: n; exists N. Unshelve. all: by end_near. Qed. -Lemma summable_eseries_esum (f : (\bar R)^nat) (P : pred nat) : - summable P f -> \sum_(i \sum_(i Pfoo. -by rewrite -nneseries_esum// -nneseries_esum// [LHS]summable_eseries. +by rewrite -nneseries_esum// -nneseries_esum// [LHS]esummable_eseries. Qed. -End summable_nat. +End esummable_nat. +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_fine_sum)] +Notation summable_fine_sum := esummable_fine_sum (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_cvg)] +Notation summable_cvg := esummable_cvg (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_nneseries_lim)] +Notation summable_nneseries_lim := esummable_nneseries_lim (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_eseries)] +Notation summable_eseries := esummable_eseries (only parsing). +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_eseries_esum)] +Notation summable_eseries_esum := esummable_eseries_esum (only parsing). Section esumB. Local Open Scope ereal_scope. -Variables (R : realType) (T : choiceType). +Context {R : realType} {T : choiceType}. Implicit Types (D : set T) (f g : T -> \bar R). Let esum_posneg D f := esum D f^\+ - esum D f^\-. @@ -1049,7 +1069,7 @@ move=> Sa; rewrite /esum_posneg [X in _ - X](_ : _ = 0) ?sube0. apply: eq_esum => t St; rewrite funeposE; apply/max_idPl; exact: Sa. Qed. -Lemma esumB D f g : summable D f -> summable D g -> +Lemma esumB D f g : esummable D f -> esummable D g -> (forall i, D i -> 0 <= f i) -> (forall i, D i -> 0 <= g i) -> \esum_(i in D) (f \- g)^\+ i - \esum_(i in D) (f \- g)^\- i = \esum_(i in D) f i - \esum_(i in D) g i. @@ -1061,26 +1081,26 @@ have /eqP : esum D (f \- g)^\+ + esum_posneg D g = apply eq_esum => i Di; rewrite funeposE funenegE. have [fg|fg] := leP 0 (f i - g i). rewrite max_r 1?leeNl ?oppe0// add0e subeK//. - by rewrite fin_num_abs (summable_pinfty Dg). + by rewrite fin_num_abs (esummable_pinfty Dg). rewrite add0e max_l; first by rewrite leeNr oppe0 ltW. - rewrite fin_num_oppeB//; first by rewrite fin_num_abs (summable_pinfty Dg). - by rewrite -addeA addeCA addeA subeK// fin_num_abs (summable_pinfty Df). + rewrite fin_num_oppeB//; first by rewrite fin_num_abs (esummable_pinfty Dg). + by rewrite -addeA addeCA addeA subeK// fin_num_abs (esummable_pinfty Df). rewrite [X in _ == X -> _]addeC -sube_eq. - rewrite fin_numD; apply/andP; split. rewrite (eq_esum _ _ (abse \o (f \- g)^\+))//. by move=> t Dt; rewrite /= gee0_abs. - by rewrite -summableE; exact/summable_funepos/summableB. - move: Dg; rewrite summableE (eq_esum _ _ g)//. + by rewrite -esummableE; exact/esummable_funepos/esummableB. + move: Dg; rewrite esummableE (eq_esum _ _ g)//. by move=> t Tt; rewrite gee0_abs// g0. by rewrite ge0_esum_posneg// => t Tt; rewrite gee0_abs// g0. - rewrite fin_num_adde_defr// ge0_esum_posneg//. - rewrite (eq_esum _ _ (abse \o f))// -?summableE// => i Di. + rewrite (eq_esum _ _ (abse \o f))// -?esummableE// => i Di. by rewrite /= gee0_abs// f0. rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq. -- rewrite ge0_esum_posneg// (eq_esum _ _ (abse \o f))// -?summableE// => i Di. +- rewrite ge0_esum_posneg// (eq_esum _ _ (abse \o f))// -?esummableE// => i Di. by rewrite /= gee0_abs// f0. - rewrite fin_num_adde_defl// ge0_esum_posneg//. - rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di. + rewrite (@eq_esum _ _ _ _ (abse \o g))// -?esummableE// => i Di. by rewrite /= gee0_abs// g0. by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->. Qed. @@ -1089,115 +1109,84 @@ End esumB. Section esum_summable. Context {R : realType} {T : choiceType}. -Implicit Types (S : T -> \bar R). +Implicit Types (D : set T) (f g : T -> \bar R). -Lemma summable_esum_funepos S : - summable [set: T] S -> \esum_(t in [set: T]) S^\+ t \is a fin_num. +Lemma esummable_esum_funepos D f : + esummable D f -> \esum_(t in D) f^\+ t \is a fin_num. Proof. -move => /summable_funepos. -rewrite summableE. -rewrite (@eq_esum _ _ _ (fun y : T => S^\+ y) (fun y : T => `|S^\+ y|)) //=. -by move => ??; rewrite gee0_abs. +move=> /esummable_funepos; rewrite esummableE => ffin. +by rewrite (eq_esum _ _ (fun y => `|f^\+ y|))//= => t Dt; rewrite gee0_abs. Qed. -Lemma summable_esum_fin_num S : - summable [set: T] S -> \esum_(i in [set:T]) S i \is a fin_num. +Lemma esummable_esum_funeneg D f : + esummable D f -> \esum_(t in D) f^\- t \is a fin_num. Proof. -move=> sm; rewrite /esum fin_numB; apply/andP; split. -- rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funepos_ge0. - exact: (summable_esum_funepos sm). -- have smN : summable [set: T] (\- S) by rewrite -summableN. - rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funeneg_ge0. - by rewrite -funeposN; exact: (summable_esum_funepos smN). +rewrite esummableN => /esummable_esum_funepos. +by under eq_esum do rewrite funeposN. Qed. -Lemma summable_esumN S : - summable [set : T] S -> \esum_(i in [set:T]) - S i = - \esum_(i in [set:T]) S i. +Lemma esummable_esum_fin_num D f : + esummable D f -> \esum_(i in D) f i \is a fin_num. Proof. -move=> hs; rewrite /esum funeposN funenegN oppeB. -- apply: fin_num_adde_defr. - rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funepos_ge0. - exact: (summable_esum_funepos hs). -- by rewrite addeC. +by move=> sm; rewrite esumE fin_numB; apply/andP; split; + [exact: esummable_esum_funepos|exact: esummable_esum_funeneg]. Qed. -Lemma summable_esumZ_pos S : - summable [set : T] S -> - forall d : \bar R, 0 <= d -> d \is a fin_num -> - \esum_(x in [set:T]) d * S x = d * \esum_(x in [set:T]) S x. +Lemma esummable_esumN D f : + esummable D f -> \esum_(i in D) - f i = - \esum_(i in D) f i. Proof. -move=> h d d0 dfin. +move=> hs; rewrite [in RHS]esumE oppeB. + by rewrite fin_num_adde_defr// esummable_esum_funepos. +rewrite [in LHS]esumE. +under eq_esum do rewrite funeposN. +under [in X in _ - X]eq_esum do rewrite funenegN. +by rewrite addeC. +Qed. + +Let nonneg_esummable_esumZ D f d : esummable D f -> 0 <= d -> d \is a fin_num -> + \esum_(x in D) d * f x = d * \esum_(x in D) f x. +Proof. +move=> h d0 dfin. have -> : d = (fine d)%:E by rewrite fineK. have ? : (0 <= fine d)%R by rewrite -lee_fin fineK. -have ? : (0 <= (fine d)%:E) by rewrite fineK. -have ? : (fine d)%:E \is a fin_num by []. -rewrite [in LHS]/esum ge0_funeposM// ge0_funenegM//. -rewrite (PosEsum.pos_esumZ _ (fun t _ => funepos_ge0 S t)) //. -rewrite (PosEsum.pos_esumZ _ (fun t _ => funeneg_ge0 S t)) //. -rewrite -muleBr //. -apply: fin_num_adde_defr. -rewrite /PosEsum.pos_esum -ge0_esum; first by move=> x _; exact: funepos_ge0. -exact: (summable_esum_funepos h). -Qed. - -Lemma summable_esumZ S c : - `|c| \is a fin_num -> summable [set : T] S -> - \esum_(x in [set : T]) c * S x = c * \esum_(x in [set : T]) S x. -Proof. -move=> hf h. -have [c0|c0|->] := comparable_ltgtP (comparableT c 0). -- rewrite (eq_esum _ _ (fun x => - (`|c| * S x))). - + by move=> x _; rewrite lte0_abs// mulNe oppeK. - rewrite (summable_esumN (summableZ hf h)). - rewrite (summable_esumZ_pos h (abse_ge0 c) hf). - by rewrite lte0_abs// mulNe oppeK. -- apply: (summable_esumZ_pos h (ltW c0)). - by rewrite -abse_fin_num. -- rewrite [in RHS]mul0e; under eq_esum do rewrite mul0e. - by rewrite esum0. -Qed. - -Lemma esum_posneg (h : T -> \bar R) : - \esum_(x in [set:T]) h x = - \esum_(x in [set:T]) h^\+ x - \esum_(x in [set:T]) h^\- x. +rewrite esumE ge0_funeposM// ge0_funenegM// !esumZ// -muleBr//. + by rewrite fin_num_adde_defr// esummable_esum_funepos. +by rewrite [in RHS]esumE. +Qed. + +Lemma esummable_esumZ D f c : `|c| \is a fin_num -> esummable D f -> + \esum_(x in D) c * f x = c * \esum_(x in D) f x. Proof. -rewrite [in RHS]ge0_esum; first by move=> x _; exact: funepos_ge0. -rewrite [in RHS]ge0_esum; first by move=> x _; exact: funeneg_ge0. -by rewrite /esum. +move=> cmin Df; have [c0|c0|->] := comparable_ltgtP (comparableT c 0). +- rewrite -(oppeK c) -(@lte0_abs _ c)//. + under eq_esum do rewrite mulNe. + rewrite esummable_esumN; first exact: esummableZl. + by rewrite nonneg_esummable_esumZ// mulNe. +- by rewrite (nonneg_esummable_esumZ _ (ltW c0))// -abse_fin_num. +- by rewrite mul0e esum1// => t _; rewrite mul0e. Qed. -Lemma summable_esumD S1 S2 : - summable [set: T] S1 -> summable [set: T] S2 -> - \esum_(x in [set : T]) (S1 x + S2 x) = - \esum_(x in [set : T]) S1 x + \esum_(x in [set : T]) S2 x. +Lemma esummable_esumD D f g : esummable D f -> esummable D g -> + \esum_(x in D) (f x + g x) = \esum_(x in D) f x + \esum_(x in D) g x. Proof. move=> sm1 sm2. -rewrite -(funeDB S1 S2). -rewrite (esum_posneg ((S1^\+ \+ S2^\+) \- (S1^\- \+ S2^\-))). -rewrite (@esumB _ _ [set:T] (S1^\+ \+ S2^\+) (S1^\- \+ S2^\-) - (summableD (summable_funepos sm1) (summable_funepos sm2)) - (summableD (summable_funeneg sm1) (summable_funeneg sm2)) - (fun i _ => adde_ge0 (funepos_ge0 S1 i) (funepos_ge0 S2 i)) - (fun i _ => adde_ge0 (funeneg_ge0 S1 i) (funeneg_ge0 S2 i))). -rewrite (@esumD _ _ [set:T] (S1^\+) (S2^\+) - (fun i _ => funepos_ge0 S1 i) (fun i _ => funepos_ge0 S2 i)). -rewrite (@esumD _ _ [set:T] (S1^\-) (S2^\-) - (fun i _ => funeneg_ge0 S1 i) (fun i _ => funeneg_ge0 S2 i)). -rewrite [in RHS](esum_posneg S1) [in RHS](esum_posneg S2). -rewrite oppeD. - apply: fin_num_adde_defl. - exact: (summable_esum_fin_num (summable_funeneg sm2)). +rewrite -(funeDB f g) (esumE _ ((f^\+ \+ g^\+) \- (f^\- \+ g^\-))). +rewrite (@esumB _ _ D (f^\+ \+ g^\+) (f^\- \+ g^\-)). + by apply: esummableD => //; exact: esummable_funepos. + by apply: esummableD => //; exact: esummable_funeneg. + by move=> t _; rewrite adde_ge0. + by move=> t _; rewrite adde_ge0. +rewrite esumD// esumD// [in RHS](esumE _ f) [in RHS](esumE _ g) oppeD. + rewrite fin_num_adde_defl// esummable_esum_fin_num//. + exact: esummable_funeneg. by rewrite addeACA. Qed. -Lemma summable_esumB {V : choiceType} S1 S2 : - summable [set: T] S1 -> summable [set: T] S2 -> - \esum_(x in [set : T]) (S1 x - S2 x) = - \esum_(x in [set : T]) S1 x - \esum_(x in [set : T]) S2 x. +Lemma esummable_esumB D f g : esummable D f -> esummable D g -> + \esum_(x in D) (f x - g x) = \esum_(x in D) f x - \esum_(x in D) g x. Proof. move=> sm1 sm2. -have nS2 : summable [set: T] (\- S2) by rewrite -summableN. -by rewrite (summable_esumD sm1 nS2) (summable_esumN sm2). +by rewrite esummable_esumD ?esummable_esumN// -esummableN. Qed. End esum_summable. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 706a0a57b4..10d9bcf564 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -887,16 +887,15 @@ End integral_measure_add. Section subadditive_countable. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variable (mu : {measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} (mu : {measure set T -> \bar R}). -Lemma integrable_summable (F : (set T)^nat) (g : T -> \bar R): +Lemma integrable_esummable (F : (set T)^nat) (g : T -> \bar R): trivIset setT F -> (forall k, measurable (F k)) -> mu.-integrable (\bigcup_k F k) g -> - summable [set: nat] (fun i => \int[mu]_(x in F i) g x). + esummable [set: nat] (fun i => \int[mu]_(x in F i) g x). Proof. move=> tF mF fi. -rewrite /summable -(_ : [set _ | true] = setT); first exact/seteqP. +rewrite /esummable -(_ : [set _ | true] = setT); first exact/seteqP. rewrite -nneseries_esum//. have [mf {fi}] := integrableP _ _ _ fi. rewrite ge0_integral_bigcup//; first exact: measurableT_comp. @@ -938,24 +937,25 @@ transitivity ((\sum_(i n _; exact: integral_ge0. rewrite [X in _ - X]nneseries_esum; first by move=> n _; exact: integral_ge0. rewrite set_true -esumB//=. - - apply: integrable_summable => //; apply: integrable_funepos => //. + - apply: integrable_esummable => //; apply: integrable_funepos => //. exact: bigcup_measurable. - - apply: integrable_summable => //; apply: integrable_funeneg => //. + - apply: integrable_esummable => //; apply: integrable_funeneg => //. exact: bigcup_measurable. - by move=> n _; exact: integral_ge0. - by move=> n _; exact: integral_ge0. -rewrite summable_eseries. - under [X in summable _ X]eq_fun do rewrite -integralE. - by rewrite fun_true; exact: integrable_summable. +rewrite esummable_eseries. + under [X in esummable _ X]eq_fun do rewrite -integralE. + by rewrite fun_true; exact: integrable_esummable. by congr (_ - _)%E; rewrite nneseries_esum// set_true. Qed. End subadditive_countable. +#[deprecated(since="mathcomp-analysis 1.18.0", use=integrable_esummable)] +Notation integrable_summable := integrable_esummable (only parsing). Section sequence_of_measures. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variable m_ : {measure set T -> \bar R}^nat. +Context {d} {T : measurableType d} {R : realType} (m_ : {measure set T -> \bar R}^nat). Let m := mseries m_ O. Lemma integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) : @@ -983,11 +983,11 @@ have fineKp : \sum_(n n _; exact/fine_ge0/integral_ge0. rewrite nneseries_esum; first by move=> n _; exact/fine_ge0/integral_ge0. rewrite -esumB//. - - by rewrite /= /summable -nneseries_esum// -fineKp. - - by rewrite /summable /= -nneseries_esum// -fineKn; exact: fmoo. + - by rewrite /= /esummable -nneseries_esum// -fineKp. + - by rewrite /esummable /= -nneseries_esum// -fineKn; exact: fmoo. - by move=> n _; exact/fine_ge0/integral_ge0. - by move=> n _; exact/fine_ge0/integral_ge0. -rewrite -summable_eseries_esum. +rewrite -esummable_eseries_esum. apply: (@le_lt_trans _ _ (\esum_(i in (fun=> true)) `|(fine (\int[m_ i]_(x in D) f x))%:E|)). do 2 rewrite ge0_esum//. @@ -1012,9 +1012,9 @@ End sequence_of_measures. Section integral_counting. Local Open Scope ereal_scope. -Variable R : realType. +Context {R : realType}. -Lemma integral_count (a : nat -> \bar R) : summable setT a -> +Lemma integral_count (a : nat -> \bar R) : esummable [set: nat] a -> \int[counting]_t (a t) = \sum_(k sa. @@ -1023,10 +1023,10 @@ transitivity (\int[mseries (fun n => \d_ n) O]_t a t). by rewrite /= counting_dirac. rewrite (@integral_measure_series _ _ R (fun n => \d_ n) setT)//=. - move=> n; apply/integrableP; split=> [//|]. - by rewrite integral_dirac//= diracT mul1e (summable_pinfty sa). -- by apply: summable_integral_dirac => //; exact: summable_funeneg. -- by apply: summable_integral_dirac => //; exact: summable_funepos. -- by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e. + by rewrite integral_dirac//= diracT mul1e (esummable_pinfty sa). +- by apply: esummable_integral_dirac => //; exact: esummable_funeneg. +- by apply: esummable_integral_dirac => //; exact: esummable_funepos. +- by apply: eq_eseriesr => i _; rewrite integral_dirac//= diracT mul1e. Qed. End integral_counting. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 9c8a37166b..e17b6b8827 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -649,17 +649,19 @@ Qed. End integral_dirac. -Lemma summable_integral_dirac {R : realType} (a : (\bar R)^nat) : - summable setT a -> (\sum_(n (\sum_(n sa. apply: (@le_lt_trans _ _ (\sum_(i // n _; rewrite integral_dirac//. - move: (@summable_pinfty _ _ _ _ sa n Logic.I). + move: (@esummable_pinfty _ _ _ _ sa n Logic.I). by case: (a n) => //= r _; rewrite indicE/= mem_set// mul1r. -move: (sa); rewrite /summable -fun_true -nneseries_esum//; apply: le_lt_trans. +move: (sa); rewrite /esummable -fun_true -nneseries_esum//; apply: le_lt_trans. by apply: lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey. Qed. +#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_integral_dirac)] +Notation summable_integral_dirac := esummable_integral_dirac (only parsing). Section integral_measure_sum_nnsfun. Local Open Scope ereal_scope. From ce3acabdb94b1dc17c5ac50b5164dd16ca91e87d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 9 Aug 2026 18:37:45 +0900 Subject: [PATCH 4/7] complete changelog --- CHANGELOG_UNRELEASED.md | 10 ++++++---- theories/esum.v | 5 +++-- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1215ecd979..840c0e85b2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,12 +21,14 @@ + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, `at_left_shift`, `at_right_shift` - in `esum.v`: + + lemmas `pos_esum_ge1`, `le_pos_esum_fine`, `sum_esum_ge`, `le_esum_fine`, + `subset_esum`, `esum0`, `esum_if_eq_op_set1`, `esum_neq0`, `esum_ge1` + lemmas `eq_esummable`, `le_esummable`, `esummableZl`, `esummableZr`, `esummableMl`, `esummableMr`, `esummableM` - + lemmas `esummable_esum_funepos`, `esummable_esum_funeneg`, - `esummable_esum_fin_num`, `esummable_esumN` - + lemma `esumE` - + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB` + + lemmas `esummable_esum_funepos`, `esummable_esum_funeneg`, + `esummable_esum_fin_num`, `esummable_esumN` + + lemma `esumE` + + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB` ### Changed diff --git a/theories/esum.v b/theories/esum.v index a393a2eed5..f012c89846 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -542,7 +542,8 @@ Lemma esum_ge {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) x : x <= \esum_(i in I) f i. Proof. by move=> f0 If; rewrite ge0_esum// PosEsum.pos_esum_ge. Qed. -Lemma esum_unit {R : realType} {T : choiceType} (f : T -> \bar R) x : +(* TODO: is this lemma really useful? *) +Lemma esum_if_eq_op_set1 {R : realType} {T : choiceType} (f : T -> \bar R) x : \esum_(i in [set: T]) (if x == i then f i else 0) = f x. Proof. by rewrite esum_if_eq_op esum_set1. Qed. @@ -1149,7 +1150,7 @@ Proof. move=> h d0 dfin. have -> : d = (fine d)%:E by rewrite fineK. have ? : (0 <= fine d)%R by rewrite -lee_fin fineK. -rewrite esumE ge0_funeposM// ge0_funenegM// !esumZ// -muleBr//. +rewrite esumE (ge0_funeposM f)// (ge0_funenegM f)// !esumZ// -muleBr//. by rewrite fin_num_adde_defr// esummable_esum_funepos. by rewrite [in RHS]esumE. Qed. From 3a0189e01c6399c7b33f93ac382734fad240f9b7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 9 Aug 2026 18:48:45 +0900 Subject: [PATCH 5/7] memo --- theories/esum.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/esum.v b/theories/esum.v index f012c89846..df97d55fb5 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -155,6 +155,7 @@ Lemma pos_esum_ge (T1 : choiceType) (I : set T1) (a : T1 -> \bar R) x : x <= \esum_(i in I) a i. Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed. +(* TODO: better name wanted *) Lemma pos_esum_ge1 S f x : S x -> f x <= \esum_(i in S) f i. Proof. move=> Sx; apply: pos_esum_ge; exists [set x]; last by rewrite fsbig_set1. @@ -564,6 +565,7 @@ apply: contra_neqP => /forall2NP a0; apply: esum1 => t /mem_set It. by have [|/negP/negPn/eqP//] := a0 t; rewrite It. Qed. +(* TODO: better name wanted *) Lemma esum_ge1 {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) : (forall x, I x -> 0 <= f x) -> forall x, I x -> f x <= \esum_(i in I) f i. From acceba5e622d279d7c3a50da2c65f7c4390c0fb0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 9 Aug 2026 21:09:23 +0900 Subject: [PATCH 6/7] compat with Rocq 9.2 --- theories/esum.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/esum.v b/theories/esum.v index df97d55fb5..88e3918ab7 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1152,9 +1152,9 @@ Proof. move=> h d0 dfin. have -> : d = (fine d)%:E by rewrite fineK. have ? : (0 <= fine d)%R by rewrite -lee_fin fineK. -rewrite esumE (ge0_funeposM f)// (ge0_funenegM f)// !esumZ// -muleBr//. +rewrite esumE muleBr//. by rewrite fin_num_adde_defr// esummable_esum_funepos. -by rewrite [in RHS]esumE. +by rewrite -!esumZ// -(ge0_funeposM f)// -(ge0_funenegM f)// -esumE. Qed. Lemma esummable_esumZ D f c : `|c| \is a fin_num -> esummable D f -> @@ -1162,7 +1162,7 @@ Lemma esummable_esumZ D f c : `|c| \is a fin_num -> esummable D f -> Proof. move=> cmin Df; have [c0|c0|->] := comparable_ltgtP (comparableT c 0). - rewrite -(oppeK c) -(@lte0_abs _ c)//. - under eq_esum do rewrite mulNe. + under [LHS]eq_esum do rewrite mulNe. rewrite esummable_esumN; first exact: esummableZl. by rewrite nonneg_esummable_esumZ// mulNe. - by rewrite (nonneg_esummable_esumZ _ (ltW c0))// -abse_fin_num. From 5a6b52dc66987e899476b420845dbc22fb56c632 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 9 Aug 2026 22:01:16 +0900 Subject: [PATCH 7/7] compact with 9.1 --- theories/esum.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/esum.v b/theories/esum.v index 88e3918ab7..f358d3767c 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1152,7 +1152,7 @@ Proof. move=> h d0 dfin. have -> : d = (fine d)%:E by rewrite fineK. have ? : (0 <= fine d)%R by rewrite -lee_fin fineK. -rewrite esumE muleBr//. +rewrite [in RHS]esumE muleBr//. by rewrite fin_num_adde_defr// esummable_esum_funepos. by rewrite -!esumZ// -(ge0_funeposM f)// -(ge0_funenegM f)// -esumE. Qed.