Weighted area integration on injective regular parametrizations

For an injective map with injective derivative on a Borel set, pushing forward Lebesgue measure weighted by the geometric Jacobian gives normalized Hausdorff measure on its image. This yields weighted area integration and the corresponding Bochner integrability criterion in arbitrary codimension. No global continuity or differentiability outside the parameter set is required.

The nonnegative formulas allow infinite integrals. The Bochner formula is accompanied by an integrability equivalence, so finite surface integrals can be verified in parameter coordinates. These results concern the regular injective case; singular derivatives and multiplicities are not treated here.

The construction uses MeasureTheory.lintegral_normDet_fderiv_eq_euclideanHausdorffMeasure_image. The measure transport and integral proofs adapt Mathlib's determinant change of variables in Mathlib.MeasureTheory.Function.Jacobian to rectangular derivatives and normDet.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §3.3 (the area formula).

theorem TauCeti.restrict_map_withDensity_normDet_fderiv_eq_euclideanHausdorffMeasure {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hf : Set.InjOn f s) : MeasureTheory.Measure.map (s.domRestrict f) (MeasureTheory.Measure.comap Subtype.val (MeasureTheory.volume.withDensity fun (x : U) => ENNReal.ofReal (↑(fderiv ℝ f x)).normDet)) = (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)).restrict (f '' s)

The restricted parametrization pushes forward the Jacobian-weighted parameter measure to normalized Hausdorff measure on its image. The subtype formulation requires no measurable extension of the parametrization outside its domain.

theorem TauCeti.lintegral_image_eq_lintegral_normDet_fderiv_mul {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hf : Set.InjOn f s) (g : V → ENNReal) : ∫⁻ (y : V) in f '' s, g y ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U) = ∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet * g (f x)

Weighted area integration for an injective regular parametrization, with normalized Hausdorff measure in the target. The weight need not be measurable.

theorem TauCeti.lintegral_normDet_fderiv_mul_eq_lintegral_invFunOn {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hf : Set.InjOn f s) (g : U → ENNReal) : ∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet * g x = ∫⁻ (y : V) in f '' s, g (Function.invFunOn f s y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)

The weighted injective area formula written with a weight on the parameter space. The inverse on the image is unambiguous by injectivity on s.

theorem TauCeti.integrableOn_image_iff_integrableOn_normDet_fderiv_smul {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hf : Set.InjOn f s) (g : V → F) : MeasureTheory.IntegrableOn g (f '' s) (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) ↔ MeasureTheory.IntegrableOn (fun (x : U) => (↑(fderiv ℝ f x)).normDet • g (f x)) s MeasureTheory.volume

Surface integrability is equivalent to integrability of the Jacobian-weighted pullback under an injective regular parametrization.

theorem TauCeti.integral_image_eq_integral_normDet_fderiv_smul {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hf : Set.InjOn f s) (g : V → F) : ∫ (y : V) in f '' s, g y ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U) = ∫ (x : U) in s, (↑(fderiv ℝ f x)).normDet • g (f x)

Bochner area integration for an injective regular parametrization. Integrability can be checked by integrableOn_image_iff_integrableOn_normDet_fderiv_smul.