18 search results for "tag:"category:Mathematics/Real Calculus and Topology""
-
coq-actuary
No documentation
Formalization of actuarial mathematics in Coq2.6MITUsed by 0 other packages11 Nov 2023 -
coq-coqtail
No documentation
Library of mathematical theorems tools proved inside the Coq8.20LGPL-3.0-onlyUsed by 0 other packages14 Jul 2024 -
coq-coquelicot
No documentation
A Coq formalization of real analysis compatible with the stard library3.4.4LGPL-3.0-or-laterUsed by 10 other packages30 Jul 2025 -
coq-corn
No documentation
The Coq Constructive Repository at Nijmegen9.0.0GPL-2.0Used by 0 other packages29 Aug 2025 -
coq-fourcolor-reals
No documentation
Interface for real numbers used in the Four Color Theorem1.4.2CECILL-BUsed by 3 other packages13 Nov 2025 -
coq-hol-light
No documentation
HOL-Light library in Coqlogpath:HOLLight date:2025-01-20 category:Mathematics/Arithmetic Number Theory/Miscellaneous category:Mathematics/Real Numbers category:Mathematics/Real Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendental3.0.0CeCILL-2.1Used by 0 other packages21 Jan 2025 -
coq-improper-integrals
No documentation
Additions to the coquelicot library for hling improper integrals0.1.0MITUsed by 0 other packages19 Apr 2018 -
coq-interval
No documentation
A Coq tactic for proving bounds on real-valued expressions automatically4.11.4CeCILL-CUsed by 8 other packages23 Feb 2026 -
coq-num-analysis
No documentation
Numerical Analysis in Coq1.0.0LGPL-3.0-or-laterUsed by 0 other packages06 Sep 2022 -
coq-pi-agm
No documentation
Computing thouss or millions of digits of PI with arithmetic-geometric means1.2.8CECILL-BUsed by 0 other packages20 Jun 2024 -
coq-quantumlib
No documentation
Coq library for reasoning about quantum programs1.8.0MITUsed by 0 other packages14 Oct 2025 -
coq-topology
No documentation
General topology in Coq10.2.0LGPL-2.1-or-laterUsed by 0 other packages21 Aug 2023 -
rocq-mathcomp-analysis
No documentation
An analysis library for mathematical componentscategory:Mathematics/Real Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Lau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis1.16.0CECILL-CUsed by 2 other packages16 Mar 2026 -
rocq-mathcomp-analysis-stdlib
No documentation
A library to link real numbers from mathematical components Stdlib1.16.0CECILL-CUsed by 1 other packages16 Mar 2026 -
rocq-num-analysis-fem
No documentation
The finite element method2.2.0LGPL-3.0-or-laterUsed by 1 other packages13 Mar 2026 -
rocq-num-analysis-lax-milgram
No documentation
Lax-Milgram theorem2.2.0LGPL-3.0-or-laterUsed by 1 other packages13 Mar 2026 -
rocq-num-analysis-lebesgue
No documentation
Lebesgue integralcategory:Mathematics/Real Topology date:2026-03 logpath:NumAnalysis.Lebesgue keyword:sigma-algebra keyword:monotone class theorem keyword:Dynkin pi-lambda theorem keyword:measure theory keyword:Lebesgue measure keyword:simple function keyword:adapted sequence keyword:Beppo Levi (monotone convergence) theorem keyword:Fatou lemma keyword:Lebesgue (dominated convergence) theorem keyword:Lebesgue induction principle keyword:Tonelli theorem keyword:Bochner integral2.2.0LGPL-3.0-or-laterUsed by 1 other packages13 Mar 2026 -
rocq-pi-agm
No documentation
Computing thouss or millions of digits of PI with arithmetic-geometric means1.2.9CECILL-BUsed by 0 other packages14 Aug 2025