Surface measure on normal graphs

The normal graph parametrization of a function φ : E → ℝ sends y to (φ y, y) in the Euclidean product WithLp 2 (ℝ × E). When φ is K-Lipschitz, this parametrization is (K + 1)-Lipschitz and its inverse on the graph, the second projection, is 1-Lipschitz. Consequently, normalized Hausdorff measure on the graph is quantitatively equivalent to volume measure on the parameter space.

For a differentiable graph, the geometric Jacobian of the parametrization is sqrt (1 + ‖fderiv ℝ φ x‖²). The weighted area formula therefore becomes the classical graph surface-integration formula, with both extended nonnegative and Bochner integral versions. These results allow an L² trace constructed in graph coordinates to be interpreted as a trace with respect to Euclidean surface measure.

Main declarations

• TauCeti.volume_le_euclideanHausdorffMeasure_normalGraphEmbedding_image: surface measure on a graph dominates volume in the parameter space.
• LipschitzWith.euclideanHausdorffMeasure_normalGraphEmbedding_image_le: the reverse bound for a Lipschitz graph.
• LipschitzWith.map_volume_normalGraphEmbedding_le_surfaceMeasure and LipschitzWith.surfaceMeasure_le_smul_map_volume_normalGraphEmbedding: the corresponding comparison of measures on the graph.
• LipschitzWith.euclideanHausdorffMeasure_normalGraphEmbedding_image_eq_zero_iff: null sets correspond under a Lipschitz graph parametrization.
• TauCeti.lintegral_normalGraphEmbedding_image_eq_lintegral_sqrt_one_add_norm_fderiv_sq_mul: weighted surface integration on a differentiable normal graph.
• euclideanHausdorffMeasure_normalGraphEmbedding_image_eq_lintegral_sqrt_one_add_norm_fderiv_sq: the surface measure of a differentiable normal graph.
• integrableOn_normalGraphEmbedding_image_iff_integrableOn_sqrt_one_add_norm_fderiv_sq_smul: integrability on a differentiable normal graph.
• TauCeti.integral_normalGraphEmbedding_image_eq_integral_sqrt_one_add_norm_fderiv_sq_smul: Bochner surface integration on a differentiable normal graph.

The graph Jacobian itself, DifferentiableAt.normDet_fderiv_normalGraphEmbedding, is in TauCeti.Analysis.Calculus.FDeriv.WithLp.

References

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

Exact surface integration

theorem TauCeti.lintegral_normalGraphEmbedding_image_eq_lintegral_sqrt_one_add_norm_fderiv_sq_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {φ : E → ℝ} {s : Set E} (hs : MeasurableSet s) (hφ : ∀ x ∈ s, DifferentiableAt ℝ φ x) (g : WithLp 2 (ℝ × E) → ENNReal) : ∫⁻ (y : WithLp 2 (ℝ × E)) in normalGraphEmbedding φ '' s, g y ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E) = ∫⁻ (x : E) in s, ENNReal.ofReal √(1 + ‖fderiv ℝ φ x‖ ^ 2) * g (normalGraphEmbedding φ x)

Weighted surface integration on a differentiable normal graph. The weight is allowed to be nonmeasurable and both sides are extended nonnegative integrals.

theorem TauCeti.euclideanHausdorffMeasure_normalGraphEmbedding_image_eq_lintegral_sqrt_one_add_norm_fderiv_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {φ : E → ℝ} {s : Set E} (hs : MeasurableSet s) (hφ : ∀ x ∈ s, DifferentiableAt ℝ φ x) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (normalGraphEmbedding φ '' s) = ∫⁻ (x : E) in s, ENNReal.ofReal √(1 + ‖fderiv ℝ φ x‖ ^ 2)

The normalized Euclidean surface measure of a differentiable normal graph is the integral of the classical surface factor sqrt (1 + ‖Dφ‖²).

