Half-spaces, epigraphs, and graphs in an ℓ² product

This file defines the open normal half-space and the open region above the graph of a continuous function in WithLp 2 (ℝ × E). These are the model domains used by graph flattening and Sobolev trace theory. It also defines the normal graph parametrization y ↦ (φ y, y) and records its elementary metric properties.

Main declarations

• TauCeti.normalHalfSpace: the region above a constant normal coordinate.
• TauCeti.normalEpigraph: the region above the graph of a continuous function.
• TauCeti.normalGraphEmbedding: the normal graph parametrization y ↦ (φ y, y).
• TauCeti.frontier_setOf_lt_fst: the frontier of a continuous epigraph is its graph.
• LipschitzWith.normalGraphEmbedding: a K-Lipschitz function has a (K + 1)-Lipschitz graph parametrization.
• ContinuousLinearMap.normalGraphL: the continuous linear graph map x ↦ (A x, x).
• ContinuousLinearMap.injective_normalGraphL: the linear graph map is injective.
• ContinuousLinearMap.range_normalGraphL: its range is the linear graph of A.

def TauCeti.normalHalfSpace {E : Type u_1} [TopologicalSpace E] (a : ℝ) : TopologicalSpace.Opens (WithLp 2 (ℝ × E))

The open half-space to the right of the normal coordinate a in the ℓ² product ℝ × E.

@[simp]

theorem TauCeti.mem_normalHalfSpace {E : Type u_1} [TopologicalSpace E] (a : ℝ) (x : WithLp 2 (ℝ × E)) : x ∈ normalHalfSpace a ↔ a < x.ofLp.1

Membership in the normal-coordinate half-space is a strict inequality.

theorem TauCeti.coe_normalHalfSpace {E : Type u_1} [TopologicalSpace E] (a : ℝ) : ↑(normalHalfSpace a) = {x : WithLp 2 (ℝ × E) | a < x.ofLp.1}

As a set, the right normal half-space is {x | a < x.fst}.

def TauCeti.normalEpigraph {E : Type u_1} [TopologicalSpace E] (φ : C(E, ℝ)) : TopologicalSpace.Opens (WithLp 2 (ℝ × E))

The open region {x | φ x.snd < x.fst} above the graph of a continuous function φ : E → ℝ in the ℓ² product ℝ × E.

@[simp]

theorem TauCeti.mem_normalEpigraph {E : Type u_1} [TopologicalSpace E] (φ : C(E, ℝ)) (x : WithLp 2 (ℝ × E)) : x ∈ normalEpigraph φ ↔ φ x.snd < x.fst

Membership in the region above the graph is a strict inequality.

theorem TauCeti.coe_normalEpigraph {E : Type u_1} [TopologicalSpace E] (φ : C(E, ℝ)) : ↑(normalEpigraph φ) = {x : WithLp 2 (ℝ × E) | φ x.snd < x.fst}

As a set, the region above the graph is {x | φ x.snd < x.fst}.

@[simp]

theorem TauCeti.normalEpigraph_zero {E : Type u_1} [TopologicalSpace E] : normalEpigraph 0 = normalHalfSpace 0

The region above the graph of 0 is the half-space {0 < t}.

def TauCeti.normalGraphEmbedding {E : Type u_1} (φ : E → ℝ) (y : E) : WithLp 2 (ℝ × E)

The normal graph parametrization y ↦ (φ y, y) in WithLp 2 (ℝ × E).

@[simp]

theorem TauCeti.normalGraphEmbedding_fst {E : Type u_1} (φ : E → ℝ) (y : E) : (normalGraphEmbedding φ y).fst = φ y

The normal coordinate of the graph parametrization is the graphing function.

@[simp]

theorem TauCeti.normalGraphEmbedding_snd {E : Type u_1} (φ : E → ℝ) (y : E) : (normalGraphEmbedding φ y).snd = y

The tangential coordinate of the graph parametrization is its argument.

theorem TauCeti.injective_normalGraphEmbedding {E : Type u_1} (φ : E → ℝ) : Function.Injective (normalGraphEmbedding φ)

The normal graph parametrization is injective.

theorem TauCeti.range_normalGraphEmbedding {E : Type u_1} (φ : E → ℝ) : Set.range (normalGraphEmbedding φ) = {x : WithLp 2 (ℝ × E) | x.fst = φ x.snd}

The range of the normal graph parametrization is the graph equation t = φ y.

theorem TauCeti.antilipschitzWith_normalGraphEmbedding {E : Type u_1} [PseudoMetricSpace E] (φ : E → ℝ) : AntilipschitzWith 1 (normalGraphEmbedding φ)

The second projection is a 1-Lipschitz inverse to the graph parametrization on its range.

theorem LipschitzWith.normalGraphEmbedding {E : Type u_1} [SeminormedAddCommGroup E] {K : NNReal} {φ : E → ℝ} (hφ : LipschitzWith K φ) : LipschitzWith (K + 1) (TauCeti.normalGraphEmbedding φ)

A K-Lipschitz function has a (K + 1)-Lipschitz normal graph parametrization.

theorem Continuous.isClosed_range_normalGraphEmbedding {E : Type u_1} [TopologicalSpace E] {φ : E → ℝ} (hφ : Continuous φ) : IsClosed (Set.range (TauCeti.normalGraphEmbedding φ))

A continuous normal graph is closed in the product ℝ × E, represented by WithLp 2.

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

The frontier of the region strictly above the graph of a continuous function is the graph.

def ContinuousLinearMap.normalGraphL {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] ℝ) : E →L[ℝ] WithLp 2 (ℝ × E)

The continuous linear graph map x ↦ (A x, x) associated to A : E →L[ℝ] ℝ.

@[simp]

theorem ContinuousLinearMap.normalGraphL_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] ℝ) (x : E) : A.normalGraphL x = TauCeti.normalGraphEmbedding (⇑A) x

The continuous linear graph map is the normal graph parametrization of A.

theorem ContinuousLinearMap.coe_normalGraphL {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] ℝ) : ⇑A.normalGraphL = TauCeti.normalGraphEmbedding ⇑A

As a function, the continuous linear graph map is the normal graph parametrization of A.

theorem ContinuousLinearMap.injective_normalGraphL {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] ℝ) : Function.Injective ⇑A.normalGraphL

A continuous linear normal graph map is injective, since its tangential coordinate is its argument.

theorem ContinuousLinearMap.range_normalGraphL {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] ℝ) : ↑(↑A.normalGraphL).range = {z : WithLp 2 (ℝ × E) | z.fst = A z.snd}

The range of the normal graph linear map is the graph of the functional.