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

Radon-Nikodym chain rule #1083

Merged
merged 13 commits into from
Jan 6, 2024
Merged

Radon-Nikodym chain rule #1083

merged 13 commits into from
Jan 6, 2024

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Nov 9, 2023 •
edited
Loading

Motivation for this change

Need a last pass of cleaning.

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Compatibility with MathComp 2.0
  • I added the label TODO: HB port to make sure someone ports this PR to
    the hierarchy-builder branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Nov 9, 2023
@affeldt-aist affeldt-aist added this to the 0.6.6 milestone Nov 9, 2023
@affeldt-aist
Copy link
Member Author

@IshiguroYoshihiro The CI fails with Coq 8.14, 8.15, that may just be a matter of adding a [the content/measure/charge _ _ of _] somewhere. Don't hesitate to create an opam switch with an old Coq version.

@affeldt-aist affeldt-aist modified the milestones: 0.6.6, 0.6.7 Nov 11, 2023
@IshiguroYoshihiro IshiguroYoshihiro mentioned this pull request Dec 1, 2023
Merged
3 tasks
IshiguroYoshihiro and others added 5 commits December 21, 2023 15:56
@IshiguroYoshihiro @affeldt-aist
Radon_Nikodym chain rule
4bddc61 
Co-authored-by: IshiguroYoshihiro <103252572+IshiguroYoshihiro@users.noreply.github.com>
@IshiguroYoshihiro @affeldt-aist
fix
f849d9a
@IshiguroYoshihiro @affeldt-aist
add changelog and generalize
ad35771
@IshiguroYoshihiro @affeldt-aist
add max_cvg_0_cvg_0
47aa954
@affeldt-aist
fix
5881fe1
Tragicus
Tragicus reviewed Dec 22, 2023
View reviewed changes
Copy link
Collaborator

@Tragicus Tragicus left a comment

Choose a reason for hiding this comment

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

Here is a first review, there should be a second one afterwards (potentially after this one is resolved). It has quite a lot of uninteresting golfing, but I did not dare commit anything (@affeldt-aist ?).

CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
CHANGELOG_UNRELEASED.md Show resolved Hide resolved
CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
CHANGELOG_UNRELEASED.md Show resolved Hide resolved
theories/charge.v Outdated Show resolved Hide resolved
theories/sequences.v Outdated Show resolved Hide resolved
theories/measure.v Show resolved Hide resolved
theories/sequences.v Outdated Show resolved Hide resolved
theories/charge.v Outdated Show resolved Hide resolved
theories/charge.v Outdated Show resolved Hide resolved
@affeldt-aist @Tragicus
addressing comments by Quentin (wip)
444560a 
Co-authored-by: Tragicus <96025499+Tragicus@users.noreply.github.com>
@affeldt-aist
Copy link
Member Author

Here is a first review, there should be a second one afterwards (potentially after this one is resolved). It has quite a lot of uninteresting golfing, but I did not dare commit anything (@affeldt-aist ?).

Thank you very much! I addressed the easiest comments in the last commit and will address the others very soon.

@affeldt-aist
Copy link
Member Author

Here is a first review, there should be a second one afterwards (potentially after this one is resolved). It has quite a lot of uninteresting golfing, but I did not dare commit anything (@affeldt-aist ?).

Thank you very much! I addressed the easiest comments in the last commit and will address the others very soon.

That should be it.

@affeldt-aist
Copy link
Member Author

Thank you very much! I addressed the easiest comments in the last commit and will address the others very soon.

That should be it.

@Tragicus Do you think it can be merged now?

Tragicus
Tragicus approved these changes Jan 5, 2024
View reviewed changes
Copy link
Collaborator

@Tragicus Tragicus left a comment

Choose a reason for hiding this comment

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

I had another quick read through, it looks good to me.

theories/charge.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist merged commit 74b4d4f into math-comp:master Jan 6, 2024
26 of 30 checks passed
affeldt-aist added a commit to affeldt-aist/analysis that referenced this pull request Jan 9, 2024
@affeldt-aist
Radon-Nikodym chain rule (math-comp#1083)
d369429 
* Radon_Nikodym chain rule
---------
Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
Co-authored-by: IshiguroYoshihiro <103252572+IshiguroYoshihiro@users.noreply.github.com>
Co-authored-by: Tragicus <96025499+Tragicus@users.noreply.github.com>
proux01 pushed a commit that referenced this pull request Jan 9, 2024
@affeldt-aist @proux01
Radon-Nikodym chain rule (#1083)
aed4ed5 
* Radon_Nikodym chain rule
---------
Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
Co-authored-by: IshiguroYoshihiro <103252572+IshiguroYoshihiro@users.noreply.github.com>
Co-authored-by: Tragicus <96025499+Tragicus@users.noreply.github.com>
@proux01 proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jan 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Tragicus Tragicus Tragicus approved these changes

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

Successfully merging this pull request may close these issues.
4 participants
@affeldt-aist @Tragicus @proux01 @IshiguroYoshihiro