theorem TauCeti.integrableOn_normalGraphEmbedding_image_iff_integrableOn_sqrt_one_add_norm_fderiv_sq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} {s : Set E} (hs : MeasurableSet s) (hφ : ∀ x ∈ s, DifferentiableAt ℝ φ x) (g : WithLp 2 (ℝ × E) → F) : MeasureTheory.IntegrableOn g (normalGraphEmbedding φ '' s) (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) ↔ MeasureTheory.IntegrableOn (fun (x : E) => √(1 + ‖fderiv ℝ φ x‖ ^ 2) • g (normalGraphEmbedding φ x)) s MeasureTheory.volume

Integrability on a differentiable normal graph is equivalent to integrability of the pullback multiplied by the classical surface factor.

theorem TauCeti.integral_normalGraphEmbedding_image_eq_integral_sqrt_one_add_norm_fderiv_sq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} {s : Set E} (hs : MeasurableSet s) (hφ : ∀ x ∈ s, DifferentiableAt ℝ φ x) (g : WithLp 2 (ℝ × E) → F) : ∫ (y : WithLp 2 (ℝ × E)) in normalGraphEmbedding φ '' s, g y ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E) = ∫ (x : E) in s, √(1 + ‖fderiv ℝ φ x‖ ^ 2) • g (normalGraphEmbedding φ x)

Bochner surface integration on a differentiable normal graph. Its two sides are integrable simultaneously by TauCeti.integrableOn_normalGraphEmbedding_image_iff_integrableOn_sqrt_one_add_norm_fderiv_sq_smul.

Lipschitz graph measure comparison

theorem TauCeti.volume_le_euclideanHausdorffMeasure_normalGraphEmbedding_image {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (φ : E → ℝ) (s : Set E) : MeasureTheory.volume s ≤ (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (normalGraphEmbedding φ '' s)

Euclidean surface measure of a normal graph dominates volume of its parameter set. This lower bound uses only that the tangential projection is 1-Lipschitz.

theorem LipschitzWith.euclideanHausdorffMeasure_normalGraphEmbedding_image_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {K : NNReal} {φ : E → ℝ} (hφ : LipschitzWith K φ) (s : Set E) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (TauCeti.normalGraphEmbedding φ '' s) ≤ ↑(K + 1) ^ Module.finrank ℝ E * MeasureTheory.volume s

The Euclidean surface measure of a K-Lipschitz normal graph over s is at most (K + 1) ^ dim E times the volume of s.

theorem LipschitzWith.map_volume_normalGraphEmbedding_le_surfaceMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {K : NNReal} {φ : E → ℝ} (hφ : LipschitzWith K φ) : MeasureTheory.Measure.map (TauCeti.normalGraphEmbedding φ) MeasureTheory.volume ≤ (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).restrict (Set.range (TauCeti.normalGraphEmbedding φ))

Pushing volume forward by a Lipschitz graph parametrization gives a measure bounded by Euclidean surface measure restricted to the graph.

theorem LipschitzWith.surfaceMeasure_le_smul_map_volume_normalGraphEmbedding {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {K : NNReal} {φ : E → ℝ} (hφ : LipschitzWith K φ) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).restrict (Set.range (TauCeti.normalGraphEmbedding φ)) ≤ ↑(K + 1) ^ Module.finrank ℝ E • MeasureTheory.Measure.map (TauCeti.normalGraphEmbedding φ) MeasureTheory.volume

Euclidean surface measure restricted to a K-Lipschitz graph is at most (K + 1) ^ dim E times the pushforward of volume by its parametrization.

theorem LipschitzWith.euclideanHausdorffMeasure_normalGraphEmbedding_image_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {K : NNReal} {φ : E → ℝ} (hφ : LipschitzWith K φ) (s : Set E) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (TauCeti.normalGraphEmbedding φ '' s) = 0 ↔ MeasureTheory.volume s = 0

A set has zero volume exactly when its image in a Lipschitz normal graph has zero Euclidean surface measure.