|
1 | 1 | # OpenGA Conventions |
2 | 2 |
|
3 | | -Canonical conventions for the mathematical objects in OpenGALib. Each entry cites the textbook source. **Conventions are non-negotiable once anchored** — disagreements are answered by citation, not by re-argument. The Lean source is authoritative when prose and code disagree. |
| 3 | +Canonical conventions, each with textbook source. **Non-negotiable once anchored** — disagreements are answered by citation. The Lean source is authoritative when prose and code disagree. |
4 | 4 |
|
5 | | ---- |
| 5 | +## Curvature sign |
6 | 6 |
|
7 | | -## Curvature sign convention |
8 | | - |
9 | | -OpenGA uses the **do Carmo** sign convention throughout the Riemannian and Comparison layers: |
| 7 | +OpenGA uses do Carmo's convention throughout Riemannian and Comparison: |
10 | 8 |
|
11 | 9 | $$R(X, Y) Z = \nabla_X \nabla_Y Z - \nabla_Y \nabla_X Z - \nabla_{[X, Y]} Z.$$ |
12 | 10 |
|
13 | | -Ricci curvature is the trace of $R(\,\cdot\,, Y) Z$ in its first slot; sectional curvature of a 2-plane spanned by $X, Y$ is |
| 11 | +Ricci is the trace of $R(\,\cdot\,, Y) Z$ in its first slot; sectional curvature of the 2-plane spanned by $X, Y$ is |
14 | 12 |
|
15 | 13 | $$K(X, Y) = \frac{\langle R(X, Y) Y, X \rangle}{\langle X, X \rangle \langle Y, Y \rangle - \langle X, Y \rangle^2}.$$ |
16 | 14 |
|
17 | | -Ground truth: do Carmo, *Riemannian Geometry*, Ch. 4 §2 (definition of $R$), Ch. 4 §3 (Ricci and sectional curvatures). This is the convention used by Petersen, Cheeger–Ebin, and the majority of the geometric-analysis literature. |
| 15 | +Ground truth: do Carmo, *Riemannian Geometry*, Ch. 4 §2–§3. Same convention as Petersen and Cheeger–Ebin. |
18 | 16 |
|
19 | 17 | Implementation: `OpenGALib/Riemannian/Curvature/RiemannCurvature.lean`. |
20 | 18 |
|
21 | | ---- |
22 | | - |
23 | 19 | ## Length functional |
24 | 20 |
|
25 | | -The length of a continuous path in a pseudo-extended-metric space is the metric-side total variation: |
| 21 | +Length of a continuous path in a pseudo-extended-metric space is the metric-side total variation: |
26 | 22 |
|
27 | 23 | $$\operatorname{pathLength}(\gamma) := \operatorname{eVariationOn}(\gamma, [0, 1]).$$ |
28 | 24 |
|
29 | | -Ground truth: Burago–Burago–Ivanov, *A Course in Metric Geometry*, §2.1. |
30 | | - |
31 | | -This is OpenGA's canonical "length" primitive. It does not reference any smooth structure on the target space, so it applies uniformly to metric spaces, Riemannian manifolds (via the `OpenGALib/Bridges/RiemannianToLength` bridge), Alexandrov spaces, and limits of these. |
32 | | - |
33 | | -Implementation: `OpenGALib.pathLength` in `OpenGALib/MetricGeometry/LengthSpace.lean`, wrapping Mathlib's `eVariationOn`. |
| 25 | +Ground truth: Burago–Burago–Ivanov §2.1. |
34 | 26 |
|
35 | | -The Mathlib tangent-integral length `Manifold.pathELength` (used inside `IsRiemannianManifold`) is a *separate* concept and lives only at the Riemannian boundary. Equality of the two on `C¹` paths over Riemannian manifolds is the content of the `IsRiemannianManifold.toLengthSpace` bridge. |
| 27 | +Applies uniformly to metric spaces, Riemannian manifolds (via `Bridges/RiemannianToLength`), Alexandrov spaces, and limits. The Mathlib tangent-integral length `Manifold.pathELength` (used inside `IsRiemannianManifold`) is a *separate* concept; equality on `C¹` paths is the content of `IsRiemannianManifold.toLengthSpace`. |
36 | 28 |
|
37 | | ---- |
| 29 | +Implementation: `OpenGALib.pathLength` in `OpenGALib/MetricGeometry/LengthSpace.lean`, wrapping `eVariationOn`. |
38 | 30 |
|
39 | 31 | ## Geodesic existence |
40 | 32 |
|
41 | | -A `GeodesicSpace` is a length space in which the path-length infimum is attained between every pair of points. The class only asserts existence — neither uniqueness nor regularity is part of the OpenGA definition. |
| 33 | +`GeodesicSpace` = length space in which the path-length infimum is attained between every pair of points. Existence only — neither uniqueness nor regularity is part of the definition. |
42 | 34 |
|
43 | | -Ground truth: Burago–Burago–Ivanov §2.5.5. |
44 | | - |
45 | | -The Hopf–Rinow theorem (complete Riemannian manifolds are geodesic spaces) belongs to Layer 3a; Layer 1 is metric-only. |
| 35 | +Ground truth: Burago–Burago–Ivanov §2.5.5. Hopf–Rinow (complete Riemannian ⇒ geodesic) belongs to Layer 3a; Layer 1 is metric-only. |
46 | 36 |
|
47 | 37 | Implementation: `OpenGALib.GeodesicSpace` in `OpenGALib/MetricGeometry/GeodesicSpace.lean`. |
48 | 38 |
|
49 | | ---- |
50 | | - |
51 | 39 | ## Metric measure space |
52 | 40 |
|
53 | | -A `MetricMeasureSpace M` is a `structure` carrying a `PseudoEMetricSpace M` together with a `MeasureTheory.Measure M`. The metric and measure are stored as data (not as typeclasses) so a single carrier may host multiple metric-measure structures. |
54 | | - |
55 | | -Ground truth: Gromov, *Metric Structures for Riemannian and Non-Riemannian Spaces*, §3¹⁄₂.5 (mm-spaces); Burago–Burago–Ivanov §1.7. |
| 41 | +`MetricMeasureSpace M` = `structure` carrying a `PseudoEMetricSpace M` together with a `MeasureTheory.Measure M`. Both stored as data (not typeclasses), so a single carrier may host multiple metric-measure structures. No regularity / σ-finiteness / Radon hypotheses baked in — added at the use site, matching Mathlib's `MeasureTheory.Measure` discipline. |
56 | 42 |
|
57 | | -No regularity / σ-finiteness / Radon hypotheses are baked into the structure. Stronger hypotheses are added at the use site, matching Mathlib's `MeasureTheory.Measure` discipline. |
| 43 | +Ground truth: Gromov §3¹⁄₂.5 (mm-spaces); Burago–Burago–Ivanov §1.7. |
58 | 44 |
|
59 | 45 | Implementation: `MetricMeasureSpace` in `OpenGALib/MetricGeometry/MetricMeasureSpace.lean`. |
0 commit comments