Feature esum psum esum only by affeldt-aist · Pull Request #1978 · math-comp/analysis

affeldt-aist · 2026-05-20T02:19:41Z

Motivation for this change

closes #1954

This PR intends to extract the reusable part of PR #1954

new lemmas about esum
removal of fpos and fneg (superseded by funrpos and funrneg)

TODO: completed (?)

~~some scripts still need to be linted~~
~~some lemmas are wrongly named~~
~~ome lemmas are not in the right files~~

fyi: @lyonel2017 @strub

Checklist

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

PRs with several commits that make sense individually and that
all compile are preferentially merged into master.
PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

affeldt-aist · 2026-06-12T01:04:40Z

@t6s I am pinging you because this PR changes the definition of esum, I thought you may want to know

affeldt-aist · 2026-06-16T13:20:22Z

@lyonel2017 @strub rebased

t6s · 2026-06-22T01:14:40Z

It looks like there are several chunks of changes contained in this PR, making it difficult to review it at once. Can you provide a bit more detailed description of intention for each of them? For example, which lemmas do you consider are important?

affeldt-aist · 2026-06-23T12:27:55Z

It looks like there are several chunks of changes contained in this PR, making it difficult to review it at once.
Can you provide a bit more detailed description of intention for each of them?
For example, which lemmas do you consider are important?

This is maybe for @lyonel2017 and @strub to say because this PR is used to develop another one.

From my viewpoint, the main change is the definition of esum which has become:

Definition esum S f := pos_esum S f^\+ - pos_esum S f^\-.

Before that, it was only the positive part.

lyonel2017 · 2026-06-23T13:00:07Z

This is maybe for @lyonel2017 and @strub to say because this PR is used to develop another one.

I started porting the distr.v file from experimental_real to use esum. The idea is to better integrate the result present in experimental_reals into mathcomp-analysis. The current status is available here counting_distr.v (the branch is not up to date with this PR). For me all the changes present in this PR are required for the porting.

t6s · 2026-06-25T08:51:02Z

 Qed.
 End SumTh.

+Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) :


Noting that esum has a very similar definition to sum, the following proof strategy is also possible:
discard the negative part of esum, and show PosEsum.pos_esum and psum are equal.

An attempt is as follows, but resulted in a longer proof:

Lemma ge0_funenegET : forall [T : Type] [R : realDomainType] [f : T -> \bar R], (forall x : T, (0%R <= f x)%E) -> f^\-%E = cst 0. Proof. move=> ? ? ? H; apply/funext => ?. have ->// := @ge0_funenegE _ _ setT. by rewrite mem_set. Qed. Lemma ge0_funrposET : forall [T : Type] [R : realDomainType] [f : T -> R], (forall x : T, 0 <= f x) -> f^\+ = f. Proof. move=> ? ? ? H; apply/funext => ?. have ->// := @ge0_funrposE _ _ setT. by rewrite mem_set. Qed. Lemma fsetsTE (T : choiceType) : fsets [set: T] = finite_set. Proof. by apply/funext=> ?; apply/propext; split => // -[]. Qed. Lemma exists_fsetE (T : choiceType) (P : {fset T} -> Prop) : (exists J : {fset T}, P J) = (exists2 J : set T, finite_set J & P (fset_set J)). Proof. apply/propext; split. by case=> J ?; exists [set` J]%classic => //; rewrite set_fsetK. by case=> J ? ?; exists (fset_set J). Qed. Lemma exists_finite_setE (T : choiceType) (P : set T -> Prop) : (exists2 J : set T, finite_set J & P J) = (exists J : {fset T}, P [set` J]%classic). Proof. rewrite exists_fsetE; apply/propext; split => -[] J ?. by move=> ?; exists J => //; rewrite fset_setK. by rewrite fset_setK// => ?; exists J. Qed. Lemma esymE (T : Type) (x y : T) : (x = y) = (y = x). Proof. by apply/propext; split => /esym. Qed. Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) : (forall i, 0 <= f i) -> summable f -> \esum_(x in [set: T]) (f x)%:E = (psum f)%:E. Proof. move=> f0 h. rewrite /esum ge0_funenegET// [X in (_ - X)%E]PosEsum.pos_esum1// sube0. rewrite /PosEsum.pos_esum fsetsTE. rewrite /psum/=; case:asboolP => // _. set S := (S in sup S). have S_has_ubound : has_ubound S. by case: h => M HM; exists M => ?/= [] J ->; exact: HM. (* summable f -> has_ubound S; (S in the definition of psum) *) have S_nonempty : (S !=set0)%classic. by exists 0, fset0; rewrite big1// => i; have := fsvalP i. (* S always has the sum over the emptyset as its elements *) rewrite -ereal_sup_EFin; [exact: S_has_ubound | exact: S_nonempty |]. congr ereal_sup. under eq_imagel do rewrite fsbig_finite//= funerpos/= sumEFin. rewrite -[LHS]image_comp; congr image. rewrite /S; apply: funext=> x/=. rewrite exists_finite_setE; congr ex; apply/funext => J. rewrite [LHS]esymE; congr eq. rewrite -(big_seq_fsetE _ _ xpredT (Num.norm \o f))/= set_fsetK. apply: eq_bigr => ? _. by rewrite ger0_norm// ge0_funrposET. Qed.

