Skip to content

change of sigma-algebra#2016

Open
affeldt-aist wants to merge 3 commits into
math-comp:masterfrom
affeldt-aist:measurableTypeR
Open

change of sigma-algebra#2016
affeldt-aist wants to merge 3 commits into
math-comp:masterfrom
affeldt-aist:measurableTypeR

Conversation

@affeldt-aist

@affeldt-aist affeldt-aist commented Jul 2, 2026

Copy link
Copy Markdown
Member
Motivation for this change

This PR proposes a change of default sigma-algebra for real numbers (from ocitv to open sets) so that @Brixfoly can easily further generalize to normed modules.

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist changed the title broken change of sigma-algebra Jul 3, 2026
Co-authored-by: adjevahi <arthur.djevahirdjian@ens-lyon.fr>
Co-authored-by: Alessandro Bruni <brun@itu.dk>
@affeldt-aist

Copy link
Copy Markdown
Member Author

@Brixfoly @hoheinzollern this PR should be almost clean and ready to support experiments with normedModType

@affeldt-aist
affeldt-aist requested a review from CohenCyril July 7, 2026 13:33
@affeldt-aist

Copy link
Copy Markdown
Member Author

PR #2017 provides evidence that this current PR (2016) is useful to generalize to sigma-algebras over normed modules.

@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Jul 16, 2026
@affeldt-aist affeldt-aist modified the milestones: 1.18.0, 1.17.0 Jul 16, 2026
@affeldt-aist

affeldt-aist commented Jul 16, 2026

Copy link
Copy Markdown
Member Author

Since it has been shown useful for PR #2017 (and therefore tested), written by three people, it does not break the CI, we will merge soon unless somebody objects.

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.

1 participant