Skip to content

Pull requests: math-comp/analysis

New pull request New
82 Open 1,420 Closed
82 Open 1,420 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 reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Counting distribution
#2064 opened Jul 29, 2026 by lyonel2017 Contributor Loading…
2 tasks
1.18.0
Counting esum
#2063 opened Jul 29, 2026 by lyonel2017 Contributor Loading…
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 lyonel2017 Contributor Loading…
2 tasks
1.18.0
10
Proof of interchange_psum using esum
#2061 opened Jul 29, 2026 by lyonel2017 Contributor Loading…
2 tasks
1.18.0
5
is_derive_trmx
#2060 opened Jul 29, 2026 by yosakaon Contributor Loading…
2 tasks
fixes #1968 (finI_from) documentation 📝 This issue/PR is about documentation of the library / repository
#2056 opened Jul 28, 2026 by affeldt-aist Member Loading…
2 tasks done
1.17.0
1
2
experimental_reals: make psumZ rewrite direction explicit
#2054 opened Jul 28, 2026 by JasonGross • Draft
deflists docs
#2052 opened Jul 24, 2026 by hoheinzollern Member • Draft
2 tasks
Fix some notation levels w.r.t. Corelib
#2042 opened Jul 19, 2026 by hivert Member Loading…
1
4
is_derive_mulmx enhancement ✨ This issue/PR is about adding new features enhancing the library
#2040 opened Jul 16, 2026 by yosakaon Contributor Loading…
1 of 2 tasks
1.17.0
2
Continuity of Rintegral in its bounds
#2038 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 5 tasks
1.18.0
Rintegral manipulation lemmas
#2037 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 tasks done
1.18.0
lemmas around exponential growth
#2036 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 6 tasks
1.18.0
new series convergence criteria
#2035 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 3 tasks
1.18.0
L'Hôpital's rule for ∞/∞ forms
#2034 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 3 tasks
1.18.0
derivable_oo_LRcontinuous stability lemmas
#2033 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 3 tasks
1.18.0
Derivative limit theorem
#2032 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 4 tasks
1.18.0
normed type neighborhood lemmas
#2030 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 of 4 tasks
1.18.0
normed module identity convergence lemmas
#2029 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 tasks done
8
Lemmas for functions bounded on a range
#2028 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 tasks done
1.18.0
New topology lemmas
#2027 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
2 tasks done
new derive.v lemmas
#2026 opened Jul 15, 2026 by amolinamounier Collaborator Loading…
3 of 5 tasks
1.18.0
Hausdorff ctvs
#2022 opened Jul 8, 2026 by mkerjean Collaborator • Draft
2 tasks
variants of {sup,inf}_le enhancement ✨ This issue/PR is about adding new features enhancing the library
#2021 opened Jul 8, 2026 by affeldt-aist Member Loading…
1 task done
1.17.0
4
Measurable type for normed modules (generalizes PR#2016)
#2017 opened Jul 7, 2026 by Brixfoly Contributor Loading…
2 tasks
ProTip! Filter pull requests by the default branch with base:master.