Higher order differential calculus in mathlib
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909772436996096 |
|---|---|
| author | Gouëzel, Sébastien |
| author_facet | Gouëzel, Sébastien |
| contents | We report on the higher-order differential calculus library developed inside the Lean mathematical library mathlib. To support a broad range of applications, we depart in several ways from standard textbook definitions: we allow arbitrary fields of scalars, we work with functions defined on domains rather than full spaces, and we integrate analytic functions in the broader scale of smooth functions. These generalizations introduce significant challenges, which we address from both the mathematical and the formalization perspectives. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_04922 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Higher order differential calculus in mathlib Gouëzel, Sébastien Logic in Computer Science We report on the higher-order differential calculus library developed inside the Lean mathematical library mathlib. To support a broad range of applications, we depart in several ways from standard textbook definitions: we allow arbitrary fields of scalars, we work with functions defined on domains rather than full spaces, and we integrate analytic functions in the broader scale of smooth functions. These generalizations introduce significant challenges, which we address from both the mathematical and the formalization perspectives. |
| title | Higher order differential calculus in mathlib |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.04922 |