12 search results for "tag:"category:Mathematics/Real Calculus and Topology""

Showing 1 - 12
  1. coq-actuary

    No documentation

    Formalization of actuarial mathematics in Coq
    category:Mathematics/Real Calculus and Topology keyword:present value keyword:life tables keyword:annuities keyword:reserves keyword:actuarial mathematics logpath:Actuary date:2023-11-11
    Yosuke Ito
    2.6
    MIT
    Used by 0 other packages
    11 Nov 2023
  2. coq-coqtail

    No documentation

    Library of mathematical theorems and tools proved inside the Coq
    category:Mathematics/Real Calculus and Topology keyword:real analysis keyword:complex analysis date:2024-07-13 logpath:Coqtail
    Guillaume Allais Sylvain Dailler Hugo Férée Jean-Marie Madiot Pierre-Marie Pédrot et al.
    8.20
    LGPL-3.0-only
    Used by 0 other packages
    14 Jul 2024
  3. coq-coquelicot

    No documentation

    A Coq formalization of real analysis compatible with the standard library
    keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology logpath:Coquelicot date:2024-07-04
    Sylvie Boldo <sylvie.boldo@inria.fr> Catherine Lelay <catherine.lelay@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    3.4.2
    LGPL-3.0-or-later
    Used by 7 other packages
    04 Jul 2024
  4. coq-corn

    No documentation

    The Coq Constructive Repository at Nijmegen
    category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology category:Mathematics/Exact Real computation keyword:constructive mathematics keyword:algebra keyword:real calculus keyword:real numbers keyword:Fundamental Theorem of Algebra logpath:CoRN date:2024-04-23
    Evgeny Makarov Robbert Krebbers Eelis van der Weegen Bas Spitters Jelle Herold et al.
    8.19.0
    GPL-2.0
    Used by 0 other packages
    23 Apr 2024
  5. coq-fourcolor-reals

    No documentation

    Interface for real numbers used in the Four Color Theorem
    category:Mathematics/Real Calculus and Topology keyword:real numbers logpath:fourcolor.reals date:2024-11-15
    Georges Gonthier
    1.4.0
    CECILL-B
    Used by 2 other packages
    15 Nov 2024
  6. coq-improper-integrals

    No documentation

    Additions to the coquelicot library for handling improper integrals
    keyword:real analysis category:Mathematics/Real Calculus and Topology
    Yves Bertot <yves.bertot@inria.fr>
    0.1.0
    MIT
    Used by 0 other packages
    19 Apr 2018
  7. coq-interval

    No documentation

    A Coq tactic for proving bounds on real-valued expressions automatically
    keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2024-10-21
    Guillaume Melquiond <guillaume.melquiond@inria.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr> Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>
    4.11.1
    CeCILL-C
    Used by 7 other packages
    22 Oct 2024
  8. coq-mathcomp-analysis

    No documentation

    An analysis library for mathematical components
    category:Mathematics/Real Calculus and Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Landau 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.analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.8.0
    CECILL-C
    Used by 7 other packages
    19 Dec 2024
  9. coq-num-analysis

    No documentation

    Numerical Analysis in Coq
    category:Mathematics/Real Calculus and Topology keyword:real analysis keyword:Lax-Milgram theorem keyword:Lebesgue integration keyword:Tonelli theorem keyword:Bochner integration logpath:Lebesgue logpath:LM date:2022-09-06
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    1.0.0
    LGPL-3.0-or-later
    Used by 0 other packages
    06 Sep 2022
  10. coq-pi-agm

    No documentation

    Computing thousands or millions of digits of PI with arithmetic-geometric means
    keyword:real analysis keyword:pi category:Mathematics/Real Calculus and Topology logpath:agm date:2020-06-23
    Yves Bertot <yves.bertot@inria.fr>
    1.2.8
    CECILL-B
    Used by 0 other packages
    20 Jun 2024
  11. coq-quantumlib

    No documentation

    Coq library for reasoning about quantum programs
    keyword:quantum keyword:qwire keyword:sqir keyword:matrices keyword:vectors keyword:linear algebra keyword:complex numbers category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology date:2024-05-27 logpath:QuantumLib
    inQWIRE
    1.5.1
    MIT
    Used by 0 other packages
    29 Jul 2024
  12. coq-topology

    No documentation

    General topology in Coq
    category:Mathematics/Real Calculus and Topology date:2023-08-18 keyword:topology keyword:filters keyword:nets keyword:metric spaces keyword:real analysis keyword:Urysohn's lemma keyword:Tietze extension theorem logpath:Topology
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 0 other packages
    21 Aug 2023