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

differentiation under integral #1435

Merged
merged 7 commits into from
Feb 6, 2025
Merged

differentiation under integral #1435

merged 7 commits into from
Feb 6, 2025

Conversation

affeldt-aist
Copy link
Member

Motivation for this change

this can certainly be generalized but this version has already been used to prove the Gauss integral so it is maybe worth having anyway

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 Dec 16, 2024
@affeldt-aist affeldt-aist added this to the 1.8.0 milestone Dec 16, 2024
CohenCyril
CohenCyril reviewed Dec 17, 2024
View reviewed changes
theories/normedtype.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

I have added the gauss integral as an application of differentiation under integral

@affeldt-aist affeldt-aist modified the milestones: 1.8.0, 1.9.0 Dec 18, 2024
@affeldt-aist affeldt-aist force-pushed the ftc_20241217 branch 2 times, most recently from b02f9b6 to c8beda2 Compare January 7, 2025 15:17
@affeldt-aist
Copy link
Member Author

@IshiguroYoshihiro do you have improvements to propose?

@affeldt-aist
Copy link
Member Author

ping? :-)

CohenCyril
CohenCyril reviewed Jan 19, 2025
View reviewed changes
theories/ftc.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

@CohenCyril CI's green

@affeldt-aist
Copy link
Member Author

ah, forgot to put ge0_cvgn_integral in the changelog, one sec

CohenCyril
CohenCyril requested changes Feb 5, 2025
View reviewed changes
Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

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

Wait a sec

@affeldt-aist
Copy link
Member Author

Many thanks for the careful review!

@affeldt-aist affeldt-aist merged commit 3b24356 into math-comp:master Feb 6, 2025
32 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril approved these changes

Assignees
No one assigned
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Milestone
1.9.0
Development

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