List view

metric structure

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 1589

#1589 In math-comp/analysis;

· affeldt-aist opened on Apr 24, 2025

generalize <code>cvg_nbhsP</code> in <code>realfun.v</code> to any metric space

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

Status: Open.

#1437 In math-comp/analysis;

· affeldt-aist opened on Dec 17, 2024

naming and definition of <code>monotonous</code>

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

Status: Open.

#1133 In math-comp/analysis;

· affeldt-aist opened on Jan 7, 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

Normed vector types, infinite norm, norm equivalence thm, continuity …

Status: Open (in progress).

math-comp/analysisnumber 1718

#1718 In math-comp/analysis;

· Tragicus opened on Sep 16, 2025

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

<code>R^o</code> type constraints in <code>ln_concave</code>

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

help 🆘This author/reviewer of this issue/PR needs external helpThis author/reviewer of this issue/PR needs external help

Status: Open (in progress).

math-comp/analysisnumber 1010

#1010 In math-comp/analysis;

· affeldt-aist opened on Aug 11, 2023

<code>Lnorm0</code>

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

Double-check local notations in <code>hoelder.v</code>

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

use of deprecated options of Rocqnavi to generate the documentation

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

Status: Open.

#1749 In math-comp/analysis;

· affeldt-aist opened on Nov 7, 2025

Bolzano weierstrass

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 1787

#1787 In math-comp/analysis;

· affeldt-aist opened on Dec 4, 2025

fixes #1804

Status: Open (in progress).

math-comp/analysisnumber 1806

#1806 In math-comp/analysis;

· affeldt-aist opened on Dec 22, 2025