Flattening a graph boundary

For a continuous real function γ on a topological space E, the shear (t, y) ↦ (t - γ(y), y) is an ambient homeomorphism of the product WithLp 2 (ℝ × E). It carries the region γ(y) < t to the positive normal half-space and its graph to height zero. Its inverse adds γ(y) to the normal coordinate.

At points where γ is differentiable, the derivative is the linear shear (s, z) ↦ (s - Dγ(y) z, z). Its determinant is one and its operator norm is at most 1 + ‖Dγ(y)‖, as is that of the derivative of the inverse. For a K-Lipschitz γ, both the shear and its inverse are (1 + K)-Lipschitz. These are the chart estimates used to transfer Sobolev trace and extension operators from a half-space to a domain with a graph boundary. The shear also preserves Lebesgue measure, requiring only continuity of γ. The homeomorphism uses Mathlib's Equiv.prodShear to translate each real fiber; the differential reuses ContinuousLinearEquiv.skewProd.

The ambient product is WithLp 2 (ℝ × E), so it has the Euclidean norm when E is an inner product space. The linear shear and its determinant require only a real module with a topology, with finite dimension for the determinant. The norm estimate needs only a real seminormed space; the differential results are stated for real normed spaces, without finite dimension or an inner product. Volume preservation requires a finite-dimensional real inner product space.

References

L. C. Evans, Partial Differential Equations, Chapter 5, §§5.4–5.5 (boundary flattening for extension and trace theorems).

def TauCeti.graphFlattening {E : Type u_1} [TopologicalSpace E] (γ : E → ℝ) (hγ : Continuous γ) : WithLp 2 (ℝ × E) ≃ₜ WithLp 2 (ℝ × E)

The ambient homeomorphism subtracting the height of a continuous graph from the normal coordinate.

@[simp]

theorem TauCeti.graphFlattening_apply {E : Type u_1} [TopologicalSpace E] (γ : E → ℝ) (hγ : Continuous γ) (x : WithLp 2 (ℝ × E)) : (graphFlattening γ hγ) x = WithLp.toLp 2 (x.fst - γ x.snd, x.snd)

The graph-flattening map subtracts the graph height.

@[simp]

theorem TauCeti.graphFlattening_symm_apply {E : Type u_1} [TopologicalSpace E] (γ : E → ℝ) (hγ : Continuous γ) (x : WithLp 2 (ℝ × E)) : (graphFlattening γ hγ).symm x = WithLp.toLp 2 (x.fst + γ x.snd, x.snd)

The inverse graph-flattening map adds the graph height.

theorem TauCeti.graphFlattening_symm {E : Type u_1} [TopologicalSpace E] (γ : E → ℝ) (hγ : Continuous γ) : (graphFlattening γ hγ).symm = graphFlattening (-γ) ⋯

Inverting graph flattening negates the graph height.

theorem TauCeti.graphFlattening_image_lt {E : Type u_1} [TopologicalSpace E] (γ : E → ℝ) (hγ : Continuous γ) : ⇑(graphFlattening γ hγ) '' {x : WithLp 2 (ℝ × E) | γ x.snd < x.fst} = {x : WithLp 2 (ℝ × E) | 0 < x.fst}

Flattening takes the region strictly above a graph onto the positive normal half-space.

theorem TauCeti.graphFlattening_image_eq {E : Type u_1} [TopologicalSpace E] (γ : E → ℝ) (hγ : Continuous γ) : ⇑(graphFlattening γ hγ) '' {x : WithLp 2 (ℝ × E) | x.fst = γ x.snd} = {x : WithLp 2 (ℝ × E) | x.fst = 0}

Flattening takes the graph itself onto the zero normal hyperplane.

theorem TauCeti.lipschitzWith_graphFlattening {E : Type u_1} [SeminormedAddCommGroup E] {γ : E → ℝ} {K : NNReal} (hγ : LipschitzWith K γ) : LipschitzWith (1 + K) ⇑(graphFlattening γ ⋯)

Graph flattening by a K-Lipschitz height is (1 + K)-Lipschitz.

theorem TauCeti.lipschitzWith_graphFlattening_symm {E : Type u_1} [SeminormedAddCommGroup E] {γ : E → ℝ} {K : NNReal} (hγ : LipschitzWith K γ) : LipschitzWith (1 + K) ⇑(graphFlattening γ ⋯).symm

Inverse graph flattening by a K-Lipschitz height is (1 + K)-Lipschitz.

