Surface patch area is invariant under injective reparametrization

Proved

OpenGA.RicciFlow.patchArea_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 and $\Omega\subseteq\mathbb R^2$ be measurable. Suppose $\varphi:\mathbb R^2\to\mathbb R^2$ is differentiable at every point of $\Omega$ and injective on $\Omega$ , and $f:\mathbb R^2\to M$ is differentiable at every point of $\varphi(\Omega)$ . Then

\int_\Omega J_g(f\circ\varphi)(u)\,du=\int_{\varphi(\Omega)}J_gf(v)\,dv.

These are Bochner integrals; in particular, the identity identifies the usual finite areas whenever the density is integrable. The surface map $f$ need not be injective, so multiplicity is retained. This establishes compatibility of local area integrals under changes of surface coordinates; it does not yet construct an integral on a closed surface.

Preamble

import Theorems.Thm_OpenGA_RicciFlow_surfaceDensity_comp
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.patchArea_comp
    (g : SmoothRiemannianMetric I M) (f : SurfaceParameter → M)
    {φ : SurfaceParameter → SurfaceParameter} {Ω : Set SurfaceParameter}
    (hΩ : MeasurableSet Ω) (hφ : ∀ u ∈ Ω, DifferentiableAt ℝ φ u)
    (hinj : Set.InjOn φ Ω)
    (hf : ∀ v ∈ φ '' Ω, MDifferentiableAt 𝓘(ℝ, SurfaceParameter) I f v) :
    patchArea g (f ∘ φ) Ω = patchArea g f (φ '' Ω) := by sorry

Source

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

View graph