Surface measure in a Lipschitz boundary chart

A Lipschitz boundary chart parametrizes the part of the frontier inside its cylinder by

y ↦ e.symm (normalGraphEmbedding φ y).

This file identifies the image of that parametrization and compares tangential Lebesgue measure with normalized Euclidean Hausdorff measure on the frontier. It also gives the weighted area formula in chart coordinates. These results are the measure-theoretic bridge from local Sobolev traces in graph coordinates to traces on the boundary itself.

Main declarations

• Set.IsLipschitzChartWith.image_boundaryParametrization: the chart parametrization covers exactly the frontier inside the chart cylinder.
• Set.IsLipschitzChartWith.volume_le_euclideanHausdorffMeasure_frontier_inter: surface measure dominates tangential volume in a chart.
• Set.IsLipschitzChartWith.euclideanHausdorffMeasure_frontier_inter_le: the converse estimate, with explicit dependence on the Lipschitz constant.
• Set.IsLipschitzChartWith.lintegral_frontier_inter_eq: the weighted area formula in chart coordinates.
• Set.IsLipschitzChartWith.map_snd_euclideanHausdorffMeasure_frontier_inter_le: the tangential coordinate pushes surface measure on a frontier patch forward to a bounded multiple of tangential volume.
• Set.IsLipschitzChartWith.ae_restrict_frontier_inter_iff: a property of the tangential coordinate holds almost everywhere on a frontier patch exactly when it holds for almost every tangential parameter in the chart.

References

• L. C. Evans and R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., §3.3 (the area formula and Lipschitz graphs).
• W. McLean, Strongly Elliptic Systems and Boundary Integral Equations, §3.1.

theorem TauCeti.measurableSet_frontier_inter_preimage_normalCylinder {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (Omega : Set F) (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (a b : ℝ) : MeasurableSet (frontier Omega ∩ ⇑e ⁻¹' normalCylinder a b)

The part of the frontier of a set lying in the preimage of a chart cylinder is measurable.

theorem AffineIsometryEquiv.measurable_snd_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) : Measurable fun (x : F) => (e x).snd

The tangential coordinate x ↦ (e x).snd read through a chart map is measurable.

theorem Set.IsLipschitzChartWith.measurableSet_normalGraphEmbedding_preimage_normalCylinder {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : MeasurableSet (TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b)

The tangential parameters whose graph points lie in the cylinder of a boundary chart form an open, hence measurable, set.

theorem Set.IsLipschitzChartWith.lipschitzWith_boundaryParametrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : LipschitzWith (L + 1) fun (y : E) => e.symm (TauCeti.normalGraphEmbedding phi y)

The graph parametrization of a Lipschitz boundary chart is Lipschitz, with the same bound as the normal graph parametrization.

theorem Set.IsLipschitzChartWith.image_boundaryParametrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : (fun (y : E) => e.symm (TauCeti.normalGraphEmbedding phi y)) '' TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b = frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b

A Lipschitz chart parametrizes exactly the part of the frontier lying inside its cylinder.

theorem Set.IsLipschitzChartWith.volume_le_euclideanHausdorffMeasure_frontier_inter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : MeasureTheory.volume (TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b) ≤ (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b)

In a Lipschitz boundary chart, normalized surface measure dominates tangential Lebesgue measure.

theorem Set.IsLipschitzChartWith.euclideanHausdorffMeasure_frontier_inter_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b) ≤ ↑(L + 1) ^ Module.finrank ℝ E * MeasureTheory.volume (TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b)

In a Lipschitz boundary chart, normalized surface measure is at most (L + 1) ^ dim E times tangential Lebesgue measure.

theorem Set.IsLipschitzChartWith.map_snd_euclideanHausdorffMeasure_frontier_inter_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : MeasureTheory.Measure.map (fun (x : F) => (e x).snd) ((MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).restrict (frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b)) ≤ ↑(L + 1) ^ Module.finrank ℝ E • MeasureTheory.volume

Reading off the tangential coordinate pushes normalized surface measure on the frontier patch of a Lipschitz chart forward to at most (L + 1) ^ dim E times tangential Lebesgue measure.

theorem Set.IsLipschitzChartWith.euclideanHausdorffMeasure_image_boundaryParametrization_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) (s : Set E) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) ((fun (y : E) => e.symm (TauCeti.normalGraphEmbedding phi y)) '' s) = 0 ↔ MeasureTheory.volume s = 0

A set of tangential parameters is Lebesgue-null exactly when the corresponding part of the boundary chart is null for normalized surface measure.

theorem Set.IsLipschitzChartWith.euclideanHausdorffMeasure_frontier_inter_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)) (frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b) = 0 ↔ MeasureTheory.volume (TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b) = 0

The frontier patch in a Lipschitz boundary chart has zero normalized surface measure exactly when its set of tangential parameters has zero Lebesgue measure.

theorem Set.IsLipschitzChartWith.ae_restrict_frontier_inter_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) {P : E → Prop} : (∀ᵐ (x : F) ∂(MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).restrict (frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b), P (e x).snd) ↔ ∀ᵐ (y : E) ∂MeasureTheory.volume.restrict (TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b), P y

A property of the tangential coordinate holds almost everywhere on the frontier patch of a Lipschitz boundary chart, for normalized surface measure, exactly when it holds for almost every tangential parameter whose graph point lies in the chart cylinder.

theorem Set.IsLipschitzChartWith.lintegral_frontier_inter_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e phi a b) (g : F → ENNReal) : ∫⁻ (x : F) in frontier Omega ∩ ⇑e ⁻¹' TauCeti.normalCylinder a b, g x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E) = ∫⁻ (y : E) in TauCeti.normalGraphEmbedding phi ⁻¹' TauCeti.normalCylinder a b, ENNReal.ofReal (↑(fderiv ℝ (fun (z : E) => e.symm (TauCeti.normalGraphEmbedding phi z)) y)).normDet * g (e.symm (TauCeti.normalGraphEmbedding phi y))

Weighted area formula in a Lipschitz boundary chart. Surface integration over the part of the frontier inside the chart cylinder is integration over its tangential parameters, weighted by the geometric Jacobian of the boundary parametrization. The weight need not be measurable.