Further refactored; this ge0_psumEpos_esum can also be used to shorten esumEsum.

Lemma ge0_psumEpos_esum {R : realType} {T : choiceType} (f : T -> R) : (forall i, 0 <= f i) -> summable f -> (psum f)%:E = PosEsum.pos_esum [set: T] (EFin \o f). Proof. move=> f0 h. rewrite /psum/=; case: asboolP => // _. rewrite /PosEsum.pos_esum fsetsTE. set S := (S in sup S). have S_has_ubound : has_ubound S. by case: h => M HM; exists M => ?/= [] J ->; exact: HM. (* summable f -> has_ubound S; (S in the definition of psum) *) have S_nonempty : (S !=set0)%classic. by exists 0, fset0; rewrite big1// => i; have := fsvalP i. (* S always has the sum over the emptyset as its elements *) rewrite -ereal_sup_EFin; [exact: S_has_ubound | exact: S_nonempty |]. congr ereal_sup. under [RHS]eq_imagel do rewrite fsbig_finite//= sumEFin. rewrite -[RHS]image_comp; congr image. rewrite /S; apply: funext=> x/=. rewrite exists_finite_setE; congr ex; apply/funext => J. rewrite [LHS]esymE; congr eq. rewrite -(big_seq_fsetE _ _ xpredT (Num.norm \o f))/= set_fsetK. apply: eq_bigr => ? _. by rewrite ger0_norm. Qed. Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) : (forall i, 0 <= f i) -> summable f -> \esum_(x in [set: T]) (f x)%:E = (psum f)%:E. Proof. move=> f0 h. rewrite /esum ge0_funenegET// [X in (_ - X)%E]PosEsum.pos_esum1// sube0. by rewrite psumEpos_esum// funerpos ge0_funrposET. Qed.

I am not sure we need to revise the proof scripts,
even though I am still unsure about the quality of the API:
this PR is certainly an improvement but work remains.
For example, what about renaming psum to pos_sum (to match pos_esum and also because it looks like "partial sum" to me, since we use gt0 to say "positive" in MathComp---of course in lemmas).

This is a right observation to say that some lemma should bridge pos_esum and psum,
but while pos_esum is "hidden" in a Module, psum isn't yet.

But, if we were to really "hide" psum in a Module, it is maybe reasonable to postpone because the API of psum contains infamous admitted lemmas (__admitted__psumB and __admitted__interchange_psum).
Fixing the latter is a goal of @lyonel2017, so we shall come back to it anyway.

The last commit (86ec8af) proves __admitted_psumB (it was about time...).

Noting that esum has a very similar definition to sum, the following proof strategy is also possible: discard the negative part of esum, and show PosEsum.pos_esum and psum are equal.

An attempt is as follows, but resulted in a longer proof:

[crunch] Lemma fsetsTE (T : choiceType) : fsets [set: T] = finite_set. Proof. by apply/funext=> ?; apply/propext; split => // -[]. Qed. [crunch]

I kept this lemma but didn't integrate the other ones.
In particular, I didn't keep ge0_funenegET and its pos variant because iirc they were introduced at some point but turned out to be less useful than their extensional variants (forall x, ... x = ... x).

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

t6s

After playing for a while with this code, I have a feeling that the code is in a consistent state.
I am inspired to do some additions (other than I suggested in the previous review comments) to fsbig, which could possibly simplify PosEsum, psum, and esum, but I will let them go into a separate PR rather than requesting changes here.

t6s · 2026-06-28T13:41:48Z

ah, but one thing: naming conventions seem to be incoherent between esum_psum and esumEsum

affeldt-aist · 2026-06-28T13:48:50Z

ah, but one thing: naming conventions seem to be incoherent between esum_psum and esumEsum

Yes indeed, esum_sum seems better than esumEsum.
Thank you for you time trying to optimize this PR, I understand it is difficult to context switch.

* Add missing lemmas for distr * use fun{r,e}{pos,neg} instead of f{pos,neg} * esum lemmas from PR math-comp#1954 * new definition of esum * prove __admitted__psumB --------- Co-authored-by: Lionel Blatter <lionel.blatter@wanadoo.fr> Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

lyonel2017 suggested changes Jun 9, 2026

View reviewed changes

Comment thread theories/esum.v Outdated

Comment thread theories/esum.v Outdated

Comment thread theories/esum.v Outdated

affeldt-aist force-pushed the feature-esum-psum-esum-only branch from d5fc795 to bc6feda Compare June 10, 2026 01:34

affeldt-aist commented Jun 10, 2026

View reviewed changes

Comment thread theories/esum.v Outdated

affeldt-aist force-pushed the master branch from 61d83df to 2f0f888 Compare June 11, 2026 02:34

affeldt-aist force-pushed the feature-esum-psum-esum-only branch 3 times, most recently from 8e0aacb to 3aec29b Compare June 12, 2026 01:01

affeldt-aist requested a review from strub June 13, 2026 03:25

affeldt-aist force-pushed the feature-esum-psum-esum-only branch from 4d86e16 to ba957d0 Compare June 16, 2026 13:18

affeldt-aist added this to the 1.17.0 milestone Jun 16, 2026

affeldt-aist requested a review from t6s June 16, 2026 13:21

t6s reviewed Jun 24, 2026

View reviewed changes

Comment thread experimental_reals/realsum.v

t6s reviewed Jun 25, 2026

View reviewed changes

lyonel2017 and others added 12 commits June 28, 2026 16:10

Add missing lemmas for distr

b0ebd5c

use fun{r,e}{pos,neg} instead of f{pos,neg}

4e08890

linting

b510a97

Add additonal lemmas

8ed0613

Add aditional lemmas

ebe6695

esum lemmas from PR 1954

f29b18e

fix opam

a81a6f0

fix CI

84faca0

fix CI

c682894

mv

cd2e7a1

gen esumZ, esum_esup_comm

7f2443d

address comments

337d6f9

affeldt-aist added 10 commits June 28, 2026 16:10

fix

7fda57b

mv

9092b1c

rm weak variants of lemmmas

0dff44a

new definition of esum

10398ec

restore esum_unit

237a29c

fix changelog

8d0d2cc

nitpick

0bfdcdc

upd toolbox

c627503

fix

c3c2bb7

fix

ae2b17b

affeldt-aist force-pushed the feature-esum-psum-esum-only branch from ba957d0 to ae2b17b Compare June 28, 2026 09:54

affeldt-aist and others added 4 commits June 28, 2026 20:12

prove __admitted__psumB

86ec8af

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

fix

aa68618

fix changelog

a1fa23c

fsetsTE

4a07230

t6s approved these changes Jun 28, 2026

View reviewed changes

fix

72d9452

affeldt-aist merged commit e656ced into math-comp:master Jun 28, 2026
45 checks passed

affeldt-aist deleted the feature-esum-psum-esum-only branch June 28, 2026 15:02

Uh oh!

Conversation

affeldt-aist commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Checklist

Merge policy

Reminder to reviewers

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

affeldt-aist commented Jun 12, 2026

Uh oh!

affeldt-aist commented Jun 16, 2026

Uh oh!

t6s commented Jun 22, 2026

Uh oh!

affeldt-aist commented Jun 23, 2026

Uh oh!

lyonel2017 commented Jun 23, 2026

Uh oh!

Uh oh!

t6s Jun 25, 2026

Choose a reason for hiding this comment

Uh oh!

t6s Jun 25, 2026

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 28, 2026

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 28, 2026

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 28, 2026

Choose a reason for hiding this comment

Uh oh!

t6s left a comment

Choose a reason for hiding this comment

Uh oh!

t6s commented Jun 28, 2026

Uh oh!

affeldt-aist commented Jun 28, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

affeldt-aist commented May 20, 2026 •

edited

Loading

affeldt-aist Jun 28, 2026 •

edited

Loading

affeldt-aist Jun 28, 2026 •

edited

Loading