diff --git a/OpenGALib/Riemannian.lean b/OpenGALib/Riemannian.lean index f1fbe6f..ed1052b 100644 --- a/OpenGALib/Riemannian.lean +++ b/OpenGALib/Riemannian.lean @@ -10,11 +10,11 @@ import OpenGALib.Riemannian.Operators.Hessian import OpenGALib.Riemannian.Operators.Laplacian import OpenGALib.Riemannian.Operators.SecondFundamentalForm import OpenGALib.Riemannian.TensorBundle.BundleSectionContinuity -import OpenGALib.Riemannian.Util.ChartJacobianSmooth -import OpenGALib.Riemannian.Util.ChartJacobianSmoothness -import OpenGALib.Riemannian.Util.CovDerivBridges -import OpenGALib.Riemannian.Util.DivergenceSimp -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.Chart.ChartJacobianCLM +import OpenGALib.Riemannian.Util.Chart.ChartJacobianEntries +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges +import OpenGALib.Riemannian.Util.Simp.OperatorSimp +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness import OpenGALib.Riemannian.TensorBundle.Defs import OpenGALib.Riemannian.TangentBundle.TangentSmooth import OpenGALib.Riemannian.Instances.EuclideanSpace diff --git a/OpenGALib/Riemannian/Connection/Koszul.lean b/OpenGALib/Riemannian/Connection/Koszul.lean index 4028387..edd26fa 100644 --- a/OpenGALib/Riemannian/Connection/Koszul.lean +++ b/OpenGALib/Riemannian/Connection/Koszul.lean @@ -3,7 +3,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality import Mathlib.Geometry.Manifold.VectorField.LieBracket import OpenGALib.Riemannian.Manifold.SmoothManifold import OpenGALib.Riemannian.TangentBundle.TangentSmooth -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness /-! # Koszul functional and its algebraic identities diff --git a/OpenGALib/Riemannian/Connection/LeviCivita.lean b/OpenGALib/Riemannian/Connection/LeviCivita.lean index db2527b..21b3246 100644 --- a/OpenGALib/Riemannian/Connection/LeviCivita.lean +++ b/OpenGALib/Riemannian/Connection/LeviCivita.lean @@ -6,11 +6,11 @@ import Mathlib.Geometry.Manifold.VectorField.LieBracket import OpenGALib.Riemannian.Manifold.SmoothManifold import OpenGALib.Riemannian.TangentBundle.TangentSmooth import OpenGALib.Riemannian.TensorBundle.MusicalIso -import OpenGALib.Riemannian.Util.TangentHelpers +import OpenGALib.Riemannian.Util.Tangent.TangentHelpers import OpenGALib.Riemannian.Connection.Koszul import OpenGALib.Riemannian.Connection.RieszExtraction -import OpenGALib.Riemannian.Util.CovDerivSmoothness -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivSmoothness +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness import OpenGALib.Util.Attributes /-! diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean index 0693dae..d2797d6 100644 --- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean +++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean @@ -2,8 +2,8 @@ import OpenGALib.Riemannian.Connection.LeviCivita import OpenGALib.Riemannian.Connection.LeviCivita import OpenGALib.Riemannian.TangentBundle.TangentSmooth import OpenGALib.Riemannian.Operators.HessianLie -import OpenGALib.Riemannian.Util.MetricInnerSmoothness --- `riemannCurvature HasMetric.metric X Y Z` notation is now defined inline in `Connection.lean` +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness +-- `Riem(X, Y) Z` notation is now defined inline in `Connection.lean` -- alongside `riemannCurvature`; it transitively reaches us via the -- `import OpenGALib.Riemannian.Connection.LeviCivita` above. import Mathlib.LinearAlgebra.Trace @@ -11,7 +11,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.InnerProductSpace.Trace import Mathlib.Geometry.Manifold.VectorField.LieBracket import Mathlib.Analysis.Calculus.FDeriv.Symmetric -import OpenGALib.Riemannian.Util.CovDerivBridges +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges /-! # Riemann curvature, Ricci, and scalar curvature @@ -1086,4 +1086,3 @@ theorem sectionalCurvature_symmetric rw [hXY]; ring end Riemannian - diff --git a/OpenGALib/Riemannian/Curvature/Tensoriality.lean b/OpenGALib/Riemannian/Curvature/Tensoriality.lean index 3af5e87..ad66cb3 100644 --- a/OpenGALib/Riemannian/Curvature/Tensoriality.lean +++ b/OpenGALib/Riemannian/Curvature/Tensoriality.lean @@ -1,6 +1,6 @@ import OpenGALib.Riemannian.Curvature.RiemannCurvature import OpenGALib.Riemannian.Operators.Gradient -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame import Mathlib.Geometry.Manifold.BumpFunction import Mathlib.LinearAlgebra.Dimension.Free diff --git a/OpenGALib/Riemannian/Manifold/SmoothManifold.lean b/OpenGALib/Riemannian/Manifold/SmoothManifold.lean index fece6bd..384b073 100644 --- a/OpenGALib/Riemannian/Manifold/SmoothManifold.lean +++ b/OpenGALib/Riemannian/Manifold/SmoothManifold.lean @@ -1,5 +1,4 @@ import OpenGALib.Riemannian.Metric.RiemannianMetric -import OpenGALib.Riemannian.Util.MetricNotation import OpenGALib.Util.Attributes import OpenGALib.Riemannian.TangentBundle.LocallyConstant diff --git a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean index 12579c7..aa98f5a 100644 --- a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean +++ b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean @@ -9,7 +9,7 @@ import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame.Smoothness import OpenGALib.Util.Notation import Mathlib.Analysis.InnerProductSpace.Trace -import OpenGALib.Riemannian.Util.CovDerivBridges +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges /-! # Bochner expansion: Ricci-identity-driven chain diff --git a/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean index 101341a..a15bbb4 100644 --- a/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean +++ b/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean @@ -6,10 +6,10 @@ import OpenGALib.Riemannian.Curvature.Tensoriality import OpenGALib.Riemannian.Operators.Gradient import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame.Smoothness -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness import OpenGALib.Util.Notation import Mathlib.Analysis.InnerProductSpace.Trace -import OpenGALib.Riemannian.Util.CovDerivBridges +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges /-! # Bochner anchor — Hessian expansion of `|∇f|²` diff --git a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean index 922604c..ecfce13 100644 --- a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean +++ b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean @@ -1,10 +1,10 @@ import OpenGALib.Riemannian.Operators.Bochner.HessianExpansion import OpenGALib.Riemannian.Operators.Bochner.BochnerExpansion import OpenGALib.Riemannian.Operators.ConnectionLaplacian -import OpenGALib.Riemannian.Util.ConnectionLaplacianSimp +import OpenGALib.Riemannian.Util.Simp.OperatorSimp import OpenGALib.Util.MFDeriv -import OpenGALib.Riemannian.Util.MetricInnerSmoothness -import OpenGALib.Riemannian.Util.CovDerivBridges +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges /-! # Per-summand chain of the heart-of-Bochner identity diff --git a/OpenGALib/Riemannian/Operators/Gradient.lean b/OpenGALib/Riemannian/Operators/Gradient.lean index a80b1b8..1f23887 100644 --- a/OpenGALib/Riemannian/Operators/Gradient.lean +++ b/OpenGALib/Riemannian/Operators/Gradient.lean @@ -1,6 +1,6 @@ import OpenGALib.Riemannian.Connection.LeviCivita import OpenGALib.Riemannian.TensorBundle.MusicalIso -import OpenGALib.Riemannian.Util.MfderivApplySection +import OpenGALib.Riemannian.Util.Tangent.MfderivApplySection /-! # Manifold gradient diff --git a/OpenGALib/Riemannian/Operators/Hessian.lean b/OpenGALib/Riemannian/Operators/Hessian.lean index ed9cf33..48ec21f 100644 --- a/OpenGALib/Riemannian/Operators/Hessian.lean +++ b/OpenGALib/Riemannian/Operators/Hessian.lean @@ -5,7 +5,8 @@ import Mathlib.Algebra.Order.Chebyshev import Mathlib.LinearAlgebra.Dimension.Free import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas import Mathlib.Analysis.InnerProductSpace.PiL2 -import OpenGALib.Riemannian.Util.CovDerivBridges +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges +import OpenGALib.Riemannian.Util.Metric.MetricNotation /-! # Hessian on a Riemannian manifold diff --git a/OpenGALib/Riemannian/Operators/Laplacian.lean b/OpenGALib/Riemannian/Operators/Laplacian.lean index 7a1934b..9b928e8 100644 --- a/OpenGALib/Riemannian/Operators/Laplacian.lean +++ b/OpenGALib/Riemannian/Operators/Laplacian.lean @@ -1,6 +1,6 @@ import OpenGALib.Riemannian.Operators.Hessian import Mathlib.Analysis.InnerProductSpace.PiL2 -import OpenGALib.Riemannian.Util.CovDerivBridges +import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges /-! # Laplace–Beltrami operator diff --git a/OpenGALib/Riemannian/TangentBundle/TangentSmooth.lean b/OpenGALib/Riemannian/TangentBundle/TangentSmooth.lean index 7c96edc..83a79ae 100644 --- a/OpenGALib/Riemannian/TangentBundle/TangentSmooth.lean +++ b/OpenGALib/Riemannian/TangentBundle/TangentSmooth.lean @@ -13,7 +13,7 @@ import Mathlib.LinearAlgebra.Basis.Defs import Mathlib.LinearAlgebra.Dimension.Finite import Mathlib.LinearAlgebra.FreeModule.Finite.Basic import OpenGALib.Riemannian.TangentBundle.LocallyConstant -import OpenGALib.Riemannian.Util.FlatChartDerivs +import OpenGALib.Riemannian.Util.Chart.FlatChartDerivs /-! # Tangent bundle smoothness API diff --git a/OpenGALib/Riemannian/Util/ChartJacobianSmooth.lean b/OpenGALib/Riemannian/Util/Chart/ChartJacobianCLM.lean similarity index 99% rename from OpenGALib/Riemannian/Util/ChartJacobianSmooth.lean rename to OpenGALib/Riemannian/Util/Chart/ChartJacobianCLM.lean index b800019..c2e8876 100644 --- a/OpenGALib/Riemannian/Util/ChartJacobianSmooth.lean +++ b/OpenGALib/Riemannian/Util/Chart/ChartJacobianCLM.lean @@ -10,7 +10,7 @@ import Mathlib.LinearAlgebra.Basis.Defs import Mathlib.LinearAlgebra.Dimension.Free /-! -# Smoothness of chart-Jacobian-related continuous linear map-valued functions +# Smoothness of chart-Jacobian CLM-valued functions For a smooth manifold `M` with model `(I : ModelWithCorners ℝ E H)` and a base point `α : M`, the tangent-bundle trivialization at `α` provides diff --git a/OpenGALib/Riemannian/Util/ChartJacobianSmoothness.lean b/OpenGALib/Riemannian/Util/Chart/ChartJacobianEntries.lean similarity index 100% rename from OpenGALib/Riemannian/Util/ChartJacobianSmoothness.lean rename to OpenGALib/Riemannian/Util/Chart/ChartJacobianEntries.lean diff --git a/OpenGALib/Riemannian/Util/FlatChartDerivs.lean b/OpenGALib/Riemannian/Util/Chart/FlatChartDerivs.lean similarity index 100% rename from OpenGALib/Riemannian/Util/FlatChartDerivs.lean rename to OpenGALib/Riemannian/Util/Chart/FlatChartDerivs.lean diff --git a/OpenGALib/Riemannian/Util/Chart/README.md b/OpenGALib/Riemannian/Util/Chart/README.md new file mode 100644 index 0000000..55be8b7 --- /dev/null +++ b/OpenGALib/Riemannian/Util/Chart/README.md @@ -0,0 +1,9 @@ +# `Util/Chart/` + +Chart-frame and chart-Jacobian engineering modules. + +| File | Role | +|------|------| +| [`ChartJacobianCLM.lean`](./ChartJacobianCLM.lean) | CLM-valued chart-Jacobian smoothness. | +| [`ChartJacobianEntries.lean`](./ChartJacobianEntries.lean) | Scalar chart-Jacobian matrix-entry smoothness. | +| [`FlatChartDerivs.lean`](./FlatChartDerivs.lean) | Flat chart derivative engineering for tangent maps. | diff --git a/OpenGALib/Riemannian/Util/CovDerivBridges.lean b/OpenGALib/Riemannian/Util/CovDeriv/CovDerivBridges.lean similarity index 100% rename from OpenGALib/Riemannian/Util/CovDerivBridges.lean rename to OpenGALib/Riemannian/Util/CovDeriv/CovDerivBridges.lean diff --git a/OpenGALib/Riemannian/Util/CovDerivSmoothness.lean b/OpenGALib/Riemannian/Util/CovDeriv/CovDerivSmoothness.lean similarity index 98% rename from OpenGALib/Riemannian/Util/CovDerivSmoothness.lean rename to OpenGALib/Riemannian/Util/CovDeriv/CovDerivSmoothness.lean index f2fc164..04fc510 100644 --- a/OpenGALib/Riemannian/Util/CovDerivSmoothness.lean +++ b/OpenGALib/Riemannian/Util/CovDeriv/CovDerivSmoothness.lean @@ -1,13 +1,13 @@ import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality import Mathlib.Geometry.Manifold.VectorField.LieBracket import OpenGALib.Riemannian.Manifold.SmoothManifold -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness import OpenGALib.Riemannian.TangentBundle.TangentSmooth import OpenGALib.Riemannian.TensorBundle.MusicalIso -import OpenGALib.Riemannian.Util.MfderivApplySection +import OpenGALib.Riemannian.Util.Tangent.MfderivApplySection import OpenGALib.Riemannian.Connection.Koszul import OpenGALib.Riemannian.Connection.RieszExtraction -import OpenGALib.Riemannian.Util.TangentHelpers +import OpenGALib.Riemannian.Util.Tangent.TangentHelpers /-! # Tensoriality + smoothness machinery for `koszulCovDeriv` diff --git a/OpenGALib/Riemannian/Util/CovDeriv/README.md b/OpenGALib/Riemannian/Util/CovDeriv/README.md new file mode 100644 index 0000000..21d1d66 --- /dev/null +++ b/OpenGALib/Riemannian/Util/CovDeriv/README.md @@ -0,0 +1,6 @@ +# CovDeriv + +Covariant-derivative utilities are split by import direction. +`CovDerivSmoothness.lean` is pre-`LeviCivita` scaffolding used to construct the +connection. `CovDerivBridges.lean` is post-`LeviCivita` simp glue for +`covDeriv` and `covDerivAt`, kept separate to avoid an import cycle. diff --git a/OpenGALib/Riemannian/Util/DivergenceSimp.lean b/OpenGALib/Riemannian/Util/DivergenceSimp.lean deleted file mode 100644 index 46c8edc..0000000 --- a/OpenGALib/Riemannian/Util/DivergenceSimp.lean +++ /dev/null @@ -1,42 +0,0 @@ -import OpenGALib.Riemannian.Operators.Divergence - -/-! -# Divergence — simp def-unfold - -Engineering simp lemma exposing the definition of `divergence` as a sum -of `HasMetric.metric.metricInner (∇_{B_i} X) B_i` over the smooth $g$-orthonormal frame. -Imported by callers that need to rewrite at the level of the frame sum -rather than against the opaque operator name. --/ - -noncomputable section - -open Bundle -open scoped ContDiff Manifold Bundle Riemannian InnerProductSpace - -namespace Riemannian -namespace Operators - -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] - [CompleteSpace E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] - {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] - {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M] - [IsLocallyConstantChartedSpace H M] - [hm : HasMetric I M] - -/-- **Eng.** Definitional unfold of `divergence` as a sum of -`HasMetric.metric.metricInner (∇_{B_i} X) B_i` over the smooth $g$-orthonormal frame. Pure -`rfl`; tagged `@[simp]` for tactic-level rewrites. -/ -@[simp] lemma divergence_def - (g : RiemannianMetric I M) - (X : VectorFieldSection I M) (x : M) : - divergence (I := I) (M := M) g X x = - ∑ i, g.metricInner x - (covDeriv g (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i) X x) - (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i x) := - rfl - -end Operators -end Riemannian - -end diff --git a/OpenGALib/Riemannian/Util/CotangentFunctional.lean b/OpenGALib/Riemannian/Util/Metric/CotangentFunctional.lean similarity index 99% rename from OpenGALib/Riemannian/Util/CotangentFunctional.lean rename to OpenGALib/Riemannian/Util/Metric/CotangentFunctional.lean index 6583f67..dc7728d 100644 --- a/OpenGALib/Riemannian/Util/CotangentFunctional.lean +++ b/OpenGALib/Riemannian/Util/Metric/CotangentFunctional.lean @@ -1,6 +1,6 @@ import OpenGALib.Riemannian.Connection.Koszul -import OpenGALib.Riemannian.Util.TangentHelpers -import OpenGALib.Riemannian.Util.MetricInnerSmoothness +import OpenGALib.Riemannian.Util.Tangent.TangentHelpers +import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness /-! # Half-Koszul cotangent functional diff --git a/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean b/OpenGALib/Riemannian/Util/Metric/MetricInnerSmoothness.lean similarity index 100% rename from OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean rename to OpenGALib/Riemannian/Util/Metric/MetricInnerSmoothness.lean diff --git a/OpenGALib/Riemannian/Util/MetricNotation.lean b/OpenGALib/Riemannian/Util/Metric/MetricNotation.lean similarity index 100% rename from OpenGALib/Riemannian/Util/MetricNotation.lean rename to OpenGALib/Riemannian/Util/Metric/MetricNotation.lean diff --git a/OpenGALib/Riemannian/Util/Metric/README.md b/OpenGALib/Riemannian/Util/Metric/README.md new file mode 100644 index 0000000..dc0221e --- /dev/null +++ b/OpenGALib/Riemannian/Util/Metric/README.md @@ -0,0 +1,9 @@ +# `Util/Metric/` + +Metric notation, smoothness, and cotangent-functional support modules. + +| File | Role | +|------|------| +| [`MetricNotation.lean`](./MetricNotation.lean) | Polymorphic metric inner-product and norm-squared notation. | +| [`MetricInnerSmoothness.lean`](./MetricInnerSmoothness.lean) | Pointwise, set, and global `metricInner` smoothness variants. | +| [`CotangentFunctional.lean`](./CotangentFunctional.lean) | Half-Koszul cotangent-functional construction. | diff --git a/OpenGALib/Riemannian/Util/README.md b/OpenGALib/Riemannian/Util/README.md new file mode 100644 index 0000000..2ef02b8 --- /dev/null +++ b/OpenGALib/Riemannian/Util/README.md @@ -0,0 +1,37 @@ +# `Riemannian/Util/` — engineering tax for the Riemannian layer + +Per OpenGA's anchor-purity discipline, anchor files expose only +`**Math.**`-tagged declarations; `**Eng.**` and `**Mixed.**` plumbing lives +under `Util/`. The files are grouped by the downstream layer they support. + +## Directories + +| Theme | Directory | Files | +| --- | --- | --- | +| Chart Jacobian | [`Chart/`](./Chart/) | `ChartJacobianCLM.lean`, `ChartJacobianEntries.lean`, `FlatChartDerivs.lean` | +| Tangent / section glue | [`Tangent/`](./Tangent/) | `TangentHelpers.lean`, `TensorBundleCoercions.lean`, `MfderivApplySection.lean` | +| Metric inner / notation | [`Metric/`](./Metric/) | `MetricInnerSmoothness.lean`, `MetricNotation.lean`, `CotangentFunctional.lean` | +| Covariant derivative | [`CovDeriv/`](./CovDeriv/) | `CovDerivSmoothness.lean`, `CovDerivBridges.lean` | +| Operator simp lemmas | [`Simp/`](./Simp/) | `OperatorSimp.lean` | + +`ChartJacobianSmooth.lean` was renamed to `Chart/ChartJacobianCLM.lean` +because it proves smoothness of continuous-linear-map-valued chart-Jacobian +composites. `ChartJacobianSmoothness.lean` was renamed to +`Chart/ChartJacobianEntries.lean` because it proves scalar matrix-entry +smoothness. + +`ConnectionLaplacianSimp.lean` and `DivergenceSimp.lean` were merged into +`Simp/OperatorSimp.lean`. `CovDerivBridges.lean` remains a separate +post-`LeviCivita` bridge file: it imports `Connection.LeviCivita`, while +`Connection.LeviCivita` imports `CovDerivSmoothness.lean`; absorbing the bridge +lemmas into `CovDerivSmoothness.lean` would create an import cycle. + +## Conventions + +* Every declaration docstring starts with `**Math.**`, `**Eng.**`, or + `**Mixed.**`. +* Util files may contain engineering declarations; sibling anchor folders keep + the mathematical surface clean. +* Subdirectory names carry the grouping role. File names describe concrete + content and avoid generic `Helpers` / `Base` / `Foundation` suffixes except + where the historical API name is retained. diff --git a/OpenGALib/Riemannian/Util/ConnectionLaplacianSimp.lean b/OpenGALib/Riemannian/Util/Simp/OperatorSimp.lean similarity index 56% rename from OpenGALib/Riemannian/Util/ConnectionLaplacianSimp.lean rename to OpenGALib/Riemannian/Util/Simp/OperatorSimp.lean index c0a9abb..816a2fc 100644 --- a/OpenGALib/Riemannian/Util/ConnectionLaplacianSimp.lean +++ b/OpenGALib/Riemannian/Util/Simp/OperatorSimp.lean @@ -1,18 +1,18 @@ import OpenGALib.Riemannian.Operators.ConnectionLaplacian +import OpenGALib.Riemannian.Operators.Divergence /-! -# Connection Laplacian — simp def-unfold +# Operator simp def-unfolds -Engineering simp lemma exposing the definition of `connectionLaplacian` -as a sum of `secondCovDerivSection` over the smooth $g$-orthonormal -frame. Imported by callers that need to rewrite at the level of the -frame sum rather than against the opaque operator name. +Engineering simp lemmas exposing definitions of small Riemannian operators +against the smooth $g$-orthonormal frame. Imported by callers that need to +rewrite at the level of frame sums rather than against opaque operator names. -/ noncomputable section open Bundle -open scoped ContDiff Manifold Bundle Riemannian +open scoped ContDiff Manifold Bundle Riemannian InnerProductSpace namespace Riemannian namespace Operators @@ -36,6 +36,18 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i) α := rfl +/-- **Eng.** Definitional unfold of `divergence` as a sum of +`metricInner (∇_{B_i} X) B_i` over the smooth $g$-orthonormal frame. Pure +`rfl`; tagged `@[simp]` for tactic-level rewrites. -/ +@[simp] lemma divergence_def + (g : RiemannianMetric I M) + (X : VectorFieldSection I M) (x : M) : + divergence (I := I) (M := M) g X x = + ∑ i, g.metricInner x + (covDeriv g (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i) X x) + (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i x) := + rfl + end Operators end Riemannian diff --git a/OpenGALib/Riemannian/Util/Simp/README.md b/OpenGALib/Riemannian/Util/Simp/README.md new file mode 100644 index 0000000..5768765 --- /dev/null +++ b/OpenGALib/Riemannian/Util/Simp/README.md @@ -0,0 +1,5 @@ +# Simp + +Simp utilities collect small operator unfoldings used explicitly by downstream +proofs. `OperatorSimp.lean` combines the connection-Laplacian and divergence +definitional simp lemmas. diff --git a/OpenGALib/Riemannian/Util/MfderivApplySection.lean b/OpenGALib/Riemannian/Util/Tangent/MfderivApplySection.lean similarity index 100% rename from OpenGALib/Riemannian/Util/MfderivApplySection.lean rename to OpenGALib/Riemannian/Util/Tangent/MfderivApplySection.lean diff --git a/OpenGALib/Riemannian/Util/Tangent/README.md b/OpenGALib/Riemannian/Util/Tangent/README.md new file mode 100644 index 0000000..d9c87f6 --- /dev/null +++ b/OpenGALib/Riemannian/Util/Tangent/README.md @@ -0,0 +1,9 @@ +# `Util/Tangent/` + +Tangent-bundle glue and section-level helper modules. + +| File | Role | +|------|------| +| [`TangentHelpers.lean`](./TangentHelpers.lean) | Chart-bundle smoothness bridges. | +| [`TensorBundleCoercions.lean`](./TensorBundleCoercions.lean) | Tensor-bundle fiber-to-model coercion algebra. | +| [`MfderivApplySection.lean`](./MfderivApplySection.lean) | Smoothness of `mfderiv f` applied to a tangent-bundle section. | diff --git a/OpenGALib/Riemannian/Util/TangentHelpers.lean b/OpenGALib/Riemannian/Util/Tangent/TangentHelpers.lean similarity index 100% rename from OpenGALib/Riemannian/Util/TangentHelpers.lean rename to OpenGALib/Riemannian/Util/Tangent/TangentHelpers.lean diff --git a/OpenGALib/Riemannian/Util/TensorBundleCoercions.lean b/OpenGALib/Riemannian/Util/Tangent/TensorBundleCoercions.lean similarity index 100% rename from OpenGALib/Riemannian/Util/TensorBundleCoercions.lean rename to OpenGALib/Riemannian/Util/Tangent/TensorBundleCoercions.lean