Counting esum by lyonel2017 · Pull Request #2063 · math-comp/analysis

lyonel2017 · 2026-07-29T20:35:47Z

Motivation for this change

Provide a connection between esum and lesbegue_integrale (extracted from #2049).

Depends on #2062.

Checklist

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

affeldt-aist · 2026-08-11T06:17:10Z

PR #2062 merged -> need rebasing

lyonel2017 · 2026-08-12T09:40:27Z

PR #2062 merged -> need rebasing

I made a rebase.

affeldt-aist · 2026-08-23T04:52:16Z

Thanks for the rebase!

affeldt-aist · 2026-10-01T05:17:55Z

Note that this PR has clamp but does not actually use it, it can be removed since moreover it is the target of another PR.

lyonel2017 · 2026-10-01T11:24:48Z

Note that this PR has clamp but does not actually use it, it can be removed since moreover it is the target of another PR.

This PR is now rebase on top of master.

affeldt-aist · 2026-10-02T10:47:03Z

@lyonel2017 where do you use discrete_measurable_space in your developments? for the record, I would like to keep a pointer to a clear application for potential users. (A pointer inside #2116 could be enough.)

(I took the liberty to adapt naming to the rest of the library, trying to preserve consistency as much as possible still taking your proposals into account, do not hesitate to share concerns if any.)

lyonel2017 · 2026-10-03T19:50:13Z

@lyonel2017 where do you use discrete_measurable_space in your developments? for the record, I would like to keep a pointer to a clear application for potential users. (A pointer inside #2116 could be enough.)

I made a small experiment in the context of #2116 to check that the definition of expectation of #2064 and from random_variable.v are the same : expectationE. I'm not sure if this is the best approach for this proof.

hoheinzollern

See comments above.

hoheinzollern · 2026-10-05T07:56:08Z

 Arguments bigcup_setD1 {T I} x.
 Arguments bigcap_setD1 {T I} x.

+Lemma bigcup_idset1 {T : Type} (P : set T) : \bigcup_(i in P) [set i] = P.


is this lemma truly necessary? looks like a special case of bigcup_imset1

hoheinzollern · 2026-10-05T07:56:53Z

+(**md**************************************************************************)
+(* #                                                                          *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*   discrete_measurable_space == alias for the type of discrete measurable   *)
+(*                                types                                       *)
+(* ```                                                                        *)
+(******************************************************************************)


the header could benefit from a bit of description text

hoheinzollern · 2026-10-05T07:59:18Z

+Qed.
+
+Lemma discrete_integral_sum g (A : set T) : finite_set A ->
+  (forall x, 0 <= g x) ->


this assumption should not be needed

plus, you could actually prove integral_counting_esum first and use integral_mkcond/esum_mkcond to derive this version

hoheinzollern · 2026-10-05T08:01:18Z

+Lemma integral_counting_esum (f : T -> \bar R) : (forall x, 0 <= f x) ->
+  \int[@counting U R]_x f x = \esum_(x in [set: T]) f x.


again like the lemma above, the lemma should hold for any function, not just non-negative ones.

hoheinzollern · 2026-10-05T08:04:00Z

+Lemma nonempty_esumy {R : realType} {T : choiceType}  (A : set T) : A !=set0 ->
+  \esum_(_ in A) +oo%E = +oo%E :> \bar R.


would this be more generally applicable:

Suggested change

Lemma nonempty_esumy {R : realType} {T : choiceType} (A : set T) : A !=set0 ->

\esum_(_ in A) +oo%E = +oo%E :> \bar R.

Lemma nonempty_esumy {R : realType} {T : choiceType} (A : set T) :

A !=set0 -> \esum_(x in A) cst +oo%E x = +oo%E :> \bar R.

(maybe it's an unnecessary complication)

hoheinzollern · 2026-10-05T08:06:07Z

+Lemma infinite_esum_cst {R : realType} {T : choiceType} (c : \bar R) (A : set T) :
+  (0 < c)%E -> infinite_set A -> \esum_(_ in A) c = +oo%E.


similarly to the above, you could generalize it to:

Suggested change

Lemma infinite_esum_cst {R : realType} {T : choiceType} (c : \bar R) (A : set T) :

(0 < c)%E -> infinite_set A -> \esum_(_ in A) c = +oo%E.

Lemma infinite_esum_pos {R : realType} {T : choiceType} (c : \bar R) (f : T -> \bar R) (A : set T) :

(0 < c)%E -> (forall x, c <= f x)%E -> infinite_set A -> \esum_(x in A) f x = +oo%E.

hoheinzollern · 2026-10-05T08:07:52Z

 theories/showcase/summability.v
 theories/showcase/pnt.v

+


stray new line

hoheinzollern · 2026-10-05T08:08:07Z

+- in `classical_sets.v`
+  + lemma `bigcup_idset1`
+
+- in `esumv.v`:


affeldt-aist added this to the 1.18.0 milestone Jul 30, 2026

affeldt-aist force-pushed the master branch from 6e121ed to 219890d Compare July 30, 2026 05:56

lyonel2017 force-pushed the esum_counting branch 3 times, most recently from 4e89861 to 9db0b40 Compare August 4, 2026 15:16

lyonel2017 force-pushed the esum_counting branch from 9db0b40 to 09ac8fd Compare August 11, 2026 10:22

affeldt-aist mentioned this pull request Aug 24, 2026

Counting distribution #2064

Open

2 tasks

affeldt-aist modified the milestones: 1.18.0, 1.19.0 Aug 30, 2026

lyonel2017 force-pushed the esum_counting branch from 09ac8fd to e6ed93e Compare September 30, 2026 17:09

Connection between esum and lesbegue_integral

6e97a98

lyonel2017 force-pushed the esum_counting branch from e6ed93e to 6e97a98 Compare October 1, 2026 11:22

lyonel2017 mentioned this pull request Oct 1, 2026

Distribution have a sub probability measures #2116

Draft

2 tasks

nitpick and chaneglog

4104d0a

affeldt-aist requested a review from hoheinzollern October 2, 2026 10:48

affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Oct 2, 2026

fix

28e2f0b

affeldt-aist added experiment 🧪 This issue/PR is very experimental and removed enhancement ✨ This issue/PR is about adding new features enhancing the library labels Oct 4, 2026

hoheinzollern suggested changes Oct 5, 2026

View reviewed changes

		Lemma integral_counting_esum (f : T -> \bar R) : (forall x, 0 <= f x) ->
		\int[@counting U R]_x f x = \esum_(x in [set: T]) f x.

		Lemma nonempty_esumy {R : realType} {T : choiceType} (A : set T) : A !=set0 ->
		\esum_(_ in A) +oo%E = +oo%E :> \bar R.

		Lemma infinite_esum_cst {R : realType} {T : choiceType} (c : \bar R) (A : set T) :
		(0 < c)%E -> infinite_set A -> \esum_(_ in A) c = +oo%E.

Conversation

lyonel2017 commented Jul 29, 2026 • edited by affeldt-aist Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Checklist

Reminder to reviewers

Uh oh!

affeldt-aist commented Aug 11, 2026

Uh oh!

lyonel2017 commented Aug 12, 2026

Uh oh!

affeldt-aist commented Aug 23, 2026

Uh oh!

affeldt-aist commented Oct 1, 2026

Uh oh!

lyonel2017 commented Oct 1, 2026

Uh oh!

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

Uh oh!

Uh oh!

lyonel2017 commented Oct 3, 2026

Uh oh!

hoheinzollern left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

lyonel2017 commented Jul 29, 2026 •

edited by affeldt-aist

Loading

affeldt-aist commented Oct 2, 2026 •

edited

Loading