Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Integral count #628

Merged
merged 2 commits into from
Jul 3, 2022
Merged

Integral count #628

merged 2 commits into from
Jul 3, 2022

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Apr 4, 2022

Motivation for this change

equivalence between series and integral over the counting measure

based on PR #598

assumes PR #614, PR #616, PR #620 merged

fixes #630

@t6s

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    (do not edit former entries, only append new ones, be careful:
    merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist marked this pull request as draft April 4, 2022 10:58
@affeldt-aist affeldt-aist changed the base branch from master to counting_measure April 4, 2022 10:58
@affeldt-aist affeldt-aist force-pushed the counting_measure branch 2 times, most recently from 6fb1111 to 5ab059c Compare May 13, 2022 15:54
@affeldt-aist affeldt-aist force-pushed the integral_count branch 3 times, most recently from 6f98026 to d104271 Compare May 24, 2022 07:42
@affeldt-aist affeldt-aist marked this pull request as ready for review May 24, 2022 07:42
@affeldt-aist affeldt-aist requested a review from t6s May 24, 2022 07:42
Copy link
Member

@t6s t6s left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me

theories/esum.v Show resolved Hide resolved
theories/lebesgue_integral.v Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

affeldt-aist commented Jun 14, 2022

Looks good to me

Is it an approval for this PR and the PR it is based on?

@affeldt-aist
Copy link
Member Author

affeldt-aist commented Jun 22, 2022

We have a need for ge0_integral_measure_series in another project.
(We were about to re-prove it. :-/)

@affeldt-aist affeldt-aist changed the base branch from counting_measure to master July 2, 2022 18:18
@affeldt-aist affeldt-aist merged commit 758c241 into master Jul 3, 2022
@affeldt-aist affeldt-aist deleted the integral_count branch July 9, 2022 17:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

generalize to any choiceType
3 participants