Induced-metric patch area agrees with ambient parametrized area

Proved

OpenGA.Surface.patchArea_inducedMetric

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

colding-minicozziimmersed-surfacesriemannian-geometrysurface-area

Let $f:N\to(M,g)$ be a smooth immersion of a finite-dimensional Hausdorff manifold, and put $h=f^*g$ . Let $A\subseteq\mathbb R^2$ be measurable and suppose $p:\mathbb R^2\to N$ is differentiable at every point of $A$ . Then

\int_A J_h p(u)\,du=\int_A J_g(f\circ p)(u)\,du.

The integrals are Bochner integrals, so the equality also applies with Lean's total-integral convention; it identifies the ordinary finite areas whenever the density is integrable. Multiplicity is retained because neither map is required to be injective. This is compatibility of local patch integrals, not a claim about branch points or finite-time extinction.

Preamble

import Theorems.Thm_OpenGA_Surface_surfaceDensity_inducedMetric
import Definitions.Def_OpenGA_ImmersedMetric
import Definitions.Def_OpenGA_SurfaceArea
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.LocallyConvex.Bounded
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Normed.Operator.Bilinear
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Geometry.Manifold.BumpFunction
import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
import Mathlib.Geometry.Manifold.Diffeomorph
import Mathlib.Geometry.Manifold.MFDeriv.FDeriv
import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Geometry.Manifold.VectorBundle.Basic
import Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
import Mathlib.Geometry.Manifold.VectorBundle.Hom
import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.MeasureTheory.Integral.Bochner.Set
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Mathlib.Topology.MetricSpace.ProperSpace
import Mathlib.Topology.VectorBundle.Basic

noncomputable section

open Bundle MeasureTheory Set

open scoped Manifold ContDiff

open DifferentialGeometry OpenGA.RicciFlow

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {N : Type*} [TopologicalSpace N] [ChartedSpace H N] [IsManifold I ∞ N] [T2Space N]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {G : Type*} [TopologicalSpace G] {J : ModelWithCorners ℝ F G}
  {M : Type*} [TopologicalSpace M] [ChartedSpace G M] [IsManifold J ∞ M]

open OpenGA.Surface

Formal statement

theorem OpenGA.Surface.patchArea_inducedMetric
    (g : SmoothRiemannianMetric J M) (f : N → M) (hf : ContMDiff I J ∞ f)
    (hinj : ∀ x, Function.Injective (mfderiv I J f x))
    (p : SurfaceParameter → N) (A : Set SurfaceParameter) (hA : MeasurableSet A)
    (hp : ∀ u ∈ A, MDifferentiableAt 𝓘(ℝ, SurfaceParameter) I p u) :
    patchArea (inducedMetric g f hf hinj) p A = patchArea g (f ∘ p) A := by sorry

Source

https://github.com/MathNetwork/OpenGA/blob/58a1945f5e5ed41d2b0bf0ff83544cd7a290ee12/OpenGALib/Riemannian/Surface/Coordinates.lean#L48-L57

View graph