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

sigma-rings #1222

Merged
merged 15 commits into from
Jun 5, 2024
Merged

sigma-rings #1222

merged 15 commits into from
Jun 5, 2024

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented May 14, 2024

This PR introduces the mathematical structure of sigma-rings and
generalizes accordingly several definitions and lemmas.

Not all opportunities for generalization have been exploited yet.

  • better names for
    • AlgebraOfSets_isMeasurable (became hasMeasurableCountableUnion)
    • bigcap_measurable' (became bigcap_measurableType)

Co-authored-by: @TheoWinterhalter
Co-authored-by: @JeremyDubut
Co-authored-by: @AkihisaYamada

Motivation for this change
Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label May 14, 2024
@affeldt-aist affeldt-aist added this to the 1.3.0 milestone May 14, 2024
@affeldt-aist affeldt-aist changed the title sigma-rings (wip) sigma-rings May 15, 2024
@affeldt-aist affeldt-aist force-pushed the sigma_ring branch 2 times, most recently from ba76f02 to 197278a Compare May 16, 2024 00:37
Copy link

@TheoWinterhalter TheoWinterhalter left a comment

Choose a reason for hiding this comment

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

Only a few stylistic remarks/questions. Otherwise looks good to me. :)

CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist modified the milestones: 1.3.0, 1.2.0 May 20, 2024
Copy link

@TheoWinterhalter TheoWinterhalter left a comment

Choose a reason for hiding this comment

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

Some comments about naming, but I'm not an expert in mathcomp naming conventions.

theories/lebesgue_integral.v Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Outdated Show resolved Hide resolved
theories/measure.v Show resolved Hide resolved
theories/sequences.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist force-pushed the sigma_ring branch 2 times, most recently from cc71347 to ccd9191 Compare June 3, 2024 14:54
Copy link
Collaborator

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

Minor comments

classical/classical_sets.v Outdated Show resolved Hide resolved
classical/classical_sets.v Outdated Show resolved Hide resolved
classical/classical_sets.v Outdated Show resolved Hide resolved
classical/classical_sets.v Outdated Show resolved Hide resolved
CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
theories/measure.v Show resolved Hide resolved
theories/measure.v Show resolved Hide resolved
theories/measure.v Show resolved Hide resolved
CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

Minor comments

All very well spotted! Many thanks.

@affeldt-aist affeldt-aist merged commit 8d95107 into math-comp:master Jun 5, 2024
16 checks passed
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Jun 20, 2024
sigma-rings

Co-authored-by: @TheoWinterhalter
Co-authored-by: @JeremyDubut
Co-authored-by: @AkihisaYamada
Co-authored-by: @proux01
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.

3 participants