Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 56 min ago
PreprintarXiv licencearXiv

Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric

  • Gabriella Clemente
  • Hugo Herbelin
  • Carlos Simpson
Open at sourcePDFDOICite

Abstract

We introduce a synthetic framework for doing local Riemannian geometry that is influenced by a reverse-engineering method for formalizing in Rocq. These new perspectives and techniques lead to a synthetic Taylor formula for a Riemannian metric in normal coordinates, which is the main contribution of this work.

Related

  1. A smooth Riemannian metric on an arbitrary product of spheres with Bernoulli geodesic flow
    Keith Burns, Tomas Gedeon, Yuping Ruan
    arXivPreprintarXiv licenceFull textDynamical systemsGeometry & topologyarXiv
  2. Convergence of the Sinkhorn Riemannian metric for finitely supported measures
    Gilles Mordant, Liane Xu
    arXivPreprintCC BY 4.0Full textOptimisation & controlarXiv
  3. Metric-Free Riemannian Optimization
    Jonas Püschel
    arXivPreprintCC BY 4.0Full textNumerical analysis & scientific computingOptimisation & controlarXiv
  4. Distributional Fractional Taylor Series and Interpretation of the Fractal and Number-Theoretic Explicit Formulas
    Michel L. Lapidus, Matthew Overduin
    arXivPreprintCC BY 4.0Full textMathematical physicsarXiv
  5. A Cartan geometry from a correspondence space in Riemannian geometry
    Rodrigo Morón, Francisco J. Palomo
    arXivPreprintarXiv licenceFull textGeometry & topologyarXiv

Cite

BibTeXRIS
BibTeX
@misc{clemente2026retrosynthetic,
  title = {{Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric}},
  author = {Gabriella Clemente and Hugo Herbelin and Carlos Simpson},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.20127},
  eprint = {2609.20127},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.20127},
}
RIS
TY  - UNPB
TI  - Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric
AU  - Gabriella Clemente
AU  - Hugo Herbelin
AU  - Carlos Simpson
PY  - 2026
DA  - 2026/09/17
PB  - arXiv
DO  - 10.48550/arxiv.2609.20127
UR  - https://arxiv.org/abs/2609.20127
AB  - We introduce a synthetic framework for doing local Riemannian geometry that is influenced by a reverse-engineering method for formalizing in Rocq. These new perspectives and techniques lead to a synthetic Taylor formula for a Riemannian metric in normal coordinates, which is the main contribution of this work.
ER  -