def TauCeti.graphFlatteningL {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [Module ℝ E] (L : E →L[ℝ] ℝ) : WithLp 2 (ℝ × E) ≃L[ℝ] WithLp 2 (ℝ × E)

The linear shear subtracting L z from the normal coordinate. This is the derivative of graphFlattening when the graph height has derivative L.

@[simp]

theorem TauCeti.graphFlatteningL_apply {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [Module ℝ E] (L : E →L[ℝ] ℝ) (x : WithLp 2 (ℝ × E)) : (graphFlatteningL L) x = WithLp.toLp 2 (x.fst - L x.snd, x.snd)

The linear graph shear has the expected normal and tangential components.

@[simp]

theorem TauCeti.graphFlatteningL_symm {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [Module ℝ E] (L : E →L[ℝ] ℝ) : (graphFlatteningL L).symm = graphFlatteningL (-L)

Inverting a linear graph shear negates its height functional.

@[simp]

theorem TauCeti.det_graphFlatteningL {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [Module ℝ E] [FiniteDimensional ℝ E] (L : E →L[ℝ] ℝ) : LinearMap.det ↑↑(graphFlatteningL L) = 1

A linear graph shear has determinant one.

theorem TauCeti.norm_graphFlatteningL_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (L : E →L[ℝ] ℝ) : ‖↑(graphFlatteningL L)‖ ≤ 1 + ‖L‖

The norm of the linear graph shear is bounded by one plus the norm of the height functional, in the WithLp 2 (L²) product norm.

theorem TauCeti.hasFDerivAt_graphFlattening {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} (hγ : Continuous γ) {x : WithLp 2 (ℝ × E)} {L : E →L[ℝ] ℝ} (hL : HasFDerivAt γ L x.snd) : HasFDerivAt (⇑(graphFlattening γ hγ)) (↑(graphFlatteningL L)) x

The derivative of graph flattening is the linear shear of the height derivative.

theorem TauCeti.fderiv_graphFlattening {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} (hγ : Continuous γ) {x : WithLp 2 (ℝ × E)} (hx : DifferentiableAt ℝ γ x.snd) : fderiv ℝ (⇑(graphFlattening γ hγ)) x = ↑(graphFlatteningL (fderiv ℝ γ x.snd))

The Fréchet derivative of graph flattening, at a differentiability point of the height.

theorem TauCeti.contDiff_graphFlattening {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {γ : E → ℝ} (hγ : ContDiff ℝ n γ) : ContDiff ℝ n ⇑(graphFlattening γ ⋯)

Graph flattening is C^n whenever the height function γ is C^n.

theorem TauCeti.contDiff_graphFlattening_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {γ : E → ℝ} (hγ : ContDiff ℝ n γ) : ContDiff ℝ n ⇑(graphFlattening γ ⋯).symm

The inverse graph chart is C^n whenever the height function γ is C^n.

theorem TauCeti.norm_fderiv_graphFlattening_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} (hγ : Continuous γ) {x : WithLp 2 (ℝ × E)} (hx : DifferentiableAt ℝ γ x.snd) : ‖fderiv ℝ (⇑(graphFlattening γ hγ)) x‖ ≤ 1 + ‖fderiv ℝ γ x.snd‖

The derivative of graph flattening has norm at most 1 + ‖Dγ(y)‖ at a differentiability point of the height.

theorem TauCeti.norm_fderiv_graphFlattening_le_one_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} {L : ℝ} (hγ : Differentiable ℝ γ) (hL : ∀ (y : E), ‖fderiv ℝ γ y‖ ≤ L) (x : WithLp 2 (ℝ × E)) : ‖fderiv ℝ (⇑(graphFlattening γ ⋯)) x‖ ≤ 1 + L

Graph flattening has derivative norm at most 1 + L when the graph function has derivative norm bounded by L.

theorem TauCeti.norm_fderiv_graphFlattening_symm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} (hγ : Continuous γ) {x : WithLp 2 (ℝ × E)} (hx : DifferentiableAt ℝ γ x.snd) : ‖fderiv ℝ (⇑(graphFlattening γ hγ).symm) x‖ ≤ 1 + ‖fderiv ℝ γ x.snd‖

The derivative of inverse graph flattening has norm at most 1 + ‖Dγ(y)‖ at a differentiability point of the height.

theorem TauCeti.det_fderiv_graphFlattening {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {γ : E → ℝ} (hγ : Continuous γ) {x : WithLp 2 (ℝ × E)} (hx : DifferentiableAt ℝ γ x.snd) : LinearMap.det ↑(fderiv ℝ (⇑(graphFlattening γ hγ)) x) = 1

The Jacobian determinant of graph flattening is one wherever the height is differentiable.

theorem TauCeti.measurePreserving_graphFlattening {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [InnerProductSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] (γ : E → ℝ) (hγ : Continuous γ) : MeasureTheory.MeasurePreserving (⇑(graphFlattening γ hγ)) MeasureTheory.volume MeasureTheory.volume

A continuous graph-flattening shear preserves Lebesgue measure. Differentiability of the height function is unnecessary for this change of variables.

theorem TauCeti.measurePreserving_graphFlattening_symm {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [InnerProductSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] (γ : E → ℝ) (hγ : Continuous γ) : MeasureTheory.MeasurePreserving (⇑(graphFlattening γ hγ).symm) MeasureTheory.volume MeasureTheory.volume

Inverse graph flattening preserves Lebesgue measure.