Formalization techniques for asymptotic reasoning in classical analysis

DOI10.6092/ISSN.1972-5787/8124MaRDI QIDQ5195290zbMATH OpenFDO

Authors Reynald Affeldt, Cyril Cohen, Damien Rouhling

Publication date 18 September 2019

Full work available at URL https://doi.org/10.6092/ISSN.1972-5787/8124

zbMATH Keywords

Bachmann-Landau notationsclassical analysisCoqformal proofs

Mathematics Subject Classification ID

Foundations: limits and generalizations, elementary topology of the line (26A03) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Verified Real Asymptotics in Isabelle/HOL
• Formalization of real analysis: a survey of proof assistants and libraries
• scientific article; zbMATH DE number 1670741
• A heuristic prover for elementary analysis in \textit{Theorema}
• scientific article; zbMATH DE number 991409

Cites work

• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• A formal proof in Coq of Lasalle's invariance principle
• A Modular Formalisation of Finite Group Theory
• An introduction to small scale reflection in Coq
• Automated Reasoning
• Canonical structures for the working Coq user
• Construction of real algebraic numbers in Coq
• Coquelicot: a user-friendly library of real analysis for Coq
• Formalization techniques for asymptotic reasoning in classical analysis
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 192934 (Why is no real title available?)
• Packaging Mathematical Structures
• Proving divide and conquer complexities in Isabelle/HOL
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cited in

(13)

• Computable analysis and notions of continuity in \textsc{Coq}
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Formalization techniques for asymptotic reasoning in classical analysis
• A formal proof of the irrationality of (3)
• Nine Chapters of Analytic Number Theory in Isabelle/HOL.
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• Measure construction by extension in dependent type theory with application to integration
• Formally-verified round-off error analysis of Runge-Kutta methods
• Computable analysis for verified exact real computation
• A comprehensive overview of the Lebesgue differentiation theorem in Coq
• Taming differentiable logics with Coq formalisation
• Formalizing concentration inequalities in Rocq: infrastructure and automation

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Coq/SSReflect
• Coquelicot
• GitHub

This page was built for publication: Formalization techniques for asymptotic reasoning in classical analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195290)