List view

shorten proof about monotonic functions

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1156 In math-comp/analysis;

· affeldt-aist opened on Jan 18, 2024

CPOs (wip)

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Draft (not ready).

math-comp/analysisnumber 1807

#1807 In math-comp/analysis;

· affeldt-aist opened on Dec 22, 2025

move the product measure out of lebesgue_integral_fubini.v

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1554 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 2025

notation for intervals

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#795 In math-comp/analysis;

· affeldt-aist opened on Nov 10, 2022

Should poweR return 0 if the exponent is negative?

Status: Open.

#1401 In math-comp/analysis;

· jmmarulang opened on Nov 18, 2024

conv_gt0 as an instance of PosNum

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1009 In math-comp/analysis;

· affeldt-aist opened on Aug 11, 2023

rm tests initv.v (now interval_inference.v)

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#880 In math-comp/analysis;

· affeldt-aist opened on Mar 15, 2023

Remove bigmaxr from Rstruct.v?

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1739 In math-comp/analysis;

· affeldt-aist opened on Oct 24, 2025

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 / repository

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

question ❓There is an unanswered question hereThere is an unanswered question here

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#68 In math-comp/analysis;

· CohenCyril opened on Apr 10, 2018

improve the interface for the product measure

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1665 In math-comp/analysis;

· affeldt-aist opened on Jul 1, 2025

Near message error

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Open.

#1320 In math-comp/analysis;

· mkerjean opened on Sep 16, 2024

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;

· zstone1 opened on Feb 24, 2022

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;

· zstone1 opened on Feb 24, 2022

potential generalization from realDomainType to numDomainType

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#696 In math-comp/analysis;

· affeldt-aist opened on Jul 13, 2022

Lnorm0

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Open.

#1643 In math-comp/analysis;

· affeldt-aist opened on Jun 19, 2025

variant of measurable_fun_eqr

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1319 In math-comp/analysis;

· affeldt-aist opened on Sep 15, 2024

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 library

Status: Open (in progress).

math-comp/analysisnumber 1674

#1674 In math-comp/analysis;

· IshiguroYoshihiro opened on Jul 4, 2025

Double-check local notations in hoelder.v

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Open.

#1644 In math-comp/analysis;

· affeldt-aist opened on Jun 19, 2025

Organization of the files in lebesgue_integral_theory

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1549 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 2025

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 / repository

Status: Open.

#151 In math-comp/analysis;

· CohenCyril opened on Sep 17, 2019

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 library

Status: Open.

#1821 In math-comp/analysis;

· affeldt-aist opened on Jan 15, 2026

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 library

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#102 In math-comp/analysis;

· CohenCyril opened on Sep 14, 2018

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 library

Status: Open.

#2 In math-comp/analysis;

· CohenCyril opened on Jan 11, 2018

introduce a generic closed_under definition

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1871 In math-comp/analysis;

· affeldt-aist opened on Mar 3, 2026

generalize the definition of filter

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1872 In math-comp/analysis;

· affeldt-aist opened on Mar 3, 2026