Revision #2473 → #3109 · back to history
modifiedRiemannian manifold (informal)8f489a8ac27e
| Field | From #2473 | To #3109 |
|---|
| note | `IsRiemannianManifold I M` is the Prop-valued typeclass registering the Riemannian-manifold predicate on a manifold equipped with an emetric structure and a Riemannian bundle on its tangent bundle. | `IsRiemannianManifold I M` is Mathlib's Prop-valued predicate registering the Riemannian-manifold structure on a manifold with an emetric structure and a Riemannian bundle on its tangent bundle. |
modifiedRiemannian metric (informal)a54850aeefc7
| Field | From #2473 | To #3109 |
|---|
| note | `ContMDiffRiemannianMetric IB n F E` is a family of inner products on the fibers of a vector bundle varying `C^n`-smoothly with the base point; applied to the tangent bundle it is exactly a Riemannian metric. | `Bundle.ContMDiffRiemannianMetric IB n F E` is a family of inner products on fibers of a vector bundle varying `C^n`-smoothly with the base point; applied to the tangent bundle it is a Riemannian metric. |
modifiedLocal isometry (surfaces)c2055187b47b
| Field | From #2473 | To #3109 |
|---|
| note | No definition of local isometry between Riemannian manifolds/surfaces exists in Mathlib; only the metric-space `Isometry` predicate is available. | No dedicated local-isometry notion for surfaces or Riemannian manifolds exists in Mathlib; only the metric-space `Isometry` predicate is available. |
modifiedIntrinsic/extrinsic propertya713aeb65d6a
| Field | From #2473 | To #3109 |
|---|
| note | Mathlib has no notion of intrinsic vs extrinsic property of a surface. | Mathlib does not formalize the intrinsic-vs-extrinsic distinction for surface properties. |
modifiedRiemannian metric and Riemannian manifolde5873192f9b0
| Field | From #2473 | To #3109 |
|---|
| note | Anchor tightened to point to the definitional sentence. | Verified: `Bundle.RiemannianMetric E` is a family of inner products on the fibers of a vector bundle; combined with `IsRiemannianManifold`, it packages the Riemannian-manifold definition. |
| note_annotation | `Bundle.RiemannianMetric E` gives a family of inner products on the fibers of a vector bundle (and `IsRiemannianManifold` packages the manifold-level assertion). | — |
modifiedContinuous/smooth Riemannian metric31459bcceb44
| Field | From #2473 | To #3109 |
|---|
| note | `IsContinuousRiemannianBundle` and `IsContMDiffRiemannianBundle` express, respectively, that the inner product on fibers varies continuously / `C^n`-smoothly with the base point. | `IsContinuousRiemannianBundle` and `IsContMDiffRiemannianBundle` express, respectively, continuous and `C^n`-smooth variation of the fiberwise inner product with the base point. |
modifiedMusical isomorphism7d805eedbdd5
| Field | From #2473 | To #3109 |
|---|
| note | The pointwise `InnerProductSpace.toDual` gives the fiberwise flat isomorphism of a Hilbert space with its dual, but the bundle-level musical isomorphism between the tangent and cotangent bundles is not built in Mathlib. | `InnerProductSpace.toDual` gives the pointwise flat isomorphism of a Hilbert space with its dual, but the bundle-level musical isomorphism between the tangent and cotangent bundles is not built in Mathlib. |
modifiedIsometry944442fb5605
| Field | From #2473 | To #3109 |
|---|
| note | Anchor changed to the primary definitional sentence; the previous snippet 'a diffeomorphism' was too generic. | Verified: Mathlib's `Isometry` for (pseudo)emetric spaces subsumes the induced-distance case, but there is no dedicated Riemannian-isometry predicate preserving the metric tensor. |
| note_annotation | Mathlib's `Isometry` for (pseudo)emetric spaces applies at the level of the induced distance, but there is no dedicated `RiemannianIsometry` preserving the smooth structure and the metric tensor. | — |
modifiedRiemannian volume formc4194010724b
| Field | From #2473 | To #3109 |
|---|
| note | The Riemannian volume form on an oriented Riemannian manifold is not defined in Mathlib; only the pointwise `Orientation.volumeForm` on a single inner product space exists. | The Riemannian volume form on an oriented Riemannian manifold is not defined in Mathlib; only pointwise `Orientation.volumeForm` on a single inner product space exists. |
modifiedEuclidean metricbf6af90d7432
| Field | From #2473 | To #3109 |
|---|
| note | `riemannianMetricVectorSpace F` is the canonical Riemannian metric on an inner product space given by its inner product on each tangent space, and `EuclideanSpace` is the standard inner-product model. | `riemannianMetricVectorSpace F` is the canonical Riemannian metric on an inner product space given by its inner product on each tangent space, matching the Euclidean metric on `EuclideanSpace`. |
modifiedRiemannian submanifolddbd786d7968d
| Field | From #2473 | To #3109 |
|---|
| note | Anchor sharpened to the defining phrase. | Verified: Riemannian submanifolds and induced metrics are absent from Mathlib. |
| note_annotation | Riemannian submanifolds and the induced metric are not formalized. | — |
modifiedFlat torusc8404234c778
| Field | From #2473 | To #3109 |
|---|
| note | Anchor tightened to the naming phrase. | Verified: the flat torus as a Riemannian manifold is not present in Mathlib. |
| note_annotation | The flat torus as a Riemannian manifold is not present in Mathlib. | — |
modifiedPositive combinations of metricsedcae84901d7
| Field | From #2473 | To #3109 |
|---|
| note | Anchor moved to the conclusion of the proposition. | Verified: no lemma stating that positive linear combinations of Riemannian metrics remain Riemannian is in Mathlib. |
| note_annotation | No lemma stating that positive linear combinations of Riemannian metrics remain Riemannian is in Mathlib. | — |
modifiedExistence of Riemannian metric40ba7cadcc2f
| Field | From #2473 | To #3109 |
|---|
| note | Mathlib only constructs the canonical Riemannian metric on inner product spaces; the general existence result for arbitrary smooth manifolds (via partitions of unity) is not there. | Only the canonical metric on inner product spaces (`riemannianMetricVectorSpace`) is in Mathlib; the general existence result via partitions of unity is not. |
modifiedAdmissible curve and lengthb7b2cc5ecf22
| Field | From #2473 | To #3109 |
|---|
| note | `Manifold.pathELength` gives the length integral of a `C^1` path in a manifold whose tangent spaces have an `ENorm`; piecewise-smooth admissible curves are subsumed as `C^1` paths. | `Manifold.pathELength` computes the length integral of a `C^1` path in a manifold whose tangent spaces carry an `ENorm`; piecewise-smooth admissible curves are subsumed. |
modifiedRiemannian distance is a metric6a1a9fe3536b
| Field | From #2473 | To #3109 |
|---|
| note | `EMetricSpace.ofRiemannianMetric` builds an emetric space structure whose topology agrees with the manifold's, using `riemannianEDist`; positivity/triangle inequality are proved but only an `ℝ≥0∞`-valued distance is provided. | `EMetricSpace.ofRiemannianMetric` produces an emetric-space structure whose topology matches the manifold's, using `riemannianEDist`; the ℝ-valued distance version is not there. |
modifiedCompactness iff finite diameter (complete)f00e371f344e
| Field | From #2473 | To #3109 |
|---|
| note | Anchor sharpened from the generic 'If' to the actual proposition text. | Verified: the Riemannian 'complete ∧ finite diameter ↔ compact' statement (invoking Hopf–Rinow) is not in Mathlib. |
| note_annotation | The Riemannian statement 'complete ∧ finite diameter ↔ compact' (invoking Hopf–Rinow) is not in Mathlib. | — |
modifiedAffine connection3a218351b067
| Field | From #2473 | To #3109 |
|---|
| note | `CovariantDerivative I F V` is a bundled Koszul connection on a vector bundle; taking `V = TangentSpace I` recovers an affine connection on a manifold. | `CovariantDerivative I F V` is Mathlib's bundled Koszul connection on a vector bundle; taking `V = TangentSpace I` recovers an affine connection on a manifold. |
modifiedTorsion-free connection240091057396
| Field | From #2473 | To #3109 |
|---|
| note | Mathlib defines `CovariantDerivative.torsion` on the tangent bundle and characterizes torsion-freeness via `torsion_eq_zero_iff` (⇔ `∇_X Y - ∇_Y X = [X,Y]`). | Mathlib defines `CovariantDerivative.torsion` on the tangent bundle and characterizes torsion-freeness via `torsion_eq_zero_iff` (⇔ `∇_X Y − ∇_Y X = [X,Y]`). |
modifiedExistence and uniqueness of geodesicsf88ba9f8e0b4
| Field | From #2473 | To #3109 |
|---|
| note | The local existence and uniqueness of geodesics is not in Mathlib. | Local existence and uniqueness of geodesics is not in Mathlib. |
modifiedHopf–Rinow theorem495aa58e4b6f
| Field | From #2473 | To #3109 |
|---|
| note | Anchor moved from the generic 'Let' to the theorem's characterizing sentence. | Verified: the Hopf–Rinow theorem is not in Mathlib. |
| note_annotation | The Hopf–Rinow theorem is not in Mathlib. | — |
modifiedInduced norm from Riemannian metric31c58ce06b92
| Field | From #2473 | To #3109 |
|---|
| mathlib.decl | Bundle.instNormedAddCommGroup | Bundle.RiemannianMetric.toCore |
| mathlib.match_kind | exact | special_case |
| note | Under `[RiemannianBundle E]`, Mathlib installs a `NormedAddCommGroup (E b)` and `InnerProductSpace ℝ (E b)` on each fiber via `RiemannianMetric.toCore`, giving the induced norm on tangent spaces. | `Bundle.RiemannianMetric.toCore` yields an `InnerProductSpace.Core` on each fiber, from which anonymous scoped `NormedAddCommGroup` and `InnerProductSpace` instances on `E b` are derived (the previously cited `Bundle.instNormedAddCommGroup` name does not exist). |
addedMetric tensor66691c547769
addedAcceleration of a curve3d5f408004a5
addedSectional curvaturef1eec7715a1c
addedScalar curvature4aee58e5e103
addedIsometric Riemannian manifolds6cc35528c91a