# Gigli’s characterization of Alexandrov curvature

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Weak Hessian bounds along every geodesic in RCD spaces](../../preprints/Weak-Hessian-bounds-along-every-geodesic-in-RCD-spaces-September-24-2026/weak-hessian-geodesics.pdf)

## Scope

The formalization transfers a weak Hessian upper bound to every prescribed minimizing geodesic in an $\mathrm{RCD}(K,N)$ space with finite $N>1$. If a bounded globally Lipschitz function $F$ has weak Hessian bounded above by $G$ times the metric, where $G$ is bounded and continuous, then every constant-speed geodesic $\gamma:[0,1]\to X$ satisfies $(F\circ\gamma)''\le G(\gamma)\,d(\gamma(0),\gamma(1))^2$ in the distributional sense. Constant geodesics are included. The space is complete and separable with full support and measure finite on bounded sets; compactness and metric nonbranching are not assumed.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Weak Hessian bounds along every geodesic | [WeakHessian.lean](../ComparatorChallenges/WeakHessian.lean) |