Surface area density under a change of parameters

Proved

OpenGA.RicciFlow.surfaceDensity_comp

by Xinze-Li-Moqian · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

colding-minicozzipoincare-foundationsriemannian-geometrysurface-area

Let $(M,g)$ be a smooth Riemannian manifold, $f:\mathbb R^2\to M$ , and $\varphi:\mathbb R^2\to\mathbb R^2$ . Suppose $\varphi$ has derivative $A$ at $u$ and $f$ is differentiable at $\varphi(u)$ . Then

J_g(f\circ\varphi)(u)=|\det A|\,J_gf(\varphi(u)).

The determinant is computed in the standard orthonormal parameter basis. Neither $A$ nor $df$ must be injective; orientation reversal and degenerate derivatives are allowed. This is the pointwise coordinate compatibility of parametrized surface area.

Preamble

import Definitions.Def_OpenGA_SurfaceArea
import Mathlib.MeasureTheory.Function.Jacobian

noncomputable section

open Bundle Matrix MeasureTheory Set Filter

open scoped Manifold ContDiff Topology

open DifferentialGeometry

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]

open OpenGA.RicciFlow

Formal statement

theorem OpenGA.RicciFlow.surfaceDensity_comp
    (g : SmoothRiemannianMetric I M) (f : SurfaceParameter → M)
    {φ : SurfaceParameter → SurfaceParameter} {u : SurfaceParameter}
    {A : SurfaceParameter →L[ℝ] SurfaceParameter} (hφ : HasFDerivAt φ A u)
    (hf : MDifferentiableAt 𝓘(ℝ, SurfaceParameter) I f (φ u)) :
    surfaceDensity g (f ∘ φ) u =
      |(LinearMap.toMatrix (EuclideanSpace.basisFun (Fin 2) ℝ).toBasis
        (EuclideanSpace.basisFun (Fin 2) ℝ).toBasis A.toLinearMap).det| *
      surfaceDensity g f (φ u) := by sorry

Source

https://github.com/MathNetwork/OpenGA/blob/112b4c3c69de2a05fb160e565c0e6c1eef1ce44b/OpenGALib/Interoperability/RicciFlow/SurfaceAreaCoordinates.lean#L59-L73

View graph