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.

Sign up for GitHub

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

Jump to bottom

Sums over general sets #294

Merged
merged 3 commits into from
May 4, 2021
Merged

Sums over general sets #294

merged 3 commits into from
May 4, 2021

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Nov 27, 2020 •
edited
Loading

based on PR #284 has been merged
NB: {ae m, P} notation broken, to be fixed by PR #295 , which has been merged
TODO: rebase DONE

@affeldt-aist affeldt-aist changed the base branch from master to measure_20201117 November 27, 2020 12:32
@affeldt-aist affeldt-aist marked this pull request as draft November 27, 2020 12:32
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from d028edc to c052c73 Compare November 27, 2020 13:29
@affeldt-aist affeldt-aist changed the base branch from measure_20201117 to master November 27, 2020 13:29
@affeldt-aist affeldt-aist mentioned this pull request Nov 27, 2020
Closed
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from c052c73 to cb68775 Compare November 28, 2020 07:24
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from 1aa7ea5 to ef18a61 Compare December 9, 2020 04:53
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from 4c29806 to 0eaabe8 Compare December 21, 2020 06:47
@CohenCyril CohenCyril mentioned this pull request Jan 12, 2021
Closed
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from 0eaabe8 to e42e4d1 Compare February 19, 2021 03:20
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from e42e4d1 to e076a4b Compare March 10, 2021 16:04
@affeldt-aist
Copy link
Member Author

Can we merge this?
I understand that the two files introduced by this PR are not perfect but they are useful since
they support the construction of Lebesgue measure. Moreover, we can expect substantial
improvements in the mid-term about csum (wip). Otoh, proper support of finType and countType
in cardinality.v are likely to take more time.
I therefore marked these files clearly as WIP in their headers (and explained why) and propose
to merge this PR now (after squashing a bit) and produce issues about improving them.
We can then go on using them actively and improve them more efficiently. @CohenCyril @strub

@affeldt-aist affeldt-aist marked this pull request as ready for review March 19, 2021 07:53
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch 2 times, most recently from bf0686f to e0bd633 Compare March 26, 2021 02:58
CohenCyril
CohenCyril reviewed Mar 26, 2021
View reviewed changes
theories/cardinality.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

following the discussion we had about PR #311 we should maybe take fer, etc. out of this PR and put them back to integral_sketch for the time being, right? @CohenCyril

@affeldt-aist
Copy link
Member Author

following the discussion we had about PR #311 we should maybe take fer, etc. out of this PR and put them back to integral_sketch for the time being, right? @CohenCyril

Actually, maybe the whole section funpos...

CohenCyril
CohenCyril reviewed Mar 31, 2021
View reviewed changes
theories/csum.v Outdated Show resolved Hide resolved
@CohenCyril
Copy link
Member

following the discussion we had about PR #311 we should maybe take fer, etc. out of this PR and put them back to integral_sketch for the time being, right? @CohenCyril

Actually, maybe the whole section funpos...

sure

@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from b75e9c8 to 7e068a9 Compare April 1, 2021 04:14
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch 2 times, most recently from 4f737af to 9cfa950 Compare April 25, 2021 10:03
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from 9cfa950 to 0134603 Compare April 30, 2021 05:19
affeldt-aist and others added 3 commits May 3, 2021 20:19
@affeldt-aist
sums over classical sets
b8641e4 
- contains an account of cardinality properties of classical sets (wip)
- include review and fixes by Cyril following realseq meetings
- originally motivated by the formalization of measure theory
@strub @affeldt-aist
big_setU1 -> big_fsetU1
40f77a6
@affeldt-aist
documentation and cleaning
71b3501 
- set_finite is defined with fset
@affeldt-aist affeldt-aist force-pushed the sums_over_general_sets branch from 7ced0dd to 71b3501 Compare May 3, 2021 12:55
@CohenCyril CohenCyril merged commit 8a8036f into master May 4, 2021
@CohenCyril CohenCyril deleted the sums_over_general_sets branch May 4, 2021 15:06
@affeldt-aist affeldt-aist mentioned this pull request May 12, 2021
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@affeldt-aist @CohenCyril @strub