-
Notifications
You must be signed in to change notification settings - Fork 70
OpenJul 8, 2026
Overdue by 2 month(s)
•Due by May 8, 2026
•Last updated 39% complete
List view
0 of 46 selected 0 issues of 46 selected
move the product measure out of
lebesgue_integral_fubini.vrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1554 In math-comp/analysis;conv_gt0as an instance ofPosNumenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1009 In math-comp/analysis;rm tests in
itv.v(nowinterval_inference.v)documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repositoryenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#880 In math-comp/analysis;Remove
bigmaxrfromRstruct.v?renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1739 In math-comp/analysis;Have notations for deriving and derivability
documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repositoryenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryquestion ❓There is an unanswered question hereThere is an unanswered question hererenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#68 In math-comp/analysis;improve the interface for the product measure
wish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1665 In math-comp/analysis;Near message error
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryquestion ❓There is an unanswered question hereThere is an unanswered question hereStatus: Open.#1320 In math-comp/analysis;Near Notation can't solve
g \is_near F"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"Status: Open.#549 In math-comp/analysis;near notation inference issues
"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"Status: Open.#548 In math-comp/analysis;potential generalization from
realDomainTypetonumDomainTypeenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#696 In math-comp/analysis;Lnorm0enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryexperiment 🧪This issue/PR is very experimentalThis issue/PR is very experimentalStatus: Open.#1643 In math-comp/analysis;variant of
measurable_fun_eqrwish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1319 In math-comp/analysis;Generalize integration_by_parts
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open (in progress).Double-check local notations in
hoelder.venhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryexperiment 🧪This issue/PR is very experimentalThis issue/PR is very experimentalStatus: Open.#1644 In math-comp/analysis;Organization of the files in
lebesgue_integral_theoryrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1549 In math-comp/analysis;Could we have a nix upgrade documentation somewhere? (@amahboubi)
documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repositoryStatus: Open.#151 In math-comp/analysis;factory for hausdorff + pseudometric => metric
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1821 In math-comp/analysis;Have a spec lemma for big0
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#102 In math-comp/analysis;Fix 'the_* landau notation to improve readability
renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#2 In math-comp/analysis;introduce a generic
closed_underdefinitionrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1871 In math-comp/analysis;generalize the definition of
filterenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1872 In math-comp/analysis;[port back to HB] generalize the trick used to fix the
%Escope issueenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1873 In math-comp/analysis;derive -> differentiable
wish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#304 In math-comp/analysis;Rework landau's documentation and naming convention
documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repositoryrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#103 In math-comp/analysis;Generalize to
l : \bar R?wish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1485 In math-comp/analysis;