Skip to content

Counting esum - #2063

Open
lyonel2017 wants to merge 3 commits into
math-comp:masterfrom
lyonel2017:esum_counting
Open

lyonel2017 wants to merge 3 commits into
math-comp:masterfrom
lyonel2017:esum_counting

Conversation

@lyonel2017

@lyonel2017 lyonel2017 commented Jul 29, 2026 •

Copy link
Copy Markdown
Contributor
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

@affeldt-aist affeldt-aist added this to the 1.18.0 milestone Jul 30, 2026
@lyonel2017
lyonel2017 force-pushed the esum_counting branch 3 times, most recently from 4e89861 to 9db0b40 Compare August 4, 2026 15:16
@affeldt-aist

Copy link
Copy Markdown
Member

PR #2062 merged -> need rebasing

@lyonel2017

Copy link
Copy Markdown
Contributor Author

PR #2062 merged -> need rebasing

I made a rebase.

@affeldt-aist

Copy link
Copy Markdown
Member

Thanks for the rebase!

@affeldt-aist affeldt-aist mentioned this pull request Aug 24, 2026
2 tasks
@affeldt-aist affeldt-aist modified the milestones: 1.18.0, 1.19.0 Aug 30, 2026
@affeldt-aist

Copy link
Copy Markdown
Member

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

Copy link
Copy Markdown
Contributor Author

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

affeldt-aist commented Oct 2, 2026 •

Copy link
Copy Markdown
Member

@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.)

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

Copy link
Copy Markdown
Contributor Author

@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.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants