Skip to content

Pull requests: math-comp/analysis

New pull requestNew
79 Open 1,426 Closed
79 Open 1,426 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviewsReview requiredApproved reviewChanges requested
Assignee
Filter by who’s assigned
Assigned to nobodyLoading
Sort
Sort by
NewestOldestMost commentedLeast commentedRecently updatedLeast recently updatedBest match
Most reactions
👍👎😄🎉😕❤️🚀👀

Pull requests list

Gaussian-Gaussian conjugate prior (#43) enhancement ✨ This issue/PR is about adding new features enhancing the library
#2073 opened Aug 3, 2026 by affeldt-aistMemberLoading…
2 tasks done
 1.18.0
hint is_derive_mulmx
#2071 opened Jul 31, 2026 by yosakaonContributorLoading…
2 tasks
1
Counting distribution
#2064 opened Jul 29, 2026 by lyonel2017ContributorLoading…
2 tasks
 1.18.0
Counting esum
#2063 opened Jul 29, 2026 by lyonel2017ContributorLoading…
2 tasks
 1.18.0
Add set of lemmas for esum enhancement ✨ This issue/PR is about adding new features enhancing the library
#2062 opened Jul 29, 2026 by lyonel2017ContributorLoading…
2 tasks
 1.18.0
11
Proof of interchange_psum using esum
#2061 opened Jul 29, 2026 by lyonel2017ContributorLoading…
2 tasks
 1.18.0
6
is_derive_trmx
#2060 opened Jul 29, 2026 by yosakaonContributorLoading…
2 tasks
experimental_reals: make psumZ rewrite direction explicit
#2054 opened Jul 28, 2026 by JasonGross • Draft
deflists docs
#2052 opened Jul 24, 2026 by hoheinzollernMember • Draft
2 tasks
Fix some notation levels w.r.t. Corelib
#2042 opened Jul 19, 2026 by hivertMemberLoading…
1
4
Continuity of Rintegral in its bounds
#2038 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 5 tasks
 1.18.0
Rintegral manipulation lemmas
#2037 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 tasks done
 1.18.0
lemmas around exponential growth
#2036 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 6 tasks
 1.18.0
new series convergence criteria
#2035 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 3 tasks
 1.18.0
L'Hôpital's rule for ∞/∞ forms
#2034 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 3 tasks
 1.18.0
derivable_oo_LRcontinuous stability lemmas
#2033 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 3 tasks
 1.18.0
Derivative limit theorem
#2032 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 4 tasks
 1.18.0
normed type neighborhood lemmas
#2030 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 of 4 tasks
 1.18.0
Lemmas for functions bounded on a range
#2028 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 tasks done
 1.18.0
New topology lemmas
#2027 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
2 tasks done
1
new derive.v lemmas
#2026 opened Jul 15, 2026 by amolinamounierCollaboratorLoading…
3 of 5 tasks
 1.18.0
Hausdorff ctvs
#2022 opened Jul 8, 2026 by mkerjeanCollaborator • Draft
2 tasks
Measurable type for normed modules (generalizes PR#2016)
#2017 opened Jul 7, 2026 by BrixfolyContributorLoading…
2 tasks
Topology lemmas
#2014 opened Jul 1, 2026 by BrixfolyContributorLoading…
2 tasks
2
Initial topology induced by a family of functions
#2003 opened Jun 21, 2026 by mkerjeanCollaboratorLoading…
2 tasks done
4
ProTip!no:milestone will show everything without a milestone.